Genuine bounded smooth cylinder coefficients and all their derivative jets are constructed from the actual coefficient translation orbit.

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSmooth1 {V : Type u_2} [NormedAddCommGroup V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space V)

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

Equations

• EulerCoefficientPath.instCoefficientPathSmooth1 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSmooth2 {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space V)

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

Equations

• EulerCoefficientPath.instCoefficientPathSmooth2 = inferInstance

theorem EulerCoefficientPath.cylinder_norm_iteratedFDeriv_le {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (P : ℝ) (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (n : ℕ) (t : K) (x : EulerLiftedGradientSpace.LiftDomain P) (y : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift P (fun (z : EulerLiftedGradientSpace.LiftDomain P) => (A t) z.1) x) y‖ ≤ ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A) 0‖

theorem EulerCoefficientPath.cylinder_fieldDerivative {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (P : ℝ) (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V)) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (t : K) (v : EulerLiftedGradientSpace.LiftTangent) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerTransportDerivatives.fieldDerivative P v (fun (z : EulerLiftedGradientSpace.LiftDomain P) => (A t) z.1) x = ((EulerMeanCoefficients.orbitDerivativePath A v.1) t) x.1

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSmooth3 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCoefficientPath.instCoefficientPathSmooth3 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSmooth4 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCoefficientPath.instCoefficientPathSmooth4 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSmooth5 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCoefficientPath.instCoefficientPathSmooth5 = inferInstance

@[instance_reducible]

noncomputable def EulerCoefficientPath.instCoefficientPathSmooth6 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCoefficientPath.instCoefficientPathSmooth6 = inferInstance

noncomputable def EulerCoefficientPath.smoothCoefficient {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (t : K) : EulerSpatialSobolevInverse.SmoothCoefficient P

Smooth coefficient, bundling coefficient, smooth, bound, norm_bound and the required compatibility proofs.

Equations

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

@[simp]

theorem EulerCoefficientPath.smoothCoefficient_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (t : K) (x : EulerLiftedGradientSpace.LiftDomain P) : (smoothCoefficient P A hA t).coefficient x = (A t) x.1

def EulerCoefficientPath.coefficientJet {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (q : ℕ) (t : K) : EulerSpatialSobolevInverse.CoefficientJet P EulerCylinderSobolev.standardDirection q (smoothCoefficient P A hA t)

Coefficient jet as an element of CoefficientJet P standardDirection q (smoothCoefficient P A hA t).

Equations

• One or more equations did not get rendered due to their size.
• EulerCoefficientPath.coefficientJet P A hA 0 t = EulerSpatialSobolevInverse.CoefficientJet.zero (EulerCoefficientPath.smoothCoefficient P A hA t)

theorem EulerCoefficientPath.smoothCoefficient_operator {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) (t : K) : (smoothCoefficient P A hA t).operator = (EulerLpCylinderRectangular.fullOperatorMap P) (A t)

theorem EulerCoefficientPath.smoothCoefficient_operator_continuous {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (P : ℝ) [Fact (0 < P)] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hA : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath A)) : Continuous fun (t : K) => (smoothCoefficient P A hA t).operator