The actual supported subspace of ordinary spatial L²

Support is imposed on genuine Bochner L² functions by the closed kernel of identity minus measurable-set projection. This gives a complete Hilbert space for localized propagators and keeps the support restriction explicit.

noncomputable def EulerLpSupportedSubspace.cutoff {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : ↥(MeasureTheory.Lp V 2 μ)

The actual measurable-set cutoff on a Bochner L² function.

Equations

• EulerLpSupportedSubspace.cutoff μ S hS u = MeasureTheory.MemLp.toLp (S.indicator ↑↑u) ⋯

theorem EulerLpSupportedSubspace.cutoff_ae {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : ↑↑(cutoff μ S hS u) =ᵐ[μ] S.indicator ↑↑u

Its representative is the literal indicator product.

theorem EulerLpSupportedSubspace.cutoff_norm {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : ‖cutoff μ S hS u‖ ≤ ‖u‖

Measurable-set projection is norm-decreasing.

noncomputable def EulerLpSupportedSubspace.cutoffLinear {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ↥(MeasureTheory.Lp V 2 μ) →ₗ[ℝ] ↥(MeasureTheory.Lp V 2 μ)

The actual cutoff is linear.

Equations

• EulerLpSupportedSubspace.cutoffLinear μ S hS = { toFun := EulerLpSupportedSubspace.cutoff μ S hS, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerLpSupportedSubspace.cutoffOperator {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ↥(MeasureTheory.Lp V 2 μ) →L[ℝ] ↥(MeasureTheory.Lp V 2 μ)

The supported-set projection as a genuine bounded linear map.

Equations

• EulerLpSupportedSubspace.cutoffOperator μ S hS = (EulerLpSupportedSubspace.cutoffLinear μ S hS).mkContinuous 1 ⋯

noncomputable def EulerLpSupportedSubspace.supportedSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Submodule ℝ ↥(MeasureTheory.Lp V 2 μ)

The localized Hilbert subspace is a closed kernel.

Equations

• EulerLpSupportedSubspace.supportedSpace μ S hS = (↑(ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp V 2 μ) - EulerLpSupportedSubspace.cutoffOperator μ S hS)).ker

theorem EulerLpSupportedSubspace.mem_supportedSpace_iff {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : u ∈ supportedSpace μ S hS ↔ u = cutoff μ S hS u

Membership is fixedness under actual measurable-set projection.

theorem EulerLpSupportedSubspace.mem_supportedSpace_ae {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : u ∈ supportedSpace μ S hS ↔ ∀ᵐ (x : α) ∂μ, x ∉ S → ↑↑u x = 0

Membership is exactly almost-everywhere vanishing outside the given set.

theorem EulerLpSupportedSubspace.supportedSpace_closed {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : IsClosed ↑(supportedSpace μ S hS)

The support condition is closed in the actual L² norm.

instance EulerLpSupportedSubspace.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpOfNatENNRealSubmoduleRealSupportedSpace {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) [CompleteSpace V] : CompleteSpace ↥(supportedSpace μ S hS)

theorem EulerLpSupportedSubspace.cutoff_mem {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (u : ↥(MeasureTheory.Lp V 2 μ)) : cutoff μ S hS u ∈ supportedSpace μ S hS

Every cutoff output belongs to the supported subspace.

noncomputable def EulerLpSupportedSubspace.projection {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ↥(MeasureTheory.Lp V 2 μ) →L[ℝ] ↥(supportedSpace μ S hS)

Actual projection from full spatial L² to its supported Hilbert subspace.

Equations

• EulerLpSupportedSubspace.projection μ S hS = (EulerLpSupportedSubspace.cutoffOperator μ S hS).codRestrict (EulerLpSupportedSubspace.supportedSpace μ S hS) ⋯

theorem EulerLpSupportedSubspace.projection_norm {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : ‖projection μ S hS‖ ≤ 1

The projection has norm at most one.

theorem EulerLpSupportedSubspace.projection_supported {α : Type u_1} {V : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (u : ↥(supportedSpace μ S hS)) : (projection μ S hS) ↑u = u

Inclusion after projection fixes every already supported field.