Energy Variance eq mean Square Energy sub mean Energy sq

theorem energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq    (𝓒 : CanonicalEnsemble ι) (T : Temperature) [IsProbabilityMeasure (𝓒.μProd T)]    (hE_int : Integrable 𝓒.energy (𝓒.μProd T))    (hE2_int : Integrable (fun i => (𝓒.energy i)^2) (𝓒.μProd T)) :    𝓒.energyVariance T = 𝓒.meanSquareEnergy T - (𝓒.meanEnergy T)^2 := by  unfold energyVariance meanSquareEnergy meanEnergy  set U := ∫ i, 𝓒.energy i ∂𝓒.μProd T with hU  have h_expand : (fun i => (𝓒.energy i - U)^2)      = (fun i => (𝓒.energy i)^2 - 2 * U * 𝓒.energy i + U^2) := by    funext i; ring  have h_int_E_mul_const : Integrable (fun i => 2 * U * 𝓒.energy i) (𝓒.μProd T) :=    hE_int.const_mul (2 * U)  rw [h_expand]  erw [integral_add (hE2_int.sub h_int_E_mul_const) (integrable_const _)]  erw [integral_sub hE2_int h_int_E_mul_const]  rw [integral_const_mul, integral_const, ← hU, probReal_univ, smul_eq_mul]  ring