awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] E)) (Lp E p μ) (c • (↑f : α →ₘ[μ] E))
have rw : eLpNorm (c • (↑(↑f : α →ₘ[μ] E) : α → E)) p μ < ∞
Tactic: rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_congr_ae (AEEqFun.coeFn_smul _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
have refine : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
Tactic: refine ⟨(hf.1.enorm.pow_const q.toReal).aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
have pos : ∀ (q_top : q = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
Tactic: by_cases q_top : q = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
pos : ∀ (q_top : q = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
have neg : ∀ (q_top : ¬q = ∞), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
Tactic: by_cases q_top : q = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
have pos : ∀ (q_zero : q = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
Tactic: by_cases q_zero : q = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
pos : ∀ (q_zero : q = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
have neg : ∀ (q_zero : ¬q = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
Tactic: by_cases q_zero : q = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
have pos : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
Tactic: simp only [q_zero, ENNReal.toReal_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
have pos : ∀ (p_zero : p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
Tactic: by_cases p_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
pos : ∀ (p_zero : p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
have neg : ∀ (p_zero : ¬p = 0), eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
Tactic: by_cases p_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) (p / 0) μ < ∞
have neg : eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ₑ 0) ∞ μ < ∞
Tactic: rw [ENNReal.div_zero p_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ < ∞
have neg : eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞
Tactic: rw [eLpNorm_enorm_rpow _ (ENNReal.toReal_pos q_zero q_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞
have neg : eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞
Tactic: apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞
have neg : eLpNorm f p μ ≠ ∞
Tactic: rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
    mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
have refine : eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
Tactic: refine ⟨(hf.1.norm.aemeasurable.pow_const q.toReal).aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
have pos : ∀ (q_top : q = ∞), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
Tactic: by_cases q_top : q = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
pos : ∀ (q_top : q = ∞), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
have neg : ∀ (q_top : ¬q = ∞), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
Tactic: by_cases q_top : q = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
have pos : ∀ (q_zero : q = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
Tactic: by_cases q_zero : q = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
pos : ∀ (q_zero : q = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
have neg : ∀ (q_zero : ¬q = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
Tactic: by_cases q_zero : q = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
have pos : eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
Tactic: simp only [q_zero, ENNReal.toReal_zero, Real.rpow_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
have pos : ∀ (p_zero : p = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
Tactic: by_cases p_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
pos : ∀ (p_zero : p = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
have neg : ∀ (p_zero : ¬p = 0), eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
Tactic: by_cases p_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : q = 0
p_zero : ¬p = 0
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) (p / 0) μ < ∞
have neg : eLpNorm (ε := ℝ) (fun (x : α) ↦ 1) ∞ μ < ∞
Tactic: rw [ENNReal.div_zero p_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ < ∞
have neg : eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞
Tactic: rw [eLpNorm_norm_rpow _ (ENNReal.toReal_pos q_zero q_top)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ^ q.toReal < ∞
have neg : eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞
Tactic: apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
q_top : ¬q = ∞
q_zero : ¬q = 0
⊢ eLpNorm f (p / q * ENNReal.ofReal q.toReal) μ ≠ ∞
have neg : eLpNorm f p μ ≠ ∞
Tactic: rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
    mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ ↔ MemLp f p μ
have refine : ∀ (h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ), MemLp f p μ
Tactic: refine ⟨fun h => ?_, fun h => h.enorm_rpow_div q⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ MemLp f p μ
have apply : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ
Tactic: apply (memLp_enorm_iff hf).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ
have h₁ : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal
Tactic: convert! h.enorm_rpow_div q⁻¹ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal
⊢ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) p μ
have h₂ : p = p / q / q⁻¹
Tactic: convert! h.enorm_rpow_div q⁻¹ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal
have h₁ : ∀ (x : α), ‖f x‖ₑ = ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
x : α
⊢ ‖f x‖ₑ = ‖‖f x‖ₑ ^ q.toReal‖ₑ ^ q⁻¹.toReal
have this : q.toReal * q.toReal⁻¹ = 1
Tactic: have : q.toReal * q.toReal⁻¹ = 1 :=
      CommGroupWithZero.mul_inv_cancel q.toReal <| ENNReal.toReal_ne_zero.mpr ⟨q_zero, q_top⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹
have h₁ : p = p / q * q⁻¹⁻¹
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
⊢ p = p / q / q⁻¹
have h₂ : p = p / q * q
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
⊢ p = p / q / q⁻¹
have h₃ : p = p * q⁻¹ * q
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
h₃ : p = p * q⁻¹ * q
⊢ p = p / q / q⁻¹
have h₄ : p = p * (q⁻¹ * q)
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
h₃ : p = p * q⁻¹ * q
h₄ : p = p * (q⁻¹ * q)
⊢ p = p / q / q⁻¹
have h₅ : p = p * 1
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
h₃ : p = p * q⁻¹ * q
h₄ : p = p * (q⁻¹ * q)
h₅ : p = p * 1
⊢ p = p / q / q⁻¹
have h₆ : p = p
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ
have refine : ∀ (h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ), MemLp f p μ
Tactic: refine ⟨fun h => ?_, fun h => h.norm_rpow_div q⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ MemLp f p μ
have apply : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
Tactic: apply (memLp_norm_iff hf).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
have h₁ : Eq.{u_1 + 1} (α := α → ℝ) (fun (x : α) ↦ ‖f x‖) fun (x : α) ↦ ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal
Tactic: convert! h.norm_rpow_div q⁻¹ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : Eq.{u_1 + 1} (α := α → ℝ) (fun (x : α) ↦ ‖f x‖) fun (x : α) ↦ ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal
⊢ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖) p μ
have h₂ : p = p / q / q⁻¹
Tactic: convert! h.norm_rpow_div q⁻¹ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ Eq.{u_1 + 1} (α := α → ℝ) (fun (x : α) ↦ ‖f x‖) fun (x : α) ↦ ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal
have h₁ : ∀ (x : α), ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
x : α
⊢ ‖f x‖ = ‖‖f x‖ ^ q.toReal‖ ^ q⁻¹.toReal
have h₁ : q.toReal ≠ 0
Tactic: rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg (norm_nonneg _), ← Real.rpow_mul (abs_nonneg _),
      ENNReal.toReal_inv, mul_inv_cancel₀, abs_of_nonneg (norm_nonneg _), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹
have h₁ : p = p / q * q⁻¹⁻¹
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
⊢ p = p / q / q⁻¹
have h₂ : p = p / q * q
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
⊢ p = p / q / q⁻¹
have h₃ : p = p * q⁻¹ * q
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
h₃ : p = p * q⁻¹ * q
⊢ p = p / q / q⁻¹
have h₄ : p = p * (q⁻¹ * q)
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Basic (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q.toReal) (p / q) μ
h₁ : p = p / q * q⁻¹⁻¹
h₂ : p = p / q * q
h₃ : p = p * q⁻¹ * q
h₄ : p = p * (q⁻¹ * q)
⊢ p = p / q / q⁻¹
have h₅ : p = p * 1
Tactic: rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]