Constructing the slow asymptotic base from smooth coefficient data

The cutoff-stage bounds are derived from compactness of actual derivatives on a normalized coordinate set. They are not assumptions on the output series.

@[reducible, inline]

abbrev NavierStokes.SlowBorelBase.Inner : Type

Inner: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.SlowBorelBase.Inner = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.SlowBorelBase.Chart : Type

Chart: an abbreviation for ℝ × Inner.

Equations

• NavierStokes.SlowBorelBase.Chart = (ℝ × NavierStokes.SlowBorelBase.Inner)

noncomputable def NavierStokes.SlowBorelBase.scaleMap (q : ℝ) : Chart →L[ℝ] Chart

Scale map, given by SpatialBorelExtension.timeScale q.

Equations

• NavierStokes.SlowBorelBase.scaleMap q = NavierStokes.SpatialBorelExtension.timeScale q

@[simp]

theorem NavierStokes.SlowBorelBase.scaleMap_apply (q : ℝ) (y : Chart) : (scaleMap q) y = (q * y.1, y.2)

noncomputable def NavierStokes.SlowBorelBase.localPower (b q : ℝ) : ℝ

Local power, given by SmoothCutoffs.cutoff (4 * (q - 1)) * q ^ b.

Equations

• NavierStokes.SlowBorelBase.localPower b q = NavierStokes.SmoothCutoffs.cutoff (4 * (q - 1)) * q ^ b

theorem NavierStokes.SlowBorelBase.localPower_smooth (b : ℝ) : ContDiff ℝ (↑⊤) (localPower b)

theorem NavierStokes.SlowBorelBase.localPower_eventually_eq (b : ℝ) : localPower b =ᶠ[nhds 1] fun (q : ℝ) => q ^ b

noncomputable def NavierStokes.SlowBorelBase.powerCoefficient {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : ℝ) (f : Inner → V) (y : Chart) : V

Power coefficient, given by y.1 ^ b • f y.2.

Equations

• NavierStokes.SlowBorelBase.powerCoefficient b f y = y.1 ^ b • f y.2

noncomputable def NavierStokes.SlowBorelBase.powerStage {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (c b : ℝ) (f : Inner → V) (y : Chart) : V

Power stage, given by SmoothCutoffs.scaledCutoff c y.1 • powerCoefficient b f y.

Equations

• NavierStokes.SlowBorelBase.powerStage c b f y = NavierStokes.SmoothCutoffs.scaledCutoff c y.1 • NavierStokes.SlowBorelBase.powerCoefficient b f y

noncomputable def NavierStokes.SlowBorelBase.template {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (c b : ℝ) (f : Inner → V) (y : Chart) : V

Template, given by SmoothCutoffs.cutoff (c * y.1) • (localPower b y.1 • f y.2).

Equations

• NavierStokes.SlowBorelBase.template c b f y = NavierStokes.SmoothCutoffs.cutoff (c * y.1) • NavierStokes.SlowBorelBase.localPower b y.1 • f y.2

noncomputable def NavierStokes.SlowBorelBase.jointTemplate {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (b : ℝ) (f : Inner → V) (z : ℝ × Chart) : V

Joint template, given by template z.1 b f z.2.

Equations

• NavierStokes.SlowBorelBase.jointTemplate b f z = NavierStokes.SlowBorelBase.template z.1 b f z.2

theorem NavierStokes.SlowBorelBase.powerCoefficient_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Inner → V} (hf : ContDiff ℝ (↑⊤) f) (b : ℝ) {y : Chart} (hy : 0 < y.1) : ContDiffAt ℝ (↑⊤) (powerCoefficient b f) y

theorem NavierStokes.SlowBorelBase.powerStage_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Inner → V} (hf : ContDiff ℝ (↑⊤) f) (c b : ℝ) {y : Chart} (hy : 0 < y.1) : ContDiffAt ℝ (↑⊤) (powerStage c b f) y

theorem NavierStokes.SlowBorelBase.template_smooth {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Inner → V} (hf : ContDiff ℝ (↑⊤) f) (c b : ℝ) : ContDiff ℝ (↑⊤) (template c b f)

theorem NavierStokes.SlowBorelBase.jointTemplate_smooth {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Inner → V} (hf : ContDiff ℝ (↑⊤) f) (b : ℝ) : ContDiff ℝ (↑⊤) (jointTemplate b f)

theorem NavierStokes.SlowBorelBase.template_jet_bound_by_joint {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Inner → V} (hf : ContDiff ℝ (↑⊤) f) (c b : ℝ) (m : ℕ) (y : Chart) : ‖iteratedFDeriv ℝ m (template c b f) y‖ ≤ ‖iteratedFDeriv ℝ m (jointTemplate b f) (c, y)‖ * ‖ContinuousLinearMap.inr ℝ ℝ Chart‖ ^ m

The scale is one extra parameter. Restricting an actual full derivative to the chart directions bounds the actual derivative at that fixed scale.

theorem NavierStokes.SlowBorelBase.exists_template_jet_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Inner → V} (hf : ContDiff ℝ (↑⊤) f) (b : ℝ) {K : Set Inner} (hK : IsCompact K) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ c ∈ Set.Icc 0 1, ∀ w ∈ K, ‖iteratedFDeriv ℝ m (template c b f) (1, w)‖ ≤ C

A compactness bound for actual normalized derivatives, uniform in every active cutoff scale c∈[0,1]. No stage derivative estimate is supplied.

