E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable f'
refine' aemeasurable_of_unif_approx fun ε εpos => _
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
let δ : ℝ≥0 := ⟨ε, le_of_lt εpos⟩
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
have δpos : 0 < δ := εpos
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
obtain ⟨t, A, t_disj, t_meas, t_cover, ht, _⟩ :
  ∃ (t : ℕ → Set E) (A : ℕ → E →L[ℝ] E),
    Pairwise (Disjoint on t) ∧
      (∀ n : ℕ, MeasurableSet (t n)) ∧
        (s ⊆ ⋃ n : ℕ, t n) ∧
          (∀ n : ℕ, ApproximatesLinearOn f (A n) (s ∩ t n) δ) ∧
            (s.Nonempty → ∀ n, ∃ y ∈ s, A n = f' y) :=
  exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' (fun _ => δ) fun _ =>
    δpos.ne'
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
obtain ⟨g, g_meas, hg⟩ :
    ∃ g : E → E →L[ℝ] E, Measurable g ∧ ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n :=
  exists_measurable_piecewise t t_meas (fun n _ => A n) (fun n => measurable_const) <|
    t_disj.mono fun i j h => by simp only [h.inter_eq, eqOn_empty]
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (g x) (f' x) ≤ ε
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
⊢ ∃ f, AEMeasurable f ∧ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (f x) (f' x) ≤ ε
refine' ⟨g, g_meas.aemeasurable, _⟩
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (g x) (f' x) ≤ ε

case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
⊢ ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (g x) (f' x) ≤ ε
suffices H : ∀ᵐ x : E ∂sum fun n => μ.restrict (s ∩ t n), dist (g x) (f' x) ≤ ε
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
⊢ ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
refine' ae_sum_iff.2 fun n => _
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
have E₁ : ∀ᵐ x : E ∂μ.restrict (s ∩ t n), ‖f' x - A n‖₊ ≤ δ :=
  (ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx =>
    (hf' x hx.1).mono (inter_subset_left _ _)
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
have E₂ : ∀ᵐ x : E ∂μ.restrict (s ∩ t n), g x = A n := by
  suffices H : ∀ᵐ x : E ∂μ.restrict (t n), g x = A n
  exact ae_mono (restrict_mono (inter_subset_right _ _) le_rfl) H
  filter_upwards [ae_restrict_mem (t_meas n)]
  exact hg n
case h
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
x : E
hx1 : ‖f' x - A n‖₊ ≤ { val := ε, property := (_ : 0 ≤ ε) }
hx2 : g x = A n
⊢ dist (g x) (f' x) ≤ ε
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
filter_upwards [E₁, E₂] with x hx1 hx2
case h
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
x : E
hx1 : nndist (f' x) (A n) ≤ { val := ε, property := (_ : 0 ≤ ε) }
hx2 : g x = A n
⊢ dist (g x) (f' x) ≤ ε
case h
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
x : E
hx1 : ‖f' x - A n‖₊ ≤ { val := ε, property := (_ : 0 ≤ ε) }
hx2 : g x = A n
⊢ dist (g x) (f' x) ≤ ε
rw [← nndist_eq_nnnorm] at hx1
case h
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
x : E
hx1 : nndist (f' x) (A n) ≤ { val := ε, property := (_ : 0 ≤ ε) }
hx2 : g x = A n
⊢ dist (f' x) (A n) ≤ ε
case h
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
x : E
hx1 : nndist (f' x) (A n) ≤ { val := ε, property := (_ : 0 ≤ ε) }
hx2 : g x = A n
⊢ dist (g x) (f' x) ≤ ε
rw [hx2, dist_comm]
no goals
case h
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
E₂ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
x : E
hx1 : nndist (f' x) (A n) ≤ { val := ε, property := (_ : 0 ≤ ε) }
hx2 : g x = A n
⊢ dist (f' x) (A n) ≤ ε
exact hx1
no goals
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
i j : ℕ
h : (Disjoint on t) i j
⊢ EqOn ((fun n x => A n) i) ((fun n x => A n) j) (t i ∩ t j)
simp only [h.inter_eq, eqOn_empty]
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
this : Measure.restrict μ s ≤ sum fun n => Measure.restrict μ (s ∩ t n)
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (g x) (f' x) ≤ ε
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (g x) (f' x) ≤ ε
have : μ.restrict s ≤ sum fun n => μ.restrict (s ∩ t n) := by
  have : s = ⋃ n, s ∩ t n := by
    rw [← inter_iUnion]
    exact Subset.antisymm (subset_inter Subset.rfl t_cover) (inter_subset_left _ _)
  conv_lhs => rw [this]
  exact restrict_iUnion_le
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
this : Measure.restrict μ s ≤ sum fun n => Measure.restrict μ (s ∩ t n)
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ s, dist (g x) (f' x) ≤ ε
exact ae_mono this H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
this : s = ⋃ (n : ℕ), s ∩ t n
⊢ Measure.restrict μ s ≤ sum fun n => Measure.restrict μ (s ∩ t n)
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ Measure.restrict μ s ≤ sum fun n => Measure.restrict μ (s ∩ t n)
have : s = ⋃ n, s ∩ t n := by
  rw [← inter_iUnion]
  exact Subset.antisymm (subset_inter Subset.rfl t_cover) (inter_subset_left _ _)
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
this : s = ⋃ (n : ℕ), s ∩ t n
⊢ Measure.restrict μ (⋃ (n : ℕ), s ∩ t n) ≤ sum fun n => Measure.restrict μ (s ∩ t n)
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
this : s = ⋃ (n : ℕ), s ∩ t n
⊢ Measure.restrict μ s ≤ sum fun n => Measure.restrict μ (s ∩ t n)
conv_lhs => rw [this]
no goals
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
this : s = ⋃ (n : ℕ), s ∩ t n
⊢ Measure.restrict μ (⋃ (n : ℕ), s ∩ t n) ≤ sum fun n => Measure.restrict μ (s ∩ t n)
exact restrict_iUnion_le
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ s = s ∩ ⋃ (i : ℕ), t i
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ s = ⋃ (n : ℕ), s ∩ t n
rw [← inter_iUnion]
no goals
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
H : ∀ᵐ (x : E) ∂sum fun n => Measure.restrict μ (s ∩ t n), dist (g x) (f' x) ≤ ε
⊢ s = s ∩ ⋃ (i : ℕ), t i
exact Subset.antisymm (subset_inter Subset.rfl t_cover) (inter_subset_left _ _)
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
H : ∀ᵐ (x : E) ∂Measure.restrict μ (t n), g x = A n
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n

case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (t n), g x = A n
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n
suffices H : ∀ᵐ x : E ∂μ.restrict (t n), g x = A n
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (t n), g x = A n
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
H : ∀ᵐ (x : E) ∂Measure.restrict μ (t n), g x = A n
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), g x = A n

case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (t n), g x = A n
exact ae_mono (restrict_mono (inter_subset_right _ _) le_rfl) H
case h
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ (a : E), a ∈ t n → g a = A n
case H
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ᵐ (x : E) ∂Measure.restrict μ (t n), g x = A n
filter_upwards [ae_restrict_mem (t_meas n)]
no goals
case h
E : Type u_1
F : Type ?u.709818
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : MeasurableSet s
hf' : ∀ (x : E), x ∈ s → HasFDerivWithinAt f (f' x) s x
ε : ℝ
εpos : ε > 0
δ : ℝ≥0 := { val := ε, property := (_ : 0 ≤ ε) }
δpos : 0 < δ
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) δ
right✝ : Set.Nonempty s → ∀ (n : ℕ), ∃ y, y ∈ s ∧ A n = f' y
g : E → E →L[ℝ] E
g_meas : Measurable g
hg : ∀ (n : ℕ) (x : E), x ∈ t n → g x = A n
n : ℕ
E₁ : ∀ᵐ (x : E) ∂Measure.restrict μ (s ∩ t n), ‖f' x - A n‖₊ ≤ δ
⊢ ∀ (a : E), a ∈ t n → g a = A n
exact hg n