Stampacchia 1d

theorem stampacchia_1d {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) :    ∀ᵐ x ∂(volume.restrict (Ioo a b)), u x = 0 → g x = 0 := by  obtain ⟨C, hC⟩ := w11_ae_eq_ac_representative hab hu hg hweak  set F := fun x => C + ∫ t in a..x, g t  -- We need global a.e. differentiability. Use g̃ = indicator (Ioo a b) g (globally integrable).  -- F̃(x) = C + ∫_a^x g̃ agrees with F on (a,b) and is globally a.e. differentiable.  set g' := (Ioo a b).indicator g  have hg'_li : LocallyIntegrable g' volume :=    ((integrable_indicator_iff measurableSet_Ioo).mpr hg).locallyIntegrable  -- F̃ has derivative g̃ a.e. globally (by FTC for locally integrable functions)  set F' := fun x => C + ∫ t in a..x, g' t  have hF'_ae : ∀ᵐ x, HasDerivAt F' (g' x) x := by    filter_upwards [LocallyIntegrable.ae_hasDerivAt_integral hg'_li] with x hx    have := (hasDerivAt_const x C).add (hx a)    simp only [zero_add] at this; exact this  -- Apply deriv_eq_zero_ae_on_zeroSet to F'  have hF'_deriv_ae : ∀ᵐ x, HasDerivAt F' (deriv F' x) x :=    hF'_ae.mono fun x hx => by rwa [hx.deriv]  have hF'_zero := deriv_eq_zero_ae_on_zeroSet hF'_deriv_ae  -- On (a,b): g' = g, F' = F, so combine with hC and hF'_zero.  have hint_eq : ∀ x ∈ Ioo a b,      (∫ t in a..x, g' t) = ∫ t in a..x, g t := by    intro x hx; apply intervalIntegral.integral_congr_ae; apply ae_of_all    intro t ht; rw [uIoc_of_le hx.1.le] at ht    exact indicator_of_mem (show t ∈ Ioo a b from ⟨ht.1, lt_of_le_of_lt ht.2 hx.2⟩) g  filter_upwards [ae_restrict_of_ae (s := Ioo a b) hF'_ae,                   ae_restrict_of_ae (s := Ioo a b) hF'_zero,                   hC, ae_restrict_mem measurableSet_Ioo] with x hF'_d hF'_z hu_eq hx_mem  intro hu_zero  have hg'_eq : g' x = g x := indicator_of_mem hx_mem g  have hF'_eq : F' x = C + ∫ t in a..x, g t := by    change C + ∫ t in a..x, g' t = _; congr 1; exact hint_eq x hx_mem  rw [← hg'_eq, ← hF'_d.deriv]  exact hF'_z (by rw [hF'_eq]; show C + ∫ t in a..x, g t = 0; linarith [hu_eq])