noncomputable def NavierStokes.SlowBorelBase.blownJet {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (m : ℕ) (F : Chart → V) (y : Chart) : Chart [×m]→L[ℝ] V

Jets in the chart obtained by freezing the scale at the evaluation point and replacing q by q·s. The inner variables are left unscaled.

Equations

• NavierStokes.SlowBorelBase.blownJet m F y = iteratedFDeriv ℝ m (F ∘ ⇑(NavierStokes.SlowBorelBase.scaleMap y.1)) (1, y.2)

theorem NavierStokes.SlowBorelBase.powerStage_scale_germ {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (c b : ℝ) (f : Inner → V) {q : ℝ} (hq : 0 < q) (w : Inner) : powerStage c b f ∘ ⇑(scaleMap q) =ᶠ[nhds (1, w)] fun (y : ℝ × Inner) => q ^ b • template (c * q) b f y

theorem NavierStokes.SlowBorelBase.powerStage_germ {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (c b : ℝ) (f : Inner → V) {q : ℝ} (hq : 0 < q) (w : Inner) : powerStage c b f =ᶠ[nhds (q, w)] fun (y : ℝ × Inner) => q ^ b • template (c * q) b f ((scaleMap q⁻¹) y)

theorem NavierStokes.SlowBorelBase.powerStage_blown_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Inner → V} (hf : ContDiff ℝ (↑⊤) f) (c b : ℝ) {q C : ℝ} (hq : 0 < q) (w : Inner) (m : ℕ) (hb : ‖iteratedFDeriv ℝ m (template (c * q) b f) (1, w)‖ ≤ C) : ‖blownJet m (powerStage c b f) (q, w)‖ ≤ C * q ^ b

theorem NavierStokes.SlowBorelBase.powerStage_jet_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : Inner → V} (hf : ContDiff ℝ (↑⊤) f) (c b : ℝ) {q C : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) (hC : 0 ≤ C) (w : Inner) (m : ℕ) (hb : ‖iteratedFDeriv ℝ m (template (c * q) b f) (1, w)‖ ≤ C) : ‖iteratedFDeriv ℝ m (powerStage c b f) (q, w)‖ ≤ C * q ^ (b - ↑m)

theorem NavierStokes.SlowBorelBase.powerStage_eventually_zero {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (c b : ℝ) (f : Inner → V) {q : ℝ} (hcq : 1 < c * q) (w : Inner) : powerStage c b f =ᶠ[nhds (q, w)] fun (x : ℝ × Inner) => 0

theorem NavierStokes.SlowBorelBase.powerStage_jet_zero {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (c b : ℝ) (f : Inner → V) {q : ℝ} (hcq : 1 < c * q) (w : Inner) (m : ℕ) : iteratedFDeriv ℝ m (powerStage c b f) (q, w) = 0

theorem NavierStokes.SlowBorelBase.powerStage_blown_zero {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (c b : ℝ) (f : Inner → V) {q : ℝ} (hcq : 1 < c * q) (w : Inner) (m : ℕ) : blownJet m (powerStage c b f) (q, w) = 0

noncomputable def NavierStokes.SlowBorelBase.positiveCoefficient {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (h : ℝ) (f : ℕ → Inner → V) (j : ℕ) : Chart → V

The order-zero coefficient is kept uncut. This sequence contains only the positive corrections, with a zero placeholder at index zero.

Equations

• NavierStokes.SlowBorelBase.positiveCoefficient h f j = if j = 0 then fun (x : NavierStokes.SlowBorelBase.Chart) => 0 else NavierStokes.SlowBorelBase.powerCoefficient (2 * h * ↑j) (f j)

noncomputable def NavierStokes.SlowBorelBase.slowStage {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h : ℝ) (f : ℕ → Inner → V) : ℕ → Chart → V

Slow stage, given by SolenoidalDiagonal.cutStage (fun j => (a j : ℝ)) Prod.fst (positiveCoefficient h f).

Equations

• NavierStokes.SlowBorelBase.slowStage a h f = NavierStokes.SolenoidalDiagonal.cutStage (fun (j : ℕ) => ↑(a j)) Prod.fst (NavierStokes.SlowBorelBase.positiveCoefficient h f)

noncomputable def NavierStokes.SlowBorelBase.positiveSum {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h : ℝ) (f : ℕ → Inner → V) : Chart → V

Positive sum, given by SolenoidalDiagonal.potentialSum (fun j => (a j : ℝ)) Prod.fst (positiveCoefficient h f).

Equations

• NavierStokes.SlowBorelBase.positiveSum a h f = NavierStokes.SolenoidalDiagonal.potentialSum (fun (j : ℕ) => ↑(a j)) Prod.fst (NavierStokes.SlowBorelBase.positiveCoefficient h f)

noncomputable def NavierStokes.SlowBorelBase.slowSum {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h : ℝ) (f : ℕ → Inner → V) (y : Chart) : V

Slow sum, given by f 0 y.2 + positiveSum a h f y.

Equations

• NavierStokes.SlowBorelBase.slowSum a h f y = f 0 y.2 + NavierStokes.SlowBorelBase.positiveSum a h f y

noncomputable def NavierStokes.SlowBorelBase.cutPrefix {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h : ℝ) (f : ℕ → Inner → V) (J : ℕ) (y : Chart) : V

Cut prefix, given by f 0 y.2 + ∑ j ∈ Finset.range (J + 1), slowStage a h f j y.

Equations

• NavierStokes.SlowBorelBase.cutPrefix a h f J y = f 0 y.2 + ∑ j ∈ Finset.range (J + 1), NavierStokes.SlowBorelBase.slowStage a h f j y

noncomputable def NavierStokes.SlowBorelBase.uncutPrefix {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (h : ℝ) (f : ℕ → Inner → V) (J : ℕ) (y : Chart) : V

Uncut prefix, given by f 0 y.2 + ∑ j ∈ Finset.range (J + 1), positiveCoefficient h f j y.

Equations

• NavierStokes.SlowBorelBase.uncutPrefix h f J y = f 0 y.2 + ∑ j ∈ Finset.range (J + 1), NavierStokes.SlowBorelBase.positiveCoefficient h f j y

@[simp]

theorem NavierStokes.SlowBorelBase.slowStage_zero {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h : ℝ) (f : ℕ → Inner → V) : slowStage a h f 0 = 0

theorem NavierStokes.SlowBorelBase.slowStage_eq {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {j : ℕ} (hj : j ≠ 0) (a : ℕ → ℕ) (h : ℝ) (f : ℕ → Inner → V) : slowStage a h f j = powerStage (↑(a j)) (2 * h * ↑j) (f j)

theorem NavierStokes.SlowBorelBase.positiveCoefficient_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (h : ℝ) (j : ℕ) {y : Chart} (hy : 0 < y.1) : ContDiffAt ℝ (↑⊤) (positiveCoefficient h f j) y

theorem NavierStokes.SlowBorelBase.slowStage_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (a : ℕ → ℕ) (h : ℝ) (j : ℕ) {y : Chart} (hy : 0 < y.1) : ContDiffAt ℝ (↑⊤) (slowStage a h f j) y

structure NavierStokes.SlowBorelBase.AdmissibleScales {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (h : ℝ) (f : ℕ → Inner → V) (K : Set Inner) (a : ℕ → ℕ) : Prop

The quantitative properties proved by choosing the cutoff scales from the actual coefficient derivatives. These are later reused without repeating the compactness and numerical selection arguments.

• positive (j : ℕ) : 0 < a j
• doubling (j : ℕ) : 2 * a j ≤ a (j + 1)
• strictMono : StrictMono a
• ordinary (j : ℕ) : 1 ≤ j → ∀ m ≤ j + 2, ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ K, ‖iteratedFDeriv ℝ m (slowStage a h f j) (q, w)‖ ≤ (1 / 2) ^ j * q ^ (h * ↑j - ↑m)
• blown (j : ℕ) : 1 ≤ j → ∀ m ≤ j + 2, ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ K, ‖blownJet m (slowStage a h f j) (q, w)‖ ≤ (1 / 2) ^ j * q ^ (h * ↑j)

theorem NavierStokes.SlowBorelBase.exists_admissibleScales {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {h : ℝ} (hh : 0 < h) {K : Set Inner} (hK : IsCompact K) (B : ℕ) : ∃ (a : ℕ → ℕ), B ≤ a 0 ∧ AdmissibleScales h f K a

A single doubling schedule enforces every finite jet requirement in both ordinary and rescaled coordinates. Its only analytic input is smoothness of the individual coefficients on a fixed compact inner-coordinate set.

theorem NavierStokes.SlowBorelBase.slowStage_locally_zero {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) (h : ℝ) (f : ℕ → Inner → V) {y : Chart} (hy : 0 < y.1) : ∃ (N : ℕ), ∀ᶠ (z : Chart) in nhds y, ∀ (j : ℕ), N ≤ j → slowStage a h f j z = 0

theorem NavierStokes.SlowBorelBase.positiveSum_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (h : ℝ) {y : Chart} (hy : 0 < y.1) : ContDiffAt ℝ (↑⊤) (positiveSum a h f) y

theorem NavierStokes.SlowBorelBase.slowSum_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (h : ℝ) {y : Chart} (hy : 0 < y.1) : ContDiffAt ℝ (↑⊤) (slowSum a h f) y

theorem NavierStokes.SlowBorelBase.slowSum_smoothOn {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (h : ℝ) : ContDiffOn ℝ (↑⊤) (slowSum a h f) {y : Chart | 0 < y.1}

theorem NavierStokes.SlowBorelBase.ordinary_tail_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K : Set Inner} (ha : AdmissibleScales h f K a) {q : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) {w : Inner} (hw : w ∈ K) (J m : ℕ) (hm : m ≤ J + 3) : ‖iteratedFDeriv ℝ m (fun (y : Chart) => slowSum a h f y - cutPrefix a h f J y) (q, w)‖ ≤ (1 / 2) ^ J * q ^ (h * (↑J + 1) - ↑m)

Actual ordinary derivatives of the infinite sum minus a cut prefix.

theorem NavierStokes.SlowBorelBase.blown_tail_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K : Set Inner} (ha : AdmissibleScales h f K a) {q : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) {w : Inner} (hw : w ∈ K) (J m : ℕ) (hm : m ≤ J + 3) : ‖blownJet m (fun (y : Chart) => slowSum a h f y - cutPrefix a h f J y) (q, w)‖ ≤ (1 / 2) ^ J * q ^ (h * (↑J + 1))

Actual derivatives after freezing the dilation at the evaluation scale. The same one schedule works for every eventually prescribed jet order.

theorem NavierStokes.SlowBorelBase.cutPrefix_eventually_uncut {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h : ℝ) (f : ℕ → Inner → V) (J : ℕ) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (y : Chart), |y.1| < δ → cutPrefix a h f J =ᶠ[nhds y] uncutPrefix h f J

theorem NavierStokes.SlowBorelBase.exists_ordinary_uncut_tail {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K : Set Inner} (ha : AdmissibleScales h f K a) (M Jmin : ℕ) (P : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ M ≤ J ∧ ∃ (δ : ℝ), 0 < δ ∧ ∀ m ≤ M, ∀ (q : ℝ), 0 < q → q < δ → ∀ w ∈ K, ‖iteratedFDeriv ℝ m (fun (y : Chart) => slowSum a h f y - uncutPrefix h f J y) (q, w)‖ ≤ (1 / 2) ^ J * q ^ P

Every requested finite ordinary jet has a sufficiently late *uncut * prefix with any prescribed remainder power. The prefix depends on both requests; this does not assert that one fixed tail is flat to all orders.

theorem NavierStokes.SlowBorelBase.exists_blown_uncut_tail {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K : Set Inner} (ha : AdmissibleScales h f K a) (M Jmin : ℕ) (P : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ M ≤ J ∧ ∃ (δ : ℝ), 0 < δ ∧ ∀ m ≤ M, ∀ (q : ℝ), 0 < q → q < δ → ∀ w ∈ K, ‖blownJet m (fun (y : Chart) => slowSum a h f y - uncutPrefix h f J y) (q, w)‖ ≤ (1 / 2) ^ J * q ^ P

theorem NavierStokes.SlowBorelBase.exists_stage_blown_power_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K : Set Inner} (hK : IsCompact K) (a : ℕ → ℕ) (h : ℝ) (j m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℝ), 0 < q → ∀ w ∈ K, ‖blownJet m (slowStage a h f j) (q, w)‖ ≤ C * q ^ (2 * h * ↑j)

A fixed stage keeps its full q^(2hj) order. Only the tail estimates spend half this gain to absorb coefficient growth.

theorem NavierStokes.SlowBorelBase.blownJet_sum {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_1} (s : Finset ι) (F : ι → Chart → V) {q : ℝ} {w : Inner} (hF : ∀ i ∈ s, ContDiffAt ℝ (↑⊤) (F i) (q, w)) (m : ℕ) : blownJet m (fun (y : Chart) => ∑ i ∈ s, F i y) (q, w) = ∑ i ∈ s, blownJet m (F i) (q, w)

theorem NavierStokes.SlowBorelBase.norm_blownJet_le_sub_add {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {F G : Chart → V} {q : ℝ} {w : Inner} (hF : ContDiffAt ℝ (↑⊤) F (q, w)) (hG : ContDiffAt ℝ (↑⊤) G (q, w)) (m : ℕ) : ‖blownJet m F (q, w)‖ ≤ ‖blownJet m (fun (y : Chart) => F y - G y) (q, w)‖ + ‖blownJet m G (q, w)‖

theorem NavierStokes.SlowBorelBase.normalized_correction_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K : Set Inner} (hK : IsCompact K) (ha : AdmissibleScales h f K a) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ K, ‖blownJet m (fun (y : Chart) => slowSum a h f y - f 0 y.2) (q, w)‖ ≤ C * q ^ (2 * h)

The normalized correction is O(q^(2h)) in every fixed blown-up jet. This estimates derivatives of the actual sum; no bound on its tail is assumed.

noncomputable def NavierStokes.SlowBorelBase.innerBox (lo hi : ℝ) : Set Inner

Inner box, given by Icc lo hi ×ˢ Icc (-1) 1.

Equations

• NavierStokes.SlowBorelBase.innerBox lo hi = Set.Icc lo hi ×ˢ Set.Icc (-1) 1

theorem NavierStokes.SlowBorelBase.innerBox_isCompact (lo hi : ℝ) : IsCompact (innerBox lo hi)

noncomputable def NavierStokes.SlowBorelBase.physicalChart (h : ℝ) (p : Chart) : Chart

Physical chart as an element of Chart.

Equations

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

theorem NavierStokes.SlowBorelBase.physicalChart_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Chart} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (physicalChart h) p

theorem NavierStokes.SlowBorelBase.physicalChart_positive {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Chart} (hp : p.1 < 1) : 0 < (physicalChart h p).1

theorem NavierStokes.SlowBorelBase.physicalChart_inner_mem {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : Chart} (hp : p.1 < 1) (hX : PhysicalCoordinateBounds.physicalX (2 * h) p ∈ Set.Icc lo hi) : (physicalChart h p).2 ∈ innerBox lo hi

theorem NavierStokes.SlowBorelBase.physicalChart_jet_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (lo hi : ℝ) (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : Chart), p.1 < 1 → (physicalChart h p).1 ≤ 1 → (physicalChart h p).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ n (physicalChart h) p‖ ≤ C * (physicalChart h p).1 ^ (-↑n)

The actual similarity-coordinate map loses at most one q-power per physical derivative, uniformly on a fixed bounded X range.

theorem NavierStokes.SlowBorelBase.physicalChart_finite_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (lo hi : ℝ) (n : ℕ) : ∃ (D : ℝ), 1 ≤ D ∧ ∀ (p : Chart), p.1 < 1 → (physicalChart h p).1 ≤ 1 → (physicalChart h p).2.1 ∈ Set.Icc lo hi → ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i (physicalChart h) p‖ ≤ (D / (physicalChart h p).1) ^ i

theorem NavierStokes.SlowBorelBase.physical_composition_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {F : Chart → V} (hF : ContDiffOn ℝ (↑⊤) F {y : Chart | 0 < y.1}) {p : Chart} (hp : p.1 < 1) (n : ℕ) {C D : ℝ} (hC : ∀ i ≤ n, ‖iteratedFDeriv ℝ i F (physicalChart h p)‖ ≤ C) (hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv ℝ i (physicalChart h) p‖ ≤ D ^ i) : ‖iteratedFDeriv ℝ n (F ∘ physicalChart h) p‖ ≤ ↑n.factorial * C * D ^ n

A quantitative chain rule on the actual positive-time domain.

theorem NavierStokes.SlowBorelBase.exists_physical_uncut_tail {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (lo hi : ℝ) (ha : AdmissibleScales h f (innerBox lo hi) a) (m Jmin : ℕ) (P : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ m ≤ J ∧ ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 < C ∧ ∀ (p : Chart), p.1 < 1 → (physicalChart h p).1 < δ → (physicalChart h p).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m ((fun (y : Chart) => slowSum a h f y - uncutPrefix h f J y) ∘ physicalChart h) p‖ ≤ C * (physicalChart h p).1 ^ P

Actual physical derivatives of a tail have arbitrary prescribed decay after choosing the prefix for that derivative order and requested power.

@[simp]

theorem NavierStokes.SlowBorelBase.physicalChart_eq (h : ℝ) (p : Chart) : physicalChart h p = (SimilarityProfile.q h p, SimilarityProfile.inner h p)

noncomputable def NavierStokes.SlowBorelBase.physicalProfile {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h b : ℝ) (f : ℕ → Inner → V) (p : Chart) : V

Restoring a fixed leading q-power after summing the normalized data.

Equations

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

theorem NavierStokes.SlowBorelBase.physicalProfile_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) {p : Chart} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (physicalProfile a h b f) p

theorem NavierStokes.SlowBorelBase.physicalProfile_smoothOn {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) : ContDiffOn ℝ (↑⊤) (physicalProfile a h b f) (Set.Iio 1 ×ˢ Set.univ)

noncomputable def NavierStokes.SlowBorelBase.coefficientWeight (a : ℕ → ℕ) (h q : ℝ) (j : ℕ) : ℝ

Coefficient weight, with branches according to j = 0.

Equations

• NavierStokes.SlowBorelBase.coefficientWeight a h q j = if j = 0 then 0 else NavierStokes.SmoothCutoffs.scaledCutoff (↑(a j)) q * q ^ (2 * h * ↑j)

theorem NavierStokes.SlowBorelBase.slowSum_finite_at_scale {a : ℕ → ℕ} (ha : StrictMono a) (h : ℝ) {q : ℝ} (hq : 0 < q) : ∃ (N : ℕ), ∀ (f : ℕ → Inner → ℝ) (w : Inner), slowSum a h f (q, w) = f 0 w + ∑ j ∈ Finset.range N, coefficientWeight a h q j * f j w

For a fixed positive q, a single finite set represents every coefficient family, at every inner point. This is independent of the coefficient values.

theorem NavierStokes.SlowBorelBase.hasDerivAt_slowSum_X {a : ℕ → ℕ} (ha : StrictMono a) (h : ℝ) {f : ℕ → Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {q : ℝ} (hq : 0 < q) (X eta : ℝ) : HasDerivAt (fun (x : ℝ) => slowSum a h f (q, x, eta)) (slowSum a h (fun (j : ℕ) => SimilarityProfile.partialX (f j)) (q, X, eta)) X

Differentiation in X commutes with the actual locally finite series. The cutoff depends only on q, so no radial cutoff term appears.

theorem NavierStokes.SlowBorelBase.hasDerivAt_physicalProfile_s {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) {p : Chart} (hp : p.1 < 1) : HasDerivAt (fun (s : ℝ) => physicalProfile a h b f (p.1, s, p.2.2)) (physicalProfile a h (b - 1) (fun (j : ℕ) => SimilarityProfile.partialX (f j)) p) p.2.1

theorem NavierStokes.SlowBorelBase.partialS_physicalProfile {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) {p : Chart} (hp : p.1 < 1) : AxisymmetricFields.partialS (physicalProfile a h b f) p = physicalProfile a h (b - 1) (fun (j : ℕ) => SimilarityProfile.partialX (f j)) p

noncomputable def NavierStokes.SlowBorelBase.physicalUncutPrefix {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (h b : ℝ) (f : ℕ → Inner → V) (J : ℕ) (p : Chart) : V

Physical uncut prefix, given by (physicalChart h p).1 ^ b • uncutPrefix h f J (physicalChart h p).

Equations

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

theorem NavierStokes.SlowBorelBase.uncutPrefix_smoothOn {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (h : ℝ) (J : ℕ) : ContDiffOn ℝ (↑⊤) (uncutPrefix h f J) {y : Chart | 0 < y.1}

theorem NavierStokes.SlowBorelBase.norm_smul_jet_le_on {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {F : Chart → ℝ} {G : Chart → V} {U : Set Chart} (hU : IsOpen U) (hF : ContDiffOn ℝ (↑⊤) F U) (hG : ContDiffOn ℝ (↑⊤) G U) {p : Chart} (hp : p ∈ U) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : Chart) => F y • G y) p‖ ≤ ∑ i ∈ Finset.range (m + 1), ↑(m.choose i) * ‖iteratedFDeriv ℝ i F p‖ * ‖iteratedFDeriv ℝ (m - i) G p‖

theorem NavierStokes.SlowBorelBase.powered_physical_tail_of_chart_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (lo hi b : ℝ) (ha : StrictMono a) (J M : ℕ) (P E δ : ℝ) (hE : 0 ≤ E) (hδ : 0 < δ) (hb : ∀ m ≤ M, ∀ (q : ℝ), 0 < q → q < δ → ∀ w ∈ innerBox lo hi, ‖iteratedFDeriv ℝ m (fun (y : Chart) => slowSum a h f y - uncutPrefix h f J y) (q, w)‖ ≤ E * q ^ (P - b + ↑M)) : ∃ (δ' : ℝ) (C : ℝ), 0 < δ' ∧ 0 < C ∧ ∀ m ≤ M, ∀ (p : Chart), p.1 < 1 → (physicalChart h p).1 < δ' → (physicalChart h p).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m (fun (y : Chart) => physicalProfile a h b f y - physicalUncutPrefix h b f J y) p‖ ≤ C * (physicalChart h p).1 ^ P

Restoring any fixed leading q-power preserves arbitrary-order asymptotic summation. All products and derivatives here are the actual physical ones.

theorem NavierStokes.SlowBorelBase.exists_powered_physical_tail_finite {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (lo hi b : ℝ) (ha : AdmissibleScales h f (innerBox lo hi) a) (M Jmin : ℕ) (P : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ M ≤ J ∧ ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 < C ∧ ∀ m ≤ M, ∀ (p : Chart), p.1 < 1 → (physicalChart h p).1 < δ → (physicalChart h p).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m (fun (y : Chart) => physicalProfile a h b f y - physicalUncutPrefix h b f J y) p‖ ≤ C * (physicalChart h p).1 ^ P

theorem NavierStokes.SlowBorelBase.exists_powered_physical_tail {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (lo hi b : ℝ) (ha : AdmissibleScales h f (innerBox lo hi) a) (m Jmin : ℕ) (P : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ m ≤ J ∧ ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 < C ∧ ∀ (p : Chart), p.1 < 1 → (physicalChart h p).1 < δ → (physicalChart h p).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m (fun (y : Chart) => physicalProfile a h b f y - physicalUncutPrefix h b f J y) p‖ ≤ C * (physicalChart h p).1 ^ P

theorem NavierStokes.SlowBorelBase.slowStage_map {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) (a : ℕ → ℕ) (h : ℝ) (f : ℕ → Inner → V) (j : ℕ) : slowStage a h (fun (n : ℕ) (w : Inner) => L (f n w)) j = ⇑L ∘ slowStage a h f j

theorem NavierStokes.SlowBorelBase.slowSum_map {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) {a : ℕ → ℕ} (ha : StrictMono a) (h : ℝ) (f : ℕ → Inner → V) {y : Chart} (hy : 0 < y.1) : slowSum a h (fun (n : ℕ) (w : Inner) => L (f n w)) y = L (slowSum a h f y)

theorem NavierStokes.SlowBorelBase.norm_jet_map_le {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W) {F : Chart → V} {y : Chart} (hF : ContDiffAt ℝ (↑⊤) F y) (m : ℕ) : ‖iteratedFDeriv ℝ m (⇑L ∘ F) y‖ ≤ ‖L‖ * ‖iteratedFDeriv ℝ m F y‖

theorem NavierStokes.SlowBorelBase.AdmissibleScales.map {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Type} [NormedAddCommGroup W] [NormedSpace ℝ W] {a : ℕ → ℕ} {h : ℝ} {f : ℕ → Inner → V} {K : Set Inner} (ha : AdmissibleScales h f K a) (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (L : V →L[ℝ] W) (hL : ‖L‖ ≤ 1) : AdmissibleScales h (fun (j : ℕ) (w : Inner) => L (f j w)) K a

structure NavierStokes.SlowBorelBase.Coefficients : Type

Smooth coefficient data before asymptotic summation. The radial and swirl potentials below are constructed by actual integration from these data.

• axial : ℕ → Inner → ℝ

  Axial of Coefficients, of type ℕ → Inner → ℝ.

• phi : ℕ → Inner → ℝ

  Phi of Coefficients, of type ℕ → Inner → ℝ.

• pressure : ℕ → Inner → ℝ

  Pressure field of Coefficients, of type ℕ → Inner → ℝ.

• stressTheta : ℕ → Inner → ℝ

  Stress theta of Coefficients, of type ℕ → Inner → ℝ.

• stressAxial : ℕ → Inner → ℝ

  Stress axial of Coefficients, of type ℕ → Inner → ℝ.

structure NavierStokes.SlowBorelBase.SmoothCoefficients (d : Coefficients) : Prop

Smooth coefficients data, collecting axial, phi, pressure, stressTheta, stressAxial.

• axial (j : ℕ) : ContDiff ℝ (↑⊤) (d.axial j)
• phi (j : ℕ) : ContDiff ℝ (↑⊤) (d.phi j)
• pressure (j : ℕ) : ContDiff ℝ (↑⊤) (d.pressure j)
• stressTheta (j : ℕ) : ContDiff ℝ (↑⊤) (d.stressTheta j)
• stressAxial (j : ℕ) : ContDiff ℝ (↑⊤) (d.stressAxial j)

noncomputable def NavierStokes.SlowBorelBase.globalRadialDomain : ProfileHistories.RadialDomain

Global radial domain, bundling carrier, isOpen, scale_mem.

Equations

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

theorem NavierStokes.SlowBorelBase.average_smooth {f : Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (ProfileHistories.average f)

theorem NavierStokes.SlowBorelBase.primitive_smooth {f : Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (ProfileHistories.primitive f)

theorem NavierStokes.SlowBorelBase.partialX_primitive {f : Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) : SimilarityProfile.partialX (ProfileHistories.primitive f) = f

@[reducible, inline]

abbrev NavierStokes.SlowBorelBase.Bundle : Type

Bundle: an abbreviation for Fin 7 → ℝ.

Equations

• NavierStokes.SlowBorelBase.Bundle = (Fin 7 → ℝ)

noncomputable def NavierStokes.SlowBorelBase.coefficientBundle (C : ℝ) (d : Coefficients) (j : ℕ) (w : Inner) : Bundle

One bundle forces one common cutoff schedule for the streams, angular data, pressure, and both stress components.

Equations

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

theorem NavierStokes.SlowBorelBase.coefficientBundle_smooth {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) (j : ℕ) : ContDiff ℝ (↑⊤) (coefficientBundle C d j)

noncomputable def NavierStokes.SlowBorelBase.bundleComponent (C : ℝ) (d : Coefficients) (i : Fin 7) : ℕ → Inner → ℝ

Bundle component, defined pointwise by coefficientBundle C d j w i.

Equations

• NavierStokes.SlowBorelBase.bundleComponent C d i j w = NavierStokes.SlowBorelBase.coefficientBundle C d j w i

theorem NavierStokes.SlowBorelBase.bundleComponent_smooth {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) (i : Fin 7) (j : ℕ) : ContDiff ℝ (↑⊤) (bundleComponent C d i j)

theorem NavierStokes.SlowBorelBase.admissible_component {a : ℕ → ℕ} {h C : ℝ} {d : Coefficients} (hd : SmoothCoefficients d) {K : Set Inner} (ha : AdmissibleScales h (coefficientBundle C d) K a) (i : Fin 7) : AdmissibleScales h (bundleComponent C d i) K a

noncomputable def NavierStokes.SlowBorelBase.streamFactor (a : ℕ → ℕ) (h C : ℝ) (d : Coefficients) : Chart → ℝ

H=S/s, with its smooth value at the axis provided by the radial average.

Equations

• NavierStokes.SlowBorelBase.streamFactor a h C d = NavierStokes.SlowBorelBase.physicalProfile a h (-NavierStokes.CoordinateAlgebra.A h) (NavierStokes.SlowBorelBase.bundleComponent C d 0)

noncomputable def NavierStokes.SlowBorelBase.swirlPotential (a : ℕ → ℕ) (h C : ℝ) (d : Coefficients) : Chart → ℝ

Swirl potential, given by physicalProfile a h (1 / 2 - CoordinateAlgebra.A h) (bundleComponent C d 1).

Equations

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

noncomputable def NavierStokes.SlowBorelBase.integratedStream (a : ℕ → ℕ) (h C : ℝ) (d : Coefficients) (p : Chart) : ℝ

Integrated stream, given by p.2.1 * streamFactor a h C d p.

Equations

• NavierStokes.SlowBorelBase.integratedStream a h C d p = p.2.1 * NavierStokes.SlowBorelBase.streamFactor a h C d p

noncomputable def NavierStokes.SlowBorelBase.baseVelocity (a : ℕ → ℕ) (h C : ℝ) (d : Coefficients) : ProblemStatement.VelocityField

Base velocity, given by AxisymmetricFields.velocity (streamFactor a h C d) (swirlPotential a h C d).

Equations

• NavierStokes.SlowBorelBase.baseVelocity a h C d = NavierStokes.AxisymmetricFields.velocity (NavierStokes.SlowBorelBase.streamFactor a h C d) (NavierStokes.SlowBorelBase.swirlPotential a h C d)

noncomputable def NavierStokes.SlowBorelBase.basePressure (a : ℕ → ℕ) (h C : ℝ) (d : Coefficients) : ProblemStatement.PressureField

Base pressure, defined pointwise by physicalProfile a h (-2 * CoordinateAlgebra.A h) (bundleComponent C d 2) (AxisymmetricFields.profilePoint z.1 z.2).

Equations

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

noncomputable def NavierStokes.SlowBorelBase.baseStressTheta (a : ℕ → ℕ) (h C : ℝ) (d : Coefficients) : Chart → ℝ

Base stress theta, given by physicalProfile a h (-CoordinateAlgebra.A h - 1 / 2) (bundleComponent C d 3).

Equations

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

noncomputable def NavierStokes.SlowBorelBase.baseStressAxial (a : ℕ → ℕ) (h C : ℝ) (d : Coefficients) : Chart → ℝ

Base stress axial, given by physicalProfile a h (-CoordinateAlgebra.A h - 1 / 2) (bundleComponent C d 4).

Equations

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

theorem NavierStokes.SlowBorelBase.baseVelocity_smooth {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (baseVelocity a h C d) (Set.Iio 1 ×ˢ Set.univ)

theorem NavierStokes.SlowBorelBase.baseVelocity_divergence_zero {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (baseVelocity a h C d) t x = 0

Exact Cartesian incompressibility, including the axis, follows from the actual curl of the asymptotically summed potentials.

theorem NavierStokes.SlowBorelBase.exists_base_fields {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : Coefficients} (hd : SmoothCoefficients d) (C lo hi : ℝ) (B : ℕ) : ∃ (a : ℕ → ℕ), B ≤ a 0 ∧ AdmissibleScales h (coefficientBundle C d) (innerBox lo hi) a ∧ ContDiffOn ℝ (↑⊤) (baseVelocity a h C d) (Set.Iio 1 ×ˢ Set.univ) ∧ ∀ t < 1, ∀ (x : ProblemStatement.Space), ProblemStatement.spatialDivergence (baseVelocity a h C d) t x = 0

Existence of the shared schedule and the actual smooth, exactly solenoidal base uses only the supplied smooth coefficient sequence.

theorem NavierStokes.SlowBorelBase.uncutPrefix_eq_sum {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (h : ℝ) (f : ℕ → Inner → V) (J : ℕ) (y : Chart) : uncutPrefix h f J y = ∑ j ∈ Finset.range (J + 1), powerCoefficient (2 * h * ↑j) (f j) y

theorem NavierStokes.SlowBorelBase.physicalUncutPrefix_eq_finiteProfile {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (b : ℝ) (f : ℕ → Inner → ℝ) (J : ℕ) {p : Chart} (hp : p.1 < 1) : physicalUncutPrefix h b f J p = SlowExpansionResidual.finiteProfile J h b f p

The uncut physical prefix is the same finite expansion used in the explicit coefficient residual calculation.

theorem NavierStokes.SlowBorelBase.slowSum_inner_mul {a : ℕ → ℕ} (ha : StrictMono a) (h : ℝ) (f : ℕ → Inner → ℝ) (r : Inner → ℝ) {y : Chart} (hy : 0 < y.1) : slowSum a h (fun (j : ℕ) (w : Inner) => r w * f j w) y = r y.2 * slowSum a h f y

theorem NavierStokes.SlowBorelBase.integratedStream_eq_primitive {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) (d : Coefficients) {p : Chart} (hp : p.1 < 1) : integratedStream a h C d p = physicalProfile a h (1 - CoordinateAlgebra.A h) (fun (j : ℕ) => ProfileHistories.primitive (d.axial j)) p

The integrated stream is literally the cut sum of q^(1−A+λj) times the radial primitives, with its smooth axis factor retained.

theorem NavierStokes.SlowBorelBase.partialS_integratedStream {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) {p : Chart} (hp : p.1 < 1) : AxisymmetricFields.partialS (integratedStream a h C d) p = physicalProfile a h (-CoordinateAlgebra.A h) d.axial p

theorem NavierStokes.SlowBorelBase.partialS_radial_mul {H : Chart → ℝ} {p : Chart} (hH : DifferentiableAt ℝ H p) : AxisymmetricFields.partialS (fun (y : AxisymmetricFields.ProfilePoint) => y.2.1 * H y) p = H p + p.2.1 * AxisymmetricFields.partialS H p

theorem NavierStokes.SlowBorelBase.baseVelocity_axial {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) : (baseVelocity a h C d (t, x)).ofLp 2 = physicalProfile a h (-CoordinateAlgebra.A h) d.axial (AxisymmetricFields.profilePoint t x)

The actual axial component is the direct cut sum of the axial profiles; the derivative of the integrated stream has been computed, not postulated.

theorem NavierStokes.SlowBorelBase.partialX_swirl_primitive {f : Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) (C : ℝ) : (SimilarityProfile.partialX fun (w : SimilarityProfile.InnerPoint) => -C⁻¹ * ProfileHistories.primitive f w) = fun (w : Inner) => -C⁻¹ * f w

theorem NavierStokes.SlowBorelBase.partialS_swirlPotential {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) {p : Chart} (hp : p.1 < 1) : AxisymmetricFields.partialS (swirlPotential a h C d) p = -C⁻¹ * physicalProfile a h (-CoordinateAlgebra.A h - 1 / 2) d.phi p

theorem NavierStokes.SlowBorelBase.physicalUncutPrefix_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) (J : ℕ) {p : Chart} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (physicalUncutPrefix h b f J) p

theorem NavierStokes.SlowBorelBase.compact_jet_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : E → V} {U K : Set E} (hU : IsOpen U) (hF : ContDiffOn ℝ (↑⊤) F U) (hK : IsCompact K) (hKU : K ⊆ U) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ x ∈ K, ‖iteratedFDeriv ℝ m F x‖ ≤ C

theorem NavierStokes.SlowBorelBase.compact_map_finite_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : E → V} (hF : ContDiff ℝ (↑⊤) F) {K : Set E} (hK : IsCompact K) (M : ℕ) : ∃ (D : ℝ), 1 ≤ D ∧ ∀ x ∈ K, ∀ (i : ℕ), 1 ≤ i → i ≤ M → ‖iteratedFDeriv ℝ i F x‖ ≤ D ^ i

noncomputable def NavierStokes.SlowBorelBase.cartesianChart (h : ℝ) (z : ProblemStatement.SpaceTime) : Chart

Cartesian chart, given by physicalChart h (AxisymmetricFields.profilePoint z.1 z.2).

Equations

• NavierStokes.SlowBorelBase.cartesianChart h z = NavierStokes.SlowBorelBase.physicalChart h (NavierStokes.AxisymmetricFields.profilePoint z.1 z.2)

noncomputable def NavierStokes.SlowBorelBase.cartesianProfile {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h b : ℝ) (f : ℕ → Inner → V) (z : ProblemStatement.SpaceTime) : V

Cartesian profile, given by physicalProfile a h b f (AxisymmetricFields.profilePoint z.1 z.2).

Equations

• NavierStokes.SlowBorelBase.cartesianProfile a h b f z = NavierStokes.SlowBorelBase.physicalProfile a h b f (NavierStokes.AxisymmetricFields.profilePoint z.1 z.2)

noncomputable def NavierStokes.SlowBorelBase.cartesianUncutPrefix {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (h b : ℝ) (f : ℕ → Inner → V) (J : ℕ) (z : ProblemStatement.SpaceTime) : V

Cartesian uncut prefix, given by physicalUncutPrefix h b f J (AxisymmetricFields.profilePoint z.1 z.2).

Equations

• NavierStokes.SlowBorelBase.cartesianUncutPrefix h b f J z = NavierStokes.SlowBorelBase.physicalUncutPrefix h b f J (NavierStokes.AxisymmetricFields.profilePoint z.1 z.2)

theorem NavierStokes.SlowBorelBase.exists_cartesian_profile_tail {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (lo hi b : ℝ) (ha : AdmissibleScales h f (innerBox lo hi) a) {K : Set ProblemStatement.SpaceTime} (hK : IsCompact K) (m Jmin : ℕ) (P : ℝ) : ∃ (J : ℕ), Jmin ≤ J ∧ m ≤ J ∧ ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 < C ∧ ∀ z ∈ K, z.1 < 1 → (cartesianChart h z).1 < δ → (cartesianChart h z).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => cartesianProfile a h b f y - cartesianUncutPrefix h b f J y) z‖ ≤ C * (cartesianChart h z).1 ^ P

The map (t,x)↦(t,(|x_perp|²/2,x₃)) is smooth at the axis. On any fixed compact Cartesian set its derivatives have finite bounds, so the proved physical-profile tail estimates imply actual Cartesian space-time estimates.

theorem NavierStokes.SlowBorelBase.normalized_correction_smul_inner {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K U : Set Inner} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) (ha : AdmissibleScales h f K a) {r : Inner → ℝ} (hr : ContDiffOn ℝ (↑⊤) r U) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ K, ‖blownJet m (fun (y : Chart) => r y.2 • (slowSum a h f y - f 0 y.2)) (q, w)‖ ≤ C * q ^ (2 * h)

Multiplication by a smooth fixed inner-coordinate factor preserves the derived q^(2h) bound. This handles the radius factor on an active annulus.

noncomputable def NavierStokes.SlowBorelBase.normalizedSwirl (a : ℕ → ℕ) (h C : ℝ) (d : Coefficients) (y : Chart) : ℝ

Normalized swirl, given by Real.sqrt (2 * y.2.1) / C * slowSum a h d.phi y.

Equations

• NavierStokes.SlowBorelBase.normalizedSwirl a h C d y = √(2 * y.2.1) / C * NavierStokes.SlowBorelBase.slowSum a h d.phi y

noncomputable def NavierStokes.SlowBorelBase.leadingSwirl (C : ℝ) (d : Coefficients) (w : Inner) : ℝ

Leading swirl, given by Real.sqrt (2 * w.1) / C * d.phi 0 w.

Equations

• NavierStokes.SlowBorelBase.leadingSwirl C d w = √(2 * w.1) / C * d.phi 0 w

theorem NavierStokes.SlowBorelBase.normalized_tangential_bounds {a : ℕ → ℕ} {h C lo hi : ℝ} (hh : 0 < h) (hlo : 0 < lo) {d : Coefficients} (hd : SmoothCoefficients d) (ha : AdmissibleScales h (coefficientBundle C d) (innerBox lo hi) a) (m : ℕ) : ∃ (B : ℝ), 0 < B ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ innerBox lo hi, ‖blownJet m (fun (y : Chart) => normalizedSwirl a h C d y - leadingSwirl C d y.2) (q, w)‖ ≤ B * q ^ (2 * h) ∧ ‖blownJet m (fun (y : Chart) => slowSum a h d.axial y - d.axial 0 y.2) (q, w)‖ ≤ B * q ^ (2 * h)

Both normalized tangential components have the claimed O(q^(2h)) correction on every fixed active annulus, in every fixed blown-up jet.

theorem NavierStokes.SlowBorelBase.baseVelocity_angularMoment {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) : -x.ofLp 1 * (baseVelocity a h C d (t, x)).ofLp 0 + x.ofLp 0 * (baseVelocity a h C d (t, x)).ofLp 1 = 2 * AxisymmetricFields.radialEnergy x * C⁻¹ * physicalProfile a h (-CoordinateAlgebra.A h - 1 / 2) d.phi (AxisymmetricFields.profilePoint t x)

theorem NavierStokes.SlowBorelBase.angularMoment_eq_normalizedSwirl {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : Coefficients} (hd : SmoothCoefficients d) (C : ℝ) {t : ℝ} (ht : t < 1) (x : ProblemStatement.Space) : -x.ofLp 1 * (baseVelocity a h C d (t, x)).ofLp 0 + x.ofLp 0 * (baseVelocity a h C d (t, x)).ofLp 1 = √(2 * AxisymmetricFields.radialEnergy x) * (cartesianChart h (t, x)).1 ^ (-CoordinateAlgebra.A h) * normalizedSwirl a h C d (cartesianChart h (t, x))

normalizedSwirl is the actual q^A-normalized tangential velocity: the displayed Cartesian angular momentum is r times q^(-A) times that value. The identity includes the axis without division by r.

theorem NavierStokes.SlowBorelBase.normalized_stress_weighted_compact {a : ℕ → ℕ} {h C : ℝ} (hh : 0 < h) {d : Coefficients} (hd : SmoothCoefficients d) {K U : Set Inner} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) (ha : AdmissibleScales h (coefficientBundle C d) K a) {r : Inner → ℝ} (hr : ContDiffOn ℝ (↑⊤) r U) (m : ℕ) : ∃ (B : ℝ), 0 < B ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ K, ‖blownJet m (fun (y : Chart) => r y.2 * (slowSum a h d.stressTheta y - d.stressTheta 0 y.2)) (q, w)‖ ≤ B * q ^ h ∧ ‖blownJet m (fun (y : Chart) => r y.2 * (slowSum a h d.stressAxial y - d.stressAxial 0 y.2)) (q, w)‖ ≤ B * q ^ h

Smooth fixed inner weights, including reciprocal annular weights on compact subsets where they are smooth, preserve the proved tensor estimate. This is an interior weighted statement; it does not presume the edge bounds.

theorem NavierStokes.SlowBorelBase.uncut_fixed_prefix_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K : Set Inner} (ha : AdmissibleScales h f K a) (J : ℕ) : ∃ (δ : ℝ), 0 < δ ∧ δ ≤ 1 ∧ ∀ m ≤ J + 3, ∀ (q : ℝ), 0 < q → q < δ → ∀ w ∈ K, ‖iteratedFDeriv ℝ m (fun (y : Chart) => slowSum a h f y - uncutPrefix h f J y) (q, w)‖ ≤ (1 / 2) ^ J * q ^ (h * (↑J + 1) - ↑m)

The same cutoff plateau works for every derivative of a fixed prefix. The estimate itself retains the derivative-dependent power loss.

theorem NavierStokes.SlowBorelBase.powered_fixed_prefix_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (lo hi b : ℝ) (ha : AdmissibleScales h f (innerBox lo hi) a) (J M : ℕ) (hMJ : M ≤ J + 3) : ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 < C ∧ ∀ m ≤ M, ∀ (p : Chart), p.1 < 1 → (physicalChart h p).1 < δ → (physicalChart h p).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m (fun (y : Chart) => physicalProfile a h b f y - physicalUncutPrefix h b f J y) p‖ ≤ C * (physicalChart h p).1 ^ (h * (↑J + 1) + b - 2 * ↑M)

A fixed prefix has a growing, finite remainder order. This interface permits one common truncation across finitely many field components and leading powers. It still does not call a fixed tail flat to all orders.