Actual zero angular mean of the history solution #
Angle-independent coefficients commute with the genuine cylinder average, including the adjoint test maps. The constructed inverse and its continuous velocity therefore preserve zero mean. No pointwise mean condition is assumed on the solution.
theorem
EulerLpCylinderRectangular.fullOperatorMap_adjoint
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(Q : BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] E))
:
theorem
EulerLpCylinderRectangular.average_fullOperator_back
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(Q : BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] E))
(u : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
:
((fullOperatorMap P) Q) ((ContinuousLinearMap.adjoint (EulerCylinderAngleAverage.average P)) u) = (ContinuousLinearMap.adjoint (EulerCylinderAngleAverage.average P)) (((fullOperatorMap P) Q) u)
theorem
EulerCylinderDirichlet.Coefficients.velocityPath_average
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
((velocityPath P D) ((EulerTimeLpBoundedMap.timeLift T (EulerCylinderAngleAverage.average P)) f)) t = (EulerCylinderAngleAverage.average P) (((velocityPath P D) f) t)
theorem
EulerCylinderDirichlet.Coefficients.accelerationPath_average
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
(accelerationPath P D ((EulerCylinderAngleAverage.pathAverage P) f)) t = (EulerCylinderAngleAverage.average P) ((accelerationPath P D f) t)
theorem
EulerCylinderDirichlet.Coefficients.physicalVelocity_average
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
(physicalVelocity P D ((EulerCylinderAngleAverage.pathAverage P) f)) t = (EulerCylinderAngleAverage.average P) ((physicalVelocity P D f) t)
theorem
EulerCylinderDirichlet.Coefficients.physicalDerivative_average
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
(physicalDerivative P D ((EulerCylinderAngleAverage.pathAverage P) f)) t = (EulerCylinderAngleAverage.average P) ((physicalDerivative P D f) t)
theorem
EulerCylinderDirichlet.Coefficients.accelerationPath_zero
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerCylinderDirichlet.Coefficients.physicalVelocity_zero
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerCylinderDirichlet.Coefficients.physicalDerivative_zero
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerCylinderDirichlet.Coefficients.velocityPath_mean_zero
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) (f t) = 0)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerCylinderDirichlet.Coefficients.accelerationPath_mean_zero
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) (f t) = 0)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerCylinderDirichlet.Coefficients.physicalVelocity_mean_zero
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) (f t) = 0)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerCylinderDirichlet.Coefficients.physicalDerivative_mean_zero
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) (f t) = 0)
(t : ↑(Set.Icc 0 T))
: