The actual field estimates needed to close the recursive packet construction.
structure
EulerPacketCylinderField.ProfileBudget
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{support : Set EulerSmoothLimit.Space}
{a : EulerPacketProfileRecursion.Profile}
(G : ProfileRegularity P T hT support a)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(p : ℕ)
:
Profile budget data, collecting high, highDerivative, mean, meanDerivative,
corrector, correctorDerivative and their compatibility conditions.
- high : (G.high.normalized hT (S.high p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift p)
- highDerivative : (G.highDerivative.normalized hT (S.high p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift p)
- mean : (G.mean.normalized hT (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)
- meanDerivative : (G.meanDerivative.normalized hT (S.mean p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift p)
- corrector : (G.corrector.normalized hT (S.high p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift p)
- correctorDerivative : (G.correctorDerivative.normalized hT (S.high p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift p)
- pressure : (G.pressure.normalized hT (S.high p) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift p)
Instances For
theorem
EulerPacketCylinderField.Field.normalized_wordBound_congr
{P T : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(A : Field P T raw)
(hT : 0 ≤ T)
(g k : C(↑(Set.Icc 0 T), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t)
(hk : ∀ (t : ↑(Set.Icc 0 T)), 0 < k t)
(he : g = k)
(q d : ℕ)
(R C : ℝ)
(hb : (A.normalized hT k hk).WordBound q R C d)
:
(A.normalized hT g hg).WordBound q R C d
theorem
EulerPacketCylinderField.ProfileBudget.prefixBound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{support : Set EulerSmoothLimit.Space}
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(G : (i : ℕ) → i < p → ProfileRegularity P T hT support (a i))
(hG : ∀ (i : ℕ) (hi : i < p), ProfileBudget (G i hi) S R i)
:
PrefixBound (ProfileRegularity.prefixFields G) hT S R
theorem
EulerPacketCylinderField.ProfileBudget.transfer
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{support : Set EulerSmoothLimit.Space}
{a : EulerPacketProfileRecursion.Profile}
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
{p : ℕ}
{support' : Set EulerSmoothLimit.Space}
(hTpos : 0 < T)
{G : ProfileRegularity P T hT support a}
(hG : ProfileBudget G S R p)
(H : ProfileRegularity P T hT support' a)
:
ProfileBudget H S R p