normalizedRatio_ge_one

formal source

  53  unfold normalizedRatio
  54  exact div_pos (lt_of_lt_of_le s.omegaRms_pos s.omegaRms_le_max) s.omegaRms_pos
  55
  56theorem normalizedRatio_ge_one (s : FiniteVolumeProfile) : 1 ≤ normalizedRatio s := by
  57  unfold normalizedRatio
  58  exact (one_le_div s.omegaRms_pos).2 s.omegaRms_le_max
  59
  60theorem normalizedRatio_le_sqrt_siteCount (s : FiniteVolumeProfile) :
  61    normalizedRatio s ≤ Real.sqrt s.siteCount := by
  62  unfold normalizedRatio
  63  rw [div_le_iff₀ s.omegaRms_pos]
  64  simpa [mul_comm, mul_left_comm, mul_assoc] using s.finiteVolumeControl
  65
  66/-! ## Bounding J-cost on the lattice -/
  67
  68/-- On the half-line `[1, ∞)`, the canonical cost is bounded by the identity.
  69
  70This is the simple estimate needed for the finite-volume FRC bound:
  71`J(x) = (x + x⁻¹)/2 - 1 ≤ x` whenever `x ≥ 1`. -/
  72theorem Jcost_le_self_of_one_le {x : ℝ} (hx : 1 ≤ x) : Jcost x ≤ x := by
  73  unfold Jcost
  74  have hinv_one : x⁻¹ ≤ 1 := inv_le_one_of_one_le₀ hx
  75  have hinv_le : x⁻¹ ≤ x := le_trans hinv_one hx
  76  linarith
  77
  78/-- The explicit finite-volume recognition-cost bound on the RS lattice. -/
  79theorem finiteVolume_Jcost_bound (s : FiniteVolumeProfile) :
  80    Jcost (normalizedRatio s) ≤ Real.sqrt s.siteCount := by
  81  have h₁ : 1 ≤ normalizedRatio s := normalizedRatio_ge_one s
  82  have h₂ : Jcost (normalizedRatio s) ≤ normalizedRatio s :=
  83    Jcost_le_self_of_one_le h₁
  84  exact le_trans h₂ (normalizedRatio_le_sqrt_siteCount s)
  85
  86/-- Strong lattice FRC: the cost is bounded by the explicit finite-volume constant