theorem
proved
tactic proof
total_defect_lower_bound
show as:
view Lean formalization →
formal statement (Lean)
160private theorem total_defect_lower_bound {N : ℕ} (hN : 0 < N) (c : Configuration N) :
161 (N : ℝ) * Jlog (log_charge c / N) ≤ total_defect c := by
proof body
Tactic-mode proof.
162 have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
163 have hw_nonneg : ∀ i ∈ (Finset.univ : Finset (Fin N)), 0 ≤ (1 / (N : ℝ)) := by
164 intro _ _
165 positivity
166 have hw_sum : ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) = 1 := by
167 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
168 field_simp [hN_pos.ne']
169 have hmem : ∀ i ∈ (Finset.univ : Finset (Fin N)), Real.log (c.entries i) ∈ (Set.univ : Set ℝ) := by
170 intro _ _
171 simp
172 have hJensen :=
173 Jlog_strictConvexOn.convexOn.map_sum_le
174 (t := (Finset.univ : Finset (Fin N)))
175 (w := fun _ : Fin N => (1 / (N : ℝ)))
176 (p := fun i : Fin N => Real.log (c.entries i))
177 hw_nonneg hw_sum hmem
178 have hJensen' :
179 Jlog (log_charge c / N) ≤ (1 / (N : ℝ)) * total_defect c := by
180 have hJensen0 :
181 Jlog (∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i)) ≤
182 ∑ i : Fin N, (1 / (N : ℝ)) * Jlog (Real.log (c.entries i)) := by
183 simpa [smul_eq_mul] using hJensen
184 rw [weighted_log_average hN c, weighted_Jlog_average c] at hJensen0
185 exact hJensen0
186 have hmul := mul_le_mul_of_nonneg_left hJensen' hN_pos.le
187 simpa [div_eq_mul_inv, hN_pos.ne', mul_comm, mul_left_comm, mul_assoc] using hmul
188
189/-- Equality in the Jensen bound forces the configuration to be uniform. -/