Rectangular coefficient fields acting on actual spatial L²

Bounded continuous fields of operators E→F act on genuine Bochner L² classes, with their literal pointwise representatives. The action restricts to the closed supported spaces, where its norm needs a bound only on the support region. This supplies the physical frame and projected forcing maps.

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField1 {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (E →L[ℝ] F)

Cache the standard NormedAddCommGroup (E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField2 {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (E →L[ℝ] F)

Cache the standard NormedSpace ℝ (E →L[ℝ] F) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField3 {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (BoundedContinuousFunction α (E →L[ℝ] F))

Cache the standard NormedAddCommGroup (α →ᵇ (E →L[ℝ] F)) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField3 = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField4 {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction α (E →L[ℝ] F))

Cache the standard NormedSpace ℝ (α →ᵇ (E →L[ℝ] F)) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField4 = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField5 {α : Type u_1} {E : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] : NormedAddCommGroup ↥(MeasureTheory.Lp E 2 μ)

Cache the standard NormedAddCommGroup (Lp E 2 μ) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField5 μ = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField6 {α : Type u_1} {E : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ ↥(MeasureTheory.Lp E 2 μ)

Cache the standard NormedSpace ℝ (Lp E 2 μ) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField6 μ = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField7 {α : Type u_1} {F : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup F] : NormedAddCommGroup ↥(MeasureTheory.Lp F 2 μ)

Cache the standard NormedAddCommGroup (Lp F 2 μ) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField7 μ = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField8 {α : Type u_1} {F : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ ↥(MeasureTheory.Lp F 2 μ)

Cache the standard NormedSpace ℝ (Lp F 2 μ) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField8 μ = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField9 {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedAddCommGroup (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 μ))

Cache the standard NormedAddCommGroup (Lp E 2 μ →L[ℝ] Lp F 2 μ) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField9 μ = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorField10 {α : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : NormedSpace ℝ (↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 μ))

Cache the standard NormedSpace ℝ (Lp E 2 μ →L[ℝ] Lp F 2 μ) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorField10 μ = inferInstance

theorem EulerLpOperatorField.apply_memLp {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) (u : ↥(MeasureTheory.Lp E 2 μ)) : MeasureTheory.MemLp (fun (x : α) => (A x) (↑↑u x)) 2 μ

Literal coefficient application is genuinely square integrable.

noncomputable def EulerLpOperatorField.applyField {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) (u : ↥(MeasureTheory.Lp E 2 μ)) : ↥(MeasureTheory.Lp F 2 μ)

Actual application to a Bochner L² class.

Equations

• EulerLpOperatorField.applyField μ A u = MeasureTheory.MemLp.toLp (fun (x : α) => (A x) (↑↑u x)) ⋯

theorem EulerLpOperatorField.applyField_ae {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) (u : ↥(MeasureTheory.Lp E 2 μ)) : ↑↑(applyField μ A u) =ᵐ[μ] fun (x : α) => (A x) (↑↑u x)

noncomputable def EulerLpOperatorField.fullLinear {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) : ↥(MeasureTheory.Lp E 2 μ) →ₗ[ℝ] ↥(MeasureTheory.Lp F 2 μ)

Full linear, bundling toFun, map_add, map_smul.

Equations

• EulerLpOperatorField.fullLinear μ A = { toFun := EulerLpOperatorField.applyField μ A, map_add' := ⋯, map_smul' := ⋯ }

theorem EulerLpOperatorField.applyField_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) (u : ↥(MeasureTheory.Lp E 2 μ)) : ‖applyField μ A u‖ ≤ ‖A‖ * ‖u‖

noncomputable def EulerLpOperatorField.full {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) : ↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 μ)

The actual bounded rectangular multiplier on full spatial L².

Equations

• EulerLpOperatorField.full μ A = (EulerLpOperatorField.fullLinear μ A).mkContinuous ‖A‖ ⋯

theorem EulerLpOperatorField.full_ae {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) (u : ↥(MeasureTheory.Lp E 2 μ)) : ↑↑((full μ A) u) =ᵐ[μ] fun (x : α) => (A x) (↑↑u x)

theorem EulerLpOperatorField.full_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) : ‖full μ A‖ ≤ ‖A‖

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

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

noncomputable def EulerLpOperatorField.fullMap {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : BoundedContinuousFunction α (E →L[ℝ] F) →L[ℝ] ↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 μ)

Rectangular multiplier formation is itself a linear contraction.

Equations

• EulerLpOperatorField.fullMap μ = { toFun := EulerLpOperatorField.full μ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem EulerLpOperatorField.fullMap_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : ‖fullMap μ‖ ≤ 1

theorem EulerLpOperatorField.full_mem {α : Type u_1} {E : Type u_2} {F : Type u_3} [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 : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)) : (full μ A) ↑u ∈ EulerLpSupportedSubspace.supportedSpace μ S hS

noncomputable def EulerLpOperatorField.supported {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set α) (hS : MeasurableSet S) (A : BoundedContinuousFunction α (E →L[ℝ] F)) : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS) →L[ℝ] ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

The genuine rectangular multiplier between the supported Hilbert spaces.

Equations

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

theorem EulerLpOperatorField.supported_ae {α : Type u_1} {E : Type u_2} {F : Type u_3} [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 : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)) : ↑↑↑((supported μ S hS A) u) =ᵐ[μ] fun (x : α) => (A x) (↑↑↑u x)

theorem EulerLpOperatorField.supported_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set α) (hS : MeasurableSet S) (A : BoundedContinuousFunction α (E →L[ℝ] F)) (C : ℝ) (hC : 0 ≤ C) (hA : ∀ x ∈ S, ‖A x‖ ≤ C) : ‖supported μ S hS A‖ ≤ C

Only values on the supporting region enter the actual operator norm.

theorem EulerLpOperatorField.supported_norm_sq_lower {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set α) (hS : MeasurableSet S) (A : BoundedContinuousFunction α (E →L[ℝ] F)) (c : ℝ) (hc : 0 ≤ c) (hA : ∀ x ∈ S, ∀ (v : E), c * ‖v‖ ^ 2 ≤ ‖(A x) v‖ ^ 2) (u : ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)) : c * ‖u‖ ^ 2 ≤ ‖(supported μ S hS A) u‖ ^ 2

A pointwise lower frame bound becomes the actual spatial-L² lower frame bound.