# Documentation

Mathlib.MeasureTheory.Function.L2Space

# L^2 space #

If E is an inner product space over 𝕜 (ℝ or ℂ), then Lp E 2 μ (defined in lp_space.lean) 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 λ x, ⟪f x, g x⟫ is integrable.
• L2.inner_product_space : Lp E 2 μ is an inner product space.
theorem MeasureTheory.Memℒp.integrable_sq {α : Type u_1} {m : } {μ : } {f : α} (h : ) :
theorem MeasureTheory.memℒp_two_iff_integrable_sq_norm {α : Type u_1} {F : Type u_2} {m : } {μ : } {f : αF} (hf : ) :
theorem MeasureTheory.memℒp_two_iff_integrable_sq {α : Type u_1} {m : } {μ : } {f : α} (hf : ) :
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 => inner 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 => inner (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 : ) :
theorem MeasureTheory.Integrable.inner_const {α : Type u_1} {m : } {μ : } {E : Type u_2} {𝕜 : Type u_3} [] [] {f : αE} (hf : ) (c : E) :
theorem integral_inner {α : Type u_1} {m : } {μ : } {E : Type u_2} {𝕜 : Type u_3} [] [] [] [] {f : αE} (hf : ) (c : E) :
∫ (x : α), inner c (f x)μ = inner 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 : α), inner c (f x)μ = 0) :
∫ (x : α), f xμ = 0
theorem MeasureTheory.L2.snorm_rpow_two_norm_lt_top {α : Type u_1} {F : Type u_3} [] {μ : } (f : { x // x }) :
MeasureTheory.snorm (fun x => f x ^ 2) 1 μ <
theorem MeasureTheory.L2.snorm_inner_lt_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : { x // x }) (g : { x // x }) :
MeasureTheory.snorm (fun x => inner (f x) (g x)) 1 μ <
theorem MeasureTheory.L2.inner_def {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : { x // x }) (g : { x // x }) :
inner f g = ∫ (a : α), inner (f a) (g a)μ
theorem MeasureTheory.L2.integral_inner_eq_sq_snorm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : { x // x }) :
∫ (a : α), inner (f a) (f a)μ = ↑(ENNReal.toReal (∫⁻ (a : α), f a‖₊ ^ 2μ))
theorem MeasureTheory.L2.mem_L1_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : { x // x }) (g : { x // x }) :
MeasureTheory.AEEqFun.mk (fun x => inner (f x) (g x)) (_ : MeasureTheory.AEStronglyMeasurable (fun x => inner (f x) (g x)) μ)
theorem MeasureTheory.L2.integrable_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] (f : { x // x }) (g : { x // x }) :
MeasureTheory.Integrable fun x => inner (f x) (g x)
instance MeasureTheory.L2.innerProductSpace {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [] [] {μ : } [] :
InnerProductSpace 𝕜 { x // x }
theorem MeasureTheory.L2.inner_indicatorConstLp_eq_set_integral_inner {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [] [] {μ : } [] {s : Set α} (f : { x // x }) (hs : ) (c : E) (hμs : μ s ) :
inner () f = ∫ (x : α) in s, inner 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⟫ ∂μ.

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 : { x // x }) :
inner () f = inner 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.

theorem MeasureTheory.L2.inner_indicatorConstLp_one {α : Type u_1} {𝕜 : Type u_4} [] [] {μ : } {s : Set α} (hs : ) (hμs : μ s ) (f : { x // x }) :
inner () 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 : ) :
inner (↑() f) (↑() g) = ∫ (x : α), ↑(starRingEnd ((fun a => 𝕜) 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(α, 𝕜)) :
inner (↑() f) (↑() g) = ∫ (x : α), ↑(starRingEnd ((fun x => 𝕜) 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.