Translation covariance of the actual mean acceleration

The Gram inverse on the fixed solenoidal time space is the genuine coercive inverse. Its translated family has the same lower bound, and its application is the spatial orbit of the original acceleration. The final identification uses the already proved strong equation of the actual variational solution.

@[instance_reducible]

noncomputable def instMeanGramTranslation1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• instMeanGramTranslation1 = inferInstance

@[instance_reducible]

noncomputable def instMeanGramTranslation2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• instMeanGramTranslation2 = inferInstance

@[instance_reducible]

noncomputable def instMeanGramTranslation3 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• instMeanGramTranslation3 T = inferInstance

@[instance_reducible]

noncomputable def instMeanGramTranslation4 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• instMeanGramTranslation4 T = inferInstance

@[instance_reducible]

noncomputable def instMeanGramTranslation5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• instMeanGramTranslation5 T = inferInstance

@[instance_reducible]

noncomputable def instMeanGramTranslation6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• instMeanGramTranslation6 T = inferInstance

theorem EulerMeanGramTranslation.translatedFrame_lower (T : ℝ) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hF : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (a : EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace) : c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F)) t) v‖ ^ 2

The actual spatially translated frame retains its original lower bound.

theorem EulerMeanGramTranslation.frameMultiplier_adjoint_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F)))) ((EulerMeanTimeTranslation.timeTranslation T a) f) = (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T F))) f)

The adjoint frame multiplier transforms by ordinary spatial translation.

theorem EulerMeanGramTranslation.gramOperator_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerTimeLpGramInverse.gramOperator T hT (EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F))) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) u) = (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerTimeLpGramInverse.gramOperator T hT (EulerMeanVariationalInverse.solenoidalFrame T F)) u)

Spatial translation conjugates the actual time Gram operator.

theorem EulerMeanGramTranslation.gramSolver_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hc : 0 < c) (hF : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (g : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerTimeLpGramInverse.gramSolver T hT (EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F)) c hc ⋯) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) g) = (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerTimeLpGramInverse.gramSolver T hT (EulerMeanVariationalInverse.solenoidalFrame T F) c hc hF) g)

The actual coercive Gram inverse is covariant; no regularity of an inverse or of the unknown solution is assumed.

noncomputable def EulerMeanGramTranslation.meanAcceleration (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hc : 0 < c) (hF : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

The genuine fixed-coordinate acceleration recovered from velocity and forcing.

Equations

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

theorem EulerMeanGramTranslation.meanAcceleration_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hc : 0 < c) (hF : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : meanAcceleration T hT (EulerMeanOperatorTranslation.translatePath T a F) (EulerMeanOperatorTranslation.translatePath T a F₁) c hc ⋯ ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v) ((EulerMeanTimeTranslation.timeTranslation T a) f) = (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) (meanAcceleration T hT F F₁ c hc hF v f)

The translated acceleration is obtained by the actual translated coefficients.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.acceleration_eq_meanAcceleration {T : ℝ} {hT : 0 ≤ T} {FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)} {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : StrongMeanEvolution T hT FInv F F₁ A L u f) (c : ℝ) (hc : 0 < c) (hF : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2) : s.acceleration = EulerMeanGramTranslation.meanAcceleration T hT F F₁ c hc hF s.velocityLp f

The acceleration already constructed from the strong weak-solution theorem is exactly the coercive Gram solve used for the spatial estimates.