Actual coefficient multiplication on supported spatial L²

Bounded continuous coefficient fields act on the closed supported subspace of ordinary spatial L². Crucially, the operator norm can be bounded using only coefficient values on the support set. Thus the localized (H3) propagator bound is retained without any estimate outside its stated region.

@[reducible, inline]

abbrev EulerLpSupportedMultiplier.Field {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [NormedAddCommGroup V] [InnerProductSpace ℝ V] : Type (max u_1 u_2)

Field: an abbreviation for α →ᵇ (V →L[ℝ] V).

Equations

• EulerLpSupportedMultiplier.Field = BoundedContinuousFunction α (V →L[ℝ] V)

noncomputable def EulerLpSupportedMultiplier.full {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A : Field) : ↥(MeasureTheory.Lp V 2 μ) →L[ℝ] ↥(MeasureTheory.Lp V 2 μ)

The ordinary full-space L² coefficient multiplier.

Equations

• EulerLpSupportedMultiplier.full μ A = EulerLiftedPressure.coefficientOperator ⇑A ⋯ ‖A‖₊ ⋯

theorem EulerLpSupportedMultiplier.full_ae {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A : Field) (u : ↥(MeasureTheory.Lp V 2 μ)) : ↑↑((full μ A) u) =ᵐ[μ] fun (x : α) => (A x) (↑↑u x)

Its representative is actual pointwise multiplication.

theorem EulerLpSupportedMultiplier.full_mem {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (A : Field) (u : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)) : (full μ A) ↑u ∈ EulerLpSupportedSubspace.supportedSpace μ S hS

Coefficient multiplication cannot enlarge support.

noncomputable def EulerLpSupportedMultiplier.operator {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (A : Field) : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS) →L[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

The genuine coefficient operator on the supported Hilbert space.

Equations

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

theorem EulerLpSupportedMultiplier.operator_ae {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (A : Field) (u : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)) : ↑↑↑((operator μ S hS A) u) =ᵐ[μ] fun (x : α) => (A x) (↑↑↑u x)

The supported operator retains the actual pointwise representative.

theorem EulerLpSupportedMultiplier.operator_apply_norm_le {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (A : Field) (C : ℝ) (hbound : ∀ x ∈ S, ‖A x‖ ≤ C) (u : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)) : ‖(operator μ S hS A) u‖ ≤ C * ‖u‖

The actual L² bound only requires control on the set supporting the input.

theorem EulerLpSupportedMultiplier.operator_norm_le {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (A : Field) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ x ∈ S, ‖A x‖ ≤ C) : ‖operator μ S hS A‖ ≤ C

The localized coefficient bound is the genuine supported-space operator bound.

theorem EulerLpSupportedMultiplier.operator_congr_on {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (A B : Field) (hAB : ∀ x ∈ S, A x = B x) : operator μ S hS A = operator μ S hS B

Equality on the supporting set suffices for equality of the actual operators.

theorem EulerLpSupportedMultiplier.operator_add {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (A B : Field) : operator μ S hS (A + B) = operator μ S hS A + operator μ S hS B

Addition of coefficient fields is actual addition of supported multipliers.

theorem EulerLpSupportedMultiplier.operator_smul {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (r : ℝ) (A : Field) : operator μ S hS (r • A) = r • operator μ S hS A

Scalar multiplication commutes with the actual supported multiplier.

theorem EulerLpSupportedMultiplier.operator_mul {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) (A B : Field) : operator μ S hS (A * B) = operator μ S hS A ∘SL operator μ S hS B

Pointwise composition of fields is actual operator composition.

theorem EulerLpSupportedMultiplier.operator_one {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : operator μ S hS 1 = ContinuousLinearMap.id ℝ ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

The identity field gives the identity on the supported space.

noncomputable def EulerLpSupportedMultiplier.operatorMap {α : Type u_1} {V : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set α) (hS : MeasurableSet S) : Field →L[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace μ S hS) →L[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

Coefficient-to-operator lifting is a genuine bounded linear map.

Equations

• EulerLpSupportedMultiplier.operatorMap μ S hS = { toFun := EulerLpSupportedMultiplier.operator μ S hS, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }