awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : (a : α) → ℝ≥0∞ := fun (a : α) ↦ 2 * ENNReal.ofReal (bound a)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ‖F 0 a‖ ≤ bound a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ bound x) x} x}
      a
⊢ 0 ≤ᶠ[ae μ] bound
have h₂ : ∀ (a : α), ‖F 0 a‖ ≤ bound a → 0 a ≤ bound a
Tactic: filter_upwards [h_bound 0] with _ h using le_trans (norm_nonneg _) h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞
have rw : ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Tactic: rw [lintegral_const_mul']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
rw : ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞
have hr : ‖c‖ₑ ≠ ∞
Tactic: rw [lintegral_const_mul']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedAddCommGroup 𝕜
inst_2 : SMulZeroClass 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ∞
have a : ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞
Tactic: calc
    ∫⁻ a : α, ‖c • f a‖ₑ ∂μ ≤ ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_mono fun i ↦ enorm_smul_le
    _ < ∞ := by
      rw [lintegral_const_mul']
      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞
have rw : ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Tactic: rw [lintegral_const_mul']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
rw : ‖c‖ₑ * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞
have hr : ‖c‖ₑ ≠ ∞
Tactic: rw [lintegral_const_mul']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
ε'' : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
𝕜 : Type u_7
inst_2 : NormedAddGroup 𝕜
inst_3 : SMul 𝕜 ε''
inst_4 : ENormSMulClass 𝕜 ε''
c : 𝕜
f : α → ε''
hf : HasFiniteIntegral f μ
⊢ ∫⁻ (a : α), ‖(c • f) a‖ₑ ∂μ < ∞
have a : ∫⁻ (a : α), ‖c‖ₑ * ‖f a‖ₑ ∂μ < ∞
Tactic: calc
    ∫⁻ a : α, ‖c • f a‖ₑ ∂μ = ∫⁻ a : α, ‖c‖ₑ * ‖f a‖ₑ ∂μ := lintegral_congr fun i ↦ enorm_smul _ _
    _ < ∞ := by
      rw [lintegral_const_mul']
      exacts [mul_lt_top coe_lt_top hf, coe_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
c : 𝕜
hc : IsUnit c
f : α → β
⊢ HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ
have obtain : ∀ (c : 𝕜ˣ), HasFiniteIntegral ((↑c : 𝕜) • f) μ ↔ HasFiniteIntegral f μ
Tactic: obtain ⟨c, rfl⟩ := hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral ((↑c : 𝕜) • f) μ ↔ HasFiniteIntegral f μ
have mp : HasFiniteIntegral ((↑c : 𝕜) • f) μ → HasFiniteIntegral f μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
𝕜 : Type u_7
inst_1 : NormedRing 𝕜
inst_2 : MulActionWithZero 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
mp : HasFiniteIntegral ((↑c : 𝕜) • f) μ → HasFiniteIntegral f μ
⊢ HasFiniteIntegral ((↑c : 𝕜) • f) μ ↔ HasFiniteIntegral f μ
have mpr : HasFiniteIntegral f μ → HasFiniteIntegral ((↑c : 𝕜) • f) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral (goal)
Goal:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
s : Set α
⊢ HasFiniteIntegral f (μ.restrict s)
have refine : ∫⁻ (a : α) in s, ‖f a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
Tactic: refine lt_of_le_of_lt ?_ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
⊢ MemLp f 1 μ ↔ Integrable f μ
have simp_rw : MemLp f 1 μ ↔ AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
Tactic: simp_rw [Integrable, hasFiniteIntegral_iff_enorm, MemLp, eLpNorm_one_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
simp_rw : MemLp f 1 μ ↔ AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
⊢ MemLp f 1 μ ↔ Integrable f μ
have simp_rw₁ : MemLp f 1 μ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Tactic: simp_rw [Integrable, hasFiniteIntegral_iff_enorm, MemLp, eLpNorm_one_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
simp_rw : MemLp f 1 μ ↔ AEStronglyMeasurable f μ ∧ HasFiniteIntegral f μ
simp_rw₁ : MemLp f 1 μ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
⊢ MemLp f 1 μ ↔ Integrable f μ
have simp_rw₂ : AEStronglyMeasurable f μ ∧ eLpNorm f 1 μ < ∞ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Tactic: simp_rw [Integrable, hasFiniteIntegral_iff_enorm, MemLp, eLpNorm_one_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
⊢ Integrable.{u_5, u_1} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
have this : AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ
Tactic: have : AEStronglyMeasurable (fun _ : α => c) μ := aestronglyMeasurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
this : AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ
⊢ Integrable.{u_5, u_1} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
have rw : AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ ∧
    HasFiniteIntegral.{u_1, u_5} (ε := ε) (fun (x : α) ↦ c) μ ↔
  ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
Tactic: rw [Integrable, and_iff_right this, hasFiniteIntegral_const_iff_enorm hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
this : AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ
rw :
  AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ ∧
      HasFiniteIntegral.{u_1, u_5} (ε := ε) (fun (x : α) ↦ c) μ ↔
    ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
⊢ Integrable.{u_5, u_1} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
have rw₁ : HasFiniteIntegral.{u_1, u_5} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
Tactic: rw [Integrable, and_iff_right this, hasFiniteIntegral_const_iff_enorm hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ε
hc : ‖c‖ₑ ≠ ∞
this : AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ
rw :
  AEStronglyMeasurable.{u_1, u_5} (β := ε) (fun (x : α) ↦ c) μ ∧
      HasFiniteIntegral.{u_1, u_5} (ε := ε) (fun (x : α) ↦ c) μ ↔
    ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
rw₁ : HasFiniteIntegral.{u_1, u_5} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
⊢ Integrable.{u_5, u_1} (ε := ε) (fun (x : α) ↦ c) μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
have rw₂ : ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ ↔ ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ
Tactic: rw [Integrable, and_iff_right this, hasFiniteIntegral_const_iff_enorm hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
c : β
⊢ Integrable.{u_2, u_1} (ε := β) (fun (x : α) ↦ c) μ ↔ c = 0 ∨ IsFiniteMeasure μ
have rw : ‖c‖ₑ = 0 ∨ IsFiniteMeasure μ ↔ c = 0 ∨ IsFiniteMeasure μ
Tactic: rw [integrable_const_iff_enorm enorm_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
have rw : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ
Tactic: rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
have rw : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ
Tactic: rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
have pos : ∀ (h_zero : p = 0), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
Tactic: by_cases h_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
pos : ∀ (h_zero : p = 0), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
have neg : ∀ (h_zero : ¬p = 0), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
Tactic: by_cases h_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
have pos : ∀ (h_top : p = ∞), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
pos : ∀ (h_top : p = ∞), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
have neg : ∀ (h_top : ¬p = ∞), Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
have pos : ∀ (h_zero : p = 0), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
Tactic: by_cases h_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
pos : ∀ (h_zero : p = 0), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
have neg : ∀ (h_zero : ¬p = 0), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
Tactic: by_cases h_zero : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
have pos : ∀ (h_top : p = ∞), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
h_zero : ¬p = 0
pos : ∀ (h_top : p = ∞), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
have neg : ∀ (h_top : ¬p = ∞), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ
Tactic: by_cases h_top : p = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ ↔ MemLp f p μ
have rw : Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ ↔
  MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (p / p) μ
Tactic: rw [← memLp_enorm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
    ENNReal.div_self p_zero p_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
rw :
  Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ ↔
    MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (p / p) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ ↔ MemLp f p μ
have rw₁ : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ ↔ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (p / p) μ
Tactic: rw [← memLp_enorm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
    ENNReal.div_self p_zero p_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
rw :
  Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ ↔
    MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (p / p) μ
rw₁ :
  MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ ↔
    MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) (p / p) μ
⊢ Integrable (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ ↔ MemLp f p μ
have rw₂ : MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ ↔ MemLp (ε := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) 1 μ
Tactic: rw [← memLp_enorm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
    ENNReal.div_self p_zero p_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp f p μ
have rw : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) (p / p) μ
Tactic: rw [← memLp_norm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
    ENNReal.div_self p_zero p_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
rw : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) (p / p) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp f p μ
have rw₁ : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) (p / p) μ
Tactic: rw [← memLp_norm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
    ENNReal.div_self p_zero p_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : AEStronglyMeasurable f μ
p_zero : p ≠ 0
p_top : p ≠ ∞
rw : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) (p / p) μ
rw₁ : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) (p / p) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) μ ↔ MemLp f p μ
have rw₂ : MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p.toReal) 1 μ
Tactic: rw [← memLp_norm_rpow_iff (q := p) hf p_zero p_top, ← memLp_one_iff_integrable,
    ENNReal.div_self p_zero p_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
have inl : ∀ (hp : LE.le (α := ℝ) 0 0) (hpq : 0 ≤ q), Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ 0) μ
Tactic: rcases hp.eq_or_lt with (rfl | hp)
Cleared hypotheses: p, hp, hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
inl : ∀ (hp : LE.le (α := ℝ) 0 0) (hpq : 0 ≤ q), Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ 0) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
have inr : ∀ (hp : 0 < p), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
Tactic: rcases hp.eq_or_lt with (rfl | hp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
have inr : ∀ (hq : LE.le (α := ℝ) 0 0) (hpq : p ≤ 0) (hint : Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ 0) μ),
  Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
Tactic: rcases hq.eq_or_lt with (rfl | hq)
Cleared hypotheses: q, hq, hpq, hint
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
inr :
  ∀ (hq : LE.le (α := ℝ) 0 0) (hpq : p ≤ 0) (hint : Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ 0) μ),
    Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
have inr₁ : ∀ (hq : 0 < q), Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
Tactic: rcases hq.eq_or_lt with (rfl | hq)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
have inr : MemLp f (ENNReal.ofReal p) μ
Tactic: rw [← ENNReal.toReal_ofReal hp.le, integrable_norm_rpow_iff hf (by simp [hp]) (by simp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ MemLp f (ENNReal.ofReal p) μ
have hint₁ : MemLp f (ENNReal.ofReal q) μ
Tactic: rw [← ENNReal.toReal_ofReal hq.le, integrable_norm_rpow_iff hf (by simp [hq]) (by simp)] at hint
Cleared hypotheses: hint, hp, hq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℕ
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ
have simp_rw : ∀ (hint : Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ (↑q : ℝ)) μ),
  Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ (↑p : ℝ)) μ
Tactic: simp_rw [← Real.rpow_natCast] at *
Cleared hypotheses: hint
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : Integrable f μ
⊢ Integrable f μ'
have rw : ∀ (hf : MemLp f 1 μ), MemLp f 1 μ'
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf