Continuous-time and same-radius word estimates for the actual spatial mean.

@[instance_reducible]

noncomputable def EulerCylinderSpatialMean.instCylinderSpatialMeanPath1 (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))

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

Equations

• EulerCylinderSpatialMean.instCylinderSpatialMeanPath1 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSpatialMean.instCylinderSpatialMeanPath2 (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))

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

Equations

• EulerCylinderSpatialMean.instCylinderSpatialMeanPath2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSpatialMean.instCylinderSpatialMeanPath3 {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerCylinderSpatialEmbedding.SpatialL2 V))

Cache the standard NormedAddCommGroup C(K,SpatialL2 V) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSpatialMean.instCylinderSpatialMeanPath3 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSpatialMean.instCylinderSpatialMeanPath4 {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerCylinderSpatialEmbedding.SpatialL2 V))

Cache the standard NormedSpace ℝ C(K,SpatialL2 V) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSpatialMean.instCylinderSpatialMeanPath4 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSpatialMean.instCylinderSpatialMeanPath5 (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup (C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V)) →L[ℝ] C(K, ↥(EulerCylinderSpatialEmbedding.SpatialL2 V)))

Cache the standard NormedAddCommGroup (C(K,CylinderL2 P V) →L[ℝ] C(K,SpatialL2 V)) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSpatialMean.instCylinderSpatialMeanPath5 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSpatialMean.instCylinderSpatialMeanPath6 (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ (C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V)) →L[ℝ] C(K, ↥(EulerCylinderSpatialEmbedding.SpatialL2 V)))

Cache the standard NormedSpace ℝ (C(K,CylinderL2 P V) →L[ℝ] C(K,SpatialL2 V)) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSpatialMean.instCylinderSpatialMeanPath6 P = inferInstance

noncomputable def EulerCylinderSpatialMean.pathMean (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [TopologicalSpace K] : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V)) →L[ℝ] C(K, ↥(EulerCylinderSpatialEmbedding.SpatialL2 V))

Path mean, given by (mean P).compLeftContinuous ℝ K.

Equations

• EulerCylinderSpatialMean.pathMean P = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderSpatialMean.mean P)

@[simp]

theorem EulerCylinderSpatialMean.pathMean_apply (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [TopologicalSpace K] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))) (t : K) : ((pathMean P) p) t = (mean P) (p t)

noncomputable def EulerCylinderSpatialMean.spatialPathTranslation {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [TopologicalSpace K] (a : EulerSmoothLimit.Space) : C(K, ↥(EulerCylinderSpatialEmbedding.SpatialL2 V)) →L[ℝ] C(K, ↥(EulerCylinderSpatialEmbedding.SpatialL2 V))

Spatial path translation, given by (EulerLpTranslation.translation a).toContinuousLinearMap.compLeftContinuous ℝ K.

Equations

• EulerCylinderSpatialMean.spatialPathTranslation a = ContinuousLinearMap.compLeftContinuous ℝ K (EulerLpTranslation.translation a).toContinuousLinearMap

theorem EulerCylinderSpatialMean.pathMean_translation (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [TopologicalSpace K] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))) (a : EulerLiftedGradientSpace.LiftTangent) : (pathMean P) ((EulerLpCylinderTranslation.pathTranslate P a) p) = (spatialPathTranslation a.1) ((pathMean P) p)

theorem EulerCylinderSpatialMean.pathMean_norm (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [TopologicalSpace K] [CompactSpace K] : ‖pathMean P‖ ≤ P⁻¹ * √P

theorem EulerCylinderSpatialMean.pathMean_orbit_contDiff (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (spatialPathTranslation a) ((pathMean P) p)

All ordinary spatial derivatives of the mean are inherited from the actual mixed orbit.

theorem EulerCylinderSpatialMean.pathMean_block_bound (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [TopologicalSpace K] [CompactSpace K] {X : Type u_3} {ι : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [Fintype ι] (directions : ι → X) (q : ℕ) (f : X → C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (pathMean P) (f y)) n x ≤ P⁻¹ * √P * EulerParameterWordGevrey.block directions q f n x

theorem EulerCylinderSpatialMean.pathMean_block_majorant (P : ℝ) [Fact (0 < P)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [TopologicalSpace K] [CompactSpace K] {X : Type u_3} {ι : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [Fintype ι] (directions : ι → X) (q : ℕ) (f : X → C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))) (hf : ContDiff ℝ (↑⊤) f) (R C : ℝ) (d : ℕ) (hb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (pathMean P) (f y)) n x ≤ P⁻¹ * √P * C * EulerGevrey.majorant R d n