ring_coercivity

formal source

 365
 366/-- Coercivity: for charge m ≠ 0, ring n has cost ≥ π²κm²/(4n).
 367    Uses the quadratic lower bound on phiCost. -/
 368theorem ring_coercivity {n : ℕ} (hn : 0 < n) (s : AnnularRingSample n) :
 369    Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) ≤ ringCost s := by
 370  let u : ℝ := -(2 * Real.pi * s.winding) / (8 * n : ℝ)
 371  have hphi := phiCost_quadratic_lb u
 372  have hmul :=
 373    mul_le_mul_of_nonneg_left hphi (by positivity : 0 ≤ (8 * n : ℝ))
 374  have hleft :
 375      Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) ≤
 376        (8 * n : ℝ) * phiCost u := by
 377    have hcalc :
 378        (8 * n : ℝ) * (kappa * u ^ 2 / 2) =
 379          Real.pi ^ 2 * kappa * (s.winding : ℝ) ^ 2 / (4 * n : ℝ) := by
 380      dsimp [u]
 381      field_simp [show (8 * n : ℝ) ≠ 0 by positivity]
 382      ring
 383    rw [← hcalc]
 384    exact hmul
 385  exact hleft.trans (jensen_ring_bound hn s)
 386
 387/-- The topological floor: minimum possible cost for charge m on ring n. -/
 388noncomputable def topologicalFloor (n : ℕ) (m : ℤ) : ℝ :=
 389  (8 * n : ℝ) * phiCost (-(2 * Real.pi * m) / (8 * n))
 390
 391/-- The exact Jensen lower bound written as a named topological floor. -/
 392theorem ringCost_ge_topologicalFloor {n : ℕ} (hn : 0 < n) (s : AnnularRingSample n) :
 393    topologicalFloor n s.winding ≤ ringCost s := by
 394  simpa [topologicalFloor] using jensen_ring_bound hn s
 395
 396/-- Ring-level perturbative upper bound above the topological floor.
 397
 398If each sampled increment is the uniform winding increment