Actual mean outputs as constant-angle cylinder paths

The ordinary spatial L² field is embedded in the product measure. Its genuine translation orbit, literal raw representative and true time derivative are preserved by the same bounded linear embedding.

@[instance_reducible]

noncomputable def EulerMeanPacketProvider.instMeanPacketCylinderFields1 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPacketProvider.instMeanPacketCylinderFields1 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPacketProvider.instMeanPacketCylinderFields2 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPacketProvider.instMeanPacketCylinderFields2 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPacketProvider.instMeanPacketCylinderFields3 (P T : ℝ) [Fact (0 < P)] : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerMeanPacketProvider.instMeanPacketCylinderFields3 P T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPacketProvider.instMeanPacketCylinderFields4 (P T : ℝ) [Fact (0 < P)] : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerMeanPacketProvider.instMeanPacketCylinderFields4 P T = inferInstance

noncomputable def EulerMeanPacketProvider.spatialEmbeddingPath (P T : ℝ) [Fact (0 < P)] : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Spatial embedding path, given by (embedding (V := Space) P).compLeftContinuous ℝ (Icc (0 : ℝ) T).

Equations

• EulerMeanPacketProvider.spatialEmbeddingPath P T = ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSpatialEmbedding.embedding P)

@[simp]

theorem EulerMeanPacketProvider.spatialEmbeddingPath_apply (P T : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (t : ↑(Set.Icc 0 T)) : ((spatialEmbeddingPath P T) p) t = (EulerCylinderSpatialEmbedding.embedding P) (p t)

theorem EulerMeanPacketProvider.spatialEmbeddingPath_translation (P T : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (a : EulerLiftedGradientSpace.LiftTangent) : (EulerLpCylinderTranslation.pathTranslate P a) ((spatialEmbeddingPath P T) p) = (spatialEmbeddingPath P T) ((EulerMeanTimeContinuousTranslation.pathTranslation T a.1) p)

theorem EulerMeanPacketProvider.spatialEmbeddingPath_orbit (P T : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((spatialEmbeddingPath P T) p)

theorem EulerMeanPacketProvider.spatialEmbeddingPath_time (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (p q : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (h : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (q t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((spatialEmbeddingPath P T) p)) (((spatialEmbeddingPath P T) q) t) (Set.Icc 0 T) ↑t

noncomputable def EulerMeanPacketProvider.Forcing.toCylinderField (P : ℝ) [Fact (0 < P)] {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerPacketCylinderField.Field P D.T raw

Literal smooth mean forcing becomes an actual cylinder witness with no angular dependence.

Equations

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

@[simp]

theorem EulerMeanPacketProvider.Forcing.toCylinderField_path (P : ℝ) [Fact (0 < P)] {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : (toCylinderField P G).path = (spatialEmbeddingPath P D.T) G.path

noncomputable def EulerMeanPacketProvider.Forcing.vectorCylinderField (P : ℝ) [Fact (0 < P)] {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerPacketCylinderField.Field P D.T G.vector

Vector cylinder field, given by G.vectorForcing.toCylinderField P.

Equations

• EulerMeanPacketProvider.Forcing.vectorCylinderField P G = EulerMeanPacketProvider.Forcing.toCylinderField P G.vectorForcing

noncomputable def EulerMeanPacketProvider.Forcing.vectorDerivativeCylinderField (P : ℝ) [Fact (0 < P)] {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerPacketCylinderField.Field P D.T G.vectorDerivative

Vector derivative cylinder field, given by G.vectorDerivativeForcing.toCylinderField P.

Equations

• EulerMeanPacketProvider.Forcing.vectorDerivativeCylinderField P G = EulerMeanPacketProvider.Forcing.toCylinderField P G.vectorDerivativeForcing

theorem EulerMeanPacketProvider.Forcing.vectorCylinderField_time (P : ℝ) [Fact (0 < P)] {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerPacketCylinderField.TimeDerivative ⋯ (vectorCylinderField P G) (vectorDerivativeCylinderField P G)

noncomputable def EulerMeanPacketProvider.meanSolveCylinderField (P : ℝ) [Fact (0 < P)] (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) : EulerPacketCylinderField.Field P D.T (meanSolve D raw).1

Mean solve cylinder field, given by ((Classical.choice h).vectorCylinderField P).congr (fun _ _ _ => by rw [meanSolve_of_admissible D raw h]).

Equations

• EulerMeanPacketProvider.meanSolveCylinderField P D raw h = (EulerMeanPacketProvider.Forcing.vectorCylinderField P (Classical.choice h)).congr ⋯