W11 ae eq ac representative

theorem w11_ae_eq_ac_representative    {a b : ℝ} (hab : a < b) {u g : ℝ → ℝ}    (hu : IntegrableOn u (Ioo a b) volume)    (hg : IntegrableOn g (Ioo a b) volume)    (hweak : ∀ φ : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) φ → HasCompactSupport φ →      tsupport φ ⊆ Ioo a b →      ∫ x in Ioo a b, u x * deriv φ x = -∫ x in Ioo a b, g x * φ x) :    ∃ C : ℝ, u =ᵐ[volume.restrict (Ioo a b)]      fun x => C + ∫ t in a..x, g t := by  set F := fun x => ∫ t in a..x, g t  have h_uF_test : ∀ φ : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) φ → HasCompactSupport φ →      tsupport φ ⊆ Ioo a b →      ∫ x in Ioo a b, (u x - F x) * deriv φ x = 0 := by    intro φ hφ hφ_cs hφ_supp    -- Convert set integral on Ioo to interval integral (they agree for volume)    have conv := setIntegral_Ioo_eq_interval hab.le    rw [conv]; simp_rw [sub_mul]    -- Split ∫(u*φ' - F*φ') = ∫u*φ' - ∫F*φ'    have hu_ii : IntervalIntegrable (fun x => u x * deriv φ x) volume a b :=      integrableOn_Ioo_intervalIntegrable hab.le        ((hu.bdd_mul (hφ.continuous_deriv (by norm_cast)).aestronglyMeasurable.restrict          (ae_of_all _ fun x => (hφ_cs.deriv.exists_bound_of_continuous            (hφ.continuous_deriv (by norm_cast))).choose_spec x)).congr          (ae_of_all _ fun x => by ring))    have hF_ii : IntervalIntegrable (fun x => (∫ t in a..x, g t) * deriv φ x) volume a b := by      apply integrableOn_Ioo_intervalIntegrable hab.le      have hcont := (intervalIntegral.continuousOn_primitive (μ := volume)        (integrableOn_Icc_of_Ioo hg)).congr        (fun x hx => by show ∫ t in a..x, g t = _; rw [intervalIntegral.integral_of_le hx.1])      exact (hcont.mul (hφ.continuous_deriv (by norm_cast)).continuousOn).integrableOn_compact        isCompact_Icc |>.mono_set Ioo_subset_Icc_self    rw [intervalIntegral.integral_sub hu_ii hF_ii,        ← conv, hweak φ hφ hφ_cs hφ_supp, conv, ac_ibp_step hab hg hφ hφ_supp]; ring  obtain ⟨D, hD⟩ := du_bois_reymond hab    (hu.sub (integrable_primitive hab hg))    h_uF_test  exact ⟨D, hD.mono (fun x hx => by simp at hx; linarith)⟩