Genuine mean time traces and physical fields in fixed Sobolev word blocks

The fixed time reconstruction and actual frame products preserve the input radius. No conversion of forcing or solution tensors is used.

@[instance_reducible]

noncomputable def EulerMeanTimeSobolev.instMeanTimeSobolev1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanTimeSobolev.instMeanTimeSobolev1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTimeSobolev.instMeanTimeSobolev2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

Equations

• EulerMeanTimeSobolev.instMeanTimeSobolev2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanTimeSobolev.instMeanTimeSobolev3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanTimeSobolev.instMeanTimeSobolev4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTimeSobolev.instMeanTimeSobolev5 (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

• EulerMeanTimeSobolev.instMeanTimeSobolev5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTimeSobolev.instMeanTimeSobolev6 (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

• EulerMeanTimeSobolev.instMeanTimeSobolev6 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTimeSobolev.instMeanTimeSobolev7 (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

• EulerMeanTimeSobolev.instMeanTimeSobolev7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTimeSobolev.instMeanTimeSobolev8 (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

• EulerMeanTimeSobolev.instMeanTimeSobolev8 T = inferInstance

theorem EulerMeanTimeSobolev.framePathApply_translation_block_gevrey {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (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) (Rc R CF Cv : ℝ) (hRc : 0 ≤ Rc) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ 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 Rc 0 n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) v) n a ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) ((EulerContinuousTimeIntegral.multiplier (EulerMeanVariationalInverse.solenoidalFrame T F)) v)) n a ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF * Cv * EulerGevrey.majorant R d n

Multiplication by the genuine mean frame preserves the fixed base order and the external radius. Its coefficient cost is paid once.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.coordinateVelocityPath_translation_block_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) {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (q : ℕ) (hTpos : 0 < T) (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 Cv Ca : ℝ) (d : ℕ) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp) n a ≤ Cv * EulerGevrey.majorant R d n) (hab : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.acceleration) n a ≤ Ca * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) s.coordinateVelocityPath) n a ≤ (T⁻¹ * √T * Cv + 2 * √T * Ca) * EulerGevrey.majorant R d n

The actual H¹ coordinate trace preserves all external/base spatial words.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.continuousVelocity_eq_frame {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) (hTpos : 0 < T) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t) : s.continuousVelocity = (EulerContinuousTimeIntegral.multiplier (solenoidalFrame T F)) s.coordinateVelocityPath

The continuous physical velocity is the literal frame product at every time.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.classicalPhysicalDerivative_translation_block_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) {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (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)) (Rc R CF CF₁ Cv Ca : ℝ) (hRc : 0 ≤ Rc) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ 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 Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) s.coordinateVelocityPath) n a ≤ Cv * EulerGevrey.majorant R d n) (hab : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) (s.classicalAcceleration c hc hLower fC)) n a ≤ Ca * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) (s.classicalPhysicalDerivative c hc hLower fC)) n a ≤ 3 * (EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF₁ * Cv + EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF * Ca) * EulerGevrey.majorant R d n

The actual physical time derivative is bounded by its two real frame products, in exactly the same fixed Sobolev blocks.