# L^2 space #

If E is an inner product space over 𝕜 (ℝ or ℂ), then Lp E 2 μ (defined in Mathlib.MeasureTheory.Function.LpSpace) is also an inner product space, with inner product defined as inner f g = ∫ a, ⟪f a, g a⟫ ∂μ.

### Main results #

• mem_L1_inner : for f and g in Lp E 2 μ, the pointwise inner product fun x ↦ ⟪f x, g x⟫ belongs to Lp 𝕜 1 μ.
• integrable_inner : for f and g in Lp E 2 μ, the pointwise inner product fun x ↦ ⟪f x, g x⟫ is integrable.
• L2.innerProductSpace : Lp E 2 μ is an inner product space.
theorem MeasureTheory.Memℒp.integrable_sq {α : Type u_1} {m : } {μ : } {f : α} (h : ) :
MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ
theorem MeasureTheory.memℒp_two_iff_integrable_sq_norm {α : Type u_1} {F : Type u_2} {m : } {μ : } {f : αF} (hf : ) :
MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ
theorem MeasureTheory.memℒp_two_iff_integrable_sq {α : Type u_1} {m : } {μ : } {f : α} (hf : ) :
MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ
theorem MeasureTheory.Memℒp.const_inner {α : Type u_1} {m : } {p : ENNReal} {μ : } {E : Type u_2} {𝕜 : Type u_3} [] [] (c : E) {f : αE} (hf : ) :
MeasureTheory.Memℒp (fun (a : α) => c, f a⟫_𝕜) p μ
theorem MeasureTheory.Memℒp.inner_const {α : Type u_1} {m : } {p : ENNReal} {μ : } {E : Type u_2} {𝕜 : Type u_3} [] [] {f : αE} (hf : ) (c : E) :
MeasureTheory.Memℒp (fun (a : α) => f a, c⟫_𝕜) p μ
theorem MeasureTheory.Integrable.const_inner {α : Type u_1} {m : } {μ : } {E : Type u_2} {𝕜 : Type u_3} [] [] {f : αE} (c : E) (hf : ) :
MeasureTheory.Integrable (fun (x : α) => c, f x⟫_𝕜) μ
theorem MeasureTheory.Integrable.inner_const {α : Type u_1} {m : } {μ : } {E : Type u_2} {𝕜 : Type u_3} [] [] {f : αE} (hf : ) (c : E) :
MeasureTheory.Integrable (fun (x : α) => f x, c⟫_𝕜) μ
theorem integral_inner {α : Type u_1} {m : } {μ : } {E : Type u_2} {𝕜 : Type u_3} [] [] [] [] {f : αE} (hf : ) (c : E) :
∫ (x : α), c, f x⟫_𝕜μ = c, ∫ (x : α), f xμ⟫_𝕜
theorem integral_eq_zero_of_forall_integral_inner_eq_zero {α : Type u_1} {m : } {μ : } {E : Type u_2} (𝕜 : Type u_3) [] [] [] [] (f : αE) (hf : ) (hf_int : ∀ (c : E), ∫ (x : α), c, f x⟫_𝕜μ = 0) :
∫ (x : α), f xμ = 0
theorem MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top {α : Type u_1} {F : Type u_3} [] {μ : } (f : ()) :
MeasureTheory.eLpNorm (fun (x : α) => f x ^ 2) 1 μ <
@[deprecated MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top]
theorem MeasureTheory.L2.snorm_rpow_two_norm_lt_top {α : Type u_1} {F : Type u_3} [] {μ : } (f : ()) :
MeasureTheory.eLpNorm (fun (x : α) => f x ^ 2) 1 μ <

Alias of MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top.

theorem MeasureTheory.L2.eLpNorm_inner_lt_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : ()) (g : ()) :
MeasureTheory.eLpNorm (fun (x : α) => f x, g x⟫_𝕜) 1 μ <
@[deprecated MeasureTheory.L2.eLpNorm_inner_lt_top]
theorem MeasureTheory.L2.snorm_inner_lt_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : ()) (g : ()) :
MeasureTheory.eLpNorm (fun (x : α) => f x, g x⟫_𝕜) 1 μ <

Alias of MeasureTheory.L2.eLpNorm_inner_lt_top.

