annularExcess

formal source

 465  ∑ n : Fin N, topologicalFloor (n.val + 1) m
 466
 467/-- The excess cost above the topological floor for an annular mesh. -/
 468noncomputable def annularExcess {N : ℕ} (mesh : AnnularMesh N) : ℝ :=
 469  annularCost mesh - annularTopologicalFloor N mesh.charge
 470
 471/-- Annular coercivity: for charge m ≠ 0, total annular cost diverges
 472    as Θ(m² log N). Specifically:
 473    annularCost ≥ (π²κ/4) · m² · ∑_{n=1}^{N} 1/n. -/
 474theorem annular_coercivity {N : ℕ} (hN : 0 < N) (mesh : AnnularMesh N)
 475    (hm : mesh.charge ≠ 0) :
 476    Real.pi ^ 2 * kappa / 4 * (mesh.charge : ℝ) ^ 2 *
 477      ∑ n : Fin N, (1 : ℝ) / ((n : ℝ) + 1) ≤ annularCost mesh := by
 478  have hterm : ∀ n : Fin N,
 479      Real.pi ^ 2 * kappa / 4 * (mesh.charge : ℝ) ^ 2 * ((1 : ℝ) / ((n : ℝ) + 1))
 480        ≤ ringCost (mesh.rings n) := by
 481    intro n
 482    have hn' : 0 < n.val + 1 := Nat.succ_pos _
 483    have hcoer := ring_coercivity hn' (mesh.rings n)
 484    rw [mesh.uniform_charge n] at hcoer
 485    simpa [div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using hcoer
 486  calc
 487    Real.pi ^ 2 * kappa / 4 * (mesh.charge : ℝ) ^ 2 *
 488        ∑ n : Fin N, (1 : ℝ) / ((n : ℝ) + 1)
 489        = ∑ n : Fin N, Real.pi ^ 2 * kappa / 4 * (mesh.charge : ℝ) ^ 2 *
 490            ((1 : ℝ) / ((n : ℝ) + 1)) := by
 491            rw [Finset.mul_sum]
 492    _ ≤ ∑ n : Fin N, ringCost (mesh.rings n) := by
 493          exact Finset.sum_le_sum (fun n _ => hterm n)
 494    _ = annularCost mesh := by
 495          rfl
 496
 497/-- The harmonic sum diverges, so nonzero charge forces unbounded cost. -/
 498theorem harmonic_sum_diverges :