awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
A : E →L[ℝ] E
δ' : ℝ
δ'pos : 0 < δ'
hδ' : ∀ (B : E →L[ℝ] E), dist B A < δ' → dist B.det A.det < (↑ε : ℝ)
δ'' : ℝ≥0 := Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (δ' / 2) ⋯
I'' : ∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ'' : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)
hA : A.det ≠ 0
m : ℝ≥0 := |A.det|.toNNReal - ε
I : (↑m : ℝ≥0∞) < ENNReal.ofReal |A.det|
δ : ℝ≥0
h :
  ∀ (s : Set E) (f : E → E),
    ApproximatesLinearOn f A s δ →
      HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (f '' s)
δpos : 0 < δ
t : Set E
g : E → E
htg : ApproximatesLinearOn g A t (min δ δ'')
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this : HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤ (μ : (a : Set E) → ℝ≥0∞) (g '' t)
⊢ HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
have inr : ∀
  (this :
    HMul.hMul (β := ℝ≥0∞) ((↑|A.det|.toNNReal : ℝ≥0∞) - (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
      (μ : (a : Set E) → ℝ≥0∞) (g '' t)),
  0 < (↑ε : ℝ≥0∞) →
    (↑ε : ℝ≥0∞) < (↑|A.det|.toNNReal : ℝ≥0∞) → Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [ENNReal.coe_sub, ENNReal.sub_mul, tsub_le_iff_right] at this
Cleared hypotheses: this
-- 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
have this : ∀ (A : E →L[ℝ] E),
  ∃ (δ : ℝ≥0),
    0 < δ ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t δ →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
Tactic: have :
    ∀ A : E →L[ℝ] E,
      ∃ δ : ℝ≥0,
        0 < δ ∧
          (∀ B : E →L[ℝ] E, ‖B - A‖ ≤ δ → |B.det - A.det| ≤ ε) ∧
            ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t δ →
              ENNReal.ofReal |A.det| * μ t ≤ μ (g '' t) + ε * μ t := by
    intro A
    obtain ⟨δ', δ'pos, hδ'⟩ : ∃ (δ' : ℝ), 0 < δ' ∧ ∀ B, dist B A < δ' → dist B.det A.det < ↑ε := by
      refine continuousAt_iff.1 ?_ ε εpos
      exact ContinuousLinearMap.continuous_det.continuousAt
    let δ'' : ℝ≥0 := ⟨δ' / 2, (half_pos δ'pos).le⟩
    have I'' : ∀ B : E →L[ℝ] E, ‖B - A‖ ≤ ↑δ'' → |B.det - A.det| ≤ ↑ε := by
      intro B hB
      rw [← Real.dist_eq]
      apply (hδ' B _).le
      rw [dist_eq_norm]
      exact hB.trans_lt (half_lt_self δ'pos)
    rcases eq_or_ne A.det 0 with (hA | hA)
    · refine ⟨δ'', half_pos δ'pos, I'', ?_⟩
      simp only [hA, forall_const, zero_mul, ENNReal.ofReal_zero, imp_true_iff,
        zero_le, abs_zero]
    let m : ℝ≥0 := Real.toNNReal |A.det| - ε
    have I : (m : ℝ≥0∞) < ENNReal.ofReal |A.det| := by
      simp only [m, ENNReal.ofReal, ENNReal.coe_sub]
      apply ENNReal.sub_lt_self ENNReal.coe_ne_top
      · simpa only [abs_nonpos_iff, Real.toNNReal_eq_zero, ENNReal.coe_eq_zero, Ne] using hA
      · simp only [εpos.ne', ENNReal.coe_eq_zero, Ne, not_false_iff]
    rcases ((mul_le_addHaar_image_of_lt_det μ A I).and self_mem_nhdsWithin).exists with ⟨δ, h, δpos⟩
    refine ⟨min δ δ'', lt_min δpos (half_pos δ'pos), ?_, ?_⟩
    · intro B hB
      apply I'' _ (hB.trans _)
      simp only [le_refl, NNReal.coe_min, min_le_iff, or_true]
    · intro t g htg
      rcases eq_or_ne (μ t) ∞ with (ht | ht)
      · simp only [ht, εpos.ne', ENNReal.mul_top, ENNReal.coe_eq_zero, le_top, Ne,
          not_false_iff, _root_.add_top]
      have := h t g (htg.mono_num (min_le_left _ _))
      rwa [ENNReal.coe_sub, ENNReal.sub_mul, tsub_le_iff_right] at this
      simp only [ht, imp_true_iff, Ne, not_false_iff]
-- 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
this :
  ∀ (A : E →L[ℝ] E),
    ∃ (δ : ℝ≥0),
      0 < δ ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑δ : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t δ →
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
                HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                  (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
have choose : ∀ (δ : (A : E →L[ℝ] E) → ℝ≥0)
  (hδ :
    ∀ (A : E →L[ℝ] E),
      0 < δ A ∧
        (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
          ∀ (t : Set E) (g : E → E),
            ApproximatesLinearOn g A t (δ A) →
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
                HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                  (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))),
  ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
have obtain : ∀ (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))),
  ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
Tactic: 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) (δ (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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
⊢ s = ⋃ (n : ℕ), s ∩ t n
have rw : s = s ∩ ⋃ (i : ℕ), t i
Tactic: rw [← inter_iUnion]
-- 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞))
have s_eq : s = ⋃ (n : ℕ), s ∩ t n
Tactic: have s_eq : s = ⋃ n, s ∩ t n := by
    rw [← inter_iUnion]
    exact Subset.antisymm (subset_inter Subset.rfl t_cover) 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
| ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
have rw : ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ
Tactic: rw [s_eq]
-- 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
⊢ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ = ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ
have conv_lhs : ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ =
  ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ
Tactic: conv_lhs => rw [s_eq]
-- 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
⊢ ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ
have hm : ∀ (i : ℕ), MeasurableSet (s ∩ t i)
Tactic: rw [lintegral_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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
hm : ∀ (i : ℕ), MeasurableSet (s ∩ t i)
⊢ ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ =
    ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ
have hd : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set E) Disjoint fun (n : ℕ) ↦ s ∩ t n)
Tactic: rw [lintegral_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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
⊢ LE.le (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ)
    (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞) ∂μ)
have apply : ∀ (n : ℕ),
  ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ ≤
    ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞) ∂μ
