awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
have this : ∀ (A : E →L[ℝ] E),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t δ →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: have :
      ∀ A : E →L[ℝ] E, ∃ δ : ℝ≥0, 0 < δ ∧
        ∀ (t : Set E), ApproximatesLinearOn f A t δ →
          μ (f '' t) ≤ (Real.toNNReal |A.det| + ε : ℝ≥0) * μ t := by
    intro A
    let m : ℝ≥0 := Real.toNNReal |A.det| + ε
    have I : ENNReal.ofReal |A.det| < m := by
      simp only [m, ENNReal.ofReal, lt_add_iff_pos_right, εpos, 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
this :
  ∀ (A : E →L[ℝ] E),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        ∀ (t : Set E),
          ApproximatesLinearOn f A t δ →
            (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
have inr : ∀ (δ : (A : E →L[ℝ] E) → ℝ≥0)
  (hδ :
    ∀ (A : E →L[ℝ] E),
      0 < δ A ∧
        ∀ (t : Set E),
          ApproximatesLinearOn f A t (δ A) →
            (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)),
  (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
Tactic: choose δ hδ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
have inr : ∀ (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) (δ (A n)))
  (Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y),
  (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
Tactic: obtain ⟨t, A, t_disj, t_meas, t_cover, ht, Af'⟩ :
    ∃ (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 = f' y) :=
    exists_partition_approximatesLinearOn_of_hasFDerivWithinAt f s f' hf' δ fun A => (hδ A).1.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ ⋃ (i : ℕ), t i)) : ℝ≥0∞)
Tactic: rw [← image_iUnion, ← inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ ⋃ (i : ℕ), t i)) : ℝ≥0∞)
have h : s ⊆ s ∩ ⋃ (i : ℕ), t i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)))
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
have h : ∀ (i : ℕ),
  (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t i)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(|(A i).det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t i) : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ Eq (α := ℝ≥0∞)
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
have e_f : ∀ (n : ℕ),
  HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞)
Tactic: congr with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
n : ℕ
⊢ HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞)
have e_f : ∀ (y : E) (ys : y ∈ s) (hy : A n = f' y),
  HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞)
Tactic: rcases Af' h's n with ⟨y, ys, hy⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ ∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞) ≤
    (↑ε : ℝ≥0∞) * ∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t n)
have rw : (↑ε : ℝ≥0∞) * ∑' (i : ℕ), (μ : (a : Set E) → ℝ≥0∞) (s ∩ t i) ≤
  (↑ε : ℝ≥0∞) * ∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t n)
Tactic: rw [ENNReal.tsum_mul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ (↑ε : ℝ≥0∞) * ∑' (i : ℕ), (μ : (a : Set E) → ℝ≥0∞) (s ∩ t i) ≤
    (↑ε : ℝ≥0∞) * ∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t n)
have bc : Summable (α := ℝ≥0∞) fun (i : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) (s ∩ t i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
bc : Summable (α := ℝ≥0∞) fun (i : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) (s ∩ t i)
⊢ (↑ε : ℝ≥0∞) * ∑' (i : ℕ), (μ : (a : Set E) → ℝ≥0∞) (s ∩ t i) ≤
    (↑ε : ℝ≥0∞) * ∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t n)
have bc₁ : Summable (α := ℝ≥0∞) fun (i : ℕ) ↦ (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ (↑ε : ℝ≥0∞) * ∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t n) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), closedBall 0 R ∩ t n) : ℝ≥0∞)
have hn : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ closedBall 0 R ∩ t n)
Tactic: rw [measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
hn : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ closedBall 0 R ∩ t n)
⊢ (↑ε : ℝ≥0∞) * ∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t n) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), closedBall 0 R ∩ t n) : ℝ≥0∞)
have h : ∀ (i : ℕ), MeasurableSet (closedBall 0 R ∩ t i)
Tactic: rw [measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), closedBall 0 R ∩ t n) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
have grw : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ ⋃ (i : ℕ), t i) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
Tactic: grw [← inter_iUnion, inter_subset_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
grw :
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ ⋃ (i : ℕ), t i) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), closedBall 0 R ∩ t n) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
have grw₁ : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
Tactic: grw [← inter_iUnion, inter_subset_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥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) (δ (A n))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
Tactic: calc
    μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
      rw [← image_iUnion, ← inter_iUnion]
      gcongr
      exact subset_inter Subset.rfl t_cover
    _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _
    _ ≤ ∑' n, (Real.toNNReal |(A n).det| + ε : ℝ≥0) * μ (s ∩ t n) := by
      gcongr
      exact (hδ (A _)).2 _ (ht _)
    _ = ∑' n, ε * μ (s ∩ t n) := by
      congr with n
      rcases Af' h's n with ⟨y, ys, hy⟩
      simp only [hy, h'f' y ys, Real.toNNReal_zero, abs_zero, zero_add]
    _ ≤ ε * ∑' n, μ (closedBall 0 R ∩ t n) := by
      rw [ENNReal.tsum_mul_left]
      gcongr
    _ = ε * μ (⋃ n, closedBall 0 R ∩ t n) := by
      rw [measure_iUnion]
      · exact pairwise_disjoint_mono t_disj fun n => inter_subset_right
      · intro n
        exact measurableSet_closedBall.inter (t_meas n)
    _ ≤ ε * μ (closedBall 0 R) := by grw [← inter_iUnion, inter_subset_left]