The actual source transverse solve preserves the angular zero mode constraint.

The actual supported Duhamel solution preserves zero angular mean.

theorem EulerCylinderAngleAverage.supportedAverage_operator (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (A : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) (u : ↥(EulerLpCylinderPaths.Supported P E S hS)) : (supportedAverage P S hS) (((EulerLpCylinderRectangular.supportedOperatorMap P S hS) A) u) = ((EulerLpCylinderRectangular.supportedOperatorMap P S hS) A) ((supportedAverage P S hS) u)

@[instance_reducible]

noncomputable def EulerCylinderAngleAverage.instCylinderAngleAverageEvolution1 (P : ℝ) [Fact (0 < P)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported P V S hS)

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

Equations

• EulerCylinderAngleAverage.instCylinderAngleAverageEvolution1 P S hS = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderAngleAverage.instCylinderAngleAverageEvolution2 (P : ℝ) [Fact (0 < P)] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported P V S hS)

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

Equations

• EulerCylinderAngleAverage.instCylinderAngleAverageEvolution2 P S hS = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderAngleAverage.instCylinderAngleAverageEvolution3 (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup C(K, ↥(EulerLpCylinderPaths.Supported P V S hS))

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

Equations

• EulerCylinderAngleAverage.instCylinderAngleAverageEvolution3 P S hS = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderAngleAverage.instCylinderAngleAverageEvolution4 (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ C(K, ↥(EulerLpCylinderPaths.Supported P V S hS))

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

Equations

• EulerCylinderAngleAverage.instCylinderAngleAverageEvolution4 P S hS = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderAngleAverage.instCylinderAngleAverageEvolution5 (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup (C(K, ↥(EulerLpCylinderPaths.Supported P V S hS)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported P V S hS)))

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

Equations

• EulerCylinderAngleAverage.instCylinderAngleAverageEvolution5 P S hS = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderAngleAverage.instCylinderAngleAverageEvolution6 (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ (C(K, ↥(EulerLpCylinderPaths.Supported P V S hS)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported P V S hS)))

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

Equations

• EulerCylinderAngleAverage.instCylinderAngleAverageEvolution6 P S hS = inferInstance

noncomputable def EulerCylinderAngleAverage.supportedPathAverage (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : C(K, ↥(EulerLpCylinderPaths.Supported P V S hS)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported P V S hS))

Supported path average, given by (supportedAverage P S hS).compLeftContinuous ℝ K.

Equations

• EulerCylinderAngleAverage.supportedPathAverage P S hS = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderAngleAverage.supportedAverage P S hS)

@[simp]

theorem EulerCylinderAngleAverage.supportedPathAverage_apply (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p : C(K, ↥(EulerLpCylinderPaths.Supported P V S hS))) (t : K) : ((supportedPathAverage P S hS) p) t = (supportedAverage P S hS) (p t)

theorem EulerCylinderAngleAverage.include_supportedPathAverage (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (p : C(K, ↥(EulerLpCylinderPaths.Supported P V S hS))) : (EulerLpCylinderPaths.includePath P S hS) ((supportedPathAverage P S hS) p) = (pathAverage P) ((EulerLpCylinderPaths.includePath P S hS) p)

theorem EulerCylinderAngleAverage.supportedPathAverage_norm (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : ‖supportedPathAverage P S hS‖ ≤ 1

theorem EulerCylinderAngleAverage.solution_average (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (U : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath P S hS T B)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P V S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P V S hS)) : (supportedPathAverage P S hS) (U.solution f a₀) = U.solution ((supportedPathAverage P S hS) f) ((supportedAverage P S hS) a₀)

Averaging the genuine forced solution equals solving with averaged data.

theorem EulerCylinderAngleAverage.solution_average_zero (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (U : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath P S hS T B)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P V S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P V S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (supportedAverage P S hS) (f t) = 0) (ha₀ : (supportedAverage P S hS) a₀ = 0) (t : ↑(Set.Icc 0 T)) : (supportedAverage P S hS) ((U.solution f a₀) t) = 0

Zero mean of the data propagates by the proved uniqueness of the actual ODE.

theorem EulerCylinderAngleAverage.solution_full_average_zero (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (U : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath P S hS T B)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P V S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P V S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (average P) ↑(f t) = 0) (ha₀ : (average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : (average P) ↑((U.solution f a₀) t) = 0

The same theorem in the ordinary cylinder L² space used by the classical representatives.

theorem EulerSourceCylinderEquation.projectedForcing_average_zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (Q : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) ↑((EulerSourceCylinderForcing.projectedForcing P S hS Q c hc hQ f) t) = 0

theorem EulerSourceCylinderEquation.coordinates_average_zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀ : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) ↑((coordinates P S hS T hT Q Q₁ c hc hQ f a₀) t) = 0

The real Gram-projected Duhamel coordinate solution has zero angular mean.

theorem EulerSourceCylinderEquation.velocity_average_zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀ : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) ↑((velocity P S hS T hT Q Q₁ c hc hQ f a₀) t) = 0

Physical reconstruction by the true frame preserves the same zero mode.

theorem EulerSourceCylinderEquation.coordinateDerivative_average_zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀ : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) ↑((coordinateDerivative P S hS T hT Q Q₁ c hc hQ f a₀) t) = 0

theorem EulerSourceCylinderEquation.velocityDerivative_average_zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀ : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) ↑((velocityDerivative P S hS T hT Q Q₁ c hc hQ f a₀) t) = 0

The actual within-time derivative also has zero mean, as follows from its equation.