Tactic: apply ENNReal.tsum_le_tsum fun 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
n : ℕ
⊢ ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| ∂μ ≤
    ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞) ∂μ
have h : ∀ᵐ (a : E) ∂μ.restrict (s ∩ t n), ENNReal.ofReal |(f' a).det| ≤ ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)
Tactic: apply lintegral_mono_ae
-- 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
n : ℕ
⊢ ∀ᵐ (a : E) ∂μ.restrict (s ∩ t n), ENNReal.ofReal |(f' a).det| ≤ ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)
have h : ∀ (a : E), ‖f' a - A n‖₊ ≤ δ (A n) → ENNReal.ofReal |(f' a).det| ≤ ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)
Tactic: filter_upwards [(ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx =>
          (hf' x hx.1).mono 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
⊢ |(f' x).det| = |(A n).det + ((f' x).det - (A n).det)|
have e_a : (f' x).det = (A n).det + ((f' x).det - (A n).det)
Tactic: congr 1
-- 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
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf : InjOn f s
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det|) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞) ≤
              HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (g '' t) : ℝ≥0∞)
                (HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥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))
s_eq : s = ⋃ (n : ℕ), s ∩ t n
n : ℕ
x : E
hx : ‖f' x - A n‖₊ ≤ δ (A n)
⊢ ENNReal.ofReal |(f' x).det| ≤ ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)
have I : |(f' x).det| ≤ |(A n).det| + (↑ε : ℝ)
Tactic: have I : |(f' x).det| ≤ |(A n).det| + ε :=
        calc
          |(f' x).det| = |(A n).det + ((f' x).det - (A n).det)| := by congr 1; abel
          _ ≤ |(A n).det| + |(f' x).det - (A n).det| := abs_add_le _ _
          _ ≤ |(A n).det| + ε := add_le_add le_rfl ((hδ (A n)).2.1 _ hx)