-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem integral_inner_eq_sq_eLpNorm (f : α →₂[μ] E) :
    ∫ a, ⟪f a, f a⟫ ∂μ = ENNReal.toReal (∫⁻ a, (‖f a‖₊ : ℝ≥0∞) ^ (2 : ℝ) ∂μ)

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

case hf
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ 0 ≤ᶠ[ae μ] fun x => ‖↑↑f x‖ ^ 2

case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x => ‖↑↑f x‖ ^ 2) μ

Tactic:
rotate_left

Result:
case hf
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ 0 ≤ᶠ[ae μ] fun x => ‖↑↑f x‖ ^ 2

case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x => ‖↑↑f x‖ ^ 2) μ

α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
⊢ 2 = ↑2

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_f
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (fun a => ENNReal.ofReal (‖↑↑f a‖ ^ 2)) = fun a => ↑(‖↑↑f a‖₊ ^ 2)

Tactic:
ext1 x

Result:
case e_a.e_f.h
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

Tactic:
congr

Result:
case e_a.e_f
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (fun a => ENNReal.ofReal (‖↑↑f a‖ ^ 2)) = fun a => ↑(‖↑↑f a‖₊ ^ 2)

Proof state:
case e_a.e_f.h
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : 2 = ↑2
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)

Tactic:
rw [← Real.rpow_natCast _ 2, ← h_two, ←
  ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) zero_le_two, ofReal_norm_eq_enorm]

Result:
case e_a.e_f.h
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : 2 = ↑2
⊢ ‖↑↑f x‖ₑ ^ 2 = ↑(‖↑↑f x‖₊ ^ 2)

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ ∫ (x : α), ‖↑↑f x‖ ^ 2 ∂μ = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

case hf
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ 0 ≤ᶠ[ae μ] fun x => ‖↑↑f x‖ ^ 2

case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x => ‖↑↑f x‖ ^ 2) μ

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ ∫ (a : α), ↑‖↑↑f a‖ ^ 2 ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal

Tactic:
norm_cast

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ ∫ (x : α), ‖↑↑f x‖ ^ 2 ∂μ = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ ∫ (a : α), inner (↑↑f a) (↑↑f a) ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal

Tactic:
simp_rw [inner_self_eq_norm_sq_to_K]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ ∫ (a : α), ↑‖↑↑f a‖ ^ 2 ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal

Proof state:
case hf
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ 0 ≤ᶠ[ae μ] fun x => ‖↑↑f x‖ ^ 2

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

Result:
no goals

Proof state:
case e_a.e_f.h
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : 2 = ↑2
⊢ ‖↑↑f x‖ₑ ^ 2 = ↑(‖↑↑f x‖₊ ^ 2)

Tactic:
norm_cast

Result:
no goals

Proof state:
case e_a.e_f.h
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)

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

Result:
case e_a.e_f.h
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : 2 = ↑2
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)

Proof state:
case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x => ‖↑↑f x‖ ^ 2) μ

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

Result:
no goals