AnnularMesh

formal source

 306  ∑ j, phiCost (s.increments j)
 307
 308/-- An annular mesh of N concentric rings. -/
 309structure AnnularMesh (N : ℕ) where
 310  rings : (n : Fin N) → AnnularRingSample (n.val + 1)
 311  charge : ℤ
 312  uniform_charge : ∀ n, (rings n).winding = charge
 313
 314/-- Total annular cost over N rings. -/
 315noncomputable def annularCost {N : ℕ} (mesh : AnnularMesh N) : ℝ :=
 316  ∑ n, ringCost (mesh.rings n)
 317
 318/-! ### §3. Jensen coercivity -/
 319
 320/-- Jensen bound for phiCost on a single ring:
 321    ∑ f(Δ_j) ≥ (8n) · f(∑Δ_j / (8n)).
 322    Follows from strict convexity of cosh. -/
 323theorem jensen_ring_bound {n : ℕ} (hn : 0 < n) (s : AnnularRingSample n) :
 324    (8 * n : ℝ) * phiCost (-(2 * Real.pi * s.winding) / (8 * n)) ≤ ringCost s := by
 325  have h8n_pos : 0 < (8 * n : ℝ) := by positivity
 326  let w : Fin (8 * n) → ℝ := fun _ => 1 / (8 * n : ℝ)
 327  have hw_nonneg : ∀ i ∈ (Finset.univ : Finset (Fin (8 * n))), 0 ≤ w i := by
 328    intro _ _
 329    dsimp [w]
 330    positivity
 331  have hw_sum : ∑ i ∈ (Finset.univ : Finset (Fin (8 * n))), w i = 1 := by
 332    dsimp [w]
 333    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 334    norm_num [Nat.cast_mul]
 335    field_simp [h8n_pos.ne']
 336  have hmem : ∀ i ∈ (Finset.univ : Finset (Fin (8 * n))), s.increments i ∈ (Set.univ : Set ℝ) := by
 337    intro _ _
 338    simp
 339  have hJ :=