L^2 space

If E is an inner product space over 𝕜 (ℝ or ℂ), then Lp E 2 μ (defined in Mathlib/MeasureTheory/Function/LpSpace.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 : for f and g in Lp E 2 μ, the pointwise inner product fun x ↦ ⟪f x, g x⟫ belongs to Lp 𝕜 1 μ.
• integrable_inner : for f and g in Lp E 2 μ, the pointwise inner product fun x ↦ ⟪f x, g x⟫ is integrable.
• L2.innerProductSpace : Lp E 2 μ is an inner product space.

theorem MeasureTheory.MemLp.integrable_sq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (h : MemLp f 2 μ) : Integrable (fun (x : α) => f x ^ 2) μ

@[deprecated MeasureTheory.MemLp.integrable_sq (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.integrable_sq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (h : MemLp f 2 μ) : Integrable (fun (x : α) => f x ^ 2) μ

Alias of MeasureTheory.MemLp.integrable_sq.

theorem MeasureTheory.memLp_two_iff_integrable_sq_norm {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup F] {f : α → F} (hf : AEStronglyMeasurable f μ) : MemLp f 2 μ ↔ Integrable (fun (x : α) => ‖f x‖ ^ 2) μ

@[deprecated MeasureTheory.memLp_two_iff_integrable_sq_norm (since := "2025-02-21")]

theorem MeasureTheory.memℒp_two_iff_integrable_sq_norm {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup F] {f : α → F} (hf : AEStronglyMeasurable f μ) : MemLp f 2 μ ↔ Integrable (fun (x : α) => ‖f x‖ ^ 2) μ

Alias of MeasureTheory.memLp_two_iff_integrable_sq_norm.

theorem MeasureTheory.memLp_two_iff_integrable_sq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : AEStronglyMeasurable f μ) : MemLp f 2 μ ↔ Integrable (fun (x : α) => f x ^ 2) μ

@[deprecated MeasureTheory.memLp_two_iff_integrable_sq (since := "2025-02-21")]

theorem MeasureTheory.memℒp_two_iff_integrable_sq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ} (hf : AEStronglyMeasurable f μ) : MemLp f 2 μ ↔ Integrable (fun (x : α) => f x ^ 2) μ

Alias of MeasureTheory.memLp_two_iff_integrable_sq.

theorem MeasureTheory.MemLp.const_inner {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (c : E) {f : α → E} (hf : MemLp f p μ) : MemLp (fun (a : α) => inner 𝕜 c (f a)) p μ

@[deprecated MeasureTheory.MemLp.const_inner (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.const_inner {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (c : E) {f : α → E} (hf : MemLp f p μ) : MemLp (fun (a : α) => inner 𝕜 c (f a)) p μ

Alias of MeasureTheory.MemLp.const_inner.

theorem MeasureTheory.MemLp.inner_const {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : α → E} (hf : MemLp f p μ) (c : E) : MemLp (fun (a : α) => inner 𝕜 (f a) c) p μ

@[deprecated MeasureTheory.MemLp.inner_const (since := "2025-02-21")]

theorem MeasureTheory.Memℒp.inner_const {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : α → E} (hf : MemLp f p μ) (c : E) : MemLp (fun (a : α) => inner 𝕜 (f a) c) p μ

Alias of MeasureTheory.MemLp.inner_const.

theorem MeasureTheory.Integrable.const_inner {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : α → E} (c : E) (hf : Integrable f μ) : Integrable (fun (x : α) => inner 𝕜 c (f x)) μ

theorem MeasureTheory.Integrable.inner_const {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : α → E} (hf : Integrable f μ) (c : E) : 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) : ∫ (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) [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 α] {μ : Measure α} [NormedAddCommGroup F] (f : ↥(Lp F 2 μ)) : eLpNorm (fun (x : α) => ‖↑↑f x‖ ^ 2) 1 μ < ⊤

theorem MeasureTheory.L2.eLpNorm_inner_lt_top {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f g : ↥(Lp E 2 μ)) : eLpNorm (fun (x : α) => inner 𝕜 (↑↑f x) (↑↑g x)) 1 μ < ⊤

instance MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Inner 𝕜 ↥(Lp E 2 μ)

Equations

• MeasureTheory.L2.instInnerSubtypeAEEqFunMemAddSubgroupLpOfNatENNReal = { inner := fun (f g : ↥(MeasureTheory.Lp E 2 μ)) => ∫ (a : α), inner 𝕜 (↑↑f a) (↑↑g a) ∂μ }

theorem MeasureTheory.L2.inner_def {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f g : ↥(Lp E 2 μ)) : inner 𝕜 f g = ∫ (a : α), inner 𝕜 (↑↑f a) (↑↑g a) ∂μ

theorem MeasureTheory.L2.integral_inner_eq_sq_eLpNorm {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : ↥(Lp E 2 μ)) : ∫ (a : α), inner 𝕜 (↑↑f a) (↑↑f a) ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal

@[deprecated _private.Mathlib.MeasureTheory.Function.L2Space.0.MeasureTheory.L2.norm_sq_eq_re_inner (since := "2025-04-22")]

theorem MeasureTheory.L2.norm_sq_eq_inner' {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f : ↥(Lp E 2 μ)) : ‖f‖ ^ 2 = RCLike.re (inner 𝕜 f f)

Alias of _private.Mathlib.MeasureTheory.Function.L2Space.0.MeasureTheory.L2.norm_sq_eq_re_inner.

theorem MeasureTheory.L2.mem_L1_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f g : ↥(Lp E 2 μ)) : AEEqFun.mk (fun (x : α) => inner 𝕜 (↑↑f x) (↑↑g x)) ⋯ ∈ Lp 𝕜 1 μ

theorem MeasureTheory.L2.integrable_inner {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f g : ↥(Lp E 2 μ)) : Integrable (fun (x : α) => inner 𝕜 (↑↑f x) (↑↑g x)) μ

instance MeasureTheory.L2.innerProductSpace {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpace 𝕜 ↥(Lp E 2 μ)

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set α} (f : ↥(Lp E 2 μ)) (hs : MeasurableSet s) (c : E) (hμs : μ s ≠ ⊤) : inner 𝕜 (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_setIntegral {α : Type u_1} {E : Type u_2} (𝕜 : Type u_4) [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set α} [CompleteSpace E] [NormedSpace ℝ E] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E) (f : ↥(Lp E 2 μ)) : inner 𝕜 (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} [RCLike 𝕜] [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (f : ↥(Lp 𝕜 2 μ)) : inner 𝕜 (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 𝕜] (μ : Measure α) [IsFiniteMeasure μ] (f g : BoundedContinuousFunction α 𝕜) : inner 𝕜 ((BoundedContinuousFunction.toLp 2 μ 𝕜) f) ((BoundedContinuousFunction.toLp 2 μ 𝕜) g) = ∫ (x : α), g x * (starRingEnd 𝕜) (f 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 𝕜] (μ : Measure α) [IsFiniteMeasure μ] [CompactSpace α] (f g : C(α, 𝕜)) : inner 𝕜 ((ContinuousMap.toLp 2 μ 𝕜) f) ((ContinuousMap.toLp 2 μ 𝕜) g) = ∫ (x : α), g x * (starRingEnd 𝕜) (f 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.