theorem
proved
tactic proof
eq_constant_config_of_defect_eq
show as:
view Lean formalization →
formal statement (Lean)
190private theorem eq_constant_config_of_defect_eq {N : ℕ} (hN : 0 < N) (c : Configuration N)
191 (hEq : total_defect c = (N : ℝ) * Jlog (log_charge c / N)) :
192 c.entries = (constant_config (log_charge c / N) : Configuration N).entries := by
proof body
Tactic-mode proof.
193 have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
194 have hw_pos : ∀ i ∈ (Finset.univ : Finset (Fin N)), 0 < (1 / (N : ℝ)) := by
195 intro _ _
196 exact one_div_pos.mpr hN_pos
197 have hw_sum : ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) = 1 := by
198 rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
199 field_simp [hN_pos.ne']
200 have hmem : ∀ i ∈ (Finset.univ : Finset (Fin N)), Real.log (c.entries i) ∈ (Set.univ : Set ℝ) := by
201 intro _ _
202 simp
203 have hEq' : Jlog (log_charge c / N) = (1 / (N : ℝ)) * total_defect c := by
204 have hN_ne : (N : ℝ) ≠ 0 := hN_pos.ne'
205 calc
206 Jlog (log_charge c / N)
207 = (1 / (N : ℝ)) * ((N : ℝ) * Jlog (log_charge c / N)) := by
208 field_simp [hN_ne]
209 _ = (1 / (N : ℝ)) * total_defect c := by rw [← hEq]
210 have hMapEq :
211 Jlog (∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) • Real.log (c.entries i)) =
212 ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) • Jlog (Real.log (c.entries i)) := by
213 have hMapEq0 :
214 Jlog (∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i)) =
215 ∑ i : Fin N, (1 / (N : ℝ)) * Jlog (Real.log (c.entries i)) := by
216 rw [weighted_log_average hN c, weighted_Jlog_average c]
217 exact hEq'
218 simpa [smul_eq_mul] using hMapEq0
219 have hall :=
220 (Jlog_strictConvexOn.map_sum_eq_iff
221 (t := (Finset.univ : Finset (Fin N)))
222 (w := fun _ : Fin N => (1 / (N : ℝ)))
223 (p := fun i : Fin N => Real.log (c.entries i))
224 hw_pos hw_sum hmem).mp hMapEq
225 funext i
226 have hlog : Real.log (c.entries i) = log_charge c / N := by
227 have hlog0 : Real.log (c.entries i) = ∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i) := by
228 simpa [smul_eq_mul] using hall i (by simp)
229 rw [weighted_log_average hN c] at hlog0
230 exact hlog0
231 have hexp := congrArg Real.exp hlog
232 simpa [constant_config, Real.exp_log (c.entries_pos i)] using hexp
233
234/-! ## Existence of the Variational Step -/
235
236/-- **Lemma**: The unity configuration (all entries = 1) has zero total defect
237 and zero log-charge. -/