Marginalized jensen forking bound

lemma marginalized_jensen_forking_bound    {X : Type} (mx : m X)    (acc B : X → ℝ≥0∞) (q hinv : ℝ≥0∞)    (hinv_ne_top : hinv ≠ ⊤)    (hacc_le : ∀ x, acc x ≤ 1)    (hper : ∀ x, acc x * (acc x / q - hinv) ≤ B x) :    (∑' x, Pr[= x | mx] * acc x) *        ((∑' x, Pr[= x | mx] * acc x) / q - hinv) ≤      ∑' x, Pr[= x | mx] * B x := by  classical  set w : X → ℝ≥0∞ := fun x => Pr[= x | mx]  set μ : ℝ≥0∞ := ∑' x, w x * acc x with hμ_def  have hw_tsum_le_one : ∑' x, w x ≤ 1 := tsum_probOutput_le_one  have hμ_le_one : μ ≤ 1 := by    calc μ = ∑' x, w x * acc x := rfl      _ ≤ ∑' x, w x * 1 := by gcongr with x; exact hacc_le x      _ = ∑' x, w x := by simp      _ ≤ 1 := hw_tsum_le_one  have hμ_ne_top : μ ≠ ⊤ := ne_top_of_le_ne_top ENNReal.one_ne_top hμ_le_one  have hμ_hinv_ne_top : ∑' x, w x * acc x * hinv ≠ ⊤ := by    rw [ENNReal.tsum_mul_right]; exact ENNReal.mul_ne_top hμ_ne_top hinv_ne_top  have hCS : μ ^ 2 ≤ ∑' x, w x * acc x ^ 2 :=    ENNReal.sq_tsum_le_tsum_sq w acc hw_tsum_le_one  calc μ * (μ / q - hinv)      = μ ^ 2 / q - μ * hinv := by        rw [ENNReal.mul_sub (fun _ _ => hμ_ne_top), sq, mul_div_assoc]    _ ≤ (∑' x, w x * acc x ^ 2) / q - μ * hinv := by gcongr    _ = (∑' x, w x * acc x ^ 2 / q) - ∑' x, w x * acc x * hinv := by        rw [hμ_def]        simp_rw [div_eq_mul_inv, ENNReal.tsum_mul_right]    _ ≤ ∑' x, (w x * acc x ^ 2 / q - w x * acc x * hinv) :=        tsum_sub_tsum_le_tsum_sub _ _ hμ_hinv_ne_top    _ = ∑' x, w x * (acc x * (acc x / q - hinv)) := by        refine tsum_congr fun x => ?_        have hwx_ne_top : w x ≠ ⊤ :=          ne_top_of_le_ne_top ENNReal.one_ne_top probOutput_le_one        have hax_ne_top : acc x ≠ ⊤ :=          ne_top_of_le_ne_top ENNReal.one_ne_top (hacc_le x)        rw [ENNReal.mul_sub (fun _ _ => hax_ne_top), sq, mul_div_assoc,          ENNReal.mul_sub (fun _ _ => hwx_ne_top), mul_div_assoc, mul_assoc]    _ ≤ ∑' x, w x * B x := by gcongr with x; exact hper x