Exact identification of the packet's ordered-word blocks with the genuine Sobolev blocks used in the correction energy.
theorem
EulerPacketCylinderField.Field.toFieldTower_derivative
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(s : ℕ)
(i : Fin 4)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderSobolevSpace.derivativeOperator P s i) ((G.toFieldTower.realization (s + 1)) t) = ((G.derivative i).toFieldTower.realization s) t
theorem
EulerPacketCylinderField.Field.toFieldTower_derivative_path
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(s : ℕ)
(i : Fin 4)
:
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.derivativeOperator P s i))
(G.toFieldTower.realization (s + 1)) = (G.derivative i).toFieldTower.realization s
theorem
EulerPacketCylinderField.Field.toFieldTower_levelNorm_eq
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(s n : ℕ)
(hn : n ≤ s)
(t : ↑(Set.Icc 0 T))
:
EulerJetProductBounds.levelNorm P (EulerCylinderSobolevSpace.toJet P ((G.toFieldTower.realization s) t)) n = EulerParameterWordGevrey.wordSum EulerCylinderSobolev.standardDirection
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) (G.path t)) n 0
theorem
EulerPacketCylinderField.Field.toFieldTower_blockNorm_eq
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(s q n : ℕ)
(hn : n + q ≤ s)
(t : ↑(Set.Icc 0 T))
:
EulerH6Pressure.blockNorm P (EulerCylinderSobolevSpace.toJet P ((G.toFieldTower.realization s) t)) q n = EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) (G.path t)) n 0
theorem
EulerPacketCylinderField.Field.toFieldTower_blockNorm_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(s q n : ℕ)
(hn : n + q ≤ s)
(t : ↑(Set.Icc 0 T))
:
EulerH6Pressure.blockNorm P (EulerCylinderSobolevSpace.toJet P ((G.toFieldTower.realization s) t)) q n ≤ EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) G.path) n 0
Time evaluation is contractive for the full ordered-word block.
theorem
EulerPacketCylinderField.Field.toFieldTower_derivative_block_sum_le
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : Field P T raw)
(s q n : ℕ)
(hn : n + q ≤ s)
(t : ↑(Set.Icc 0 T))
:
∑ i : Fin 4,
EulerH6Pressure.blockNorm P
(EulerCylinderSobolevSpace.toJet P
((EulerCylinderSobolevSpace.derivativeOperator P s i) ((G.toFieldTower.realization (s + 1)) t)))
q n ≤ EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) G.path) (n + 1) 0
Summing the four genuine coordinate derivatives spends exactly one external word; there is no additional dimension factor.