uniform_config_charge

formal source

 553    entries_pos := fun _ => Real.exp_pos _ }
 554
 555/-- The uniform configuration has the correct log-charge. -/
 556theorem uniform_config_charge {N : ℕ} (hN : 0 < N) (σ : ℝ) :
 557    log_charge (uniform_config hN σ) = σ := by
 558  unfold log_charge uniform_config
 559  simp only [Real.log_exp]
 560  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin,
 561      nsmul_eq_mul, mul_div_cancel₀]
 562  exact Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN)
 563
 564/-- **Theorem (Explicit Solution)**:
 565    For any configuration c with log-charge σ, the uniform configuration
 566    with charge σ is the variational successor.
 567
 568    This is the explicit "equation of motion":
 569      entries(t+1) = [exp(σ/N), exp(σ/N), ..., exp(σ/N)]
 570    where σ = ∑ᵢ log(entries(t)ᵢ).
 571
 572    The uniform distribution minimizes total J-cost subject to fixed
 573    log-sum (by Jensen's inequality on the convex function J). -/
 574theorem uniform_is_variational_successor {N : ℕ} (hN : 0 < N)
 575    (c : Configuration N) :
 576    IsVariationalSuccessor c (uniform_config hN (log_charge c)) := by
 577  simpa [uniform_config, constant_config] using
 578    (show IsVariationalSuccessor c (constant_config (log_charge c / N)) from by
 579      constructor
 580      · show log_charge (constant_config (log_charge c / N) : Configuration N) = log_charge c
 581        rw [constant_config_log_charge]
 582        exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
 583      · intro c' hc'
 584        rw [constant_config_total_defect]
 585        have hbound := total_defect_lower_bound hN c'
 586        rw [hc'] at hbound