Descended derivative tensors of a coherent Sobolev field tower have their actual cylinder L² bounds. The estimate selects a summand of the weighted H6 norm and has no loss depending on the derivative order.
theorem
EulerAllOrderCorrectionData.FieldTower.pointField_word_ae
{P T : ℝ}
[Fact (0 < P)]
(A : FieldTower P T)
(s n : ℕ)
(hn : n ≤ s)
(w : Fin n → Fin 4)
(t : ↑(Set.Icc 0 T))
:
↑↑((EulerCylinderSobolevSpace.toJet P ((A.realization s) t)).word w) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t)
theorem
EulerAllOrderCorrectionData.FieldTower.pointField_word_memLp
{P T : ℝ}
[Fact (0 < P)]
(A : FieldTower P T)
(n : ℕ)
(w : Fin n → Fin 4)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerAllOrderCorrectionData.FieldTower.pointField_word_norm
{P T : ℝ}
[Fact (0 < P)]
(A : FieldTower P T)
(s n : ℕ)
(hn : n ≤ s)
(w : Fin n → Fin 4)
(t : ↑(Set.Icc 0 T))
:
(MeasureTheory.eLpNorm (EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t)) 2
(EulerLiftedGradientSpace.liftMeasure P)).toReal = ‖(EulerCylinderSobolevSpace.toJet P ((A.realization s) t)).word w‖
theorem
EulerAllOrderCorrectionData.FieldTower.coverTensor_memLp
{P T : ℝ}
[Fact (0 < P)]
(A : FieldTower P T)
(n : ℕ)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerAllOrderCorrectionData.FieldTower.coverTensor_norm_le_level
{P T : ℝ}
[Fact (0 < P)]
(A : FieldTower P T)
(s n : ℕ)
(hn : n ≤ s)
(t : ↑(Set.Icc 0 T))
:
theorem
EulerAllOrderCorrectionData.FieldTower.coverTensor_weighted
{P T : ℝ}
[Fact (0 < P)]
(A : FieldTower P T)
(n : ℕ)
(ρ C : ℝ)
(hρ : 0 < ρ)
(t : ↑(Set.Icc 0 T))
(hb : EulerSobolevGevreyOperators.weightedNorm P 6 n ρ ((A.realization (n + 6)) t) ≤ C)
:
(MeasureTheory.eLpNorm (EulerCylinderJetLp.tensor P (A.pointField t) n) 2
(EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * (‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * ρ⁻¹) ^ n * ↑n.factorial ^ 2
theorem
EulerAllOrderCorrectionData.FieldTower.toSmoothTimeField_jetSeries
{P T : ℝ}
[Fact (0 < P)]
(A : FieldTower P T)
(n : ℕ)
(t : ↑(Set.Icc 0 T))
:
(fun (q : EulerLiftedGradientSpace.LiftDomain P) =>
EulerCylinderCoverDescent.jetSeries P (⇑(A.toSmoothTimeField.field t)) q n) = EulerCylinderJetLp.tensor P (A.pointField t) n