E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
⊢ ↑↑μ (f '' s) ≤ 0
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
⊢ ↑↑μ (f '' s) = 0
refine' le_antisymm _ (zero_le _)
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
this :
  ∀ (A : E →L[ℝ] E),
    ∃ δ,
      0 < δ ∧
        ∀ (t : Set E),
          ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
⊢ ↑↑μ (f '' s) ≤ 0
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
⊢ ↑↑μ (f '' s) ≤ 0
have :
    ∀ A : E →L[ℝ] E, ∃ δ : ℝ≥0, 0 < δ ∧
      ∀ (t : Set E), ApproximatesLinearOn f A t δ →
        μ (f '' t) ≤ (Real.toNNReal (|A.det|) + 1 : ℝ≥0) * μ t := by
  intro A
  let m : ℝ≥0 := Real.toNNReal (|A.det|) + 1
  have I : ENNReal.ofReal (|A.det|) < m := by
    simp only [ENNReal.ofReal, lt_add_iff_pos_right, zero_lt_one, ENNReal.coe_lt_coe]
  rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩
  exact ⟨δ, h', fun t ht => h t f ht⟩
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
⊢ ↑↑μ (f '' s) ≤ 0
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
this :
  ∀ (A : E →L[ℝ] E),
    ∃ δ,
      0 < δ ∧
        ∀ (t : Set E),
          ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
⊢ ↑↑μ (f '' s) ≤ 0
choose δ hδ using this
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ ↑↑μ (f '' s) ≤ 0
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
⊢ ↑↑μ (f '' s) ≤ 0
obtain ⟨t, A, _, _, 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) (δ (A n))) ∧
            (s.Nonempty → ∀ n, ∃ y ∈ s, A n = fderivWithin ℝ f s y) :=
  exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s (fderivWithin ℝ f s)
    (fun x xs => (hf x xs).hasFDerivWithinAt) δ fun A => (hδ A).1.ne'
no goals
case intro.intro.intro.intro.intro.intro
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ ↑↑μ (f '' s) ≤ 0
calc
  μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
    apply measure_mono
    rw [← image_iUnion, ← inter_iUnion]
    exact image_subset f (subset_inter Subset.rfl t_cover)
  _ ≤ ∑' n, μ (f '' (s ∩ t n)) := (measure_iUnion_le _)
  _ ≤ ∑' n, (Real.toNNReal (|(A n).det|) + 1 : ℝ≥0) * μ (s ∩ t n) := by
    apply ENNReal.tsum_le_tsum fun n => ?_
    apply (hδ (A n)).2
    exact ht n
  _ ≤ ∑' n, ((Real.toNNReal (|(A n).det|) + 1 : ℝ≥0) : ℝ≥0∞) * 0 := by
    refine' ENNReal.tsum_le_tsum fun n => mul_le_mul_left' _ _
    exact le_trans (measure_mono (inter_subset_left _ _)) (le_of_eq hs)
  _ = 0 := by simp only [tsum_zero, MulZeroClass.mul_zero]
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
⊢ ∀ (A : E →L[ℝ] E),
    ∃ δ,
      0 < δ ∧
        ∀ (t : Set E),
          ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
intro A
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
let m : ℝ≥0 := Real.toNNReal (|A.det|) + 1
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1
I : ENNReal.ofReal (abs (ContinuousLinearMap.det A)) < ↑m
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
have I : ENNReal.ofReal (|A.det|) < m := by
  simp only [ENNReal.ofReal, lt_add_iff_pos_right, zero_lt_one, ENNReal.coe_lt_coe]
case intro.intro
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1
I : ENNReal.ofReal (abs (ContinuousLinearMap.det A)) < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑↑μ (f '' s) ≤ ↑m * ↑↑μ s
h' : 0 < δ
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1
I : ENNReal.ofReal (abs (ContinuousLinearMap.det A)) < ↑m
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
rcases ((addHaar_image_le_mul_of_det_lt μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, h'⟩
no goals
case intro.intro
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1
I : ENNReal.ofReal (abs (ContinuousLinearMap.det A)) < ↑m
δ : ℝ≥0
h : ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑↑μ (f '' s) ≤ ↑m * ↑↑μ s
h' : 0 < δ
⊢ ∃ δ,
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
exact ⟨δ, h', fun t ht => h t f ht⟩
no goals
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
A : E →L[ℝ] E
m : ℝ≥0 := Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1
⊢ ENNReal.ofReal (abs (ContinuousLinearMap.det A)) < ↑m
simp only [ENNReal.ofReal, lt_add_iff_pos_right, zero_lt_one, ENNReal.coe_lt_coe]
case h
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ f '' s ⊆ ⋃ (n : ℕ), f '' (s ∩ t n)
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ ↑↑μ (f '' s) ≤ ↑↑μ (⋃ (n : ℕ), f '' (s ∩ t n))
apply measure_mono
case h
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ f '' s ⊆ f '' (s ∩ ⋃ (i : ℕ), t i)
case h
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ f '' s ⊆ ⋃ (n : ℕ), f '' (s ∩ t n)
rw [← image_iUnion, ← inter_iUnion]
no goals
case h
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ f '' s ⊆ f '' (s ∩ ⋃ (i : ℕ), t i)
exact image_subset f (subset_inter Subset.rfl t_cover)
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ ↑↑μ (f '' (s ∩ t n)) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det (A n))) + 1) * ↑↑μ (s ∩ t n)
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ (∑' (n : ℕ), ↑↑μ (f '' (s ∩ t n))) ≤
    ∑' (n : ℕ), ↑(Real.toNNReal (abs (ContinuousLinearMap.det (A n))) + 1) * ↑↑μ (s ∩ t n)
apply ENNReal.tsum_le_tsum fun n => ?_
case a
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ ↑↑μ (f '' (s ∩ t n)) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det (A n))) + 1) * ↑↑μ (s ∩ t n)
apply (hδ (A n)).2
no goals
case a
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
exact ht n
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ ↑↑μ (s ∩ t n) ≤ 0
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ (∑' (n : ℕ), ↑(Real.toNNReal (abs (ContinuousLinearMap.det (A n))) + 1) * ↑↑μ (s ∩ t n)) ≤
    ∑' (n : ℕ), ↑(Real.toNNReal (abs (ContinuousLinearMap.det (A n))) + 1) * 0
refine' ENNReal.tsum_le_tsum fun n => mul_le_mul_left' _ _
no goals
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
n : ℕ
⊢ ↑↑μ (s ∩ t n) ≤ 0
exact le_trans (measure_mono (inter_subset_left _ _)) (le_of_eq hs)
no goals
E : Type u_1
F : Type ?u.556355
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 μ
hf : DifferentiableOn ℝ f s
hs : ↑↑μ s = 0
δ : (E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) → ↑↑μ (f '' t) ≤ ↑(Real.toNNReal (abs (ContinuousLinearMap.det A)) + 1) * ↑↑μ t
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
left✝¹ : Pairwise (Disjoint on t)
left✝ : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
⊢ (∑' (n : ℕ), ↑(Real.toNNReal (abs (ContinuousLinearMap.det (A n))) + 1) * 0) = 0
simp only [tsum_zero, MulZeroClass.mul_zero]