Du bois reymond

theorem du_bois_reymond    {a b : ℝ} (hab : a < b)    {g : ℝ → ℝ} (hg : IntegrableOn g (Ioo a b) volume)    (htest : ∀ φ : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) φ → HasCompactSupport φ →      tsupport φ ⊆ Ioo a b → ∫ x in Ioo a b, g x * deriv φ x = 0) :    ∃ C : ℝ, g =ᵐ[volume.restrict (Ioo a b)] fun _ => C := by  have ⟨ψ₀, hψ₀_smooth, hψ₀_cs, hψ₀_supp, hψ₀_int⟩ :      ∃ ψ₀ : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) ψ₀ ∧ HasCompactSupport ψ₀ ∧        tsupport ψ₀ ⊆ Ioo a b ∧ ∫ x, ψ₀ x = 1 := by    set f : ContDiffBump ((a + b) / 2) :=      ⟨(b - a) / 8, (b - a) / 4, by linarith, by linarith⟩    refine ⟨f.normed volume, f.contDiff_normed, f.hasCompactSupport_normed, ?_,      f.integral_normed⟩    rw [f.tsupport_normed_eq]; intro x hx    simp only [mem_closedBall, Real.dist_eq] at hx; rw [mem_Ioo]    have := abs_le.mp (show |x - (a + b) / 2| ≤ (b - a) / 4 from hx)    constructor <;> linarith  set c := ∫ x in Ioo a b, g x * ψ₀ x  have hmain : ∀ η : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) η → HasCompactSupport η →      tsupport η ⊆ Ioo a b → ∫ x in Ioo a b, (g x - c) * η x = 0 := by    intro η hη hη_cs hη_supp    set α := ∫ x, η x    set η₀ : ℝ → ℝ := fun x => η x - α * ψ₀ x with hη₀_def    have hαψ₀_cs : HasCompactSupport (fun x => α * ψ₀ x) := by      rw [hasCompactSupport_def]      apply hψ₀_cs.isCompact.of_isClosed_subset isClosed_closure      exact closure_mono (fun x hx => by        simp only [mem_support] at hx ⊢; intro h; exact hx (by simp [h]))    have hαψ₀_tsup : tsupport (fun x => α * ψ₀ x) ⊆ tsupport ψ₀ :=      closure_mono (fun x hx => by simp only [mem_support] at hx ⊢; intro h; exact hx (by simp [h]))    have hunion_closed : IsClosed (tsupport η ∪ tsupport (fun x => α * ψ₀ x)) :=      isClosed_closure.union isClosed_closure    have hη₀_smooth : ContDiff ℝ (⊤ : ℕ∞) η₀ := hη.sub (contDiff_const.mul hψ₀_smooth)    have hη₀_cs : HasCompactSupport η₀ := by      rw [hasCompactSupport_def]; exact (hη_cs.isCompact.union hαψ₀_cs.isCompact).of_isClosed_subset        isClosed_closure (closure_minimal (show support η₀ ⊆ _ from hη₀_def ▸ support_sub_tsupport) hunion_closed)    have hη₀_supp : tsupport η₀ ⊆ Ioo a b :=      (closure_minimal (hη₀_def ▸ support_sub_tsupport) hunion_closed).trans        (union_subset hη_supp (hαψ₀_tsup.trans hψ₀_supp))    have hη₀_int : ∫ x, η₀ x = 0 := by      have : ∫ x, η₀ x = (∫ x, η x) - ∫ x, α * ψ₀ x :=        integral_sub (integrable_of_smooth_cs hη hη_cs)          ((integrable_of_smooth_cs hψ₀_smooth hψ₀_cs).const_mul α)      rw [this, MeasureTheory.integral_const_mul, hψ₀_int, mul_one, sub_self]    obtain ⟨φ, hφ_smooth, hφ_cs, hφ_supp, hφ_deriv⟩ :=      exists_antideriv_of_zero_integral hab hη₀_smooth hη₀_cs hη₀_supp hη₀_int    have key : ∫ x in Ioo a b, g x * η₀ x = 0 := by      rw [show (fun x => g x * η₀ x) = (fun x => g x * deriv φ x) from by ext x; rw [hφ_deriv]]      exact htest φ hφ_smooth hφ_cs hφ_supp    have hgη := integrableOn_mul_of_smooth_cs hg hη.continuous hη_cs    have hgψ₀ := integrableOn_mul_of_smooth_cs hg hψ₀_smooth.continuous hψ₀_cs    have gη_eq : ∫ x in Ioo a b, g x * η x = α * ∫ x in Ioo a b, g x * ψ₀ x := by      have h_pw : ∀ x, g x * η₀ x = g x * η x - α * (g x * ψ₀ x) := by        intro x; simp [hη₀_def, mul_sub, mul_comm α, mul_assoc]      have h_sub : ∫ x in Ioo a b, g x * η₀ x =          (∫ x in Ioo a b, g x * η x) - ∫ x in Ioo a b, α * (g x * ψ₀ x) := by        simp_rw [h_pw]; exact integral_sub hgη (hgψ₀.const_mul α)      have h_smul : ∫ x in Ioo a b, α * (g x * ψ₀ x) =          α * ∫ x in Ioo a b, g x * ψ₀ x := by        simp_rw [show ∀ x, α * (g x * ψ₀ x) = α • (g x * ψ₀ x) from          fun x => (smul_eq_mul _ _).symm]; exact integral_smul α _      linarith [key, h_sub, h_smul]    have hcη : IntegrableOn (fun x => c * η x) (Ioo a b) :=      ((integrable_of_smooth_cs hη hη_cs).integrableOn).const_mul c    have hη_Ioo : ∫ x in Ioo a b, η x = α :=      setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx =>        image_eq_zero_of_notMem_tsupport (fun hmem => hx (hη_supp hmem)))    have hcη_eq : ∫ x in Ioo a b, c * η x = c * α := by      simp_rw [show ∀ x, c * η x = c • η x from fun x => (smul_eq_mul _ _).symm]      rw [MeasureTheory.integral_smul, hη_Ioo, smul_eq_mul]    simp_rw [fun x => show (g x - c) * η x = g x * η x - c * η x from by ring]    rw [integral_sub hgη hcη, gη_eq, hcη_eq]; ring  refine ⟨c, ?_⟩  set h := (Ioo a b).indicator (fun x => g x - c)  have hh_li : LocallyIntegrable h volume := by    exact ((integrable_indicator_iff measurableSet_Ioo).mpr      (hg.sub (integrableOn_const (hs := measure_Ioo_lt_top.ne)))).locallyIntegrable  have hh_zero : ∀ ψ : ℝ → ℝ, ContDiff ℝ (⊤ : ℕ∞) ψ → HasCompactSupport ψ →      ∫ x, ψ x • h x = 0 := by    intro ψ hψ hψ_cs    simp only [smul_eq_mul]    rw [show (fun x => ψ x * h x) = (Ioo a b).indicator (fun x => ψ x * (g x - c)) from by      ext x; by_cases hx : x ∈ Ioo a b <;> simp [indicator, hx, h]]    rw [MeasureTheory.integral_indicator measurableSet_Ioo,        show (fun x => ψ x * (g x - c)) = (fun x => (g x - c) * ψ x) from by ext; ring]    exact smooth_cutoff_approximation hab      (hg.sub (integrableOn_const (hs := measure_Ioo_lt_top.ne))) hψ hψ_cs hmain  have hae := ae_eq_zero_of_integral_contDiff_smul_eq_zero hh_li hh_zero  rw [Filter.EventuallyEq, ae_restrict_iff' measurableSet_Ioo]  filter_upwards [hae] with x hx hx_mem  simp only [h, indicator_of_mem hx_mem] at hx  linarith