awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 : MemLp f 1 μ
c : E
⊢ MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ ⟪f x, c⟫) 1 μ

Tactic:
hf.inner_const c

Premises used: MeasureTheory.MemLp.inner_const
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 : MemLp f 1 μ
c : E
⊢ MemLp.{u_1, u_3} (ε := 𝕜) (fun (x : α) ↦ ⟪f x, c⟫) 1 μ

Tactic:
exact hf.inner_const c

Premises used: MeasureTheory.MemLp.inner_const
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ
c : E
⊢ ∫ (x : α), ⟪c, f x⟫ ∂μ = ⟪c, ∫ (x : α), f x ∂μ⟫

Tactic:
((innerSL 𝕜 c).restrictScalars ℝ).integral_comp_comm hf

Premises used: Real, ContinuousLinearMap.restrictScalars, innerSL, ContinuousLinearMap.integral_comp_comm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.L2Space
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_3 + 1} (α := 𝕜) (∫ (x : α), ⟪∫ (x : α), f x ∂μ, f x⟫ ∂μ) 0

Tactic:
specialize hf_int (∫ x, f x ∂μ)

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Function.L2Space
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
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hf_int : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) 0), 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

Premises used: integral_inner, inner_self_eq_zero
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
F : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
⊢ ENNReal.ofReal 2 = 2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
F : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
⊢ ENNReal.ofReal 2 = 2

Tactic:
have h_two : ENNReal.ofReal (2 : ℝ) = 2 := by simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
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
rw : HPow.hPow (β := ℝ) (eLpNorm (↑(↑f : α →ₘ[μ] F) : α → F) 2 μ) 2 < ∞
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] F) : α → F) x‖ 2) 1 μ < ∞

Tactic:
rw [eLpNorm_norm_rpow f zero_lt_two, one_mul, h_two]

Premises used: MeasureTheory.AEEqFun.cast, MeasureTheory.eLpNorm_norm_rpow, zero_lt_two, Subtype.val, one_mul
-- Module: Mathlib.MeasureTheory.Function.L2Space
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
⊢ HPow.hPow (β := ℝ) (eLpNorm (↑(↑f : α →ₘ[μ] F) : α → F) 2 μ) 2 < ∞

Tactic:
ENNReal.rpow_lt_top_of_nonneg zero_le_two (Lp.eLpNorm_ne_top f)

Premises used: zero_le_two, ENNReal.rpow_lt_top_of_nonneg, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.L2Space
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
⊢ HPow.hPow (β := ℝ) (eLpNorm (↑(↑f : α →ₘ[μ] F) : α → F) 2 μ) 2 < ∞

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg zero_le_two (Lp.eLpNorm_ne_top f)

Premises used: zero_le_two, ENNReal.rpow_lt_top_of_nonneg, MeasureTheory.Lp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 : α
rw :
  ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
    ‖HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℕ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖
⊢ ‖⟪(↑(↑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]

Premises used: Nat.cast_two, Real.rpow_natCast
-- Module: Mathlib.MeasureTheory.Function.L2Space
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⟫‖ ≤
    ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖

Tactic:
norm_inner_le_norm _ _

Premises used: norm_inner_le_norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 : α
hbc : ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ ≤ 2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖
⊢ ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ ≤
    2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.L2Space
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‖ ≤ 2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖

Tactic:
le_mul_of_one_le_left (norm_nonneg _) one_le_two

Premises used: le_mul_of_one_le_left, one_le_two, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.L2Space
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‖ ≤ 2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖

Tactic:
exact le_mul_of_one_le_left (norm_nonneg _) one_le_two

Premises used: le_mul_of_one_le_left, one_le_two, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 : α
⊢ 2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ ≤
    ‖HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℕ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖

Tactic:
(two_mul_le_add_sq _ _).trans (le_abs_self _)

Premises used: two_mul_le_add_sq, le_abs_self, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 : α
g₁ :
  ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ ≤
    2 * ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ * ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖
⊢ ‖⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫‖ ≤
    ‖HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 + HPow.hPow (β := ℕ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) x‖ 2‖

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 _)

