awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
pos : ∀ (hxs : UniqueDiffWithinAt ℝ s x), derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
have neg : ∀ (hxs : ¬UniqueDiffWithinAt ℝ s x), derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
Tactic: by_cases hxs : UniqueDiffWithinAt ℝ s x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : ¬UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
have neg : 0 = log a * derivWithin f s x * a ^ f x
Tactic: rw [derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : ¬UniqueDiffWithinAt ℝ s x
neg : 0 = log a * derivWithin f s x * a ^ f x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
have neg₁ : 0 = log a * 0 * a ^ f x
Tactic: rw [derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : ¬UniqueDiffWithinAt ℝ s x
neg : 0 = log a * derivWithin f s x * a ^ f x
neg₁ : 0 = log a * 0 * a ^ f x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
have neg₂ : 0 = 0 * a ^ f x
Tactic: rw [derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
hxs : ¬UniqueDiffWithinAt ℝ s x
neg : 0 = log a * derivWithin f s x * a ^ f x
neg₁ : 0 = log a * 0 * a ^ f x
neg₂ : 0 = 0 * a ^ f x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
have neg₃ : Eq (α := ℝ) 0 0
Tactic: rw [derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      derivWithin_zero_of_not_uniqueDiffWithinAt hxs,
      mul_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x a : ℝ
ha : 0 < a
⊢ deriv (fun (x : ℝ) ↦ a ^ x) x = log a * a ^ x
have rw : log a * deriv (fun (x : ℝ) ↦ x) x * a ^ x = log a * a ^ x
Tactic: rw [deriv_const_rpow ha differentiableAt_fun_id, deriv_id'', mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x a : ℝ
ha : 0 < a
rw : log a * deriv (fun (x : ℝ) ↦ x) x * a ^ x = log a * a ^ x
⊢ deriv (fun (x : ℝ) ↦ a ^ x) x = log a * a ^ x
have rw₁ : log a * (fun (x : ℝ) ↦ (1 : ℝ)) x * a ^ x = log a * a ^ x
Tactic: rw [deriv_const_rpow ha differentiableAt_fun_id, deriv_id'', mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x a : ℝ
ha : 0 < a
rw : log a * deriv (fun (x : ℝ) ↦ x) x * a ^ x = log a * a ^ x
rw₁ : log a * (fun (x : ℝ) ↦ (1 : ℝ)) x * a ^ x = log a * a ^ x
⊢ deriv (fun (x : ℝ) ↦ a ^ x) x = log a * a ^ x
have rw₂ : log a * a ^ x = log a * a ^ x
Tactic: rw [deriv_const_rpow ha differentiableAt_fun_id, deriv_id'', mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ -1 < p - 1
have linarith : p - 1 ≤ -1 → 0 - p + (p - 1 - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have one_lt_p : -1 < p - 1
Tactic: have one_lt_p : -1 < p - 1 := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
x : ℝ
⊢ ∫ (t : ℝ) in 0..x, t ^ (p - 1) = x ^ p / p
have rw : (x ^ (p - 1 + 1) - HPow.hPow (α := ℝ) 0 (p - 1 + 1)) / (p - 1 + 1) = x ^ p / p
Tactic: rw [integral_rpow (Or.inl one_lt_p)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have obs : ∀ (x : ℝ), ∫ (t : ℝ) in 0..x, t ^ (p - 1) = x ^ p / p
Tactic: have obs : ∀ x : ℝ, ∫ t : ℝ in 0..x, t ^ (p - 1) = x ^ p / p := by
    intro x
    rw [integral_rpow (Or.inl one_lt_p)]
    simp [Real.zero_rpow p_pos.ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
have h : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) a → 0 ≤ g a
Tactic: filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
Tactic: have g_nn : ∀ᵐ t ∂volume.restrict (Ioi (0 : ℝ)), 0 ≤ g t := by
    filter_upwards [self_mem_ae_restrict (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))]
    intro t t_pos
    exact Real.rpow_nonneg (mem_Ioi.mp t_pos).le (p - 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
Tactic: have g_intble (t) (ht : 0 < t) : IntervalIntegrable g volume 0 t :=
    intervalIntegral.intervalIntegrable_rpow' one_lt_p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
  ∫⁻ (t : ℝ) in Ioi 0,
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
Tactic: have key := lintegral_comp_eq_lintegral_meas_le_mul μ f_nn f_mble g_intble g_nn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have rw : ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t) ∂μ
Tactic: rw [← key, ← lintegral_const_mul'' (ENNReal.ofReal p)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
rw :
  ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t) ∂μ
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have rw₁ : AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t)) μ
Tactic: rw [← key, ← lintegral_const_mul'' (ENNReal.ofReal p)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (∫ (t : ℝ) in 0..f a, g t) ∂μ
have simp_rw : ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ
Tactic: simp_rw [obs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
⊢ AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t)) μ
have simp_rw : AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (f ω ^ p / p)) μ
Tactic: simp_rw [obs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ
have e_f : ∀ (ω : α), ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
ω : α
⊢ ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)
have e_f : ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal (p * (f ω ^ p / p))
Tactic: rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel₀ (f ω ^ p) p_pos.ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
ω : α
e_f : ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal (p * (f ω ^ p / p))
⊢ ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal p * ENNReal.ofReal (f ω ^ p / p)
have e_f₁ : ENNReal.ofReal (f ω ^ p) = ENNReal.ofReal (f ω ^ p)
Tactic: rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel₀ (f ω ^ p) p_pos.ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : (t : ℝ) → ℝ := fun (t : ℝ) ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ) (ht : 0 < t), IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (g t))
⊢ AEMeasurable (β := ENNReal) (fun (ω : α) ↦ ENNReal.ofReal (f ω ^ p / p)) μ
have aux : AEMeasurable (β := ℝ) (fun (x : α) ↦ p) μ
Tactic: have aux := (measurable_const (a := p)).aemeasurable (μ := μ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have rw : ENNReal.ofReal p *
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
        (ENNReal.ofReal (t ^ (p - 1))) =
  ENNReal.ofReal p *
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
Tactic: rw [lintegral_rpow_eq_lintegral_meas_le_mul μ f_nn f_mble p_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1))) =
    ENNReal.ofReal p *
      ∫⁻ (t : ℝ) in Ioi 0,
        HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)
          (ENNReal.ofReal (t ^ (p - 1)))
have apply : ∫⁻ (t : ℝ) in Ioi 0,
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1))) =
  ∫⁻ (t : ℝ) in Ioi 0,
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
Tactic: apply congr_arg fun z => ENNReal.ofReal p * z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
        (ENNReal.ofReal (t ^ (p - 1))) =
    ∫⁻ (t : ℝ) in Ioi 0,
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
have h : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ENNReal)
  (fun (a : ℝ) ↦
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a_1 : α | a ≤ f a_1} : ENNReal)
      (ENNReal.ofReal (a ^ (p - 1))))
  fun (a : ℝ) ↦
  HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a_1 : α | a < f a_1} : ENNReal) (ENNReal.ofReal (a ^ (p - 1)))
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ENNReal)
    (fun (a : ℝ) ↦
      HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a_1 : α | a ≤ f a_1} : ENNReal)
        (ENNReal.ofReal (a ^ (p - 1))))
    fun (a : ℝ) ↦
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a_1 : α | a < f a_1} : ENNReal)
      (ENNReal.ofReal (a ^ (p - 1)))
have h : ∀ (t : ℝ)
  (ht :
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
      ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)),
  HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1))) =
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
Tactic: filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᶠ[ae μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
t : ℝ
ht :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal)
    ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal)
⊢ HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t ≤ f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1))) =
    HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
have h : HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1))) =
  HMul.hMul (α := ENNReal) ((μ : (a : Set α) → ENNReal) {a : α | t < f a} : ENNReal) (ENNReal.ofReal (t ^ (p - 1)))
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ Nontrivial E
have apply : 0 < Module.finrank ℝ E
Tactic: apply Module.nontrivial_of_finrank_pos (R := ℝ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (hypothesis)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
⊢ IntegrableOn f (ball 0 r) μ
have this : Nontrivial E
Tactic: haveI : Nontrivial E := by
    apply Module.nontrivial_of_finrank_pos (R := ℝ)
    positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Integral (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedAddCommGroup F
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < (↑(Module.finrank ℝ E) : ℝ)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
have pos : ∀ (hr : 0 < r),
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (y : ℝ) ↦ y ^ (HSub.hSub (α := ℝ) (↑(Module.finrank ℝ E) : ℝ) 1 - α)) (Ioo 0 r) volume
Tactic: by_cases! hr : 0 < r