Actual translated coefficient operators for the mean equation

The translated operator is literal conjugation by spatial translation on ordinary L². Its Bochner multiplier and H¹ frame derivative obey exact covariance, including the terminal primitive and initial trace.

noncomputable def EulerMeanOperatorTranslation.translateOperator (a : EulerSmoothLimit.Space) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Literal spatial conjugation of a bounded operator on ordinary L².

Equations

• EulerMeanOperatorTranslation.translateOperator a A = (EulerMeanSolenoidal.translation a).toContinuousLinearMap ∘SL A ∘SL (EulerMeanSolenoidal.translation (-a)).toContinuousLinearMap

@[simp]

theorem EulerMeanOperatorTranslation.translateOperator_apply (a : EulerSmoothLimit.Space) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (u : ↥EulerMeanSolenoidal.L2) : (translateOperator a A) u = (EulerMeanSolenoidal.translation a) (A ((EulerMeanSolenoidal.translation (-a)) u))

theorem EulerMeanOperatorTranslation.translateOperator_translation (a : EulerSmoothLimit.Space) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (u : ↥EulerMeanSolenoidal.L2) : (translateOperator a A) ((EulerMeanSolenoidal.translation a) u) = (EulerMeanSolenoidal.translation a) (A u)

Applying the translated coefficient to the translated field is exact covariance.

@[simp]

theorem EulerMeanOperatorTranslation.translateOperator_zero (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : translateOperator 0 A = A

theorem EulerMeanOperatorTranslation.translateOperator_add (a : EulerSmoothLimit.Space) (A B : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : translateOperator a (A + B) = translateOperator a A + translateOperator a B

theorem EulerMeanOperatorTranslation.translateOperator_smul (a : EulerSmoothLimit.Space) (c : ℝ) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : translateOperator a (c • A) = c • translateOperator a A

theorem EulerMeanOperatorTranslation.translateOperator_neg_cancel (a : EulerSmoothLimit.Space) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : translateOperator (-a) (translateOperator a A) = A

theorem EulerMeanOperatorTranslation.translateOperator_norm_le (a : EulerSmoothLimit.Space) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : ‖translateOperator a A‖ ≤ ‖A‖

theorem EulerMeanOperatorTranslation.translateOperator_norm (a : EulerSmoothLimit.Space) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : ‖translateOperator a A‖ = ‖A‖

noncomputable def EulerMeanOperatorTranslation.translatePath (T : ℝ) (a : EulerSmoothLimit.Space) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Translate the spatial operator at every time in the coefficient path.

Equations

• EulerMeanOperatorTranslation.translatePath T a F = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerMeanOperatorTranslation.translateOperator a (F t), continuous_toFun := ⋯ }

@[simp]

theorem EulerMeanOperatorTranslation.translatePath_apply (T : ℝ) (a : EulerSmoothLimit.Space) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (t : ↑(Set.Icc 0 T)) : (translatePath T a F) t = translateOperator a (F t)

theorem EulerMeanOperatorTranslation.translatePath_norm_le (T : ℝ) (a : EulerSmoothLimit.Space) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ‖translatePath T a F‖ ≤ ‖F‖

theorem EulerMeanOperatorTranslation.timeMultiplier_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (EulerTimeLp.timeMultiplier T hT (translatePath T a F)) ((EulerMeanTimeTranslation.timeTranslation T a) u) = (EulerMeanTimeTranslation.timeTranslation T a) ((EulerTimeLp.timeMultiplier T hT F) u)

Translation commutes with the genuine time multiplier.

theorem EulerMeanOperatorTranslation.frameMultiplier_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)) : (EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T (translatePath T a F))) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) u) = (EulerMeanTimeTranslation.timeTranslation T a) ((EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T F)) u)

The actual solenoidal frame multiplier has the corresponding covariance.

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

The genuine H¹ product derivative commutes with translated coefficients.