eq_constant_config_of_defect_eq

formal source

 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. -/
 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
 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