awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x :
  ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) ^ (n + 1) ∂μ =
    HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
x₁ :
  HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) =
    HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 2 *
      HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n - 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
⊢ ∫⁻ (a : α) in s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)), v.limRatioMeas hρ a ∂μ ≤
    (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞)
      (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))
have x₂ : HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 2 *
    HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n - 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
Tactic: calc
      (∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ) ≤ ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ :=
        lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => hx.2.2.le))
      _ = (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ = (t : ℝ≥0∞) ^ (2 : ℤ) * ((t : ℝ≥0∞) ^ (n - 1) * μ (s ∩ f ⁻¹' I)) := by
        rw [← mul_assoc, ← ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top]
        congr 2
        abel
      _ ≤ (t : ℝ≥0∞) ^ (2 : ℤ) * ρ (s ∩ f ⁻¹' I) := by
        gcongr
        rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne']
        apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
        intro x hx
        apply lt_of_lt_of_le _ hx.2.1
        rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne', ENNReal.coe_lt_coe, sub_eq_add_neg,
          zpow_add₀ t_ne_zero']
        conv_rhs => rw [← mul_one (t ^ n)]
        gcongr
        rw [zpow_neg_one]
        exact inv_lt_one_of_one_lt₀ ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
⊢ (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have C : ∀ (n : ℤ),
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
    ((HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2 • ρ : (a : Set α) → ℝ≥0∞)
        (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) :
      ℝ≥0∞)
Tactic: have C :
    ∀ n : ℤ,
      ν (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) ≤
        ((t : ℝ≥0∞) ^ 2 • ρ :) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) := by
    intro n
    let I := Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))
    have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)
    simp only [ν, I, M, withDensity_apply]
    calc
      (∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ) ≤ ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ :=
        lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => hx.2.2.le))
      _ = (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) := by
        simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
      _ = (t : ℝ≥0∞) ^ (2 : ℤ) * ((t : ℝ≥0∞) ^ (n - 1) * μ (s ∩ f ⁻¹' I)) := by
        rw [← mul_assoc, ← ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top]
        congr 2
        abel
      _ ≤ (t : ℝ≥0∞) ^ (2 : ℤ) * ρ (s ∩ f ⁻¹' I) := by
        gcongr
        rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne']
        apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
        intro x hx
        apply lt_of_lt_of_le _ hx.2.1
        rw [← ENNReal.coe_zpow (zero_lt_one.trans ht).ne', ENNReal.coe_lt_coe, sub_eq_add_neg,
          zpow_add₀ t_ne_zero']
        conv_rhs => rw [← mul_one (t ^ n)]
        gcongr
        rw [zpow_neg_one]
        exact inv_lt_one_of_one_lt₀ ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have t_ne_zero' : t ≠ 0
Tactic: have t_ne_zero' : t ≠ 0 := (zero_lt_one.trans ht).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
Tactic: have t_ne_zero : (t : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using t_ne_zero'
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have f_meas : Measurable f
Tactic: have f_meas : Measurable f := v.limRatioMeas_measurable hρ
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
have grw : LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
Tactic: grw [measure_mono inter_subset_right, v.measure_limRatioMeas_zero hρ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have A : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
  ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
Tactic: have A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0}) := by
    grw [measure_mono inter_subset_right, v.measure_limRatioMeas_zero hρ]
    exact zero_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
have apply : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply (hρ _).le.trans zero_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have B : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
  ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
Tactic: have B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞}) := by
    apply (hρ _).le.trans zero_le
    rw [← nonpos_iff_eq_zero]
    exact (measure_mono inter_subset_right).trans (v.measure_limRatioMeas_top hρ).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
have M : MeasurableSet (s ∩ f ⁻¹' I)
Tactic: have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
have simp : (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) ≤
  (↑t : ℝ≥0∞) * ∫⁻ (a : α) in s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)), v.limRatioMeas hρ a ∂μ
Tactic: simp only [ν, I, M, withDensity_apply, coe_nnreal_smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑t : ℝ≥0∞) ^ (n + 1)) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
have rw : (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) ≤
  HMul.hMul (β := ℝ≥0∞) (↑(t ^ (n + 1)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_zpow t_ne_zero']
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(t ^ (n + 1)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' I) : ℝ≥0∞)
have apply : s ∩ f ⁻¹' I ⊆ {x : α | v.limRatioMeas hρ x < (↑(t ^ (n + 1)) : ℝ≥0∞)}
Tactic: apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x < (↑(t ^ (n + 1)) : ℝ≥0∞)} x
have apply : (↑t : ℝ≥0∞) ^ (n + 1) = (↑(t ^ (n + 1)) : ℝ≥0∞)
Tactic: apply hx.2.2.trans_le (le_of_eq _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ (↑t : ℝ≥0∞) ^ (n + 1) = (↑(t ^ (n + 1)) : ℝ≥0∞)
have rw : (↑t : ℝ≥0∞) ^ (n + 1) = (↑t : ℝ≥0∞) ^ (n + 1)
Tactic: rw [ENNReal.coe_zpow t_ne_zero']
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) ^ (n + 1) ∂μ ≤ ∫⁻ (x : α) in s ∩ f ⁻¹' I, (↑t : ℝ≥0∞) * f x ∂μ
have apply : ∀ (x : α) (hx : x ∈ s ∩ f ⁻¹' I), (↑t : ℝ≥0∞) ^ (n + 1) ≤ (↑t : ℝ≥0∞) * f x
Tactic: apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ (↑t : ℝ≥0∞) ^ (n + 1) ≤ (↑t : ℝ≥0∞) * f x
have grw : (↑t : ℝ≥0∞) ^ (1 + n) ≤ (↑t : ℝ≥0∞) * f x
Tactic: grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
grw : (↑t : ℝ≥0∞) ^ (1 + n) ≤ (↑t : ℝ≥0∞) * f x
⊢ (↑t : ℝ≥0∞) ^ (n + 1) ≤ (↑t : ℝ≥0∞) * f x
have grw₁ : HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 1 * (↑t : ℝ≥0∞) ^ n ≤ (↑t : ℝ≥0∞) * f x
Tactic: grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
n : ℤ
I : Set ℝ≥0∞ := Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
grw : (↑t : ℝ≥0∞) ^ (1 + n) ≤ (↑t : ℝ≥0∞) * f x
grw₁ : HPow.hPow (β := ℤ) (↑t : ℝ≥0∞) 1 * (↑t : ℝ≥0∞) ^ n ≤ (↑t : ℝ≥0∞) * f x
⊢ (↑t : ℝ≥0∞) ^ (n + 1) ≤ (↑t : ℝ≥0∞) * f x
have grw₂ : (↑t : ℝ≥0∞) * (↑t : ℝ≥0∞) ^ n ≤ (↑t : ℝ≥0∞) * f x
Tactic: grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]