Removing the literal leading coefficient before bounding the packet remainder.
noncomputable def
EulerPacketCylinderField.Field.evaluateRemainder
{P T : ℝ}
[Fact (0 < P)]
(M : ℕ)
(hM : 1 ≤ M)
(κ : ℝ)
(f : ℕ → EulerPacketProfileRecursion.VectorField)
(G : (i : ℕ) → Field P T (f i))
:
Field P T (EulerPacketPointJets.fieldSum M κ f - κ • f 1)
Evaluate remainder as an element of Field P T (fieldSum M κ f-κ • f 1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCylinderField.Field.wordBound_evaluateRemainder
{P T : ℝ}
[Fact (0 < P)]
(N : ℕ)
(hN : 1 ≤ N)
(κ B C₂ : ℝ)
(hκ : 0 ≤ κ)
(hB : 0 ≤ B)
(hsmall : κ * B ≤ 1 / 2)
(f : ℕ → EulerPacketProfileRecursion.VectorField)
(G : (i : ℕ) → Field P T (f i))
(q : ℕ)
(R : ℝ)
(hR : 0 ≤ R)
(hzero : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), f 0 (↑t, x, θ) = 0)
(htwo : (G 2).WordBound q R C₂ 0)
(htail : ∀ (n : ℕ), 3 ≤ n → n ≤ N + 1 → (G n).WordBound q R (B ^ (n + 1)) 0)
: