Quantitative jets of the actual diagonal sum

Local finiteness identifies derivatives of the actual tsum with finite sums of actual iteratedFDerivs. Pointwise stage estimates then give quantitative tail estimates. The stage estimates themselves are explicit hypotheses, not conclusions of the numerical cutoff selection. The prefix must depend on the requested derivative order and decay power; no fixed tail is declared flat.

theorem NavierStokes.DiagonalJetBounds.eventually_zero_tail_of_locallyFinite {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] {F : ℕ → E → V} (hF : LocallyFinite fun (j : ℕ) => Function.support (F j)) (x : E) : ∃ (K : ℕ), ∀ᶠ (y : E) in nhds x, ∀ (j : ℕ), K ≤ j → F j y = 0

A common neighborhood kills all sufficiently late terms. This follows from local finiteness of the supports; pointwise finiteness alone is weaker.

theorem NavierStokes.DiagonalJetBounds.tsum_jet_identity {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {F : ℕ → E → V} {x : E} (hloc : ∃ (K : ℕ), ∀ᶠ (y : E) in nhds x, ∀ (j : ℕ), K ≤ j → F j y = 0) (hF : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (F j) x) : ContDiffAt ℝ (↑⊤) (fun (y : E) => ∑' (j : ℕ), F j y) x ∧ ∀ (m : ℕ), (Summable fun (j : ℕ) => iteratedFDeriv ℝ m (F j) x) ∧ iteratedFDeriv ℝ m (fun (y : E) => ∑' (j : ℕ), F j y) x = ∑' (j : ℕ), iteratedFDeriv ℝ m (F j) x

A common zero tail gives smoothness of the actual sum and termwise derivative identities. Summability here is proved by finite support.

theorem NavierStokes.DiagonalJetBounds.tsum_sub_prefix_jet {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {F : ℕ → E → V} {x : E} (hloc : ∃ (K : ℕ), ∀ᶠ (y : E) in nhds x, ∀ (j : ℕ), K ≤ j → F j y = 0) (hF : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (F j) x) (J m : ℕ) : (Summable fun (n : ℕ) => iteratedFDeriv ℝ m (F (J + 1 + n)) x) ∧ iteratedFDeriv ℝ m (fun (y : E) => ∑' (j : ℕ), F j y - ∑ j ∈ Finset.range (J + 1), F j y) x = ∑' (n : ℕ), iteratedFDeriv ℝ m (F (J + 1 + n)) x

The jet of the actual sum minus a finite prefix is the sum of the actual tail jets. The sum on the right is genuinely summable.

theorem NavierStokes.DiagonalJetBounds.scalar_tail_bound (g : ℕ → ℝ) (hg : Monotone g) (L q : ℝ) (hq : 0 < q) (hq1 : q ≤ 1) (J : ℕ) : (Summable fun (n : ℕ) => (1 / 2) ^ (J + 1 + n) * q ^ (g (J + 1 + n) - L)) ∧ ∑' (n : ℕ), (1 / 2) ^ (J + 1 + n) * q ^ (g (J + 1 + n) - L) ≤ (1 / 2) ^ J * q ^ (g (J + 1) - L)

The scalar estimate from DiagonalScale, with the gain already denoting the exponent retained after absorption of logarithmic factors.

theorem NavierStokes.DiagonalJetBounds.exists_prefix_gain (g L : ℕ → ℝ) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (M Jmin : ℕ) (N : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ M ≤ J ∧ ∀ m ≤ M, N ≤ g (J + 1) - L m

One prefix can accommodate every derivative in a prescribed finite jet. No monotonicity assumption is needed on the loss function.

theorem NavierStokes.DiagonalJetBounds.norm_tsum_sub_prefix_jet_le {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {F : ℕ → E → V} {x : E} (hloc : ∃ (K : ℕ), ∀ᶠ (y : E) in nhds x, ∀ (j : ℕ), K ≤ j → F j y = 0) (hF : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (F j) x) (g : ℕ → ℝ) (hg : Monotone g) (L q : ℝ) (hq : 0 < q) (hq1 : q ≤ 1) (J m : ℕ) (hbound : ∀ (j : ℕ), J < j → ‖iteratedFDeriv ℝ m (F j) x‖ ≤ (1 / 2) ^ j * q ^ (g j - L)) : ‖iteratedFDeriv ℝ m (fun (y : E) => ∑' (j : ℕ), F j y - ∑ j ∈ Finset.range (J + 1), F j y) x‖ ≤ (1 / 2) ^ J * q ^ (g (J + 1) - L)

A bound for actual stage derivatives transfers to the actual remainder. The conclusion includes the exact geometric tail coefficient.

theorem NavierStokes.DiagonalJetBounds.norm_tsum_sub_prefix_jet_le_of_locallyFinite {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {F : ℕ → E → V} {x : E} (hloc : LocallyFinite fun (j : ℕ) => Function.support (F j)) (hF : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (F j) x) (g : ℕ → ℝ) (hg : Monotone g) (L q : ℝ) (hq : 0 < q) (hq1 : q ≤ 1) (J m : ℕ) (hbound : ∀ (j : ℕ), J < j → ‖iteratedFDeriv ℝ m (F j) x‖ ≤ (1 / 2) ^ j * q ^ (g j - L)) : ‖iteratedFDeriv ℝ m (fun (y : E) => ∑' (j : ℕ), F j y - ∑ j ∈ Finset.range (J + 1), F j y) x‖ ≤ (1 / 2) ^ J * q ^ (g (J + 1) - L)

Direct version for any smooth family with locally finite supports.

def NavierStokes.DiagonalJetBounds.CutStageBounds {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℝ) (q : E → ℝ) (A : ℕ → E → V) (g L : ℕ → ℝ) (U : Set E) : Prop

The stage estimates needed by the diagonal argument, stated on actual cut potentials and their actual derivatives. Stage zero is exempt; stage j controls the finite list of derivatives through j+2.

Equations

• One or more equations did not get rendered due to their size.

theorem NavierStokes.DiagonalJetBounds.potential_tail_jet_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : E → ℝ} {A : ℕ → E → V} {g L : ℕ → ℝ} {U : Set E} (hU : IsOpen U) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hg : Monotone g) (hb : CutStageBounds a q A g L U) {x : E} (hx : x ∈ U) (hqx : 0 < q x) (hqx1 : q x ≤ 1) (J m : ℕ) (hm : m ≤ J + 3) : ‖iteratedFDeriv ℝ m (fun (y : E) => SolenoidalDiagonal.potentialSum a q A y - SolenoidalDiagonal.partialPotential a q A (J + 1) y) x‖ ≤ (1 / 2) ^ J * q x ^ (g (J + 1) - L m)

The quantitative bound for the concrete cutoff-potential tsum already constructed in SolenoidalDiagonal.

theorem NavierStokes.DiagonalJetBounds.exists_potential_tail_order {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : E → ℝ} {A : ℕ → E → V} {g L : ℕ → ℝ} {U : Set E} (hU : IsOpen U) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hg : Monotone g) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (hb : CutStageBounds a q A g L U) (M Jmin : ℕ) (N : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ M ≤ J ∧ ∀ m ≤ M, ∀ x ∈ U, 0 < q x → q x ≤ 1 → ‖iteratedFDeriv ℝ m (fun (y : E) => SolenoidalDiagonal.potentialSum a q A y - SolenoidalDiagonal.partialPotential a q A (J + 1) y) x‖ ≤ (1 / 2) ^ J * q x ^ N

Given a finite derivative ceiling and a target power, choose one prefix uniformly for every point in the positive unit-scale domain.

def NavierStokes.DiagonalJetBounds.uncutPrefix {E : Type u_1} {V : Type u_2} [NormedAddCommGroup V] (A : ℕ → E → V) (N : ℕ) (x : E) : V

The original finite stage, before multiplying its potentials by cutoffs.

Equations

• NavierStokes.DiagonalJetBounds.uncutPrefix A N x = ∑ j ∈ Finset.range N, A j x

theorem NavierStokes.DiagonalJetBounds.partialPotential_eventuallyEq_uncut {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℝ) (q : E → ℝ) (A : ℕ → E → V) (N : ℕ) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (x : E), ContinuousAt q x → |q x| < δ → SolenoidalDiagonal.partialPotential a q A N =ᶠ[nhds x] uncutPrefix A N

A single small-scale neighborhood makes the whole finite prefix equal to the original prefix locally in the spatial variables. Consequently every derivative order, not just the values at the point, agrees.

theorem NavierStokes.DiagonalJetBounds.exists_uncut_tail_order {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : E → ℝ} {A : ℕ → E → V} {g L : ℕ → ℝ} {U : Set E} (hU : IsOpen U) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hg : Monotone g) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (hb : CutStageBounds a q A g L U) (M Jmin : ℕ) (N : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ M ≤ J ∧ ∃ (δ : ℝ), 0 < δ ∧ ∀ m ≤ M, ∀ x ∈ U, 0 < q x → q x < δ → ‖iteratedFDeriv ℝ m (fun (y : E) => SolenoidalDiagonal.potentialSum a q A y - uncutPrefix A (J + 1) y) x‖ ≤ (1 / 2) ^ J * q x ^ N

The actual cut-sum remainder can be compared to the original uncut finite stage for small q, with an arbitrary prescribed finite jet and power.

theorem NavierStokes.DiagonalJetBounds.exists_uncut_tail_order_eventually {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : E → ℝ} {A : ℕ → E → V} {g L : ℕ → ℝ} {U : Set E} (hU : IsOpen U) (hq : ContDiffOn ℝ (↑⊤) q U) (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U) (hg : Monotone g) (hgtop : Filter.Tendsto g Filter.atTop Filter.atTop) (hb : CutStageBounds a q A g L U) {l : Filter E} (hlU : ∀ᶠ (x : E) in l, x ∈ U) (hlq : ∀ᶠ (x : E) in l, 0 < q x) (hqzero : Filter.Tendsto q l (nhds 0)) (M Jmin : ℕ) (N : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ M ≤ J ∧ ∀ᶠ (x : E) in l, ∀ m ≤ M, ‖iteratedFDeriv ℝ m (fun (y : E) => SolenoidalDiagonal.potentialSum a q A y - uncutPrefix A (J + 1) y) x‖ ≤ (1 / 2) ^ J * q x ^ N

Filter version of the small-scale comparison. The prefix depends on the finite derivative ceiling and target power, never on the point.