awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f (μ'.trim hm)
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
⊢ Integrable f μ'
have hf : HasFiniteIntegral f (μ'.trim hm)
Tactic: obtain ⟨hf_meas_ae, hf⟩ := hf_int
Cleared hypotheses: hf_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_meas_ae : AEStronglyMeasurable f (μ'.trim hm)
hf : HasFiniteIntegral f (μ'.trim hm)
⊢ Integrable f μ'
have refine : HasFiniteIntegral f μ'
Tactic: refine ⟨aestronglyMeasurable_of_aestronglyMeasurable_trim hm hf_meas_ae, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
G : ℕ → ℝ → ℝ
f : ℝ → ℝ
μ : Measure ℝ
hGf : ∀ᵐ (x : ℝ) ∂μ, Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))
hG : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖G n x‖ₑ) μ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ liminf (fun (x_1 : ℕ) ↦ ‖G x_1 x‖ₑ) atTop) fun (x : ℝ) ↦ ‖f x‖ₑ
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ liminf (fun (x_1 : ℕ) ↦ ‖G x_1 x‖ₑ) atTop = ‖f x‖ₑ) x} x}
    a
Tactic: filter_upwards [hGf] with x hx using hx.enorm.liminf_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L1Space.Integrable (goal)
Goal:
G : ℕ → ℝ → ℝ
f : ℝ → ℝ
μ : Measure ℝ
hGf : ∀ᵐ (x : ℝ) ∂μ, Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))
hG : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖G n x‖ₑ) μ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ Tendsto (fun (n : ℕ) ↦ G n x) atTop (𝓝 (f x))) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ liminf (fun (x_1 : ℕ) ↦ ‖G x_1 x‖ₑ) atTop = ‖f x‖ₑ) x} x}
      a
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : ℝ) ↦ liminf (fun (x_1 : ℕ) ↦ ‖G x_1 x‖ₑ) atTop) fun (x : ℝ) ↦ ‖f x‖ₑ
have h₁ : ∀ (a : ℝ), Tendsto (fun (n : ℕ) ↦ G n a) atTop (𝓝 (f a)) → liminf (fun (x : ℕ) ↦ ‖G x a‖ₑ) atTop = ‖f a‖ₑ
Tactic: filter_upwards [hGf] with x hx using hx.enorm.liminf_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) μ
have rw : MemLp f 2 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) 1 μ
Tactic: rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) 1 μ
have h : ∀ (x : α), HPow.hPow (β := ℕ) ‖f x‖ 2 = ‖f x‖ ^ ENNReal.toReal 2
Tactic: convert! (memLp_norm_rpow_iff hf two_ne_zero ENNReal.ofNat_ne_top).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
h : ∀ (x : α), HPow.hPow (β := ℕ) ‖f x‖ 2 = ‖f x‖ ^ ENNReal.toReal 2
⊢ MemLp f 2 μ ↔ MemLp (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖f x‖ 2) 1 μ
have h₁ : 1 = 2 / 2
Tactic: convert! (memLp_norm_rpow_iff hf two_ne_zero ENNReal.ofNat_ne_top).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2
have h : 1 = HMul.hMul (α := ℝ≥0∞) 2 2⁻¹
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_cancel two_ne_zero ENNReal.ofNat_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
h : 1 = HMul.hMul (α := ℝ≥0∞) 2 2⁻¹
⊢ 1 = 2 / 2
have h₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [div_eq_mul_inv, ENNReal.mul_inv_cancel two_ne_zero ENNReal.ofNat_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) (f x) 2) μ
have h : ∀ (x : α), HPow.hPow (β := ℕ) (f x) 2 = HPow.hPow (β := ℕ) ‖f x‖ 2
Tactic: convert! memLp_two_iff_integrable_sq_norm hf using 3
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
⊢ ‖⟪f x, c⟫‖ ≤ ‖c‖ * ‖f x‖
have rw : ‖⟪f x, c⟫‖ ≤ ‖f x‖ * ‖c‖
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Integrable f μ
⊢ Integrable.{u_3, u_1} (ε := 𝕜) (fun (x : α) ↦ ⟪c, f x⟫) μ
have rw : ∀ (hf : MemLp f 1 μ), MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ ⟪c, f x⟫) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
f : α → E
hf : Integrable f μ
c : E
⊢ Integrable.{u_3, u_1} (ε := 𝕜) (fun (x : α) ↦ ⟪f x, c⟫) μ
have rw : ∀ (hf : MemLp f 1 μ) (c : E), MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ ⟪f x, c⟫) 1 μ
Tactic: rw [← memLp_one_iff_integrable] at hf ⊢
Cleared hypotheses: hf, c
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
inst_4 : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : ∀ (c : E), Eq.{u_3 + 1} (α := 𝕜) (∫ (x : α), ⟪c, f x⟫ ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) 0
have hf_int₁ : Eq.{u_3 + 1} (α := 𝕜) (∫ (x : α), ⟪∫ (x : α), f x ∂μ, f x⟫ ∂μ) 0
Tactic: specialize hf_int (∫ x, f x ∂μ)
Cleared hypotheses: hf_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
inst_4 : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : Eq.{u_3 + 1} (α := 𝕜) (∫ (x : α), ⟪∫ (x : α), f x ∂μ, f x⟫ ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) 0
have rwa : ∀ (hf_int : inner.{u_3, u_2} 𝕜 (E := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ) = 0),
  Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) 0
