L^2 space #
If E is an inner product space over 𝕜 (ℝ or ℂ), then Lp E 2 μ
(defined in Mathlib.MeasureTheory.Function.LpSpace)
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 productfun x ↦ ⟪f x, g x⟫belongs toLp 𝕜 1 μ.integrable_inner: forfandginLp E 2 μ, the pointwise inner productfun x ↦ ⟪f x, g x⟫is integrable.L2.innerProductSpace:Lp E 2 μis an inner product space.
theorem
MeasureTheory.Memℒp.integrable_sq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(h : MeasureTheory.Memℒp f 2 μ)
:
MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ
theorem
MeasureTheory.memℒp_two_iff_integrable_sq_norm
{α : Type u_1}
{F : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
{f : α → F}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.Memℒp f 2 μ ↔ MeasureTheory.Integrable (fun (x : α) => ‖f x‖ ^ 2) μ
theorem
MeasureTheory.memℒp_two_iff_integrable_sq
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
MeasureTheory.Memℒp f 2 μ ↔ MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ
theorem
MeasureTheory.Memℒp.const_inner
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
{𝕜 : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(c : E)
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp (fun (a : α) => inner c (f a)) p μ
theorem
MeasureTheory.Memℒp.inner_const
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
{𝕜 : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{f : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(c : E)
:
MeasureTheory.Memℒp (fun (a : α) => inner (f a) c) p μ
theorem
MeasureTheory.Integrable.const_inner
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
{𝕜 : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{f : α → E}
(c : E)
(hf : MeasureTheory.Integrable f μ)
:
MeasureTheory.Integrable (fun (x : α) => inner c (f x)) μ
theorem
MeasureTheory.Integrable.inner_const
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
{𝕜 : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{f : α → E}
(hf : MeasureTheory.Integrable f μ)
(c : E)
:
MeasureTheory.Integrable (fun (x : α) => inner (f x) c) μ
theorem
integral_inner
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
{𝕜 : Type u_3}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
[NormedSpace ℝ E]
{f : α → E}
(hf : MeasureTheory.Integrable f μ)
(c : E)
:
theorem
integral_eq_zero_of_forall_integral_inner_eq_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{E : Type u_2}
(𝕜 : Type u_3)
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
[NormedSpace ℝ E]
(f : α → E)
(hf : MeasureTheory.Integrable f μ)
(hf_int : ∀ (c : E), ∫ (x : α), inner c (f x) ∂μ = 0)
:
∫ (x : α), f x ∂μ = 0
theorem
MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top
{α : Type u_1}
{F : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : { x : α →ₘ[μ] F // x ∈ MeasureTheory.Lp F 2 μ })
:
@[deprecated MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top]
theorem
MeasureTheory.L2.snorm_rpow_two_norm_lt_top
{α : Type u_1}
{F : Type u_3}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup F]
(f : { x : α →ₘ[μ] F // x ∈ MeasureTheory.Lp F 2 μ })
:
theorem
MeasureTheory.L2.eLpNorm_inner_lt_top
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
(g : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
MeasureTheory.eLpNorm (fun (x : α) => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤
@[deprecated MeasureTheory.L2.eLpNorm_inner_lt_top]
theorem
MeasureTheory.L2.snorm_inner_lt_top
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
(g : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
MeasureTheory.eLpNorm (fun (x : α) => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤
Alias of MeasureTheory.L2.eLpNorm_inner_lt_top.
instance
MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
:
Inner 𝕜 { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ }
theorem
MeasureTheory.L2.inner_def
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
(g : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
theorem
MeasureTheory.L2.integral_inner_eq_sq_eLpNorm
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
@[deprecated MeasureTheory.L2.integral_inner_eq_sq_eLpNorm]
theorem
MeasureTheory.L2.integral_inner_eq_sq_snorm
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
theorem
MeasureTheory.L2.mem_L1_inner
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
(g : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
MeasureTheory.AEEqFun.mk (fun (x : α) => inner (↑↑f x) (↑↑g x)) ⋯ ∈ MeasureTheory.Lp 𝕜 1 μ
theorem
MeasureTheory.L2.integrable_inner
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
(g : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
MeasureTheory.Integrable (fun (x : α) => inner (↑↑f x) (↑↑g x)) μ
instance
MeasureTheory.L2.innerProductSpace
{α : Type u_1}
{E : Type u_2}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
:
InnerProductSpace 𝕜 { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ }
Equations
- MeasureTheory.L2.innerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯
theorem
MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner
{α : Type u_1}
{E : Type u_2}
(𝕜 : Type u_4)
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{s : Set α}
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
(hs : MeasurableSet s)
(c : E)
(hμs : μ s ≠ ⊤)
:
inner (MeasureTheory.indicatorConstLp 2 hs hμs c) f = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs c and f is
equal to the integral of the inner product over s: ∫ x in s, ⟪c, f x⟫ ∂μ.
@[deprecated MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner]
theorem
MeasureTheory.L2.inner_indicatorConstLp_eq_set_integral_inner
{α : Type u_1}
{E : Type u_2}
(𝕜 : Type u_4)
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{s : Set α}
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
(hs : MeasurableSet s)
(c : E)
(hμs : μ s ≠ ⊤)
:
inner (MeasureTheory.indicatorConstLp 2 hs hμs c) f = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
Alias of MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner.
The inner product in L2 of the indicator of a set indicatorConstLp 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
MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral
{α : Type u_1}
{E : Type u_2}
(𝕜 : Type u_4)
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{s : Set α}
[CompleteSpace E]
[NormedSpace ℝ E]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : E)
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
inner (MeasureTheory.indicatorConstLp 2 hs hμs c) f = inner c (∫ (x : α) in s, ↑↑f x ∂μ)
The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs c and f is
equal to the inner product of the constant c and the integral of f over s.
@[deprecated MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral]
theorem
MeasureTheory.L2.inner_indicatorConstLp_eq_inner_set_integral
{α : Type u_1}
{E : Type u_2}
(𝕜 : Type u_4)
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{s : Set α}
[CompleteSpace E]
[NormedSpace ℝ E]
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(c : E)
(f : { x : α →ₘ[μ] E // x ∈ MeasureTheory.Lp E 2 μ })
:
inner (MeasureTheory.indicatorConstLp 2 hs hμs c) f = inner c (∫ (x : α) in s, ↑↑f x ∂μ)
Alias of MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral.
The inner product in L2 of the indicator of a set indicatorConstLp 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
MeasureTheory.L2.inner_indicatorConstLp_one
{α : Type u_1}
{𝕜 : Type u_4}
[RCLike 𝕜]
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
{s : Set α}
(hs : MeasurableSet s)
(hμs : μ s ≠ ⊤)
(f : { x : α →ₘ[μ] 𝕜 // x ∈ MeasureTheory.Lp 𝕜 2 μ })
:
inner (MeasureTheory.indicatorConstLp 2 hs hμs 1) f = ∫ (x : α) in s, ↑↑f x ∂μ
The inner product in L2 of the indicator of a set indicatorConstLp 2 hs hμs (1 : 𝕜) and
a real or complex function f is equal to the integral of f over s.
theorem
MeasureTheory.BoundedContinuousFunction.inner_toLp
{α : Type u_1}
{𝕜 : Type u_2}
[TopologicalSpace α]
[MeasurableSpace α]
[BorelSpace α]
[RCLike 𝕜]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(f : BoundedContinuousFunction α 𝕜)
(g : BoundedContinuousFunction α 𝕜)
:
inner ((BoundedContinuousFunction.toLp 2 μ 𝕜) f) ((BoundedContinuousFunction.toLp 2 μ 𝕜) g) = ∫ (x : α), (starRingEnd 𝕜) (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
MeasureTheory.ContinuousMap.inner_toLp
{α : Type u_1}
{𝕜 : Type u_2}
[TopologicalSpace α]
[MeasurableSpace α]
[BorelSpace α]
[RCLike 𝕜]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
[CompactSpace α]
(f : C(α, 𝕜))
(g : C(α, 𝕜))
:
inner ((ContinuousMap.toLp 2 μ 𝕜) f) ((ContinuousMap.toLp 2 μ 𝕜) g) = ∫ (x : α), (starRingEnd 𝕜) (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.