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.const_inner {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_2} {𝕜 : Type u_3} [IsROrC 𝕜] [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} [IsROrC 𝕜] [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} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : αE} (c : E) (hf : MeasureTheory.Integrable f) :
theorem MeasureTheory.Integrable.inner_const {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} {𝕜 : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : αE} (hf : MeasureTheory.Integrable f) (c : E) :
theorem integral_inner {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} {𝕜 : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedSpace E] {f : αE} (hf : MeasureTheory.Integrable f) (c : E) :
∫ (x : α), inner c (f x)μ = inner 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) [IsROrC 𝕜] [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.snorm_rpow_two_norm_lt_top {α : Type u_1} {F : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup F] (f : { x // x 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} [IsROrC 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : { x // x MeasureTheory.Lp E 2 }) (g : { x // x MeasureTheory.Lp E 2 }) :
MeasureTheory.snorm (fun x => inner (f x) (g x)) 1 μ <
theorem MeasureTheory.L2.inner_def {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [IsROrC 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : { x // x MeasureTheory.Lp E 2 }) (g : { x // x MeasureTheory.Lp E 2 }) :
inner f g = ∫ (a : α), inner (f a) (g a)μ
theorem MeasureTheory.L2.integral_inner_eq_sq_snorm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [IsROrC 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : { x // x MeasureTheory.Lp E 2 }) :
∫ (a : α), inner (f a) (f a)μ = ↑(ENNReal.toReal (∫⁻ (a : α), f a‖₊ ^ 2μ))
theorem MeasureTheory.L2.mem_L1_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [IsROrC 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : { x // x MeasureTheory.Lp E 2 }) (g : { x // x MeasureTheory.Lp E 2 }) :
MeasureTheory.AEEqFun.mk (fun x => inner (f x) (g x)) (_ : MeasureTheory.AEStronglyMeasurable (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} [IsROrC 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : { x // x MeasureTheory.Lp E 2 }) (g : { x // 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} [IsROrC 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
theorem MeasureTheory.L2.inner_indicatorConstLp_eq_set_integral_inner {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [IsROrC 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set α} (f : { x // 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⟫ ∂μ.

theorem MeasureTheory.L2.inner_indicatorConstLp_eq_inner_set_integral {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [IsROrC 𝕜] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set α} [CompleteSpace E] [NormedSpace E] (hs : MeasurableSet s) (hμs : μ s ) (c : E) (f : { x // 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.

theorem MeasureTheory.L2.inner_indicatorConstLp_one {α : Type u_1} {𝕜 : Type u_4} [IsROrC 𝕜] [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} [TopologicalSpace α] [MeasureTheory.MeasureSpace α] [BorelSpace α] {𝕜 : Type u_2} [IsROrC 𝕜] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction α 𝕜) (g : BoundedContinuousFunction α 𝕜) :
inner (↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) (↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) = ∫ (x : α), ↑(starRingEnd ((fun a => 𝕜) x)) (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} [TopologicalSpace α] [MeasureTheory.MeasureSpace α] [BorelSpace α] {𝕜 : Type u_2} [IsROrC 𝕜] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [CompactSpace α] (f : C(α, 𝕜)) (g : C(α, 𝕜)) :
inner (↑(ContinuousMap.toLp 2 μ 𝕜) f) (↑(ContinuousMap.toLp 2 μ 𝕜) g) = ∫ (x : α), ↑(starRingEnd ((fun x => 𝕜) x)) (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.