A genuinely smooth translated bounded-field family lifts to actual mixed cylinder coefficients.

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient1 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedAddCommGroup (V →L[ℝ] V)

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient1 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient2 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedSpace ℝ (V →L[ℝ] V)

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient2 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient3 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient3 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient4 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient4 = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient5 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,Space →ᵇ V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient5 T = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient6 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,Space →ᵇ V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient6 T = inferInstance

@[instance_reducible]

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

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient7 period S hS = inferInstance

@[instance_reducible]

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

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient8 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient9 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup (↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS))

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient9 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient10 (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ (↥(EulerLpCylinderPaths.Supported period V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported period V S hS))

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

Equations

• EulerLpCylinderCoefficients.instLpCylinderRegularCoefficient10 period S hS = inferInstance

theorem EulerLpCylinderCoefficients.mixedCoefficient_contDiff (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => liftedOperatorPath period S hS T (EulerMeanCoefficients.translateCoefficientPath B a.1)

This requires only actual translated coefficient regularity, so applies to the constructed Gram generator.

theorem EulerLpCylinderCoefficients.mixedCoefficient_bound (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (n : ℕ) (C : ℝ) (hb : ∀ (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath B) a‖ ≤ C) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => liftedOperatorPath period S hS T (EulerMeanCoefficients.translateCoefficientPath B b.1)) a‖ ≤ C

All actual mixed coefficient derivatives retain the real bounded-field derivative bound.