Uniform-time spatial calculus for the actual physical mean derivative

Multiplication by the actual mean frame commutes with spatial translation. The continuous physical derivative is the sum of the two actual frame products, so its smoothness and bounds follow without a new regularity assumption on the solution.

@[instance_reducible]

noncomputable def EulerMeanContinuousPhysical.instMeanContinuousPhysical1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousPhysical.instMeanContinuousPhysical1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousPhysical.instMeanContinuousPhysical2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

Equations

• EulerMeanContinuousPhysical.instMeanContinuousPhysical2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanContinuousPhysical.instMeanContinuousPhysical3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanContinuousPhysical.instMeanContinuousPhysical4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousPhysical.instMeanContinuousPhysical5 (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

• EulerMeanContinuousPhysical.instMeanContinuousPhysical5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousPhysical.instMeanContinuousPhysical6 (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

• EulerMeanContinuousPhysical.instMeanContinuousPhysical6 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousPhysical.instMeanContinuousPhysical7 (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

• EulerMeanContinuousPhysical.instMeanContinuousPhysical7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousPhysical.instMeanContinuousPhysical8 (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

• EulerMeanContinuousPhysical.instMeanContinuousPhysical8 T = inferInstance

theorem EulerMeanContinuousPhysical.framePathApply_orbit_eq (T : ℝ) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (v : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)) : (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) ((EulerContinuousTimeIntegral.multiplier (EulerMeanVariationalInverse.solenoidalFrame T F)) v)) = fun (a : EulerSmoothLimit.Space) => (EulerContinuousTimeIntegral.multiplier (EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanOperatorTranslation.translatePath T a F))) ((EulerMeanCoordinatePath.coordinatePathTranslation T a) v)

The actual continuous frame product has the exact translated product orbit.

theorem EulerMeanContinuousPhysical.framePathApply_translation_contDiff (T : ℝ) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (v : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)) {n : WithTop ℕ∞} (hF : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hv : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) v) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) ((EulerContinuousTimeIntegral.multiplier (EulerMeanVariationalInverse.solenoidalFrame T F)) v)

theorem EulerMeanContinuousPhysical.framePathApply_translation_gevrey (T : ℝ) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (v : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation 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) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) v) a‖ ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) ((EulerContinuousTimeIntegral.multiplier (EulerMeanVariationalInverse.solenoidalFrame T F)) v)) a‖ ≤ 3 * CF * Cv * EulerGevrey.majorant R d n

theorem EulerMeanVariationalInverse.StrongMeanEvolution.classicalPhysicalDerivative_eq_products {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) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) : s.classicalPhysicalDerivative c hc hLower fC = (EulerContinuousTimeIntegral.multiplier (solenoidalFrame T F₁)) s.coordinateVelocityPath + (EulerContinuousTimeIntegral.multiplier (solenoidalFrame T F)) (s.classicalAcceleration c hc hLower fC)

The original continuous physical derivative is exactly its two frame products.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.classicalAcceleration_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) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) {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) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) s.coordinateVelocityPath) (hf : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) (s.classicalAcceleration c hc hLower fC)

The actual continuous coordinate acceleration has a smooth spatial orbit.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.classicalPhysicalDerivative_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) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) {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) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) s.coordinateVelocityPath) (hf : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) : ContDiff ℝ n fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.classicalPhysicalDerivative c hc hLower fC)

The actual continuous B_t has a smooth spatial orbit, derived from the constructed acceleration.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.classicalPhysicalDerivative_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) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (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) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) s.coordinateVelocityPath) (ha : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) (s.classicalAcceleration c hc hLower fC)) (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) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) s.coordinateVelocityPath) a‖ ≤ Cv * EulerGevrey.majorant R d n) (hab : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) (s.classicalAcceleration c hc hLower fC)) a‖ ≤ Ca * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) (s.classicalPhysicalDerivative c hc hLower fC)) a‖ ≤ 3 * (CF₁ * Cv + CF * Ca) * EulerGevrey.majorant R d n

Uniform-time derivative estimates pay only the two actual frame-product factors.