total_defect_nonneg'

formal source

 109  ∀ c' ∈ Feasible current, total_defect next ≤ total_defect c'
 110
 111/-- **Total defect** is non-negative for any configuration. -/
 112theorem total_defect_nonneg' {N : ℕ} (c : Configuration N) :
 113    0 ≤ total_defect c := total_defect_nonneg c
 114
 115/-! ## Uniform candidate and Jensen helpers -/
 116
 117/-- Constant-entry configuration with value `exp μ` in every slot. -/
 118private noncomputable def constant_config {N : ℕ} (μ : ℝ) : Configuration N :=
 119  { entries := fun _ => Real.exp μ
 120    entries_pos := fun _ => Real.exp_pos _ }
 121
 122/-- The constant configuration has log-charge `N * μ`. -/
 123private theorem constant_config_log_charge {N : ℕ} (μ : ℝ) :
 124    log_charge (constant_config μ : Configuration N) = (N : ℝ) * μ := by
 125  unfold log_charge constant_config
 126  simp only [Real.log_exp]
 127  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 128
 129/-- The constant configuration has total defect `N * Jlog μ`. -/
 130private theorem constant_config_total_defect {N : ℕ} (μ : ℝ) :
 131    total_defect (constant_config μ : Configuration N) = (N : ℝ) * Jlog μ := by
 132  unfold total_defect constant_config
 133  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 134  rfl
 135
 136/-- Weighted average of the logs equals `log_charge / N`. -/
 137private theorem weighted_log_average {N : ℕ} (hN : 0 < N) (c : Configuration N) :
 138    (∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) * Real.log (c.entries i)) =
 139      log_charge c / N := by
 140  unfold log_charge
 141  rw [← Finset.mul_sum]
 142  ring