Genuine time derivatives for the full-cylinder rectangular products.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

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

Equations

• EulerLpCylinderRectangular.instLpCylinderFullTime5 P = inferInstance

@[instance_reducible]

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

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

Equations

• EulerLpCylinderRectangular.instLpCylinderFullTime6 P = inferInstance

@[instance_reducible]

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

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

Equations

• EulerLpCylinderRectangular.instLpCylinderFullTime7 P = inferInstance

@[instance_reducible]

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

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

Equations

• EulerLpCylinderRectangular.instLpCylinderFullTime8 P = inferInstance

theorem EulerLpCylinderRectangular.fullPath_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (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 ((fullPathMap P) A)) (((fullPathMap P) A₁) t) (Set.Icc 0 T) ↑t

theorem EulerLpCylinderRectangular.fullProduct_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (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), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (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 (((fullMultiplierMap P) A) u)) ((((fullMultiplierMap P) A₁) u) t + (((fullMultiplierMap P) A) u₁) t) (Set.Icc 0 T) ↑t