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: 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.L2.snorm_rpow_two_norm_lt_top
{α : Type u_1}
{F : Type u_3}
[measurable_space α]
{μ : measure_theory.measure α}
[normed_group F]
[measurable_space F]
[borel_space F]
[topological_space.second_countable_topology 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 α}
[measurable_space E]
[inner_product_space 𝕜 E]
[borel_space E]
[topological_space.second_countable_topology E]
(f g : ↥(measure_theory.Lp E 2 μ)) :
@[protected, instance]
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 α}
[measurable_space E]
[inner_product_space 𝕜 E]
[borel_space E]
[topological_space.second_countable_topology E]
[measurable_space 𝕜]
[borel_space 𝕜] :
has_inner 𝕜 ↥(measure_theory.Lp E 2 μ)
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 μ)) :
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 μ)) :
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)) μ
@[protected, instance]
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 α}
[measurable_space E]
[inner_product_space 𝕜 E]
[borel_space E]
[topological_space.second_countable_topology E]
[measurable_space 𝕜]
[borel_space 𝕜] :
inner_product_space 𝕜 ↥(measure_theory.Lp E 2 μ)
Equations
- measure_theory.L2.inner_product_space = {to_normed_group := measure_theory.Lp.normed_group_L2 _inst_6, to_normed_space := measure_theory.Lp.normed_space_L2 measure_theory.L2.inner_product_space._proof_3, to_has_inner := measure_theory.L2.measure_theory.Lp.has_inner _inst_12, norm_sq_eq_inner := _, conj_sym := _, add_left := _, smul_left := _}