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 #
mem_L1_inner: forfandginLp E 2 μ, the pointwise inner productλ x, ⟪f x, g x⟫belongs toLp 𝕜 1 μ.integrable_inner: forfandginLp 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.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_two_iff_integrable_sq_norm
{α : Type u_1}
{F : Type u_2}
{m : measurable_space α}
{μ : measure_theory.measure α}
[normed_add_comm_group F]
{f : α → F}
(hf : measure_theory.ae_strongly_measurable f μ) :
measure_theory.mem_ℒp f 2 μ ↔ measure_theory.integrable (λ (x : α), ‖f x‖ ^ 2) μ
theorem
measure_theory.mem_ℒp_two_iff_integrable_sq
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{f : α → ℝ}
(hf : measure_theory.ae_strongly_measurable f μ) :
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) :
theorem
measure_theory.L2.snorm_rpow_two_norm_lt_top
{α : Type u_1}
{F : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_add_comm_group F]
(f : ↥(measure_theory.Lp F 2 μ)) :
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] :
has_inner 𝕜 ↥(measure_theory.Lp E 2 μ)
Equations
- measure_theory.L2.measure_theory.Lp.has_inner = {inner := λ (f g : ↥(measure_theory.Lp E 2 μ)), ∫ (a : α), has_inner.inner (⇑f a) (⇑g a) ∂μ}
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 μ)) :
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 μ)) :
measure_theory.ae_eq_fun.mk (λ (x : α), has_inner.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 α}
[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)) μ
@[protected, instance]
noncomputable
def
measure_theory.L2.inner_product_space
{α : 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] :
inner_product_space 𝕜 ↥(measure_theory.Lp E 2 μ)
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 𝕜]
[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 ≠ ⊤) :
has_inner.inner (measure_theory.indicator_const_Lp 2 hs hμs c) f = ∫ (x : α) in s, has_inner.inner 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 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 𝕜]
[measurable_space α]
{μ : measure_theory.measure α}
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{s : set α}
[complete_space E]
[normed_space ℝ E]
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(c : E)
(f : ↥(measure_theory.Lp E 2 μ)) :
has_inner.inner (measure_theory.indicator_const_Lp 2 hs hμs c) f = has_inner.inner c (∫ (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 𝕜]
[measurable_space α]
{μ : measure_theory.measure α}
{s : set α}
(hs : measurable_set s)
(hμs : ⇑μ s ≠ ⊤)
(f : ↥(measure_theory.Lp 𝕜 2 μ)) :
has_inner.inner (measure_theory.indicator_const_Lp 2 hs 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}
[topological_space α]
[measure_theory.measure_space α]
[borel_space α]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ]
(f g : bounded_continuous_function α 𝕜) :
has_inner.inner (⇑(bounded_continuous_function.to_Lp 2 μ 𝕜) f) (⇑(bounded_continuous_function.to_Lp 2 μ 𝕜) g) = ∫ (x : α), ⇑(star_ring_end 𝕜) (⇑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}
[topological_space α]
[measure_theory.measure_space α]
[borel_space α]
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ]
[compact_space α]
(f g : C(α, 𝕜)) :
has_inner.inner (⇑(continuous_map.to_Lp 2 μ 𝕜) f) (⇑(continuous_map.to_Lp 2 μ 𝕜) g) = ∫ (x : α), ⇑(star_ring_end 𝕜) (⇑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.