Tactic: rwa [integral_inner hf, inner_self_eq_zero] at hf_int
Cleared hypotheses: hf_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
inst_4 : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
hf_int : Eq.{u_3 + 1} (α := 𝕜) (∫ (x : α), ⟪∫ (x : α), f x ∂μ, f x⟫ ∂μ) 0
rwa :
  ∀ (hf_int : inner.{u_3, u_2} 𝕜 (E := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ) = 0),
    Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) 0
have rwa₁ : ∀ (hf_int : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) 0), Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) 0
Tactic: rwa [integral_inner hf, inner_self_eq_zero] at hf_int
Cleared hypotheses: hf_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
F : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] F) : α → F) x‖ 2) 1 μ < ∞
have h_two : ENNReal.ofReal 2 = 2
Tactic: have h_two : ENNReal.ofReal (2 : ℝ) = 2 := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
F : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] F) : α → F) x‖ 2) 1 μ < ∞
have rw : HPow.hPow (β := ℝ) (eLpNorm (↑(↑f : α →ₘ[μ] F) : α → F) 2 μ) 2 < ∞
Tactic: rw [eLpNorm_norm_rpow f zero_lt_two, one_mul, h_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
x : α
⊢ ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
    ‖HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
have rw : ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
  ‖HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℕ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
Tactic: rw [← @Nat.cast_two ℝ, Real.rpow_natCast, Real.rpow_natCast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
x : α
⊢ ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ ≤
    2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
have hbc : ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ 2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
x : α
⊢ ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
    ‖HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℕ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
have g₁ : ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ ≤
  2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
Tactic: calc
      ‖⟪f x, g x⟫‖ ≤ ‖f x‖ * ‖g x‖ := norm_inner_le_norm _ _
      _ ≤ 2 * ‖f x‖ * ‖g x‖ := by
        gcongr
        exact le_mul_of_one_le_left (norm_nonneg _) one_le_two
      -- TODO(kmill): the type ascription is getting around an elaboration error
      _ ≤ ‖(‖f x‖ ^ 2 + ‖g x‖ ^ 2 : ℝ)‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
⊢ eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞
have h : ∀ (x : α),
  ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
    ‖HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
Tactic: have h : ∀ x, ‖⟪f x, g x⟫‖ ≤ ‖‖f x‖ ^ (2 : ℝ) + ‖g x‖ ^ (2 : ℝ)‖ := by
    intro x
    rw [← @Nat.cast_two ℝ, Real.rpow_natCast, Real.rpow_natCast]
    calc
      ‖⟪f x, g x⟫‖ ≤ ‖f x‖ * ‖g x‖ := norm_inner_le_norm _ _
      _ ≤ 2 * ‖f x‖ * ‖g x‖ := by
        gcongr
        exact le_mul_of_one_le_left (norm_nonneg _) one_le_two
      -- TODO(kmill): the type ascription is getting around an elaboration error
      _ ≤ ‖(‖f x‖ ^ 2 + ‖g x‖ ^ 2 : ℝ)‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h :
  ∀ (x : α),
    ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
      ‖HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
⊢ eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞
have refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) μ
Tactic: refine (eLpNorm_mono_ae (ae_of_all _ h)).trans_lt ((eLpNorm_add_le ?_ ?_ le_rfl).trans_lt ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h :
  ∀ (x : α),
    ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
      ‖HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) μ
⊢ eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞
have refine_2 : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) μ
Tactic: refine (eLpNorm_mono_ae (ae_of_all _ h)).trans_lt ((eLpNorm_add_le ?_ ?_ le_rfl).trans_lt ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h :
  ∀ (x : α),
    ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
      ‖HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) μ
