Rectangular coefficient fields on the actual cylinder

Spatial fields of operators E→F act on R³×AddCircle L², and on its closed spatial-support subspaces. All coefficient and continuous-path lifting maps are contractions. The exact mixed-translation identity is proved on L² classes, so projected forcing and physical-frame application can use the same external-word calculus as the forward solution.

Actual rectangular L² frame paths and their time derivatives

The coefficient-to-operator map is a contraction on supported Hilbert spaces. Continuous coefficient paths and their literal pointwise time derivatives therefore give genuine operator paths and derivatives. Frame lower bounds, quadratic upper bounds and pointwise composition identities pass to these actual L² operators without a support-margin constant.

@[instance_reducible]

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

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

Equations

• EulerLpOperatorField.instLpOperatorFieldPath1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerLpOperatorField.instLpOperatorFieldPath2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerLpOperatorField.instLpOperatorFieldPath3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerLpOperatorField.instLpOperatorFieldPath4 = inferInstance

@[instance_reducible]

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

Cache the standard NormedAddCommGroup (supportedSpace (V := E) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorFieldPath5 μ S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorFieldPath6 {α : Type u_1} {E : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

Cache the standard NormedSpace ℝ (supportedSpace (V := E) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorFieldPath6 μ S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorFieldPath7 {α : Type u_1} {F : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

Cache the standard NormedAddCommGroup (supportedSpace (V := F) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorFieldPath7 μ S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpOperatorField.instLpOperatorFieldPath8 {α : Type u_1} {F : Type u_3} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ ↥(EulerLpSupportedSubspace.supportedSpace μ S hS)

Cache the standard NormedSpace ℝ (supportedSpace (V := F) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorFieldPath8 μ S hS = inferInstance

@[instance_reducible]

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

Cache the standard NormedAddCommGroup (supportedSpace (V := E) μ S hS →L[ℝ] supportedSpace (V := F) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorFieldPath9 μ S hS = inferInstance

@[instance_reducible]

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

Cache the standard NormedSpace ℝ (supportedSpace (V := E) μ S hS →L[ℝ] supportedSpace (V := F) μ S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpOperatorField.instLpOperatorFieldPath10 μ S hS = inferInstance

theorem EulerLpOperatorField.supported_add {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A B : BoundedContinuousFunction α (E →L[ℝ] F)) : supported μ S hS (A + B) = supported μ S hS A + supported μ S hS B

Linearity in the actual rectangular coefficient field.

theorem EulerLpOperatorField.supported_smul {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (r : ℝ) (A : BoundedContinuousFunction α (E →L[ℝ] F)) : supported μ S hS (r • A) = r • supported μ S hS A

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

The literal linear dependence of the supported multiplier on its coefficient.

Equations

• EulerLpOperatorField.supportedLinear μ S hS = { toFun := EulerLpOperatorField.supported μ S hS, map_add' := ⋯, map_smul' := ⋯ }

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

The real coefficient-to-L²-operator map on the supported spaces.

Equations

• EulerLpOperatorField.supportedMap μ S hS = { toLinearMap := EulerLpOperatorField.supportedLinear μ S hS, cont := ⋯ }

@[simp]

theorem EulerLpOperatorField.supportedMap_apply {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A : BoundedContinuousFunction α (E →L[ℝ] F)) : (supportedMap μ S hS) A = supported μ S hS A

theorem EulerLpOperatorField.supportedMap_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : ‖supportedMap μ S hS‖ ≤ 1

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

The actual rectangular coefficient map uniformly along a compact time set.

Equations

• EulerLpOperatorField.supportedPathMap μ S hS = ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpOperatorField.supportedMap μ S hS)

@[simp]

theorem EulerLpOperatorField.supportedPathMap_apply {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {K : Type u_4} [TopologicalSpace K] (A : C(K, BoundedContinuousFunction α (E →L[ℝ] F))) (t : K) : ((supportedPathMap μ S hS) A) t = supported μ S hS (A t)

theorem EulerLpOperatorField.supportedPathMap_norm {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {K : Type u_4} [TopologicalSpace K] [CompactSpace K] : ‖supportedPathMap μ S hS‖ ≤ 1

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

Every-time pointwise lower frame bounds hold on the real L² frame path.

theorem EulerLpOperatorField.supportedPath_hasDerivWithinAt {α : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (T : ℝ) (hT : 0 ≤ T) (A A' : C(↑(Set.Icc 0 T), BoundedContinuousFunction α (E →L[ℝ] F))) (hpoint : ∀ t ∈ Set.Icc 0 T, ∀ (x : α), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT A s) x) ((EulerVolterraConvolution.extendPath T hT A' t) x) (Set.Icc 0 T) t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((supportedPathMap μ S hS) A)) (((supportedPathMap μ S hS) A') t) (Set.Icc 0 T) ↑t

Literal pointwise coefficient time derivatives give the genuine within-time operator derivative; no global time extension is assumed.

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

A localized Hessian upper bound passes to its genuine supported L² operator.

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular1 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (E →L[ℝ] F)

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular2 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (E →L[ℝ] F)

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular3 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular3 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular4 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular4 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular5 (period : ℝ) {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (BoundedContinuousFunction (EulerLiftedGradientSpace.LiftDomain period) (E →L[ℝ] F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular5 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular6 (period : ℝ) {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (BoundedContinuousFunction (EulerLiftedGradientSpace.LiftDomain period) (E →L[ℝ] F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular6 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular7 (period : ℝ) [Fact (0 < period)] {E : Type u_1} [NormedAddCommGroup E] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 period E)

Cache the standard NormedAddCommGroup (CylinderL2 period E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular7 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular8 (period : ℝ) [Fact (0 < period)] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period E)

Cache the standard NormedSpace ℝ (CylinderL2 period E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular8 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular9 (period : ℝ) [Fact (0 < period)] {F : Type u_2} [NormedAddCommGroup F] : NormedAddCommGroup ↥(EulerLpCylinderTranslation.CylinderL2 period F)

Cache the standard NormedAddCommGroup (CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular9 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular10 (period : ℝ) [Fact (0 < period)] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ ↥(EulerLpCylinderTranslation.CylinderL2 period F)

Cache the standard NormedSpace ℝ (CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular10 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular11 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedAddCommGroup (↥(EulerLpCylinderTranslation.CylinderL2 period E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular11 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular12 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : NormedSpace ℝ (↥(EulerLpCylinderTranslation.CylinderL2 period E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular12 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular13 {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular13 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular14 {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular14 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular15 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {K : Type u_3} [NormedAddCommGroup E] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))

Cache the standard NormedAddCommGroup C(K,CylinderL2 period E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular15 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular16 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))

Cache the standard NormedSpace ℝ C(K,CylinderL2 period E) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular16 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular17 (period : ℝ) [Fact (0 < period)] {F : Type u_2} {K : Type u_3} [NormedAddCommGroup F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F))

Cache the standard NormedAddCommGroup C(K,CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular17 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular18 (period : ℝ) [Fact (0 < period)] {F : Type u_2} {K : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F))

Cache the standard NormedSpace ℝ C(K,CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular18 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular19 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period F))

Cache the standard NormedAddCommGroup C(K,CylinderL2 period E →L[ℝ] CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular19 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular20 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period F))

Cache the standard NormedSpace ℝ C(K,CylinderL2 period E →L[ℝ] CylinderL2 period F) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular20 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular21 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup (C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F)))

Cache the standard NormedAddCommGroup (C(K,CylinderL2 period E) →L[ℝ] C(K,CylinderL2 period F)) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular21 period = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular22 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ (C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F)))

Cache the standard NormedSpace ℝ (C(K,CylinderL2 period E) →L[ℝ] C(K,CylinderL2 period F)) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular22 period = inferInstance

noncomputable def EulerLpCylinderRectangular.fullOperatorMap (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period F)

Actual multiplication on cylinder L² by an angle-independent field.

Equations

• EulerLpCylinderRectangular.fullOperatorMap period = EulerLpOperatorField.fullMap (EulerLiftedGradientSpace.liftMeasure period) ∘SL EulerLpCylinderTranslation.fieldLift period

@[simp]

theorem EulerLpCylinderRectangular.fullOperatorMap_apply (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) : (fullOperatorMap period) A = EulerLpOperatorField.full (EulerLiftedGradientSpace.liftMeasure period) ((EulerLpCylinderTranslation.fieldLift period) A)

theorem EulerLpCylinderRectangular.fullOperatorMap_norm (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : ‖fullOperatorMap period‖ ≤ 1

noncomputable def EulerLpCylinderRectangular.fullPathMap (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 period F))

The same contraction uniformly along a compact time set.

Equations

• EulerLpCylinderRectangular.fullPathMap period = ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpCylinderRectangular.fullOperatorMap period)

@[simp]

theorem EulerLpCylinderRectangular.fullPathMap_apply (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (t : K) : ((fullPathMap period) A) t = (fullOperatorMap period) (A t)

theorem EulerLpCylinderRectangular.fullPathMap_norm (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : ‖fullPathMap period‖ ≤ 1

noncomputable def EulerLpCylinderRectangular.fullMultiplierMap (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period F))

The actual coefficient-to-multiplication map on continuous cylinder paths.

Equations

• EulerLpCylinderRectangular.fullMultiplierMap period = EulerContinuousPathCalculus.coefficientMap ∘SL EulerLpCylinderRectangular.fullPathMap period

@[simp]

theorem EulerLpCylinderRectangular.fullMultiplierMap_apply (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) (t : K) : (((fullMultiplierMap period) A) u) t = ((fullOperatorMap period) (A t)) (u t)

theorem EulerLpCylinderRectangular.fullMultiplierMap_norm (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] : ‖fullMultiplierMap period‖ ≤ 1

theorem EulerLpCylinderRectangular.fullOperator_translation (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (a : EulerLiftedGradientSpace.LiftTangent) (A : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 period E)) : ((fullOperatorMap period) (EulerMeanCoefficients.translated A a.1)) ((EulerLpCylinderTranslation.translate period a) u) = (EulerLpCylinderTranslation.translate period a) (((fullOperatorMap period) A) u)

Literal mixed translations intertwine the actual rectangular L² multipliers.

theorem EulerLpCylinderRectangular.fullMultiplier_translation (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (a : EulerLiftedGradientSpace.LiftTangent) (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 period E))) : ((fullMultiplierMap period) (EulerMeanCoefficients.translateCoefficientPath A a.1)) ((EulerLpCylinderTranslation.pathTranslate period a) u) = (EulerLpCylinderTranslation.pathTranslate period a) (((fullMultiplierMap period) A) u)

The exact mixed-translation identity holds in the uniform continuous-path space.

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular23 (period : ℝ) [Fact (0 < period)] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported period E S hS)

Cache the standard NormedAddCommGroup (Supported period E S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular23 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular24 (period : ℝ) [Fact (0 < period)] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported period E S hS)

Cache the standard NormedSpace ℝ (Supported period E S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular24 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular25 (period : ℝ) [Fact (0 < period)] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported period F S hS)

Cache the standard NormedAddCommGroup (Supported period F S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular25 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular26 (period : ℝ) [Fact (0 < period)] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported period F S hS)

Cache the standard NormedSpace ℝ (Supported period F S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular26 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular27 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup (↥(EulerLpCylinderPaths.Supported period E S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period F S hS))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular27 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular28 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ (↥(EulerLpCylinderPaths.Supported period E S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period F S hS))

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

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular28 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular29 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))

Cache the standard NormedAddCommGroup C(K,Supported period E S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular29 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular30 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))

Cache the standard NormedSpace ℝ C(K,Supported period E S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular30 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular31 (period : ℝ) [Fact (0 < period)] {F : Type u_2} {K : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup C(K, ↥(EulerLpCylinderPaths.Supported period F S hS))

Cache the standard NormedAddCommGroup C(K,Supported period F S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular31 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular32 (period : ℝ) [Fact (0 < period)] {F : Type u_2} {K : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ C(K, ↥(EulerLpCylinderPaths.Supported period F S hS))

Cache the standard NormedSpace ℝ C(K,Supported period F S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular32 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular33 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup C(K, ↥(EulerLpCylinderPaths.Supported period E S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period F S hS))

Cache the standard NormedAddCommGroup C(K,Supported period E S hS →L[ℝ] Supported period F S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular33 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular34 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ C(K, ↥(EulerLpCylinderPaths.Supported period E S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period F S hS))

Cache the standard NormedSpace ℝ C(K,Supported period E S hS →L[ℝ] Supported period F S hS) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular34 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular35 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup (C(K, ↥(EulerLpCylinderPaths.Supported period E S hS)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported period F S hS)))

Cache the standard NormedAddCommGroup (C(K,Supported period E S hS) →L[ℝ] C(K,Supported period F S hS)) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular35 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderRectangular36 (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ (C(K, ↥(EulerLpCylinderPaths.Supported period E S hS)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported period F S hS)))

Cache the standard NormedSpace ℝ (C(K,Supported period E S hS) →L[ℝ] C(K,Supported period F S hS)) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderRectangular.instLpCylinderRectangular36 period S hS = inferInstance

noncomputable def EulerLpCylinderRectangular.supportedOperatorMap (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period E S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period F S hS)

Restriction to the closed spatial-support subspaces.

Equations

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

@[simp]

theorem EulerLpCylinderRectangular.supportedOperatorMap_coe (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (A : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) (u : ↥(EulerLpCylinderPaths.Supported period E S hS)) : ↑(((supportedOperatorMap period S hS) A) u) = ((fullOperatorMap period) A) ↑u

theorem EulerLpCylinderRectangular.supportedOperatorMap_norm (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : ‖supportedOperatorMap period S hS‖ ≤ 1

noncomputable def EulerLpCylinderRectangular.supportedPathMap (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported period E S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period F S hS))

Supported path map, given by (supportedOperatorMap (E := E) (F := F) period S hS).compLeftContinuous ℝ K.

Equations

• EulerLpCylinderRectangular.supportedPathMap period S hS = ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpCylinderRectangular.supportedOperatorMap period S hS)

noncomputable def EulerLpCylinderRectangular.supportedMultiplierMap (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported period E S hS)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported period F S hS))

Supported multiplier map as an element of C(K,Space →ᵇ E →L[ℝ] F) →L[ℝ] (C(K,Supported period E S hS) →L[ℝ] C(K,Supported period F S hS)).

Equations

• EulerLpCylinderRectangular.supportedMultiplierMap period S hS = EulerContinuousPathCalculus.coefficientMap ∘SL EulerLpCylinderRectangular.supportedPathMap period S hS

@[simp]

theorem EulerLpCylinderRectangular.supportedMultiplierMap_apply (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (u : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))) (t : K) : (((supportedMultiplierMap period S hS) A) u) t = ((supportedOperatorMap period S hS) (A t)) (u t)

theorem EulerLpCylinderRectangular.include_supportedMultiplier (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} {K : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [TopologicalSpace K] [CompactSpace K] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (u : C(K, ↥(EulerLpCylinderPaths.Supported period E S hS))) : (EulerLpCylinderPaths.includePath period S hS) (((supportedMultiplierMap period S hS) A) u) = ((fullMultiplierMap period) A) ((EulerLpCylinderPaths.includePath period S hS) u)

Inclusion identifies the supported product with the actual full-cylinder product.