AnnularRingSample

formal source

 296
 297/-- An annular sample on ring n consists of 8n phase increments
 298    with prescribed total winding. -/
 299structure AnnularRingSample (n : ℕ) where
 300  increments : Fin (8 * n) → ℝ
 301  winding : ℤ
 302  winding_constraint : ∑ j, increments j = -(2 * Real.pi * winding)
 303
 304/-- The J-cost of one ring: sum of phiCost over all angular edges. -/
 305noncomputable def ringCost {n : ℕ} (s : AnnularRingSample n) : ℝ :=
 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]