Premises used: Norm.norm, two_mul_le_add_sq, le_abs_self, MeasureTheory.AEEqFun.cast, HPow.hPow, HAdd.hAdd, LE.le.trans, OfNat.ofNat, Subtype.val, norm_inner_le_norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
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‖

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 _)
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ < ∞

Tactic:
(eLpNorm_mono_ae (ae_of_all _ h)).trans_lt ((eLpNorm_add_le ?_ ?_ le_rfl).trans_lt ?_)

Premises used: le_rfl, MeasureTheory.eLpNorm_mono_ae, MeasureTheory.ae_of_all, MeasureTheory.eLpNorm_add_le, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.L2Space
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) μ
refine_3 :
  eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ +
      eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ <
    ∞
⊢ eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞

Tactic:
refine (eLpNorm_mono_ae (ae_of_all _ h)).trans_lt ((eLpNorm_add_le ?_ ?_ le_rfl).trans_lt ?_)

Premises used: le_rfl, MeasureTheory.eLpNorm_mono_ae, MeasureTheory.ae_of_all, MeasureTheory.eLpNorm_add_le, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.L2Space
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‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) μ

Tactic:
((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
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‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) μ

Tactic:
exact ((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
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‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) μ

Tactic:
((Lp.aestronglyMeasurable g).norm.aemeasurable.pow_const _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
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‖
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) μ

Tactic:
exact ((Lp.aestronglyMeasurable g).norm.aemeasurable.pow_const _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
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_3 :
  eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ < ∞ ∧
    eLpNorm (ε := ℝ) (fun (a : α) ↦ HPow.hPow (β := ℝ) ‖(↑(↑g : α →ₘ[μ] E) : α → E) a‖ 2) 1 μ < ∞
⊢ 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]

Premises used: ENNReal.add_lt_top
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ < ∞

Tactic:
⟨eLpNorm_rpow_two_norm_lt_top f, eLpNorm_rpow_two_norm_lt_top g⟩

Premises used: And.intro, MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ < ∞

Tactic:
exact ⟨eLpNorm_rpow_two_norm_lt_top f, eLpNorm_rpow_two_norm_lt_top g⟩
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
⊢ ⟪f, g⟫ = ∫ (a : α), ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
simp_rw :
  Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), HPow.hPow (α := 𝕜) (β := ℕ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ : 𝕜) 2 ∂μ)
    (↑(∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ).toReal : 𝕜)
⊢ Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (↑(∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ).toReal : 𝕜)

Tactic:
simp_rw [inner_self_eq_norm_sq_to_K]

Premises used: inner_self_eq_norm_sq_to_K
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
norm_cast :
  ∫ (x : α), HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2 ∂μ =
    (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal
⊢ Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), HPow.hPow (α := 𝕜) (β := ℕ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ : 𝕜) 2 ∂μ)
    (↑(∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ).toReal : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Function.L2Space
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
hfm : AEStronglyMeasurable (β := ℝ) (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

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2

Tactic:
Filter.Eventually.of_forall fun x => sq_nonneg _

Premises used: Norm.norm, MeasureTheory.AEEqFun.cast, Filter.Eventually.of_forall, sq_nonneg, Filter.EventuallyLE, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2

Tactic:
exact Filter.Eventually.of_forall fun x => sq_nonneg _

Premises used: Filter.Eventually.of_forall, sq_nonneg
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2) μ

Tactic:
((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2) μ

Tactic:
exact ((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.norm
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
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∞)
⊢ (∫⁻ (a : α), ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ 2) ∂μ).toReal =
    (∫⁻ (a : α), (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ 2) : ℝ≥0∞) ∂μ).toReal

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 μ)
e_a :
  ∀ (x : α),
    ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2) =
      (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
⊢ 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:
ext1 x
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 : α
⊢ Eq (α := ℝ) 2 (↑2 : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
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 : α
⊢ Eq (α := ℝ) 2 (↑2 : ℝ)

Tactic:
have h_two : (2 : ℝ) = ((2 : ℕ) : ℝ) := by simp