Related estimates used together by the same construction modules.

The actual mean inverse on translated coefficient families

The inverse is built from the translated fixed form with the original proved coercivity constant. Its solution for translated forcing is exactly the spatial translation of the original solution. Thus regularity of known coefficient families yields genuine spatial regularity of the solved field.

@[instance_reducible]

noncomputable def EulerMeanTranslatedInverse.instMeanTranslatedInverse1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanTranslatedInverse.instMeanTranslatedInverse1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTranslatedInverse.instMeanTranslatedInverse2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

Equations

• EulerMeanTranslatedInverse.instMeanTranslatedInverse2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanTranslatedInverse.instMeanTranslatedInverse3 T = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanTranslatedInverse.instMeanTranslatedInverse4 T = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanTranslatedInverse.instMeanTranslatedInverse5 T = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanTranslatedInverse.instMeanTranslatedInverse6 T = inferInstance

noncomputable def EulerMeanTranslatedInverse.translatedMeanInverse (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (a : EulerSmoothLimit.Space) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

The genuine inverse of the translated fixed mean operator.

Equations

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

noncomputable def EulerMeanTranslatedInverse.translatedMeanSolver (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (a : EulerSmoothLimit.Space) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

The actual translated forcing-to-coordinate-derivative solver.

Equations

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

theorem EulerMeanTranslatedInverse.translatedMeanInverse_covariance (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (a : EulerSmoothLimit.Space) (g : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (translatedMeanInverse T hT F F₁ H M0 A L c hc hcoercive a) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) g) = (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerCoerciveProjection.coerciveInverse (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) c hc hcoercive) g)

The coercive inverse commutes with simultaneous translation of all coefficients.

theorem EulerMeanTranslatedInverse.translatedMeanSolver_covariance (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (a : EulerSmoothLimit.Space) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (translatedMeanSolver T hT F F₁ H M0 A L c hc hcoercive a) ((EulerMeanTimeTranslation.timeTranslation T a) f) = (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerCoerciveProjection.coerciveInverse (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) c hc hcoercive) (-(ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) f))

The translated actual solve is the spatial orbit of the original solve.

theorem EulerMeanTranslatedInverse.translatedMeanInverse_norm (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (a : EulerSmoothLimit.Space) : ‖translatedMeanInverse T hT F F₁ H M0 A L c hc hcoercive a‖ ≤ c⁻¹

Uniform coercivity gives a uniform inverse norm for the actual translated family.

theorem EulerMeanTranslatedInverse.solution_translation_contDiff (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) {n : WithTop ℕ∞} (hO : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanFixedTranslation.translatedMeanOperator T hT a F F₁ H M0 A L) (hJ : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanFixedTranslation.translatedMeanPrimitive T hT a F F₁) (hf : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerCoerciveProjection.coerciveInverse (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) c hc hcoercive) (-(ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) f))

Known coefficient and forcing smoothness gives actual spatial translation smoothness of the field solved by the genuine mean inverse.

Actual derivatives and factorial bounds for the translated multiplication operators.

theorem EulerMeanCoefficients.BoundedSmoothField.iteratedFDeriv_translation_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedSmoothField V) (n : ℕ) (a x : EulerSmoothLimit.Space) (v : Fin n → EulerSmoothLimit.Space) : ((iteratedFDeriv ℝ n (translated A.field) a) v) x = (iteratedFDeriv ℝ n (⇑A.field) (x + a)) v

Evaluating a parameter derivative gives the ordinary spatial derivative at the translated point.

theorem EulerMeanCoefficients.BoundedSmoothField.norm_iteratedFDeriv_translation_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : BoundedSmoothField V) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑A.field) x‖ ≤ C) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (translated A.field) a‖ ≤ C

Passing from pointwise spatial bounds to parameter derivatives in sup norm costs no constant.

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instBoundedCoefficientJets1 : NormedAddCommGroup Field

Cache the standard NormedAddCommGroup Field instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instBoundedCoefficientJets1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instBoundedCoefficientJets2 : NormedSpace ℝ Field

Cache the standard NormedSpace ℝ Field instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instBoundedCoefficientJets2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instBoundedCoefficientJets3 : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (EulerMeanSolenoidal.L2 →L[ℝ] EulerMeanSolenoidal.L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instBoundedCoefficientJets3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instBoundedCoefficientJets4 : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ (EulerMeanSolenoidal.L2 →L[ℝ] EulerMeanSolenoidal.L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instBoundedCoefficientJets4 = inferInstance

theorem EulerMeanCoefficients.multiplierMap_norm_le_one : ‖multiplierMap‖ ≤ 1

theorem EulerMeanCoefficients.multiplierTranslation_contDiff (A : BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => multiplier (translated A.field a)

theorem EulerMeanCoefficients.norm_iteratedFDeriv_multiplierTranslation_le (A : BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑A.field) x‖ ≤ C) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => multiplier (translated A.field b)) a‖ ≤ C