Spatial orbit estimates for the actual physical mean fields

Frame multiplication preserves genuine translation regularity and factorial bounds. These identities apply to the physical velocity, its actual time derivative, and the pressure residual constructed by the strong mean solve.

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation3 : NormedAddCommGroup (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation4 : NormedSpace ℝ (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation5 : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation6 : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation6 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation7 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation8 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation8 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation9 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation9 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPhysicalTranslation.instMeanPhysicalTranslation10 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPhysicalTranslation.instMeanPhysicalTranslation10 T = inferInstance

theorem EulerMeanPhysicalTranslation.frameApply_orbit_eq (T : ℝ) (hT : 0 ≤ T) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) ((EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T F)) v)) = fun (a : EulerSmoothLimit.Space) => (EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F))) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v)

The actual spatial orbit of a frame product.

theorem EulerMeanPhysicalTranslation.frameApply_translation_contDiff (T : ℝ) (hT : 0 ≤ T) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) {n : WithTop ℕ∞} (hF : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hv : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) ((EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T F)) v)

Genuine spatial regularity survives multiplication by the actual frame.

theorem EulerMeanPhysicalTranslation.frameApply_translation_gevrey (T : ℝ) (hT : 0 ≤ T) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v) (R CF Cv : ℝ) (hR : 0 ≤ R) (hCF : 0 ≤ CF) (hCv : 0 ≤ Cv) (d : ℕ) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant R 0 n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) v) a‖ ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) ((EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T F)) v)) a‖ ≤ 3 * CF * Cv * EulerGevrey.majorant R d n

Frame multiplication has one fixed factorial amplitude, independent of order.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityDerivative_orbit_eq {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) : (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityDerivative) = fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) ((EulerTimeLp.timeMultiplier T hT (solenoidalFrame T F₁)) s.velocityLp) + (EulerMeanTimeTranslation.timeTranslation T a) ((EulerTimeLp.timeMultiplier T hT (solenoidalFrame T F)) s.acceleration)

theorem EulerMeanVariationalInverse.StrongMeanEvolution.pressureResidual_orbit_eq {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) : (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.pressureResidual) = fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f - (EulerMeanTimeTranslation.timeTranslation T a) ((EulerTimeLp.timeMultiplier T hT (solenoidalFrame T F)) s.acceleration) - 2 • (EulerMeanTimeTranslation.timeTranslation T a) ((EulerTimeLp.timeMultiplier T hT (solenoidalFrame T F₁)) s.velocityLp)

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityField_translation_contDiff {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) {n : WithTop ℕ∞} (hF : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hv : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityField

The physical velocity has the genuine spatial regularity of the coordinate velocity.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityDerivative_translation_contDiff {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) {n : WithTop ℕ∞} (hF : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp) (ha : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.velocityDerivative

This is spatial regularity of the actual time derivative B_t.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.pressureResidual_translation_contDiff {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) {n : WithTop ℕ∞} (hF : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp) (ha : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration) (hf : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) s.pressureResidual

The actual gradient residual inherits the spatial regularity of the solved fields.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityField_translation_gevrey {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) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp) (R CF Cv : ℝ) (hR : 0 ≤ R) (hCF : 0 ≤ CF) (hCv : 0 ≤ Cv) (d : ℕ) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant R 0 n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp) a‖ ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) s.velocityField) a‖ ≤ 3 * CF * Cv * EulerGevrey.majorant R d n

A genuine all-order bound for the physical mean velocity.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityDerivative_translation_gevrey {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) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp) (ha : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration) (R CF CF₁ Cv Ca : ℝ) (hR : 0 ≤ R) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCv : 0 ≤ Cv) (hCa : 0 ≤ Ca) (d : ℕ) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant R 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant R 0 n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp) a‖ ≤ Cv * EulerGevrey.majorant R d n) (hab : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.acceleration) a‖ ≤ Ca * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) s.velocityDerivative) a‖ ≤ 3 * (CF₁ * Cv + CF * Ca) * EulerGevrey.majorant R d n

The actual B_t has a fixed polynomial factorial amplitude.