Quantitative bounds on the actual masked fields used in the known forcing.
structure
EulerPacketCylinderField.PrefixBound
{P T : ℝ}
[Fact (0 < P)]
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(F : PrefixFields P T p a)
(hT : 0 ≤ T)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
:
Prefix bound data, collecting high, mean, corrector.
- high (i : ℕ) (hi : i < p) : 1 ≤ i → ((F.high i hi).normalized hT (S.high i) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift i)
- mean (i : ℕ) (hi : i < p) : 2 ≤ i → ((F.mean i hi).normalized hT (S.mean i) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.meanShift i)
- corrector (i : ℕ) (hi : i < p) : 1 ≤ i → ((F.corrector i hi).normalized hT (S.high i) ⋯).WordBound 6 R 1 (EulerPacketShiftArithmetic.highShift i)
Instances For
theorem
EulerPacketCylinderField.PrefixBound.piece
{P T : ℝ}
[Fact (0 < P)]
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{F : PrefixFields P T p a}
{hT : 0 ≤ T}
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(B : PrefixBound F hT S R)
(hR : 0 ≤ R)
(k : KnownPiece)
(i : ℕ)
:
((F.piece k i).normalized hT (k.profile S i) ⋯).WordBound 6 R 1 (k.shift i)
theorem
EulerPacketCylinderField.PrefixBound.pieceJet
{P T : ℝ}
[Fact (0 < P)]
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{F : PrefixFields P T p a}
{hT : 0 ≤ T}
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(B : PrefixBound F hT S R)
(hR : 0 ≤ R)
(O : EulerPacketProfileRecursion.Operators)
(k : KnownPiece)
(i : ℕ)
: