Ordinary spatial covariance of the mean Gram inverse

These identities act at one actual time slice in ordinary solenoidal L². They identify the continuous acceleration family with translation of the original acceleration, including endpoint time values.

theorem EulerMeanPointwiseGramTranslation.frame_translation (a : EulerSmoothLimit.Space) (F : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (v : ↥EulerMeanSolenoidal.solenoidalSpace) : (EulerMeanOperatorTranslation.translateOperator a F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) ((EulerMeanTimeTranslation.solenoidalTranslation a) v) = (EulerMeanSolenoidal.translation a) ((F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) v)

theorem EulerMeanPointwiseGramTranslation.frameAdjoint_translation (a : EulerSmoothLimit.Space) (F : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (f : ↥EulerMeanSolenoidal.L2) : (ContinuousLinearMap.adjoint (EulerMeanOperatorTranslation.translateOperator a F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) ((EulerMeanSolenoidal.translation a) f) = (EulerMeanTimeTranslation.solenoidalTranslation a) ((ContinuousLinearMap.adjoint (F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) f)

theorem EulerMeanPointwiseGramTranslation.gram_translation (a : EulerSmoothLimit.Space) (F : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (v : ↥EulerMeanSolenoidal.solenoidalSpace) : (EulerTransverseGramInverse.gram (EulerMeanOperatorTranslation.translateOperator a F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) ((EulerMeanTimeTranslation.solenoidalTranslation a) v) = (EulerMeanTimeTranslation.solenoidalTranslation a) ((EulerTransverseGramInverse.gram (F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) v)

theorem EulerMeanPointwiseGramTranslation.translated_lower (a : EulerSmoothLimit.Space) (F : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (c : ℝ) (hF : ∀ (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖(F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) v‖ ^ 2) (v : ↥EulerMeanSolenoidal.solenoidalSpace) : c * ‖v‖ ^ 2 ≤ ‖(EulerMeanOperatorTranslation.translateOperator a F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) v‖ ^ 2

theorem EulerMeanPointwiseGramTranslation.gramInverse_translation (a : EulerSmoothLimit.Space) (F : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (c : ℝ) (hc : 0 < c) (hF : ∀ (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖(F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) v‖ ^ 2) (g : ↥EulerMeanSolenoidal.solenoidalSpace) : (EulerTransverseGramInverse.gramInverse (EulerMeanOperatorTranslation.translateOperator a F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) c hc ⋯) ((EulerMeanTimeTranslation.solenoidalTranslation a) g) = (EulerMeanTimeTranslation.solenoidalTranslation a) ((EulerTransverseGramInverse.gramInverse (F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) c hc hF) g)

noncomputable def EulerMeanPointwiseGramTranslation.acceleration (F F₁ : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (c : ℝ) (hc : 0 < c) (hF : ∀ (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖(F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) v‖ ^ 2) (v : ↥EulerMeanSolenoidal.solenoidalSpace) (f : ↥EulerMeanSolenoidal.L2) : ↥EulerMeanSolenoidal.solenoidalSpace

The actual one-time acceleration operator from the strong mean equation.

Equations

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

theorem EulerMeanPointwiseGramTranslation.acceleration_translation (a : EulerSmoothLimit.Space) (F F₁ : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (c : ℝ) (hc : 0 < c) (hF : ∀ (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖(F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL) v‖ ^ 2) (v : ↥EulerMeanSolenoidal.solenoidalSpace) (f : ↥EulerMeanSolenoidal.L2) : acceleration (EulerMeanOperatorTranslation.translateOperator a F) (EulerMeanOperatorTranslation.translateOperator a F₁) c hc ⋯ ((EulerMeanTimeTranslation.solenoidalTranslation a) v) ((EulerMeanSolenoidal.translation a) f) = (EulerMeanTimeTranslation.solenoidalTranslation a) (acceleration F F₁ c hc hF v f)

Simultaneously translating all data gives the actual translated acceleration.