refine_2 : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) μ
⊢ eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞
have refine_3 : eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ +
    eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ <
  ∞
Tactic: refine (eLpNorm_mono_ae (ae_of_all _ h)).trans_lt ((eLpNorm_add_le ?_ ?_ le_rfl).trans_lt ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
h :
  ∀ (x : α),
    ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
      ‖HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
⊢ eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ +
      eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ <
    ∞
have refine_3 : eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ < ∞ ∧
  eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ < ∞
Tactic: rw [ENNReal.add_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (↑(∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ).toReal : 𝕜)
have simp_rw : Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), HPow.hPow (α := 𝕜) (β := ℕ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ : 𝕜) 2 ∂μ)
  (↑(∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ).toReal : 𝕜)
Tactic: simp_rw [inner_self_eq_norm_sq_to_K]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), HPow.hPow (α := 𝕜) (β := ℕ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ : 𝕜) 2 ∂μ)
    (↑(∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ).toReal : 𝕜)
have norm_cast : ∫ (x : α), HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 ∂μ =
  (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ ∫ (x : α), HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 ∂μ =
    (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
have rw : (∫⁻ (a : α), ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) ∂μ).toReal =
  (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
rw :
  (∫⁻ (a : α), ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) ∂μ).toReal =
    (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
⊢ ∫ (x : α), HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 ∂μ =
    (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
have hf : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2
Tactic: rw [integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
rw :
  (∫⁻ (a : α), ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) ∂μ).toReal =
    (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
hf : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2
⊢ ∫ (x : α), HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 ∂μ =
    (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
have hfm : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) ∂μ).toReal =
    (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
have e_a : Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2))
  fun (a : α) ↦ (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ Eq.{u_1 + 1} (α := α → ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2))
    fun (a : α) ↦ (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞)
have e_a : ∀ (x : α),
  ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2) =
    (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
⊢ ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2) =
    (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
have h_two : Eq (α := ℝ) 2 (↑2 : ℝ)
Tactic: have h_two : (2 : ℝ) = ((2 : ℕ) : ℝ) := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : Eq (α := ℝ) 2 (↑2 : ℝ)
⊢ ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2) =
    (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
have e_a : HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ 2 =
  (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
Tactic: rw [← Real.rpow_natCast _ 2, ← h_two, ←
    ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) zero_le_two, ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : Eq (α := ℝ) 2 (↑2 : ℝ)
⊢ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ 2 =
    (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
have e_a : HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ 2 =
  (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = (RCLike.re : (a : 𝕜) → ℝ) ⟪f, f⟫
have h_two : ENNReal.toReal 2 = 2
Tactic: have h_two : (2 : ℝ≥0∞).toReal = 2 := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = (RCLike.re : (a : 𝕜) → ℝ) ⟪f, f⟫
have rw : HPow.hPow (β := ℕ) (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ) 2 =
  ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ
Tactic: rw [inner_def, integral_inner_eq_sq_eLpNorm, norm_def, ← ENNReal.toReal_pow, RCLike.ofReal_re,
    ENNReal.toReal_eq_toReal_iff' (ENNReal.pow_ne_top (Lp.eLpNorm_ne_top f)) _]