Literal angular averaging preserves actual raw cylinder-path admissibility.

Literal angular averages are admissible mean forcing

The cylinder-to-space mean is the actual normalized angular integral. Its proved ordinary translation regularity is converted into literal spatial L² jets, so the mean packet provider receives an actual admissible input.

The bounded cylinder-to-space operator is the literal angular integral on smooth fields.

theorem EulerCylinderSpatialMean.continuous_memLp_of_lift (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] (g : EulerSmoothLimit.Space → V) (hg : Continuous g) (hgl : MeasureTheory.MemLp (fun (z : EulerLiftedGradientSpace.LiftDomain P) => g z.1) 2 (EulerLiftedGradientSpace.liftMeasure P)) : MeasureTheory.MemLp g 2 MeasureTheory.volume

A continuous constant-angle field is spatially L² whenever its cylinder lift is L².

noncomputable def EulerCylinderSpatialMean.rawMean (P : ℝ) (f : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (y : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Raw mean, given by P⁻¹ • (∫ s in (0 : ℝ)..P, f (y,(s : AddCircle P))).

Equations

• EulerCylinderSpatialMean.rawMean P f y = P⁻¹ • ∫ (s : ℝ) in 0..P, f (y, ↑s)

theorem EulerCylinderSpatialMean.rawMean_continuous (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (f : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hf : Continuous f) (hrep : ↑↑(EulerCylinderSobolevSpace.value P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) : Continuous (rawMean P f)

theorem EulerCylinderSpatialMean.average_ae_rawMean (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (f : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hf : Continuous f) (hrep : ↑↑(EulerCylinderSobolevSpace.value P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) : ↑↑((EulerCylinderAngleAverage.average P) (EulerCylinderSobolevSpace.value P u)) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (z : EulerLiftedGradientSpace.LiftDomain P) => rawMean P f z.1

theorem EulerCylinderSpatialMean.rawMean_memLp (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (f : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hf : Continuous f) (hrep : ↑↑(EulerCylinderSobolevSpace.value P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) : MeasureTheory.MemLp (rawMean P f) 2 MeasureTheory.volume

theorem EulerCylinderSpatialMean.mean_ae_rawMean (P : ℝ) [Fact (0 < P)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace P 3)) (f : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hf : Continuous f) (hrep : ↑↑(EulerCylinderSobolevSpace.value P u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) : ↑↑((mean P) (EulerCylinderSobolevSpace.value P u)) =ᵐ[MeasureTheory.volume] rawMean P f

The actual ordinary-space L² mean has the normalized integral as its representative.

The literal angular mean of a solved cylinder path is an actual smooth spatial L² path.

theorem EulerCylinderSpatialMean.pathMean_pointField_ae (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : ↑↑(((pathMean P) p) t) =ᵐ[MeasureTheory.volume] rawMean P (EulerCylinderSmoothOrbit.pointField P p hp t)

The ordinary L² time path represents the actual angular integral at every time.

theorem EulerCylinderSpatialMean.mean_slice_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : EulerMeanSmoothRepresentative.SmoothOrbit (((pathMean P) p) t)

theorem EulerCylinderSpatialMean.mean_pointField_eq (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : EulerMeanSmoothRepresentative.representative (((pathMean P) p) t) ⋯ = rawMean P (EulerCylinderSmoothOrbit.pointField P p hp t)

Uniqueness identifies the mean solver's ordinary representative with the literal integral.

theorem EulerCylinderSpatialMean.rawMean_pointField_contDiff (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : ContDiff ℝ (↑⊤) (rawMean P (EulerCylinderSmoothOrbit.pointField P p hp t))

noncomputable def EulerMeanPacketProvider.angularMeanRaw (D : Data) (P : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : EulerPacketProfileRecursion.VectorField

The literal normalized integral of the actual cylinder representative.

Equations

• EulerMeanPacketProvider.angularMeanRaw D P p hp z = EulerCylinderSpatialMean.rawMean P (EulerCylinderSmoothOrbit.pointField P p hp (D.clamp z.1)) z.2.1

theorem EulerMeanPacketProvider.angularMean_orbit (D : Data) (P : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T a) ((EulerCylinderSpatialMean.pathMean P) p)

noncomputable def EulerMeanPacketProvider.angularMeanForcing (D : Data) (P : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : Forcing D (angularMeanRaw D P p hp)

A genuine forcing witness for the normalized angular mean.

Equations

• EulerMeanPacketProvider.angularMeanForcing D P p hp = EulerMeanPacketProvider.Forcing.ofOrbitPath ((EulerCylinderSpatialMean.pathMean P) p) ⋯ ⋯

noncomputable def EulerMeanPacketProvider.angularMeanForcingOfRaw (D : Data) (P : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 D.T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (raw : EulerPacketProfileRecursion.VectorField) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = EulerCylinderSmoothOrbit.pointField P p hp t (x, ↑θ)) : Forcing D fun (z : EulerPacketPointJets.Domain) => P⁻¹ • ∫ (θ : ℝ) in 0..P, raw (z.1, z.2.1, θ)

A raw cylinder field identified with that representative has the same admissible mean.

Equations

• EulerMeanPacketProvider.angularMeanForcingOfRaw D P p hp raw hraw = (EulerMeanPacketProvider.angularMeanForcing D P p hp).congr ⋯

noncomputable def EulerPacketCylinderField.Field.angleMean {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : Field P T (EulerPacketProfileRecursion.angleMean P raw)

Its path is the genuine average operator, and its raw field is exactly the angular integral.

Equations

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

noncomputable def EulerPacketCylinderField.Field.highPart {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : Field P T (raw - EulerPacketProfileRecursion.angleMean P raw)

Subtracting the literal mean is an operation on the actual cylinder L² path.

Equations

• G.highPart = G.sub G.angleMean

@[simp]

theorem EulerPacketCylinderField.Field.angleMean_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : G.angleMean.path = (EulerCylinderAngleAverage.pathAverage P) G.path

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

The same actual angular integral is admissible for the constructed ordinary-space mean solver.

Equations

• EulerPacketCylinderField.Field.meanForcing D G = EulerMeanPacketProvider.angularMeanForcingOfRaw D P G.path ⋯ raw ⋯