The actual small drift budget from the packet's spatial and normal word bounds, with the same radius and no full-velocity substitution.
The actual four-component transport vector retains the small normal component separately from its three scaled spatial components.
Spatial velocity map, given by velocityMap (Fin.cons 0 (fun i : Fin 3 => coordinate 3 i)).
Equations
Instances For
Normal velocity map, given by (toSpanSingleton ℝ (EuclideanSpace.single (0 : Fin 4) (1 : ℝ))).comp scalarProject.
Equations
Instances For
theorem
EulerLiftedVelocitySplit.velocityMap_L2_bound
(P : ℝ)
[Fact (0 < P)]
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(u : ↥(EulerLiftedGradientSpace.LiftL2 P))
:
‖(ContinuousLinearMap.compLpL 2 (EulerLiftedGradientSpace.liftMeasure P)
(EulerFunctionalVelocity.velocityMap (EulerSobolevTransport.velocityComponents κ m)))
u‖ ≤ 3 * |κ| * ‖u‖ + ‖(ContinuousLinearMap.compLpL 2 (EulerLiftedGradientSpace.liftMeasure P)
(EulerPacketCylinderField.normalComponentMap m))
u‖
Exact bounded-map naturality of every genuine Sobolev coordinate of an actual packet field.
theorem
EulerPacketCylinderField.Field.toFieldTower_word_eq
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(s n : ℕ)
(hn : n ≤ s)
(w : Fin n → Fin 4)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderSobolevSpace.toJet P ((G.toFieldTower.realization s) t)).word w = EulerParameterWordGevrey.wordDerivative EulerCylinderSobolev.standardDirection
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) (G.path t)) w 0
theorem
EulerPacketCylinderField.Field.toFieldTower_word_map
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(s n : ℕ)
(hn : n ≤ s)
(w : Fin n → Fin 4)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderSobolevSpace.toJet P (((G.map L).toFieldTower.realization s) t)).word w = (ContinuousLinearMap.compLpL 2 (EulerLiftedGradientSpace.liftMeasure P) L)
((EulerCylinderSobolevSpace.toJet P ((G.toFieldTower.realization s) t)).word w)
theorem
EulerPacketCylinderField.Field.toFieldTower_driftLevel_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(s n : ℕ)
(hn : n ≤ s)
(t : ↑(Set.Icc 0 T))
:
EulerSobolevDriftNorm.driftLevelNorm P n
(EulerFunctionalVelocity.velocityMap (EulerSobolevTransport.velocityComponents κ m))
((G.toFieldTower.realization s) t) ≤ 3 * |κ| * EulerJetProductBounds.levelNorm P (EulerCylinderSobolevSpace.toJet P ((G.toFieldTower.realization s) t)) n + EulerJetProductBounds.levelNorm P
(EulerCylinderSobolevSpace.toJet P (((G.map (normalComponentMap m)).toFieldTower.realization s) t)) n
theorem
EulerPacketCylinderField.Field.toFieldTower_driftBlock_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(s q n : ℕ)
(hn : n + q ≤ s)
(t : ↑(Set.Icc 0 T))
:
EulerSobolevDriftNorm.driftBlockNorm P q n
(EulerFunctionalVelocity.velocityMap (EulerSobolevTransport.velocityComponents κ m))
((G.toFieldTower.realization s) t) ≤ 3 * |κ| * EulerH6Pressure.blockNorm P (EulerCylinderSobolevSpace.toJet P ((G.toFieldTower.realization s) t)) q n + EulerH6Pressure.blockNorm P
(EulerCylinderSobolevSpace.toJet P (((G.map (normalComponentMap m)).toFieldTower.realization s) t)) q n
theorem
EulerPacketCylinderField.Field.toFieldTower_weightedDrift_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(s q N : ℕ)
(hN : N + q ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(t : ↑(Set.Icc 0 T))
:
EulerSobolevDriftNorm.weightedDriftNorm P q N ρ
(EulerFunctionalVelocity.velocityMap (EulerSobolevTransport.velocityComponents κ m))
((G.toFieldTower.realization s) t) ≤ 3 * |κ| * EulerSobolevGevreyOperators.weightedNorm P q N ρ ((G.toFieldTower.realization s) t) + EulerSobolevGevreyOperators.weightedNorm P q N ρ (((G.map (normalComponentMap m)).toFieldTower.realization s) t)
theorem
EulerPacketCylinderField.Field.WordBound.toFieldTower_weightedDrift_le_two
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{q : ℕ}
{R A₀ A₁ : ℝ}
(hG : G.WordBound q R A₀ 0)
(κ : ℝ)
(m : EulerSmoothLimit.Space)
(hNrm : (G.map (normalComponentMap m)).WordBound q R A₁ 0)
(hR : 0 ≤ R)
(hA₀ : 0 ≤ A₀)
(hA₁ : 0 ≤ A₁)
(s N : ℕ)
(hN : N + q ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(hsmall : ρ * R ≤ 1 / 2)
(t : ↑(Set.Icc 0 T))
:
EulerSobolevDriftNorm.weightedDriftNorm P q N ρ
(EulerFunctionalVelocity.velocityMap (EulerSobolevTransport.velocityComponents κ m))
((G.toFieldTower.realization s) t) ≤ 2 * (3 * |κ| * A₀ + A₁)
Separate word estimates for the full normalized vector and its actual normal component give exactly the small transport budget needed by the drift-preserving correction theorem.