# mathlibdocumentation

measure_theory.function.l2_space

# 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 λ 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 measure_theory.L2.snorm_rpow_two_norm_lt_top {α : Type u_1} {F : Type u_3} {μ : measure_theory.measure α} [normed_group F] [borel_space F] (f : μ)) :
measure_theory.snorm (λ (x : α), f x ^ 2) 1 μ <
theorem measure_theory.L2.snorm_inner_lt_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] (f g : μ)) :
measure_theory.snorm (λ (x : α), inner (f x) (g x)) 1 μ <
@[instance]
def measure_theory.L2.measure_theory.Lp.has_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] [borel_space 𝕜] :
μ)
Equations
theorem measure_theory.L2.inner_def {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] [borel_space 𝕜] (f g : μ)) :
g = (a : α), inner (f a) (g a) μ
theorem measure_theory.L2.integral_inner_eq_sq_snorm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] [borel_space 𝕜] (f : μ)) :
(a : α), inner (f a) (f a) μ = ((∫⁻ (a : α), f a∥₊ ^ 2 μ).to_real)
theorem measure_theory.L2.mem_L1_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] [borel_space 𝕜] (f g : μ)) :
measure_theory.ae_eq_fun.mk (λ (x : α), inner (f x) (g x)) _ μ
theorem measure_theory.L2.integrable_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] [borel_space 𝕜] (f g : μ)) :
measure_theory.integrable (λ (x : α), inner (f x) (g x)) μ
@[instance]
def measure_theory.L2.inner_product_space {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] [borel_space 𝕜] :
μ)
Equations
theorem measure_theory.L2.inner_indicator_const_Lp_eq_set_integral_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] [borel_space 𝕜] {s : set α} (f : μ)) (hs : measurable_set s) (c : E) (hμs : μ s ) :
inner hμs c) f = (x : α) in s, (f x) μ

The inner product in L2 of the indicator of a set indicator_const_Lp 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 measure_theory.L2.inner_indicator_const_Lp_eq_inner_set_integral {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [is_R_or_C 𝕜] {μ : measure_theory.measure α} [ E] [borel_space E] [borel_space 𝕜] {s : set α} [ E] [ E] (hs : measurable_set s) (hμs : μ s ) (c : E) (f : μ)) :
inner hμs c) f = ( (x : α) in s, f x μ)

The inner product in L2 of the indicator of a set indicator_const_Lp 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 measure_theory.L2.inner_indicator_const_Lp_one {α : Type u_1} {𝕜 : Type u_4} [is_R_or_C 𝕜] {μ : measure_theory.measure α} [borel_space 𝕜] {s : set α} (hs : measurable_set s) (hμs : μ s ) (f : μ)) :
inner hμs 1) f = (x : α) in s, f x μ

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

theorem measure_theory.bounded_continuous_function.inner_to_Lp {α : Type u_1} [borel_space α] {𝕜 : Type u_2} [is_R_or_C 𝕜] [borel_space 𝕜] (μ : measure_theory.measure α) (f g : α →ᵇ 𝕜) :
inner ( f) ( g) = (x : α), (is_R_or_C.conj (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 measure_theory.continuous_map.inner_to_Lp {α : Type u_1} [borel_space α] {𝕜 : Type u_2} [is_R_or_C 𝕜] [borel_space 𝕜] (μ : measure_theory.measure α) (f g : C(α, 𝕜)) :
inner ( 𝕜) f) ( 𝕜) g) = (x : α), (is_R_or_C.conj (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.