Prove2Me

`BookProof.NsScalarVectorCurry.eLpNorm_two_sq` {X : Type*} [MeasurableSpace X] {E : Type*} [NormedAddCommGroup E] (ρ : Measure X) (h : X → E) : (eLpNorm h 2 ρ) ^ 2 = ∫⁻ x, ‖h x‖ₑ ^

Proved
BookProof.NsScalarVectorCurry.eLpNorm_two_sq

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterNsScalarVectorCurry.

BookProof.NsScalarVectorCurry.eLpNorm_two_sq {X : Type*} [MeasurableSpace X] {E : Type*} [NormedAddCommGroup E] (ρ : Measure X) (h : X → E) : (eLpNorm h 2 ρ) ^ 2 = ∫⁻ x, ‖h x‖ₑ ^ (2 : ℝ) ∂ρ

Formalization note: Lean 4 identifier BookProof.NsScalarVectorCurry.eLpNorm_two_sq.

Preamble
-- Generated from ChapterNsScalarVectorCurry.lean — theorem BookProof.NsScalarVectorCurry.eLpNorm_two_sq
import Mathlib
import Definitions.Def_ChapterNsScalarVectorCurry
open BookProof.NsScalarVectorCurry


open MeasureTheory Filter Set
open scoped ENNReal ComplexConjugate


noncomputable section

variable {V W : Type*} [MeasurableSpace V] [MeasurableSpace W]
  {μ : Measure V} {ν : Measure W}

variable [SigmaFinite μ] [SigmaFinite ν]
Formal statement
theorem BookProof.NsScalarVectorCurry.eLpNorm_two_sq {X : Type*} [MeasurableSpace X] {E : Type*} [NormedAddCommGroup E]
    (ρ : Measure X) (h : X → E) : (eLpNorm h 2 ρ) ^ 2 = ∫⁻ x, ‖h x‖ₑ ^ (2 : ℝ) ∂ρ := by sorry

View graph