mathlib documentation

measure_theory.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 #

theorem measure_theory.L2.snorm_inner_lt_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [inner_product_space 𝕜 E] [borel_space E] [topological_space.second_countable_topology E] (f g : (measure_theory.Lp E 2 μ)) :
measure_theory.snorm (λ (x : α), inner (f x) (g x)) 1 μ <
theorem measure_theory.L2.inner_def {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [inner_product_space 𝕜 E] [borel_space E] [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜] (f g : (measure_theory.Lp E 2 μ)) :
inner f 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 𝕜] [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [inner_product_space 𝕜 E] [borel_space E] [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜] (f : (measure_theory.Lp E 2 μ)) :
(a : α), inner (f a) (f a) μ = ((∫⁻ (a : α), (nnnorm (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 𝕜] [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [inner_product_space 𝕜 E] [borel_space E] [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜] (f g : (measure_theory.Lp E 2 μ)) :
measure_theory.ae_eq_fun.mk (λ (x : α), inner (f x) (g x)) _ measure_theory.Lp 𝕜 1 μ
theorem measure_theory.L2.integrable_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] [measurable_space α] {μ : measure_theory.measure α} [measurable_space E] [inner_product_space 𝕜 E] [borel_space E] [topological_space.second_countable_topology E] [measurable_space 𝕜] [borel_space 𝕜] (f g : (measure_theory.Lp E 2 μ)) :
measure_theory.integrable (λ (x : α), inner (f x) (g x)) μ