Actual coefficient time derivatives on the cylinder

The rectangular multipliers agree with the square operators used in the constructed Duhamel evolution. Literal within-time derivatives of the coefficient fields induce true operator-path derivatives and product rules.

theorem EulerLpCylinderRectangular.supportedOperator_eq_square (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (A : BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V)) : (supportedOperatorMap period S hS) A = EulerLpCylinderCoefficients.liftedOperator period S hS A

The two literal constructions are the same actual supported L² operator.

theorem EulerLpCylinderRectangular.supportedPath_eq_square (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (A : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) : (supportedPathMap period S hS) A = EulerLpCylinderCoefficients.liftedOperatorPath period S hS T A

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime1 {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.instLpCylinderCoefficientTime1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime2 {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.instLpCylinderCoefficientTime2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime3 {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.instLpCylinderCoefficientTime3 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime4 {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.instLpCylinderCoefficientTime4 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime5 (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.instLpCylinderCoefficientTime5 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime6 (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.instLpCylinderCoefficientTime6 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime7 (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.instLpCylinderCoefficientTime7 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime8 (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.instLpCylinderCoefficientTime8 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime9 (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.instLpCylinderCoefficientTime9 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderRectangular.instLpCylinderCoefficientTime10 (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.instLpCylinderCoefficientTime10 period S hS = inferInstance

theorem EulerLpCylinderRectangular.supportedPath_hasDerivWithinAt (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), 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 period S hS) A)) (((supportedPathMap period S hS) A₁) t) (Set.Icc 0 T) ↑t

The true derivative of the actual supported coefficient operator.

theorem EulerLpCylinderRectangular.supportedProduct_hasDerivWithinAt (period : ℝ) [Fact (0 < period)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F))) (hA : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT A s) x) ((EulerVolterraConvolution.extendPath T hT A₁ t) x) (Set.Icc 0 T) t) (u u₁ : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (hu : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT u) (u₁ t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (((supportedMultiplierMap period S hS) A) u)) ((((supportedMultiplierMap period S hS) A₁) u) t + (((supportedMultiplierMap period S hS) A) u₁) t) (Set.Icc 0 T) ↑t

The product rule is a genuine within-time statement, including the interval endpoints.