Algebra and coercivity of actual full-space L² multipliers

The bounded-field multiplier preserves composition and adjoints. Pointwise frame lower bounds and Hessian upper bounds hold on the full Bochner L² space. Measurable spatial cutoffs are self-adjoint and commute with these rectangular multipliers. Thus support preservation of a variational inverse can be proved by its actual uniqueness theorem.

theorem EulerLpOperatorField.full_comp {α : Type u_1} {U : Type u_2} {E : Type u_3} {F : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) (B : BoundedContinuousFunction α (U →L[ℝ] E)) : full μ ((EulerBoundedFieldCalculus.compositionMap A) B) = full μ A ∘SL full μ B

Multiplication by the actual product field is composition on L².

theorem EulerLpOperatorField.full_neg {α : Type u_1} {E : Type u_3} {F : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) : full μ (-A) = -full μ A

theorem EulerLpOperatorField.full_eq_neg_comp {α : Type u_1} {U : Type u_2} {E : Type u_3} {F : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (C : BoundedContinuousFunction α (U →L[ℝ] F)) (A : BoundedContinuousFunction α (E →L[ℝ] F)) (B : BoundedContinuousFunction α (U →L[ℝ] E)) (hC : ∀ (x : α) (u : U), (C x) u = -(A x) ((B x) u)) : full μ C = -full μ A ∘SL full μ B

A literal coefficient identity can be lifted without introducing a new operator hypothesis.

theorem EulerLpOperatorField.full_norm_sq_lower {α : Type u_1} {E : Type u_3} {F : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) (c : ℝ) (hc : 0 ≤ c) (hA : ∀ (x : α) (v : E), c * ‖v‖ ^ 2 ≤ ‖(A x) v‖ ^ 2) (u : ↥(MeasureTheory.Lp E 2 μ)) : c * ‖u‖ ^ 2 ≤ ‖(full μ A) u‖ ^ 2

A pointwise lower frame bound is a lower bound on genuine full-space L².

theorem EulerLpOperatorField.full_quadratic_upper {α : Type u_1} {E : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : BoundedContinuousFunction α (E →L[ℝ] E)) (C : ℝ) (hA : ∀ (x : α) (v : E), inner ℝ ((A x) v) v ≤ C * ‖v‖ ^ 2) (u : ↥(MeasureTheory.Lp E 2 μ)) : inner ℝ ((full μ A) u) u ≤ C * ‖u‖ ^ 2

The actual L² Hessian inherits its pointwise quadratic upper bound.

theorem EulerLpOperatorField.full_cutoff {α : Type u_1} {E : Type u_3} {F : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set α) (hS : MeasurableSet S) (A : BoundedContinuousFunction α (E →L[ℝ] F)) (u : ↥(MeasureTheory.Lp E 2 μ)) : (full μ A) ((EulerLpSupportedSubspace.cutoffOperator μ S hS) u) = (EulerLpSupportedSubspace.cutoffOperator μ S hS) ((full μ A) u)

A rectangular coefficient commutes with literal spatial localization.

theorem EulerLpOperatorField.full_adjoint {α : Type u_1} {E : Type u_3} {F : Type u_4} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace E] [CompleteSpace F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) : ContinuousLinearMap.adjoint (full μ A) = full μ (EulerBoundedFieldCalculus.adjointMap A)

The L² adjoint is multiplication by the pointwise adjoint field.

theorem EulerLpSupportedSubspace.cutoffOperator_adjoint {α : Type u_1} {E : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set α) (hS : MeasurableSet S) : ContinuousLinearMap.adjoint (cutoffOperator μ S hS) = cutoffOperator μ S hS

The genuine measurable spatial cutoff is an orthogonal projection.