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
: forf
andg
inLp E 2 μ
, the pointwise inner productλ x, ⟪f x, g x⟫
belongs toLp 𝕜 1 μ
.integrable_inner
: forf
andg
inLp 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.
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) ∂μ}
Equations
- measure_theory.L2.inner_product_space = {to_normed_add_comm_group := {to_has_norm := measure_theory.Lp.has_norm (inner_product_space.to_normed_add_comm_group 𝕜), to_add_comm_group := (measure_theory.Lp E 2 μ).to_add_comm_group, to_metric_space := normed_add_comm_group.to_metric_space measure_theory.Lp.normed_add_comm_group, dist_eq := _}, to_normed_space := measure_theory.Lp.normed_space fact_one_le_two_ennreal, to_has_inner := measure_theory.L2.measure_theory.Lp.has_inner _inst_3, norm_sq_eq_inner := _, conj_sym := _, add_left := _, smul_left := _}
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
.
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.