instance MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] :
Inner 𝕜 ()
Equations
• MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal = { inner := fun (f g : ()) => ∫ (a : α), f a, g a⟫_𝕜μ }
theorem MeasureTheory.L2.inner_def {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : ()) (g : ()) :
f, g⟫_𝕜 = ∫ (a : α), f a, g a⟫_𝕜μ
theorem MeasureTheory.L2.integral_inner_eq_sq_eLpNorm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : ()) :
∫ (a : α), f a, f a⟫_𝕜μ = (∫⁻ (a : α), f a‖₊ ^ 2μ).toReal
@[deprecated MeasureTheory.L2.integral_inner_eq_sq_eLpNorm]
theorem MeasureTheory.L2.integral_inner_eq_sq_snorm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : ()) :
∫ (a : α), f a, f a⟫_𝕜μ = (∫⁻ (a : α), f a‖₊ ^ 2μ).toReal

Alias of MeasureTheory.L2.integral_inner_eq_sq_eLpNorm.

theorem MeasureTheory.L2.mem_L1_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : ()) (g : ()) :
MeasureTheory.AEEqFun.mk (fun (x : α) => f x, g x⟫_𝕜)
theorem MeasureTheory.L2.integrable_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : ()) (g : ()) :
MeasureTheory.Integrable (fun (x : α) => f x, g x⟫_𝕜) μ
instance MeasureTheory.L2.innerProductSpace {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] :
Equations
• MeasureTheory.L2.innerProductSpace =
theorem MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [] [] {μ : } [] {s : Set α} (f : ()) (hs : ) (c : E) (hμs : μ s ) :
, f⟫_𝕜 = ∫ (x : α) in s, c, f x⟫_𝕜μ

The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs c and f is equal to the integral of the inner product over s: ∫ x in s, ⟪c, f x⟫ ∂μ.

@[deprecated MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner]
theorem MeasureTheory.L2.inner_indicatorConstLp_eq_set_integral_inner {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [] [] {μ : } [] {s : Set α} (f : ()) (hs : ) (c : E) (hμs : μ s ) :
, f⟫_𝕜 = ∫ (x : α) in s, c, f x⟫_𝕜μ

Alias of MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner.

The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs c and f is equal to the integral of the inner product over s: ∫ x in s, ⟪c, f x⟫ ∂μ.

theorem MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [] [] {μ : } [] {s : Set α} [] [] (hs : ) (hμs : μ s ) (c : E) (f : ()) :
, f⟫_𝕜 = c, ∫ (x : α) in s, f xμ⟫_𝕜

The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs c and f is equal to the inner product of the constant c and the integral of f over s.

@[deprecated MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral]
theorem MeasureTheory.L2.inner_indicatorConstLp_eq_inner_set_integral {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [] [] {μ : } [] {s : Set α} [] [] (hs : ) (hμs : μ s ) (c : E) (f : ()) :
, f⟫_𝕜 = c, ∫ (x : α) in s, f xμ⟫_𝕜

Alias of MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral.

The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs c and f is equal to the inner product of the constant c and the integral of f over s.

theorem MeasureTheory.L2.inner_indicatorConstLp_one {α : Type u_1} {𝕜 : Type u_4} [] [] {μ : } {s : Set α} (hs : ) (hμs : μ s ) (f : ()) :
, f⟫_𝕜 = ∫ (x : α) in s, f xμ

The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs (1 : 𝕜) and a real or complex function f is equal to the integral of f over s.

theorem MeasureTheory.BoundedContinuousFunction.inner_toLp {α : Type u_1} {𝕜 : Type u_2} [] [] [] [] (μ : ) (f : ) (g : ) :
() f, () g⟫_𝕜 = ∫ (x : α), () (f x) * g xμ

For bounded continuous functions f, g on a finite-measure topological space α, the L^2 inner product is the integral of their pointwise inner product.

theorem MeasureTheory.ContinuousMap.inner_toLp {α : Type u_1} {𝕜 : Type u_2} [] [] [] [] (μ : ) [] (f : C(α, 𝕜)) (g : C(α, 𝕜)) :
() f, () g⟫_𝕜 = ∫ (x : α), () (f x) * g xμ

For continuous functions f, g on a compact, finite-measure topological space α, the L^2 inner product is the integral of their pointwise inner product.