Source bounds for the actual transverse history and its terminal trace #
The only quantitative inputs are the literal source coefficient jets and the forcing's fixed-Sobolev mixed-word bounds. The output is the constructed history path and its actual terminal coordinate, at the identical radius.
Actual physical history fields at the same external radius #
The frame products below act on the constructed cylinder coordinate paths. They retain the fixed spatial/angular Sobolev block and use the true continuous time derivative, including both endpoints.
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds1
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
:
Cache the standard NormedAddCommGroup (CylinderL2 P U) instance to shorten typeclass
synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds2
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
:
Cache the standard NormedSpace ℝ (CylinderL2 P U) instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds3
(P : ℝ)
[Fact (0 < P)]
{E : Type u_2}
[NormedAddCommGroup E]
:
Cache the standard NormedAddCommGroup (CylinderL2 P E) instance to shorten typeclass
synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds4
(P : ℝ)
[Fact (0 < P)]
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedSpace ℝ (CylinderL2 P E) instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds5
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedAddCommGroup (CylinderL2 P U →L[ℝ] CylinderL2 P E) instance to
shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds6
(P : ℝ)
[Fact (0 < P)]
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedSpace ℝ (CylinderL2 P U →L[ℝ] CylinderL2 P E) instance to shorten
typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds7
(P : ℝ)
[Fact (0 < P)]
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedAddCommGroup (CylinderL2 P E →L[ℝ] CylinderL2 P E) instance to
shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds8
(P : ℝ)
[Fact (0 < P)]
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedSpace ℝ (CylinderL2 P E →L[ℝ] CylinderL2 P E) instance to shorten
typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds9
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,CylinderL2 P U →L[ℝ] CylinderL2 P E)
instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds10
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
NormedSpace ℝ
C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))
Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,CylinderL2 P U →L[ℝ] CylinderL2 P E)
instance to shorten typeclass synthesis.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds11
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,CylinderL2 P E →L[ℝ] CylinderL2 P E)
instance to shorten typeclass synthesis.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCylinderDirichlet.Coefficients.instCylinderDirichletPhysicalBounds12
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
:
NormedSpace ℝ
C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))
Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,CylinderL2 P E →L[ℝ] CylinderL2 P E)
instance to shorten typeclass synthesis.
Equations
Instances For
theorem
EulerCylinderDirichlet.Coefficients.physicalVelocity_block_bound
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
{ι : Type u_3}
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbQ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbQ₁ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH D.lower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hT1 : T ≤ 1)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f)
(d : ℕ)
(hfb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ Cf * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (physicalVelocity P D f))
n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₀ * EulerFixedEvolutionSobolev.traceCost T * EulerGevrey.majorant R (d + 2) n
The physical history velocity A=Q ξ_t, as a true cylinder path.
theorem
EulerCylinderDirichlet.Coefficients.physicalDerivative_block_bound
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
{ι : Type u_3}
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(hQ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q))
(hQ₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.Q₁))
(hH : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.H))
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbQ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q) a‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbQ₁ :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.Q₁) a‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH D.lower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hT1 : T ≤ 1)
(hRuniform :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.lower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf
(EulerFixedEvolutionSobolev.traceCost T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f)
(d : ℕ)
(hfb :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ Cf * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (physicalDerivative P D f))
n 0 ≤ (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₁ * EulerFixedEvolutionSobolev.traceCost T + 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₀) * EulerGevrey.majorant R (d + 3) n
The actual derivative A_t=Q_t ξ_t+Q ξ_tt, with no loss of spatial radius.
theorem
EulerTransversePacketProvider.Data.frame_spatial_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : Data U)
(n : ℕ)
(C : ℝ)
(hb : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerTransversePacketProvider.Data.frameDerivative_spatial_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : Data U)
(n : ℕ)
(C : ℝ)
(hb : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
:
theorem
EulerLpCylinderTranslation.trace_block_le
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
{V : Type u_2}
{ι : Type u_3}
[TopologicalSpace K]
[CompactSpace K]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(q : ℕ)
(p : C(K, ↥(CylinderL2 P V)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P a) p)
(t : K)
(n : ℕ)
(a : EulerLiftedGradientSpace.LiftTangent)
:
EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (translate P b) (p t)) n
a ≤ EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate P b) p)
n a
theorem
EulerTransversePacketProvider.HistoryData.source_coordinate_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
{ι : Type u_2}
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbF :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbF₁ :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(B.H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q D.T Rc C₀ C₁ CH D.frameLower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.frameLower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hT1 : D.T ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (forcingPath G))
n 0 ≤ Cf * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (B.coordinatePath G))
n 0 ≤ EulerFixedEvolutionSobolev.traceCost D.T * EulerGevrey.majorant R (d + 2) n
True continuous coordinate velocity of the actual zero-endpoint solve.
theorem
EulerTransversePacketProvider.HistoryData.source_terminal_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
{ι : Type u_2}
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbF :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbF₁ :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(B.H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q D.T Rc C₀ C₁ CH D.frameLower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.frameLower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hT1 : D.T ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (forcingPath G))
n 0 ≤ Cf * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.translate P a) ↑(B.terminalInitial G).value)
n 0 ≤ EulerFixedEvolutionSobolev.traceCost D.T * EulerGevrey.majorant R (d + 2) n
The actual terminal trace used by the forward solve has the same bound.
theorem
EulerTransversePacketProvider.HistoryData.source_velocity_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
{ι : Type u_2}
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbF :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbF₁ :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(B.H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q D.T Rc C₀ C₁ CH D.frameLower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.frameLower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hT1 : D.T ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (forcingPath G))
n 0 ≤ Cf * EulerGevrey.majorant R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (B.velocityPath G))
n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₀ * EulerFixedEvolutionSobolev.traceCost D.T * EulerGevrey.majorant R (d + 2) n
Literal history velocity, with the fixed reference-plane contraction already discharged.
theorem
EulerTransversePacketProvider.HistoryData.source_derivative_bound
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : Data U}
(B : HistoryData D)
{raw : EulerPacketProfileRecursion.VectorField}
(G : Forcing P D raw)
{ι : Type u_2}
[Fintype ι]
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(Rc C₀ C₁ CH Cf R : ℝ)
(hRc : 0 ≤ Rc)
(hC₀ : 0 ≤ C₀)
(hC₁ : 0 ≤ C₁)
(hCH : 0 ≤ CH)
(hCf : 0 ≤ Cf)
(hbF :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n)
(hbF₁ :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n)
(hbH :
∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (⇑(B.H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n)
(hRweak :
2 * EulerTransverseFixedSobolev.blockCost ι q D.T Rc C₀ C₁ CH D.frameLower Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hRstrong :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.frameLower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(hT1 : D.T ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (forcingPath G))
n 0 ≤ Cf * EulerGevrey.majorant R d n)
(hRuniform :
2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.frameLower Rc C₀
(EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf
(EulerFixedEvolutionSobolev.traceCost D.T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a) (B.derivativePath G))
n 0 ≤ (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₁ * EulerFixedEvolutionSobolev.traceCost D.T + 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C₀) * EulerGevrey.majorant R (d + 3) n
The genuine history time derivative, at the identical spatial radius.