mathlib3 documentation

measure_theory.function.l2_space

L^2 space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.mem_ℒp.integrable_sq {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {f : α } (h : measure_theory.mem_ℒp f 2 μ) :
measure_theory.integrable (λ (x : α), f x ^ 2) μ
theorem measure_theory.mem_ℒp.const_inner {α : Type u_1} {m : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {E : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (c : E) {f : α E} (hf : measure_theory.mem_ℒp f p μ) :
measure_theory.mem_ℒp (λ (a : α), has_inner.inner c (f a)) p μ
theorem measure_theory.mem_ℒp.inner_const {α : Type u_1} {m : measurable_space α} {p : ennreal} {μ : measure_theory.measure α} {E : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {f : α E} (hf : measure_theory.mem_ℒp f p μ) (c : E) :
measure_theory.mem_ℒp (λ (a : α), has_inner.inner (f a) c) p μ
theorem measure_theory.integrable.const_inner {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {f : α E} (c : E) (hf : measure_theory.integrable f μ) :
measure_theory.integrable (λ (x : α), has_inner.inner c (f x)) μ
theorem measure_theory.integrable.inner_const {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {f : α E} (hf : measure_theory.integrable f μ) (c : E) :
measure_theory.integrable (λ (x : α), has_inner.inner (f x) c) μ
theorem integral_inner {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] [normed_space E] {f : α E} (hf : measure_theory.integrable f μ) (c : E) :
(x : α), has_inner.inner c (f x) μ = has_inner.inner c ( (x : α), f x μ)
theorem integral_eq_zero_of_forall_integral_inner_eq_zero {α : Type u_1} {m : measurable_space α} {μ : measure_theory.measure α} {E : Type u_2} (𝕜 : Type u_3) [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] [normed_space E] (f : α E) (hf : measure_theory.integrable f μ) (hf_int : (c : E), (x : α), has_inner.inner c (f x) μ = 0) :
(x : α), f x μ = 0
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 α} [normed_add_comm_group E] [inner_product_space 𝕜 E] (f g : (measure_theory.Lp E 2 μ)) :
measure_theory.snorm (λ (x : α), has_inner.inner (f x) (g x)) 1 μ <
@[protected, instance]
noncomputable def measure_theory.L2.measure_theory.Lp.has_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [is_R_or_C 𝕜] [measurable_space α] {μ : measure_theory.measure α} [normed_add_comm_group E] [inner_product_space 𝕜 E] :
Equations
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 α} [normed_add_comm_group E] [inner_product_space 𝕜 E] (f g : (measure_theory.Lp E 2 μ)) :
has_inner.inner f g = (a : α), has_inner.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 α} [normed_add_comm_group E] [inner_product_space 𝕜 E] (f : (measure_theory.Lp E 2 μ)) :
(a : α), has_inner.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 𝕜] [measurable_space α] {μ : measure_theory.measure α} [normed_add_comm_group E] [inner_product_space 𝕜 E] (f g : (measure_theory.Lp E 2 μ)) :
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 α} [normed_add_comm_group E] [inner_product_space 𝕜 E] (f g : (measure_theory.Lp E 2 μ)) :
measure_theory.integrable (λ (x : α), has_inner.inner (f x) (g x)) μ
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 𝕜] [measurable_space α] {μ : measure_theory.measure α} [normed_add_comm_group E] [inner_product_space 𝕜 E] {s : set α} (f : (measure_theory.Lp E 2 μ)) (hs : measurable_set s) (c : E) (hμs : μ s ) :

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⟫ ∂μ.

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 𝕜] [measurable_space α] {μ : measure_theory.measure α} {s : set α} (hs : measurable_set s) (hμs : μ s ) (f : (measure_theory.Lp 𝕜 2 μ)) :

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.

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.

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.