Documentation

Mathlib.MeasureTheory.Function.L2Space

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 #

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.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 : α) => 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 : α) => 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 : α) => 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 : α) => 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) :
∫ (x : α), c, f x⟫_𝕜μ = c, ∫ (x : α), f xμ⟫_𝕜
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 : α), c, f x⟫_𝕜μ = 0) :
∫ (x : α), f xμ = 0
theorem MeasureTheory.L2.snorm_rpow_two_norm_lt_top {α : Type u_1} {F : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : (MeasureTheory.Lp F 2 μ)) :
MeasureTheory.snorm (fun (x : α) => f x ^ 2) 1 μ <
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 : (MeasureTheory.Lp E 2 μ)) (g : (MeasureTheory.Lp E 2 μ)) :
MeasureTheory.snorm (fun (x : α) => f x, g x⟫_𝕜) 1 μ <
theorem MeasureTheory.L2.inner_def {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : (MeasureTheory.Lp E 2 μ)) (g : (MeasureTheory.Lp E 2 μ)) :
f, g⟫_𝕜 = ∫ (a : α), f a, g a⟫_𝕜μ
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 : (MeasureTheory.Lp E 2 μ)) :
∫ (a : α), f a, f a⟫_𝕜μ = (∫⁻ (a : α), f a‖₊ ^ 2μ).toReal
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 : (MeasureTheory.Lp E 2 μ)) (g : (MeasureTheory.Lp E 2 μ)) :
MeasureTheory.AEEqFun.mk (fun (x : α) => 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 : (MeasureTheory.Lp E 2 μ)) (g : (MeasureTheory.Lp E 2 μ)) :
MeasureTheory.Integrable (fun (x : α) => 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] :
Equations
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 : (MeasureTheory.Lp E 2 μ)) (hs : MeasurableSet s) (c : E) (hμs : μ s ) :
MeasureTheory.indicatorConstLp 2 hs hμs c, f⟫_𝕜 = ∫ (x : α) in s, 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⟫ ∂μ.

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 : (MeasureTheory.Lp E 2 μ)) :
MeasureTheory.indicatorConstLp 2 hs hμs c, f⟫_𝕜 = 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.

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 : (MeasureTheory.Lp 𝕜 2 μ)) :
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 α 𝕜) :
(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(α, 𝕜)) :
(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.