feat(MeasureTheory): FTC and integration by parts for absolutely continuous functions (leanprover-community#29508)

Prove Fundamental Theorem of Calculus and integration by parts for absolutely continuous functions. Part of originally planned leanprover-community#29092.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: zhuyizheng

Mathlib.lean

@@ -5068,6 +5068,7 @@ public import Mathlib.MeasureTheory.Integral.Indicator
 public import Mathlib.MeasureTheory.Integral.IntegrableOn
 public import Mathlib.MeasureTheory.Integral.IntegralEqImproper
 public import Mathlib.MeasureTheory.Integral.IntervalAverage
+public import Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Mathlib/Algebra/BigOperators/Group/Finset/Gaps.lean

@@ -35,29 +35,33 @@ variable {α β : Type*} [LinearOrder α] [CommGroup β]
   (F : Finset (α × α)) {k : ℕ} (h : F.card = k) {a b : α}
   (g : α → β)
 
+@[to_additive]
+theorem Finset.prod_eq_prod_range_intervalGapsWithin (f : α → α → β) :
+    ∏ z ∈ F, f z.1 z.2 = ∏ i ∈ range k,
+      f (F.intervalGapsWithin h a b i).2 (F.intervalGapsWithin h a b i.succ).1 := by
+  set p := F.intervalGapsWithin h a b
+  symm
+  apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))
+  · exact fun i _ ↦ F.intervalGapsWithin_mapsTo h a b (x := i) (by grind)
+  · intro i hi j hj hij
+    rw [mem_range] at hi hj
+    apply F.intervalGapsWithin_injOn h a b <;> grind
+  · intro z hz
+    obtain ⟨i, hi₁, hi₂⟩ := F.intervalGapsWithin_surjOn h a b hz
+    exact ⟨i, by grind, hi₂⟩
+  · simp
+
 @[to_additive]
 theorem Finset.prod_intervalGapsWithin_mul_prod_eq_div :
     (∏ i ∈ Finset.range (k + 1),
       g (F.intervalGapsWithin h a b i).2 / g (F.intervalGapsWithin h a b i).1) *
       ∏ z ∈ F, g z.2 / g z.1 = g b / g a := by
-  set p := F.intervalGapsWithin h a b
-  have : ∏ z ∈ F, g z.2 / g z.1 = ∏ i ∈ range k, g (p i.succ).1 / g (p i).2 := by
-    symm
-    apply prod_bij (fun (i : ℕ) hi ↦ ((p i).2, (p i.succ).1))
-    · exact fun i _ ↦ F.intervalGapsWithin_mapsTo h a b (x := i) (by grind)
-    · intro i hi j hj hij
-      rw [mem_range] at hi hj
-      apply F.intervalGapsWithin_injOn h a b <;> grind
-    · intro z hz
-      obtain ⟨i, hi₁, hi₂⟩ := F.intervalGapsWithin_surjOn h a b hz
-      exact ⟨i, by grind, hi₂⟩
-    · simp
-  rw [this, mul_comm,
+  rw [F.prod_eq_prod_range_intervalGapsWithin h (fun x y ↦ g y / g x), mul_comm,
       prod_range_succ, ← mul_assoc,
       ← prod_mul_distrib,
       prod_congr rfl (fun _ _ ↦ div_mul_div_cancel _ _ _),
       prod_range_div (fun i ↦ g (F.intervalGapsWithin h a b i).1)]
-  simp [p]
+  simp
 
 @[to_additive]
 theorem Finset.prod_intervalGapsWithin_eq_div_div_prod :

Mathlib/Analysis/Analytic/OfScalars.lean

@@ -259,7 +259,7 @@ theorem ofScalars_radius_eq_top_of_tendsto (hc : ∀ᶠ n in atTop, c n ≠ 0)
   refine radius_eq_top_of_summable_norm _ fun r' ↦ ?_
   by_cases hrz : r' = 0
   · apply Summable.comp_nat_add (k := 1)
-    simpa [hrz] using (summable_const_iff 0).mpr rfl
+    simp [hrz]
   · refine Summable.of_norm_bounded_eventually (g := fun n ↦ ‖‖c n‖ * r' ^ n‖) ?_ ?_
     · apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))
       · simp only [norm_norm]

Mathlib/Analysis/Real/OfDigits.lean

@@ -56,7 +56,7 @@ theorem summable_ofDigitsTerm {b : ℕ} {digits : ℕ → Fin b} :
     Summable (ofDigitsTerm digits) := by
   refine Summable.of_nonneg_of_le (fun _ ↦ ofDigitsTerm_nonneg) (fun _ ↦ ofDigitsTerm_le) ?_
   obtain rfl | hb := (Nat.one_le_of_lt (b_pos digits)).eq_or_lt
-  · simpa using summable_zero
+  · simp
   simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
   refine Summable.mul_left _ (summable_geometric_of_lt_one (by positivity) ?_)
   simp [inv_lt_one_iff₀, hb]

Mathlib/MeasureTheory/Covering/Vitali.lean

@@ -386,6 +386,33 @@ theorem exists_disjoint_covering_ae
     _ ≤ C * (ε / C) := by gcongr
     _ ≤ ε := ENNReal.mul_div_le
 
+/-- The measurable **Vitali covering theorem**, filter version.
+
+Assume one is given a family `t` of closed sets with nonempty interior, such that each `a ∈ t` is
+included in a ball `B (x, r)` and covers a definite proportion of the ball `B (x, 3 r)` for a given
+measure `μ` (think of the situation where `μ` is a doubling measure and `t` is a family of balls).
+Consider a (possibly non-measurable) set `s` at which the family is fine, i.e., every point of `s`
+belongs to arbitrarily small elements of `t`. Then one can extract from `t` a disjoint subfamily
+that covers almost all `s`.
+
+For more flexibility, we give a statement with a parameterized family of sets.
+-/
+theorem exists_disjoint_covering_ae'
+    [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
+    [SecondCountableTopology α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (s : Set α) (t : Set ι)
+    (C : ℝ≥0) (r : ι → ℝ) (c : ι → α) (B : ι → Set α) (hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a))
+    (μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ C * μ (B a))
+    (ht : ∀ a ∈ t, (interior (B a)).Nonempty) (h't : ∀ a ∈ t, IsClosed (B a))
+    (hf : ∀ x ∈ s, ∃ᶠ ε in 𝓝[>] 0, ∃ a ∈ t, r a = ε ∧ c a = x) :
+    ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0 := by
+  suffices ∀ x ∈ s, ∀ ε > (0 : ℝ), ∃ a ∈ t, r a ≤ ε ∧ c a = x from
+    exists_disjoint_covering_ae μ s t C r c B hB μB ht h't this
+  intro x hx ε hε
+  specialize hf x hx
+  rw [frequently_nhdsWithin_iff, frequently_nhds_iff] at hf
+  obtain ⟨_, _, ⟨a, ha₁, ha₂, ha₃⟩, _⟩ := hf (Ioo (-ε) ε) (by grind) isOpen_Ioo
+  exact ⟨a, ha₁, by grind, ha₃⟩
+
 /-- Assume that around every point there are arbitrarily small scales at which the measure is
 doubling. Then the set of closed sets `a` with nonempty interior contained in `closedBall x r` and
 covering a fixed proportion `1/C` of the ball `closedBall x (3 * r)` forms a Vitali family.