Residual and axis values of the asymptotically summed slow base

The series used here is the actual locally finite series in SlowBorelBase. The radial streams are summed before taking their Cartesian curl.

Regular finite tail coefficients at the symmetry axis

The radial flux is V_n = X * beta_n. This module uses that identity in the actual finite tails. The resulting coefficient functions contain no division by X; their finite indices and powers of q are unchanged.

noncomputable def NavierStokes.AxisTailRegularity.regularTransportKernel (h e α : ℝ) (beta u f : ℕ → SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) (i j : ℕ) : ℝ

The transport kernel after canceling the radial flux factor.

Equations

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

noncomputable def NavierStokes.AxisTailRegularity.regularRadialKernel (h : ℝ) (beta u : ℕ → SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) (i j : ℕ) : ℝ

The radial transport kernel divided by its factor X.

Equations

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

noncomputable def NavierStokes.AxisTailRegularity.regularTransportTerm (N : ℕ) (h e α : ℝ) (beta u f : ℕ → SimilarityProfile.InnerProfile) : SlowResidualMatching.TailIndex → SimilarityProfile.InnerProfile

Same omitted pairs and final viscosity term as the original transport tail.

Equations

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

noncomputable def NavierStokes.AxisTailRegularity.regularPressureTerm (N : ℕ) (h C : ℝ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) : SlowResidualMatching.PressureIndex → SimilarityProfile.InnerProfile

Each original radial pressure coefficient divided by 2X, with the factor canceled before evaluation. In particular this defines its smooth extension at X = 0, rather than using total division there.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.AxisTailRegularity.regularPressureTerm N h C phi u beta (Sum.inr (some ij)) = fun (w : NavierStokes.SimilarityProfile.InnerPoint) => -C⁻¹ ^ 2 * (phi ij.1 w * phi ij.2 w)

theorem NavierStokes.AxisTailRegularity.tail_pair_indices {N : ℕ} {ij : ℕ × ℕ} (hij : some ij ∈ SlowResidualMatching.transportIndices N) : ij.1 ≤ N ∧ ij.2 ≤ N

theorem NavierStokes.AxisTailRegularity.transportKernel_axisFactor (h e α : ℝ) (beta u f : ℕ → SimilarityProfile.InnerProfile) (i j : ℕ) {w : SimilarityProfile.InnerPoint} (hX : w.1 ≠ 0) : SlowResidualMatching.transportKernel h e α (fun (n : ℕ) => AxisSourceRegularity.axisFactor (beta n)) u f w i j = regularTransportKernel h e α beta u f w i j

theorem NavierStokes.AxisTailRegularity.radialKernel_axisFactor (h : ℝ) (beta u : ℕ → SimilarityProfile.InnerProfile) (i j : ℕ) {w : SimilarityProfile.InnerPoint} (hb : DifferentiableAt ℝ (beta j) w) : SlowResidualMatching.transportKernel h 0 (-(1 / 2)) (fun (n : ℕ) => AxisSourceRegularity.axisFactor (beta n)) u (fun (n : ℕ) => AxisSourceRegularity.axisFactor (beta n)) w i j = w.1 * regularRadialKernel h beta u w i j

Radial transport is genuinely divisible by X, including at the axis.

theorem NavierStokes.AxisTailRegularity.transportTerm_axisFactor (N : ℕ) (h e α : ℝ) (beta u f : ℕ → SimilarityProfile.InnerProfile) (i : SlowResidualMatching.TailIndex) {w : SimilarityProfile.InnerPoint} (hX : w.1 ≠ 0) : SlowResidualMatching.transportTerm N h e α (fun (n : ℕ) => AxisSourceRegularity.axisFactor (beta n)) u f i w = regularTransportTerm N h e α beta u f i w

theorem NavierStokes.AxisTailRegularity.pressureTerm_axisFactor (N : ℕ) (h C : ℝ) (phi u beta pressure : ℕ → SimilarityProfile.InnerProfile) {w : SimilarityProfile.InnerPoint} (hb : ∀ j ≤ N, ContDiffAt ℝ 2 (beta j) w) (hL : CoordinateAlgebra.L h w.2 ≠ 0) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : SlowResidualMatching.pressureTerm N h C (SlowResidualMatching.ofBeta phi u beta pressure) i w = 2 * w.1 * regularPressureTerm N h C phi u beta i w

All radial pressure branches have the factor 2X before division.

theorem NavierStokes.AxisTailRegularity.pressureTerm_div_axisFactor (N : ℕ) (h C : ℝ) (phi u beta pressure : ℕ → SimilarityProfile.InnerProfile) {w : SimilarityProfile.InnerPoint} (hb : ∀ j ≤ N, ContDiffAt ℝ 2 (beta j) w) (hL : CoordinateAlgebra.L h w.2 ≠ 0) (hX : w.1 ≠ 0) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : SlowResidualMatching.pressureTerm N h C (SlowResidualMatching.ofBeta phi u beta pressure) i w / (2 * w.1) = regularPressureTerm N h C phi u beta i w

theorem NavierStokes.AxisTailRegularity.regularTransportKernel_smoothAt (h e α : ℝ) (beta u f : ℕ → SimilarityProfile.InnerProfile) (i j : ℕ) {w : SimilarityProfile.InnerPoint} (hb : ContDiffAt ℝ (↑⊤) (beta i) w) (hu : ContDiffAt ℝ (↑⊤) (u i) w) (hf : ContDiffAt ℝ (↑⊤) (f j) w) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (fun (y : SimilarityProfile.InnerPoint) => regularTransportKernel h e α beta u f y i j) w

theorem NavierStokes.AxisTailRegularity.regularRadialKernel_smoothAt (h : ℝ) (beta u : ℕ → SimilarityProfile.InnerProfile) (i j : ℕ) {w : SimilarityProfile.InnerPoint} (hbi : ContDiffAt ℝ (↑⊤) (beta i) w) (hbj : ContDiffAt ℝ (↑⊤) (beta j) w) (hu : ContDiffAt ℝ (↑⊤) (u i) w) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (fun (y : SimilarityProfile.InnerPoint) => regularRadialKernel h beta u y i j) w

theorem NavierStokes.AxisTailRegularity.regularTransportTerm_smoothOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h e α : ℝ) (beta u f : ℕ → SimilarityProfile.InnerProfile) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {i : SlowResidualMatching.TailIndex} (hi : i ∈ SlowResidualMatching.transportIndices N) : ContDiffOn ℝ (↑⊤) (regularTransportTerm N h e α beta u f i) O

theorem NavierStokes.AxisTailRegularity.regularPressureTerm_smoothOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h C : ℝ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (hp : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : ContDiffOn ℝ (↑⊤) (regularPressureTerm N h C phi u beta i) O

Local identification with the actual coefficient functions

theorem NavierStokes.AxisTailRegularity.transportKernel_congr_germ (h e α : ℝ) {v u f v' u' f' : ℕ → SimilarityProfile.InnerProfile} (i j : ℕ) {w : SimilarityProfile.InnerPoint} (hv : v i =ᶠ[nhds w] v' i) (hu : u i =ᶠ[nhds w] u' i) (hf : f j =ᶠ[nhds w] f' j) : SlowResidualMatching.transportKernel h e α v u f w i j = SlowResidualMatching.transportKernel h e α v' u' f' w i j

theorem NavierStokes.AxisTailRegularity.transportTerm_congr_germ (N : ℕ) (h e α : ℝ) {v u f v' u' f' : ℕ → SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ∀ j ≤ N, v j =ᶠ[nhds w] v' j) (hu : ∀ j ≤ N, u j =ᶠ[nhds w] u' j) (hf : ∀ j ≤ N, f j =ᶠ[nhds w] f' j) {i : SlowResidualMatching.TailIndex} (hi : i ∈ SlowResidualMatching.transportIndices N) : SlowResidualMatching.transportTerm N h e α v u f i w = SlowResidualMatching.transportTerm N h e α v' u' f' i w

theorem NavierStokes.AxisTailRegularity.pressureTerm_congr_germ (N : ℕ) (h C : ℝ) {f g : SlowExpansionResidual.SlowProfiles} {w : SimilarityProfile.InnerPoint} (hv : ∀ j ≤ N, f.flux j =ᶠ[nhds w] g.flux j) (hu : ∀ j ≤ N, f.axial j =ᶠ[nhds w] g.axial j) (hp : ∀ j ≤ N, f.phi j =ᶠ[nhds w] g.phi j) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : SlowResidualMatching.pressureTerm N h C f i w = SlowResidualMatching.pressureTerm N h C g i w

theorem NavierStokes.AxisTailRegularity.transportTerm_eq_regular_of_germs (N : ℕ) (h e α : ℝ) {v u f beta u' f' : ℕ → SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ∀ j ≤ N, v j =ᶠ[nhds w] AxisSourceRegularity.axisFactor (beta j)) (hu : ∀ j ≤ N, u j =ᶠ[nhds w] u' j) (hf : ∀ j ≤ N, f j =ᶠ[nhds w] f' j) (hX : w.1 ≠ 0) {i : SlowResidualMatching.TailIndex} (hi : i ∈ SlowResidualMatching.transportIndices N) : SlowResidualMatching.transportTerm N h e α v u f i w = regularTransportTerm N h e α beta u' f' i w

Only agreement of the local coefficient germs is required. Global extensions may have different values for negative X.

theorem NavierStokes.AxisTailRegularity.pressureTerm_eq_regular_of_germs (N : ℕ) (h C : ℝ) {f : SlowExpansionResidual.SlowProfiles} {phi u beta : ℕ → SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ∀ j ≤ N, f.flux j =ᶠ[nhds w] AxisSourceRegularity.axisFactor (beta j)) (hu : ∀ j ≤ N, f.axial j =ᶠ[nhds w] u j) (hp : ∀ j ≤ N, f.phi j =ᶠ[nhds w] phi j) (hb : ∀ j ≤ N, ContDiffAt ℝ 2 (beta j) w) (hL : CoordinateAlgebra.L h w.2 ≠ 0) (hX : w.1 ≠ 0) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : SlowResidualMatching.pressureTerm N h C f i w / (2 * w.1) = regularPressureTerm N h C phi u beta i w

theorem NavierStokes.AxisTailRegularity.germ_of_nonnegative_eqOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) {f g : SimilarityProfile.InnerProfile} (hfg : ∀ w ∈ O, 0 ≤ w.1 → f w = g w) {w : SimilarityProfile.InnerPoint} (hw : w ∈ O) (hX : 0 < w.1) : f =ᶠ[nhds w] g

Equality on the nonnegative part of an open set gives the needed germ at every positive radial coordinate. No negative-coordinate matching is used.

theorem NavierStokes.AxisTailRegularity.transportTerm_eq_regular_on_nonnegative {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h e α : ℝ) {v u f beta u' f' : ℕ → SimilarityProfile.InnerProfile} (hv : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → v j w = w.1 * beta j w) (hu : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → u j w = u' j w) (hf : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f j w = f' j w) {w : SimilarityProfile.InnerPoint} (hw : w ∈ O) (hX : 0 < w.1) {i : SlowResidualMatching.TailIndex} (hi : i ∈ SlowResidualMatching.transportIndices N) : SlowResidualMatching.transportTerm N h e α v u f i w = regularTransportTerm N h e α beta u' f' i w

theorem NavierStokes.AxisTailRegularity.pressureTerm_eq_regular_on_nonnegative {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h C : ℝ) {f : SlowExpansionResidual.SlowProfiles} {phi u beta : ℕ → SimilarityProfile.InnerProfile} (hv : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.flux j w = w.1 * beta j w) (hu : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.axial j w = u j w) (hp : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.phi j w = phi j w) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {w : SimilarityProfile.InnerPoint} (hw : w ∈ O) (hX : 0 < w.1) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : SlowResidualMatching.pressureTerm N h C f i w / (2 * w.1) = regularPressureTerm N h C phi u beta i w

The same finite monomials, with regular inner coefficients

theorem NavierStokes.AxisTailRegularity.transportTail_eq_regular_of_germs (N : ℕ) (q h e α : ℝ) {v u f beta u' f' : ℕ → SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ∀ j ≤ N, v j =ᶠ[nhds w] AxisSourceRegularity.axisFactor (beta j)) (hu : ∀ j ≤ N, u j =ᶠ[nhds w] u' j) (hf : ∀ j ≤ N, f j =ᶠ[nhds w] f' j) (hX : w.1 ≠ 0) : SlowExpansionResidual.transportTail N q h e α v u f w = ∑ i ∈ SlowResidualMatching.transportIndices N, q ^ SlowResidualMatching.transportPower N h e i * regularTransportTerm N h e α beta u' f' i w

theorem NavierStokes.AxisTailRegularity.pressureTail_div_eq_regular_of_germs (N : ℕ) (q h C : ℝ) {f : SlowExpansionResidual.SlowProfiles} {phi u beta : ℕ → SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hv : ∀ j ≤ N, f.flux j =ᶠ[nhds w] AxisSourceRegularity.axisFactor (beta j)) (hu : ∀ j ≤ N, f.axial j =ᶠ[nhds w] u j) (hp : ∀ j ≤ N, f.phi j =ᶠ[nhds w] phi j) (hb : ∀ j ≤ N, ContDiffAt ℝ 2 (beta j) w) (hL : CoordinateAlgebra.L h w.2 ≠ 0) (hX : w.1 ≠ 0) : SlowExpansionResidual.pressureTail N q h C f w / (2 * w.1) = ∑ i ∈ SlowResidualMatching.pressureIndices N, q ^ SlowResidualMatching.pressurePower N h i * regularPressureTerm N h C phi u beta i w

theorem NavierStokes.AxisTailRegularity.radialTail_eq_regular_of_germs {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) {f : SlowExpansionResidual.SlowProfiles} {phi u beta : ℕ → SimilarityProfile.InnerProfile} {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hv : ∀ j ≤ N, f.flux j =ᶠ[nhds (SimilarityProfile.inner h p)] AxisSourceRegularity.axisFactor (beta j)) (hu : ∀ j ≤ N, f.axial j =ᶠ[nhds (SimilarityProfile.inner h p)] u j) (hphi : ∀ j ≤ N, f.phi j =ᶠ[nhds (SimilarityProfile.inner h p)] phi j) (hb : ∀ j ≤ N, ContDiffAt ℝ 2 (beta j) (SimilarityProfile.inner h p)) (hL : CoordinateAlgebra.L h (SimilarityProfile.inner h p).2 ≠ 0) : SlowExpansionResidual.pressureTail N (SimilarityProfile.q h p) h C f (SimilarityProfile.inner h p) / (2 * p.2.1) = ∑ i ∈ SlowResidualMatching.pressureIndices N, SimilarityProfile.q h p ^ (SlowResidualMatching.pressurePower N h i - 1) * regularPressureTerm N h C phi u beta i (SimilarityProfile.inner h p)

The physical radial denominator contributes precisely the original single power of q. Regularizing X costs no further power.

theorem NavierStokes.AxisTailRegularity.angular_power_lower {h : ℝ} (hh : 0 ≤ h) (N : ℕ) {i : SlowResidualMatching.TailIndex} (hi : i ∈ SlowResidualMatching.transportIndices N) : 2 * ↑N * h - 2 ≤ SlowResidualMatching.transportPower N h (SlowExpansionResidual.angularExponent h) i

theorem NavierStokes.AxisTailRegularity.axial_power_lower {h : ℝ} (hh : 0 ≤ h) (N : ℕ) {i : SlowResidualMatching.TailIndex} (hi : i ∈ SlowResidualMatching.transportIndices N) : 2 * ↑N * h - 2 ≤ SlowResidualMatching.transportPower N h (SlowExpansionResidual.axialExponent h) i

theorem NavierStokes.AxisTailRegularity.radial_power_lower {h : ℝ} (hh : 0 ≤ h) (N : ℕ) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : 2 * ↑N * h - 2 ≤ SlowResidualMatching.pressurePower N h i - 1

Actual smoothness through X = 0 and even radial pullbacks

theorem NavierStokes.AxisTailRegularity.radiusPoint_contDiff : ContDiff ℝ (↑⊤) SlowResidualMatching.radiusPoint

theorem NavierStokes.AxisTailRegularity.toRadius_smoothOn {O : Set SimilarityProfile.InnerPoint} {f : SimilarityProfile.InnerProfile} (hf : ContDiffOn ℝ (↑⊤) f O) : ContDiffOn ℝ (↑⊤) (SlowResidualMatching.toRadius f) (SlowResidualMatching.radiusPoint ⁻¹' O)

theorem NavierStokes.AxisTailRegularity.toRadius_even (f : SimilarityProfile.InnerProfile) (R η : ℝ) : SlowResidualMatching.toRadius f (-R, η) = SlowResidualMatching.toRadius f (R, η)

theorem NavierStokes.AxisTailRegularity.regularTransportTerm_right_smoothOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h e α : ℝ) (beta u f : ℕ → SimilarityProfile.InnerProfile) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {i : SlowResidualMatching.TailIndex} (hi : i ∈ SlowResidualMatching.transportIndices N) : ContDiffOn ℝ (↑⊤) (regularTransportTerm N h e α beta u f i) (O ∩ {w : SimilarityProfile.InnerPoint | 0 ≤ w.1})

theorem NavierStokes.AxisTailRegularity.regularPressureTerm_right_smoothOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h C : ℝ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (hp : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : ContDiffOn ℝ (↑⊤) (regularPressureTerm N h C phi u beta i) (O ∩ {w : SimilarityProfile.InnerPoint | 0 ≤ w.1})

theorem NavierStokes.AxisTailRegularity.regularTransportTerm_radial_smoothOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h e α : ℝ) (beta u f : ℕ → SimilarityProfile.InnerProfile) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {i : SlowResidualMatching.TailIndex} (hi : i ∈ SlowResidualMatching.transportIndices N) : ContDiffOn ℝ (↑⊤) (SlowResidualMatching.toRadius (regularTransportTerm N h e α beta u f i)) (SlowResidualMatching.radiusPoint ⁻¹' O)

theorem NavierStokes.AxisTailRegularity.regularPressureTerm_radial_smoothOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h C : ℝ) (phi u beta : ℕ → SimilarityProfile.InnerProfile) (hp : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {i : SlowResidualMatching.PressureIndex} (hi : i ∈ SlowResidualMatching.pressureIndices N) : ContDiffOn ℝ (↑⊤) (SlowResidualMatching.toRadius (regularPressureTerm N h C phi u beta i)) (SlowResidualMatching.radiusPoint ⁻¹' O)

theorem NavierStokes.BaseResidual.slowSum_eq_leading_of_positive_zero {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h q : ℝ) {f : ℕ → SlowBorelBase.Inner → V} {w : SlowBorelBase.Inner} (hz : ∀ (j : ℕ), 0 < j → f j w = 0) : SlowBorelBase.slowSum a h f (q, w) = f 0 w

Zero positive-order coefficient values are preserved by the actual sum, irrespective of the cutoff schedule.

theorem NavierStokes.BaseResidual.physicalChart_origin {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {t : ℝ} (ht : t < 1) : SlowBorelBase.physicalChart h (t, 0, 0) = (1 - t, 0, 0)

At the spatial origin the physical similarity coordinates have their exact values; this is not an asymptotic coordinate comparison.

theorem NavierStokes.BaseResidual.baseVelocity_at_origin {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) (hz : ∀ (j : ℕ), 0 < j → d.axial j (0, 0) = 0) {t : ℝ} (ht : t < 1) : SlowBorelBase.baseVelocity a h C d (t, 0) = ((1 - t) ^ (-CoordinateAlgebra.A h) * d.axial 0 (0, 0)) • ProblemStatement.coordinateVector 2

Summing and cutting the streams before differentiation preserves the leading axial value exactly when the positive axial axis constants vanish.

theorem NavierStokes.BaseResidual.baseVelocity_norm_at_origin {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) (hz : ∀ (j : ℕ), 0 < j → d.axial j (0, 0) = 0) (h0 : 0 < d.axial 0 (0, 0)) {t : ℝ} (ht : t < 1) : ‖SlowBorelBase.baseVelocity a h C d (t, 0)‖ = (1 - t) ^ (-CoordinateAlgebra.A h) * d.axial 0 (0, 0)

theorem NavierStokes.BaseResidual.baseVelocity_axis_tendsto_atTop {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) (hz : ∀ (j : ℕ), 0 < j → d.axial j (0, 0) = 0) (h0 : 0 < d.axial 0 (0, 0)) : Filter.Tendsto (fun (t : ℝ) => ‖SlowBorelBase.baseVelocity a h C d (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

The concrete Borel base retains the leading axial blow-up. No agreement with an unspecified limiting field is an input.

theorem NavierStokes.BaseResidual.baseVelocity_speedUnbounded {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) (hz : ∀ (j : ℕ), 0 < j → d.axial j (0, 0) = 0) (h0 : 0 < d.axial 0 (0, 0)) : ProblemStatement.SpeedUnboundedAtOne (SlowBorelBase.baseVelocity a h C d)

noncomputable def NavierStokes.BaseResidual.monomialLift (a b : ℝ) (f : SlowBorelBase.Inner → ℝ) (y : SlowBorelBase.Chart) : ℝ

The homogeneous lift is defined before solving the implicit coordinate equation. This makes its degree an exact scaling identity.

Equations

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

theorem NavierStokes.BaseResidual.monomialLift_smooth {f : SlowBorelBase.Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) (a b : ℝ) : ContDiffOn ℝ (↑⊤) (monomialLift a b f) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.BaseResidual.monomialLift_homogeneous (a b : ℝ) (f : SlowBorelBase.Inner → ℝ) {r : ℝ} (hr : 0 < r) {y : SlowBorelBase.Chart} (hy : y ∈ PhysicalCoordinateBounds.positiveTime) : monomialLift a b f ((PhysicalCoordinateBounds.dilation a r) y) = r ^ b * monomialLift a b f y

theorem NavierStokes.BaseResidual.pullback_eq_homogeneous (h b : ℝ) (f : SlowBorelBase.Inner → ℝ) : SimilarityProfile.pullback h b f = (monomialLift (2 * h) b f ∘ PhysicalCoordinateBounds.inverseCoordinates (2 * h)) ∘ PhysicalCoordinateBounds.timeShift

theorem NavierStokes.BaseResidual.physical_monomial_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) (b lo hi qbig : ℝ) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : SlowBorelBase.Chart), p.1 < 1 → (SlowBorelBase.physicalChart h p).1 ≤ qbig → (SlowBorelBase.physicalChart h p).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m (SimilarityProfile.pullback h b f) p‖ ≤ C * (SlowBorelBase.physicalChart h p).1 ^ (b - ↑m)

Every smooth inner monomial has actual physical jets with a loss of one power per derivative. The constant is derived by compactness and scaling.

theorem NavierStokes.BaseResidual.exists_local_coefficient_extension {U K : Set SlowBorelBase.Inner} (hU : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) : ∃ (F : SlowBorelBase.Inner → ℝ), ContDiff ℝ (↑⊤) F ∧ ∀ w ∈ K, f =ᶠ[nhds w] F

A local smooth coefficient has a genuine smooth extension on a neighborhood of a compact set. This is used only to estimate its local jets.

theorem NavierStokes.BaseResidual.physical_monomial_bound_on {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {U K : Set SlowBorelBase.Inner} (hU : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (b lo hi qbig : ℝ) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : SlowBorelBase.Chart), p.1 < 1 → (SlowBorelBase.physicalChart h p).1 ≤ qbig → (SlowBorelBase.physicalChart h p).2.1 ∈ Set.Icc lo hi → (SlowBorelBase.physicalChart h p).2 ∈ K → ‖iteratedFDeriv ℝ m (SimilarityProfile.pullback h b f) p‖ ≤ C * (SlowBorelBase.physicalChart h p).1 ^ (b - ↑m)

Local coefficient regularity suffices for the physical estimate. All coefficients with 1/X or 1/L may therefore stay on their true domain.

noncomputable def NavierStokes.BaseResidual.cartesianMonomial (h b : ℝ) (f : SlowBorelBase.Inner → ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Cartesian monomial, given by SimilarityProfile.pullback h b f (AxisymmetricFields.profilePoint z.1 z.2).

Equations

• NavierStokes.BaseResidual.cartesianMonomial h b f z = NavierStokes.SimilarityProfile.pullback h b f (NavierStokes.AxisymmetricFields.profilePoint z.1 z.2)

theorem NavierStokes.BaseResidual.cartesianMonomial_smoothAt {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SlowBorelBase.Inner → ℝ} {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hf : ContDiffAt ℝ (↑⊤) f (SlowBorelBase.cartesianChart h z).2) : ContDiffAt ℝ (↑⊤) (cartesianMonomial h b f) z

theorem NavierStokes.BaseResidual.physical_monomial_finite_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) (b lo hi : ℝ) (M : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (p : SlowBorelBase.Chart), p.1 < 1 → (SlowBorelBase.physicalChart h p).1 ≤ 1 → (SlowBorelBase.physicalChart h p).2.1 ∈ Set.Icc lo hi → ∀ m ≤ M, ‖iteratedFDeriv ℝ m (SimilarityProfile.pullback h b f) p‖ ≤ C * (SlowBorelBase.physicalChart h p).1 ^ (b - ↑M)

theorem NavierStokes.BaseResidual.cartesian_monomial_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiff ℝ (↑⊤) f) (b lo hi : ℝ) {K : Set ProblemStatement.SpaceTime} (hK : IsCompact K) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ z ∈ K, z.1 < 1 → (SlowBorelBase.cartesianChart h z).1 ≤ 1 → (SlowBorelBase.cartesianChart h z).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m (cartesianMonomial h b f) z‖ ≤ C * (SlowBorelBase.cartesianChart h z).1 ^ (b - ↑m)

On a fixed compact Cartesian set, polynomial reconstruction from squared radius adds a constant but no further loss of powers.

theorem NavierStokes.BaseResidual.cartesian_monomial_bound_on {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {U K : Set SlowBorelBase.Inner} (hU : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (b lo hi : ℝ) {B : Set ProblemStatement.SpaceTime} (hB : IsCompact B) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ z ∈ B, z.1 < 1 → (SlowBorelBase.cartesianChart h z).1 ≤ 1 → (SlowBorelBase.cartesianChart h z).2.1 ∈ Set.Icc lo hi → (SlowBorelBase.cartesianChart h z).2 ∈ K → ‖iteratedFDeriv ℝ m (cartesianMonomial h b f) z‖ ≤ C * (SlowBorelBase.cartesianChart h z).1 ^ (b - ↑m)

theorem NavierStokes.BaseResidual.norm_jet_sum_le {D : Type u_1} {V : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_3} (s : Finset ι) (f : ι → D → V) {x : D} (hf : ∀ i ∈ s, ContDiffAt ℝ (↑⊤) (f i) x) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : D) => ∑ i ∈ s, f i y) x‖ ≤ ∑ i ∈ s, ‖iteratedFDeriv ℝ m (f i) x‖

theorem NavierStokes.BaseResidual.cartesian_finite_monomials_bound {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {U K : Set SlowBorelBase.Inner} (hU : IsOpen U) (hK : IsCompact K) (hKU : K ⊆ U) {ι : Type u_1} [Fintype ι] (f : ι → SlowBorelBase.Inner → ℝ) (hf : ∀ (i : ι), ContDiffOn ℝ (↑⊤) (f i) U) (b : ι → ℝ) (bmin lo hi : ℝ) (hmin : ∀ (i : ι), bmin ≤ b i) {B : Set ProblemStatement.SpaceTime} (hB : IsCompact B) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ z ∈ B, z.1 < 1 → (SlowBorelBase.cartesianChart h z).1 ≤ 1 → (SlowBorelBase.cartesianChart h z).2.1 ∈ Set.Icc lo hi → (SlowBorelBase.cartesianChart h z).2 ∈ K → ‖iteratedFDeriv ℝ m (fun (y : ProblemStatement.SpaceTime) => ∑ i : ι, cartesianMonomial h (b i) (f i) y) z‖ ≤ C * (SlowBorelBase.cartesianChart h z).1 ^ (bmin - ↑m)

A finite family of genuine local coefficient functions yields the expected power bound for every actual Cartesian jet of its sum.

structure NavierStokes.BaseResidual.PhysicalApproach (l : Filter ProblemStatement.SpaceTime) (h lo hi : ℝ) : Type

The filter carries only geometric information: bounded physical coordinates, a fixed inner radial window, and scale tending to zero.

• carrier : Set ProblemStatement.SpaceTime

  Carrier of PhysicalApproach, of type Set SpaceTime.

• compact : IsCompact self.carrier
• in_carrier : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ self.carrier
• past : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z.1 < 1
• radial : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, (SlowBorelBase.cartesianChart h z).2.1 ∈ Set.Icc lo hi
• scale : Filter.Tendsto (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) l (nhds 0)

theorem NavierStokes.BaseResidual.PhysicalApproach.small {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (A : PhysicalApproach l h lo hi) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, (SlowBorelBase.cartesianChart h z).1 < δ

theorem NavierStokes.BaseResidual.PhysicalApproach.positive_small {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (A : PhysicalApproach l h lo hi) (hh : 0 < h) (hh1 : h < 1 / 2) : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < (SlowBorelBase.cartesianChart h z).1 ∧ (SlowBorelBase.cartesianChart h z).1 ≤ 1

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

theorem NavierStokes.BaseResidual.cartesian_prefix_finiteJetRate {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {f : ℕ → SlowBorelBase.Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) (ha : SlowBorelBase.AdmissibleScales h f (SlowBorelBase.innerBox lo hi) a) (J M : ℕ) (hM : M ≤ J + 3) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => SlowBorelBase.cartesianProfile a h b f z - SlowBorelBase.cartesianUncutPrefix h b f J z) M (h * (↑J + 1) + b - 2 * ↑M)

theorem NavierStokes.BaseResidual.finiteRate_mono {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {M N : ℕ} {r : ℝ} (hf : DiagonalResidual.FiniteJetRate l q f M r) (hNM : N ≤ M) : DiagonalResidual.FiniteJetRate l q f N r

theorem NavierStokes.BaseResidual.finiteRate_at {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {M m : ℕ} {r : ℝ} (hf : DiagonalResidual.FiniteJetRate l q f M r) (hm : m ≤ M) : DiagonalResidual.JetRate l q f m r

theorem NavierStokes.BaseResidual.finiteRate_weaken {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {M : ℕ} {r s : ℝ} (hf : DiagonalResidual.FiniteJetRate l q f M r) (hq : ∀ᶠ (x : D) in l, 0 < q x ∧ q x ≤ 1) (hsr : s ≤ r) : DiagonalResidual.FiniteJetRate l q f M s

theorem NavierStokes.BaseResidual.finiteRate_congr_on {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f g : D → E} {M : ℕ} {r : ℝ} {U : Set D} (hf : DiagonalResidual.FiniteJetRate l q f M r) (hU : IsOpen U) (hlU : ∀ᶠ (x : D) in l, x ∈ U) (hfg : Set.EqOn f g U) : DiagonalResidual.FiniteJetRate l q g M r

theorem NavierStokes.BaseResidual.finiteRate_linear {D E F : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {l : Filter D} {q : D → ℝ} {f : D → E} {M : ℕ} {r : ℝ} {U : Set D} (hf : DiagonalResidual.FiniteJetRate l q f M r) (hU : IsOpen U) (hlU : ∀ᶠ (x : D) in l, x ∈ U) (hs : ContDiffOn ℝ (↑⊤) f U) (L : E →L[ℝ] F) : DiagonalResidual.FiniteJetRate l q (fun (x : D) => L (f x)) M r

theorem NavierStokes.BaseResidual.finiteRate_add {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f g : D → E} {M : ℕ} {r : ℝ} {U : Set D} (hf : DiagonalResidual.FiniteJetRate l q f M r) (hg : DiagonalResidual.FiniteJetRate l q g M r) (hU : IsOpen U) (hlU : ∀ᶠ (x : D) in l, x ∈ U) (hsf : ContDiffOn ℝ (↑⊤) f U) (hsg : ContDiffOn ℝ (↑⊤) g U) : DiagonalResidual.FiniteJetRate l q (fun (x : D) => f x + g x) M r

theorem NavierStokes.BaseResidual.finiteRate_bilinear {D E F G : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {l : Filter D} {q : D → ℝ} {f : D → E} {g : D → F} {M : ℕ} {r s : ℝ} {U : Set D} (hf : DiagonalResidual.FiniteJetRate l q f M r) (hg : DiagonalResidual.FiniteJetRate l q g M s) (hU : IsOpen U) (hlU : ∀ᶠ (x : D) in l, x ∈ U) (hq : ∀ᶠ (x : D) in l, 0 < q x) (hsf : ContDiffOn ℝ (↑⊤) f U) (hsg : ContDiffOn ℝ (↑⊤) g U) (L : E →L[ℝ] F →L[ℝ] G) : DiagonalResidual.FiniteJetRate l q (fun (x : D) => (L (f x)) (g x)) M (r + s)

theorem NavierStokes.BaseResidual.finiteRate_fderiv {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {M : ℕ} {r : ℝ} (hf : DiagonalResidual.FiniteJetRate l q f (M + 1) r) : DiagonalResidual.FiniteJetRate l q (fderiv ℝ f) M r

theorem NavierStokes.BaseResidual.finiteRate_compact {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : Filter D} {q : D → ℝ} {f : D → E} {K : Set D} (hf : ContDiff ℝ (↑⊤) f) (hK : IsCompact K) (hlK : ∀ᶠ (x : D) in l, x ∈ K) (M : ℕ) : DiagonalResidual.FiniteJetRate l q f M 0

noncomputable def NavierStokes.BaseResidual.past : Set ProblemStatement.SpaceTime

Past, given by Iio 1 ×ˢ univ.

Equations

• NavierStokes.BaseResidual.past = Set.Iio 1 ×ˢ Set.univ

noncomputable def NavierStokes.BaseResidual.profilePast : Set SlowBorelBase.Chart

Profile past, given by Iio 1 ×ˢ univ.

Equations

• NavierStokes.BaseResidual.profilePast = Set.Iio 1 ×ˢ Set.univ

theorem NavierStokes.BaseResidual.past_isOpen : IsOpen past

theorem NavierStokes.BaseResidual.profilePast_isOpen : IsOpen profilePast

noncomputable def NavierStokes.BaseResidual.potentialFromScalars (H K : ProblemStatement.SpaceTime → ℝ) (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

Potential from scalars, given by (-(1 / 2 : ℝ) * z.2 1 * H z) • coordinateVector 0 + ((1 / 2 : ℝ) * z.2 0 * H z) • coordinateVector 1 + K z • coordinateVector 2.

Equations

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

noncomputable def NavierStokes.BaseResidual.basisInjection (i : Fin 3) : ℝ →L[ℝ] ProblemStatement.Space

Basis injection, given by (ContinuousLinearMap.id ℝ ℝ).smulRight (coordinateVector i).

Equations

• NavierStokes.BaseResidual.basisInjection i = (ContinuousLinearMap.id ℝ ℝ).smulRight (NavierStokes.ProblemStatement.coordinateVector i)

theorem NavierStokes.BaseResidual.potentialFromScalars_smooth {H K : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} (hH : ContDiffOn ℝ (↑⊤) H U) (hK : ContDiffOn ℝ (↑⊤) K U) : ContDiffOn ℝ (↑⊤) (potentialFromScalars H K) U

theorem NavierStokes.BaseResidual.potentialFromScalars_sub (H K H' K' : ProblemStatement.SpaceTime → ℝ) : (fun (z : ProblemStatement.SpaceTime) => potentialFromScalars H K z - potentialFromScalars H' K' z) = potentialFromScalars (fun (z : ProblemStatement.SpaceTime) => H z - H' z) fun (z : ProblemStatement.SpaceTime) => K z - K' z

theorem NavierStokes.BaseResidual.potential_eq_scalars (H K : SlowBorelBase.Chart → ℝ) : AxisymmetricFields.potential H K = potentialFromScalars (fun (z : ProblemStatement.SpaceTime) => H (AxisymmetricFields.profilePoint z.1 z.2)) fun (z : ProblemStatement.SpaceTime) => K (AxisymmetricFields.profilePoint z.1 z.2)

theorem NavierStokes.BaseResidual.potentialFromScalars_rate {l : Filter ProblemStatement.SpaceTime} {q H K : ProblemStatement.SpaceTime → ℝ} {U B : Set ProblemStatement.SpaceTime} {M : ℕ} {r : ℝ} (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z) (hB : IsCompact B) (hlB : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ B) (hH : ContDiffOn ℝ (↑⊤) H U) (hK : ContDiffOn ℝ (↑⊤) K U) (hrH : DiagonalResidual.FiniteJetRate l q H M r) (hrK : DiagonalResidual.FiniteJetRate l q K M r) : DiagonalResidual.FiniteJetRate l q (potentialFromScalars H K) M r

noncomputable def NavierStokes.BaseResidual.prefixStream (J : ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : SlowBorelBase.Chart → ℝ

Prefix stream, given by physicalUncutPrefix h (-CoordinateAlgebra.A h) (bundleComponent C d 0) J.

Equations

• NavierStokes.BaseResidual.prefixStream J h C d = NavierStokes.SlowBorelBase.physicalUncutPrefix h (-NavierStokes.CoordinateAlgebra.A h) (NavierStokes.SlowBorelBase.bundleComponent C d 0) J

noncomputable def NavierStokes.BaseResidual.prefixSwirl (J : ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : SlowBorelBase.Chart → ℝ

Prefix swirl, given by physicalUncutPrefix h (1 / 2 - CoordinateAlgebra.A h) (bundleComponent C d 1) J.

Equations

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

noncomputable def NavierStokes.BaseResidual.prefixPotential (J : ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.VelocityField

Prefix potential, given by AxisymmetricFields.potential (prefixStream J h C d) (prefixSwirl J h C d).

Equations

• NavierStokes.BaseResidual.prefixPotential J h C d = NavierStokes.AxisymmetricFields.potential (NavierStokes.BaseResidual.prefixStream J h C d) (NavierStokes.BaseResidual.prefixSwirl J h C d)

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

Summed potential, given by AxisymmetricFields.potential (streamFactor a h C d) (swirlPotential a h C d).

Equations

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

noncomputable def NavierStokes.BaseResidual.prefixVelocity (J : ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.VelocityField

Prefix velocity, given by SpatialCurl.spatialCurl (prefixPotential J h C d).

Equations

• NavierStokes.BaseResidual.prefixVelocity J h C d = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.BaseResidual.prefixPotential J h C d)

noncomputable def NavierStokes.BaseResidual.prefixPressure (J : ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.PressureField

Prefix pressure, given by cartesianUncutPrefix h (-2 * CoordinateAlgebra.A h) (bundleComponent C d 2) J.

Equations

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

theorem NavierStokes.BaseResidual.cartesianProfile_smooth {a : ℕ → ℕ} (ha : StrictMono a) {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → SlowBorelBase.Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) : ContDiffOn ℝ (↑⊤) (SlowBorelBase.cartesianProfile a h b f) past

theorem NavierStokes.BaseResidual.cartesianUncutPrefix_smooth {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → SlowBorelBase.Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (J : ℕ) : ContDiffOn ℝ (↑⊤) (SlowBorelBase.cartesianUncutPrefix h b f J) past

theorem NavierStokes.BaseResidual.summedPotential_smooth {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (summedPotential a h C d) past

theorem NavierStokes.BaseResidual.prefixPotential_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J : ℕ) (C : ℝ) : ContDiffOn ℝ (↑⊤) (prefixPotential J h C d) past

theorem NavierStokes.BaseResidual.potential_prefix_rate {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (J M : ℕ) (hM : M ≤ J + 3) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => summedPotential a h C d z - prefixPotential J h C d z) M (h * (↑J + 1) - CoordinateAlgebra.A h - 2 * ↑M)

Both potentials share the same derived cutoff schedule. Their difference from a fixed prefix has a finite order increasing with the prefix.

theorem NavierStokes.BaseResidual.spatialCurl_eq_full {F : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (hF : DifferentiableAt ℝ F z) : SpatialCurl.spatialCurl F z = (SpatialCurl.curlLinear ∘SL ResidualStability.spaceRestriction ProblemStatement.Space) (fderiv ℝ F z)

theorem NavierStokes.BaseResidual.spatialCurl_sub {F G : ProblemStatement.VelocityField} {z : ProblemStatement.SpaceTime} (hF : DifferentiableAt ℝ F z) (hG : DifferentiableAt ℝ G z) : SpatialCurl.spatialCurl (fun (y : ProblemStatement.SpaceTime) => F y - G y) z = SpatialCurl.spatialCurl F z - SpatialCurl.spatialCurl G z

theorem NavierStokes.BaseResidual.spatialCurl_finiteRate {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {F : ProblemStatement.VelocityField} {U : Set ProblemStatement.SpaceTime} {M : ℕ} {r : ℝ} (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hF : ContDiffOn ℝ (↑⊤) F U) (hr : DiagonalResidual.FiniteJetRate l q F (M + 1) r) : DiagonalResidual.FiniteJetRate l q (SpatialCurl.spatialCurl F) M r

theorem NavierStokes.BaseResidual.prefixVelocity_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J : ℕ) (C : ℝ) : ContDiffOn ℝ (↑⊤) (prefixVelocity J h C d) past

theorem NavierStokes.BaseResidual.velocity_prefix_rate {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (J M : ℕ) (hM : M + 1 ≤ J + 3) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => SlowBorelBase.baseVelocity a h C d z - prefixVelocity J h C d z) M (h * (↑J + 1) - CoordinateAlgebra.A h - 2 * (↑M + 1))

theorem NavierStokes.BaseResidual.pressure_prefix_rate {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (J M : ℕ) (hM : M ≤ J + 3) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => SlowBorelBase.basePressure a h C d z - prefixPressure J h C d z) M (h * (↑J + 1) - 2 * CoordinateAlgebra.A h - 2 * ↑M)

theorem NavierStokes.BaseResidual.cartesianUncutPrefix_eq_sum {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (b : ℝ) (f : ℕ → SlowBorelBase.Inner → ℝ) (J : ℕ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) : SlowBorelBase.cartesianUncutPrefix h b f J z = ∑ i : Fin (J + 1), cartesianMonomial h (b + SlowExpansionResidual.slowOrder h ↑i) (f ↑i) z

theorem NavierStokes.BaseResidual.cartesian_prefix_growth {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {f : ℕ → SlowBorelBase.Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) (J M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (SlowBorelBase.cartesianUncutPrefix h b f J) M (b - ↑M)

theorem NavierStokes.BaseResidual.prefixPotential_growth {l : Filter ProblemStatement.SpaceTime} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (prefixPotential J h C d) M (-CoordinateAlgebra.A h - ↑M)

theorem NavierStokes.BaseResidual.prefixVelocity_growth {l : Filter ProblemStatement.SpaceTime} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (prefixVelocity J h C d) M (-CoordinateAlgebra.A h - (↑M + 1))

noncomputable def NavierStokes.BaseResidual.profileDerivative (v : SlowBorelBase.Chart) (F : SlowBorelBase.Chart → ℝ) (p : SlowBorelBase.Chart) : ℝ

Profile derivative, given by fderiv ℝ F p v.

Equations

• NavierStokes.BaseResidual.profileDerivative v F p = (fderiv ℝ F p) v

noncomputable def NavierStokes.BaseResidual.cartesianDerivative (v : SlowBorelBase.Chart) (F : SlowBorelBase.Chart → ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Cartesian derivative, given by profileDerivative v F (AxisymmetricFields.profilePoint z.1 z.2).

Equations

• NavierStokes.BaseResidual.cartesianDerivative v F z = NavierStokes.BaseResidual.profileDerivative v F (NavierStokes.AxisymmetricFields.profilePoint z.1 z.2)

theorem NavierStokes.BaseResidual.profileDerivative_smooth {F : SlowBorelBase.Chart → ℝ} (hF : ContDiffOn ℝ (↑⊤) F profilePast) (v : SlowBorelBase.Chart) : ContDiffOn ℝ (↑⊤) (profileDerivative v F) profilePast

theorem NavierStokes.BaseResidual.cartesianDerivative_smooth {F : SlowBorelBase.Chart → ℝ} (hF : ContDiffOn ℝ (↑⊤) F profilePast) (v : SlowBorelBase.Chart) : ContDiffOn ℝ (↑⊤) (cartesianDerivative v F) past

theorem NavierStokes.BaseResidual.derivative_fixed_prefix_bound {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → SlowBorelBase.Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (lo hi b : ℝ) (ha : SlowBorelBase.AdmissibleScales h f (SlowBorelBase.innerBox lo hi) a) {K : Set ProblemStatement.SpaceTime} (hK : IsCompact K) (v : SlowBorelBase.Chart) (J m : ℕ) (hm : m + 1 ≤ J + 3) : ∃ (δ : ℝ) (C : ℝ), 0 < δ ∧ 0 < C ∧ ∀ z ∈ K, z.1 < 1 → (SlowBorelBase.cartesianChart h z).1 < δ → (SlowBorelBase.cartesianChart h z).2.1 ∈ Set.Icc lo hi → ‖iteratedFDeriv ℝ m (cartesianDerivative v fun (p : SlowBorelBase.Chart) => SlowBorelBase.physicalProfile a h b f p - SlowBorelBase.physicalUncutPrefix h b f J p) z‖ ≤ C * (SlowBorelBase.cartesianChart h z).1 ^ (h * (↑J + 1) + b - 2 * (↑m + 1))

A physical derivative of the actual profile remainder is estimated before the polynomial Cartesian coordinate map is applied.

theorem NavierStokes.BaseResidual.derivative_prefix_rate {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {f : ℕ → SlowBorelBase.Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) (ha : SlowBorelBase.AdmissibleScales h f (SlowBorelBase.innerBox lo hi) a) (v : SlowBorelBase.Chart) (J M : ℕ) (hM : M + 1 ≤ J + 3) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (cartesianDerivative v fun (p : SlowBorelBase.Chart) => SlowBorelBase.physicalProfile a h b f p - SlowBorelBase.physicalUncutPrefix h b f J p) M (h * (↑J + 1) + b - 2 * (↑M + 1))

noncomputable def NavierStokes.BaseResidual.annularPast : Set ProblemStatement.SpaceTime

Annular past, given by {z | z.1 < 1 ∧ 0 < AxisymmetricFields.radialEnergy z.2}.

Equations

• NavierStokes.BaseResidual.annularPast = {z : NavierStokes.ProblemStatement.SpaceTime | z.1 < 1 ∧ 0 < NavierStokes.AxisymmetricFields.radialEnergy z.2}

theorem NavierStokes.BaseResidual.annularPast_isOpen : IsOpen annularPast

theorem NavierStokes.BaseResidual.annularPast_subset : annularPast ⊆ past

theorem NavierStokes.BaseResidual.PhysicalApproach.in_annularPast {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (A : PhysicalApproach l h lo hi) (hh : 0 < h) (hh1 : h < 1 / 2) (hlo : 0 < lo) : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ annularPast

theorem NavierStokes.BaseResidual.monomial_finiteRate_on {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {U : Set SlowBorelBase.Inner} (hU : IsOpen U) (hKU : SlowBorelBase.innerBox lo hi ⊆ U) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (b : ℝ) (M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (cartesianMonomial h b f) M (b - ↑M)

noncomputable def NavierStokes.BaseResidual.radialPower (c : ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Radial power, given by (2 * AxisymmetricFields.radialEnergy z.2) ^ c.

Equations

• NavierStokes.BaseResidual.radialPower c z = (2 * NavierStokes.AxisymmetricFields.radialEnergy z.2) ^ c

theorem NavierStokes.BaseResidual.radialPower_smooth (c : ℝ) : ContDiffOn ℝ (↑⊤) (radialPower c) annularPast

theorem NavierStokes.BaseResidual.radialPower_eq_monomial {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (c : ℝ) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) : radialPower c z = cartesianMonomial h c (fun (w : SlowBorelBase.Inner) => (2 * w.1) ^ c) z

theorem NavierStokes.BaseResidual.radialPower_rate {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) (hlo : 0 < lo) (c : ℝ) (M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (radialPower c) M (c - ↑M)

noncomputable def NavierStokes.BaseResidual.stressForce (theta axial : SlowBorelBase.Chart → ℝ) (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

The manuscript's tangential radial stress operator.

Equations

• NavierStokes.BaseResidual.stressForce theta axial z = NavierStokes.SlowResidualMatching.tangentialStressForce theta axial z.1 z.2

noncomputable def NavierStokes.BaseResidual.liftProfile (F : SlowBorelBase.Chart → ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Lift profile, given by F (AxisymmetricFields.profilePoint z.1 z.2).

Equations

• NavierStokes.BaseResidual.liftProfile F z = F (NavierStokes.AxisymmetricFields.profilePoint z.1 z.2)

noncomputable def NavierStokes.BaseResidual.stressAngularScalar (theta : SlowBorelBase.Chart → ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Stress angular scalar, given by -2 * (cartesianDerivative (0, (1, 0)) theta z + 2 * radialPower (-1) z * liftProfile theta z).

Equations

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

noncomputable def NavierStokes.BaseResidual.stressAxialScalar (axial : SlowBorelBase.Chart → ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Stress axial scalar, given by -(radialPower (1 / 2) z * cartesianDerivative (0, (1, 0)) axial z + radialPower (-(1 / 2)) z * liftProfile axial z).

Equations

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

theorem NavierStokes.BaseResidual.liftProfile_smooth {F : SlowBorelBase.Chart → ℝ} (hF : ContDiffOn ℝ (↑⊤) F profilePast) : ContDiffOn ℝ (↑⊤) (liftProfile F) past

theorem NavierStokes.BaseResidual.stressForce_eq_scalars (theta axial : SlowBorelBase.Chart → ℝ) {z : ProblemStatement.SpaceTime} (hs : 0 < AxisymmetricFields.radialEnergy z.2) : stressForce theta axial z = potentialFromScalars (stressAngularScalar theta) (stressAxialScalar axial) z

theorem NavierStokes.BaseResidual.stressForce_smooth {theta axial : SlowBorelBase.Chart → ℝ} (ht : ContDiffOn ℝ (↑⊤) theta profilePast) (ha : ContDiffOn ℝ (↑⊤) axial profilePast) : ContDiffOn ℝ (↑⊤) (stressForce theta axial) annularPast

theorem NavierStokes.BaseResidual.stressForce_sub {theta axial theta' axial' : SlowBorelBase.Chart → ℝ} {z : ProblemStatement.SpaceTime} (ht : DifferentiableAt ℝ theta (AxisymmetricFields.profilePoint z.1 z.2)) (ha : DifferentiableAt ℝ axial (AxisymmetricFields.profilePoint z.1 z.2)) (ht' : DifferentiableAt ℝ theta' (AxisymmetricFields.profilePoint z.1 z.2)) (ha' : DifferentiableAt ℝ axial' (AxisymmetricFields.profilePoint z.1 z.2)) : stressForce (fun (p : SlowBorelBase.Chart) => theta p - theta' p) (fun (p : SlowBorelBase.Chart) => axial p - axial' p) z = stressForce theta axial z - stressForce theta' axial' z

theorem NavierStokes.BaseResidual.scalarConst_rate {l : Filter ProblemStatement.SpaceTime} {q F : ProblemStatement.SpaceTime → ℝ} {U : Set ProblemStatement.SpaceTime} {M : ℕ} {r : ℝ} (hF : DiagonalResidual.FiniteJetRate l q F M r) (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hs : ContDiffOn ℝ (↑⊤) F U) (c : ℝ) : DiagonalResidual.FiniteJetRate l q (fun (z : ProblemStatement.SpaceTime) => c * F z) M r

theorem NavierStokes.BaseResidual.stressForce_rate {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) (hlo : 0 < lo) {theta axial : SlowBorelBase.Chart → ℝ} (ht : ContDiffOn ℝ (↑⊤) theta profilePast) (ha : ContDiffOn ℝ (↑⊤) axial profilePast) (M : ℕ) (r : ℝ) (htv : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (liftProfile theta) M r) (hav : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (liftProfile axial) M r) (htd : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (cartesianDerivative (0, 1, 0) theta) M r) (had : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (cartesianDerivative (0, 1, 0) axial) M r) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (stressForce theta axial) M (r - 1 - ↑M)

Finite loss for the actual stress differential operator, obtained from the profile derivative and reciprocal-radius factors.

noncomputable def NavierStokes.BaseResidual.prefixStressTheta (J : ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : SlowBorelBase.Chart → ℝ

Prefix stress theta, given by physicalUncutPrefix h (-CoordinateAlgebra.A h - 1 / 2) (bundleComponent C d 3) J.

Equations

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

noncomputable def NavierStokes.BaseResidual.prefixStressAxial (J : ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : SlowBorelBase.Chart → ℝ

Prefix stress axial, given by physicalUncutPrefix h (-CoordinateAlgebra.A h - 1 / 2) (bundleComponent C d 4) J.

Equations

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

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

Base stress force, given by stressForce (baseStressTheta a h C d) (baseStressAxial a h C d).

Equations

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

noncomputable def NavierStokes.BaseResidual.prefixStressForce (J : ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.VelocityField

Prefix stress force, given by stressForce (prefixStressTheta J h C d) (prefixStressAxial J h C d).

Equations

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

theorem NavierStokes.BaseResidual.prefixProfile_smooth {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → SlowBorelBase.Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (J : ℕ) : ContDiffOn ℝ (↑⊤) (SlowBorelBase.physicalUncutPrefix h b f J) profilePast

theorem NavierStokes.BaseResidual.baseStressForce_smooth {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (baseStressForce a h C d) annularPast

theorem NavierStokes.BaseResidual.prefixStressForce_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J : ℕ) (C : ℝ) : ContDiffOn ℝ (↑⊤) (prefixStressForce J h C d) annularPast

theorem NavierStokes.BaseResidual.stress_prefix_rate {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) (hlo : 0 < lo) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (J M : ℕ) (hM : M + 1 ≤ J + 3) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => baseStressForce a h C d z - prefixStressForce J h C d z) M (h * (↑J + 1) - CoordinateAlgebra.A h - 1 / 2 - 3 * (↑M + 1))

The stress tail is passed through the actual cylindrical operator. No force-tail estimate is assumed.

noncomputable def NavierStokes.BaseResidual.chartedDomain (h : ℝ) (U : Set SlowBorelBase.Inner) : Set ProblemStatement.SpaceTime

Charted domain, given by {z | z.1 < 1 ∧ (cartesianChart h z).2 ∈ U}.

Equations

• NavierStokes.BaseResidual.chartedDomain h U = {z : NavierStokes.ProblemStatement.SpaceTime | z.1 < 1 ∧ (NavierStokes.SlowBorelBase.cartesianChart h z).2 ∈ U}

theorem NavierStokes.BaseResidual.chartedDomain_isOpen {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {U : Set SlowBorelBase.Inner} (hU : IsOpen U) : IsOpen (chartedDomain h U)

theorem NavierStokes.BaseResidual.PhysicalApproach.in_chartedDomain {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (A : PhysicalApproach l h lo hi) (hh : 0 < h) (hh1 : h < 1 / 2) {U : Set SlowBorelBase.Inner} (hU : SlowBorelBase.innerBox lo hi ⊆ U) : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ chartedDomain h U

theorem NavierStokes.BaseResidual.monomial_smoothOn {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {U : Set SlowBorelBase.Inner} (hU : IsOpen U) {f : SlowBorelBase.Inner → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) : ContDiffOn ℝ (↑⊤) (cartesianMonomial h b f) (chartedDomain h U)

theorem NavierStokes.BaseResidual.finset_monomial_rate {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {U : Set SlowBorelBase.Inner} (hU : IsOpen U) (hKU : SlowBorelBase.innerBox lo hi ⊆ U) {ι : Type u_1} (s : Finset ι) (f : ι → SlowBorelBase.Inner → ℝ) (b : ι → ℝ) (bmin : ℝ) (hf : ∀ i ∈ s, ContDiffOn ℝ (↑⊤) (f i) U) (hmin : ∀ i ∈ s, bmin ≤ b i) (M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => ∑ i ∈ s, cartesianMonomial h (b i) (f i) z) M (bmin - ↑M)

noncomputable def NavierStokes.BaseResidual.radialVector (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

Radial vector, given by z.2 0 • coordinateVector 0 + z.2 1 • coordinateVector 1.

Equations

• NavierStokes.BaseResidual.radialVector z = z.2.ofLp 0 • NavierStokes.ProblemStatement.coordinateVector 0 + z.2.ofLp 1 • NavierStokes.ProblemStatement.coordinateVector 1

noncomputable def NavierStokes.BaseResidual.angularVector (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

Angular vector, given by -z.2 1 • coordinateVector 0 + z.2 0 • coordinateVector 1.

Equations

• NavierStokes.BaseResidual.angularVector z = -z.2.ofLp 1 • NavierStokes.ProblemStatement.coordinateVector 0 + z.2.ofLp 0 • NavierStokes.ProblemStatement.coordinateVector 1

theorem NavierStokes.BaseResidual.radialVector_smooth : ContDiff ℝ (↑⊤) radialVector

theorem NavierStokes.BaseResidual.angularVector_smooth : ContDiff ℝ (↑⊤) angularVector

noncomputable def NavierStokes.BaseResidual.assembleComponents (R A Z : ProblemStatement.SpaceTime → ℝ) (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

Assemble components, given by R z • radialVector z + A z • angularVector z + Z z • coordinateVector 2.

Equations

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

theorem NavierStokes.BaseResidual.assembleComponents_eq_pack (R A Z : ProblemStatement.SpaceTime → ℝ) (z : ProblemStatement.SpaceTime) : assembleComponents R A Z z = AxisymmetricResidual.pack (z.2.ofLp 0 * R z - z.2.ofLp 1 * A z) (z.2.ofLp 1 * R z + z.2.ofLp 0 * A z) (Z z)

theorem NavierStokes.BaseResidual.assembleComponents_rate {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {U B : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hlU : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ U) (hB : IsCompact B) (hlB : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∈ B) (hq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z) {R A Z : ProblemStatement.SpaceTime → ℝ} (hR : ContDiffOn ℝ (↑⊤) R U) (hA : ContDiffOn ℝ (↑⊤) A U) (hZ : ContDiffOn ℝ (↑⊤) Z U) {M : ℕ} {r : ℝ} (hrR : DiagonalResidual.FiniteJetRate l q R M r) (hrA : DiagonalResidual.FiniteJetRate l q A M r) (hrZ : DiagonalResidual.FiniteJetRate l q Z M r) : DiagonalResidual.FiniteJetRate l q (assembleComponents R A Z) M r

noncomputable def NavierStokes.BaseResidual.transportTailField (N : ℕ) (h e α : ℝ) (v u f : ℕ → SlowBorelBase.Inner → ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Transport tail field, given by transportTail N (cartesianChart h z).1 h e α v u f (cartesianChart h z).2.

Equations

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

noncomputable def NavierStokes.BaseResidual.radialTailField (N : ℕ) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (z : ProblemStatement.SpaceTime) : ℝ

Radial tail field, given by pressureTail N (cartesianChart h z).1 h C f (cartesianChart h z).2 / (2 * AxisymmetricFields.radialEnergy z.2).

Equations

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

theorem NavierStokes.BaseResidual.transportTailField_eq (N : ℕ) (h e α : ℝ) (v u f : ℕ → SlowBorelBase.Inner → ℝ) : transportTailField N h e α v u f = fun (z : ProblemStatement.SpaceTime) => ∑ i ∈ SlowResidualMatching.transportIndices N, cartesianMonomial h (SlowResidualMatching.transportPower N h e i) (SlowResidualMatching.transportTerm N h e α v u f i) z

theorem NavierStokes.BaseResidual.transportTailField_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (N : ℕ) (e α : ℝ) (v u f : ℕ → SlowBorelBase.Inner → ℝ) (hv : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (v j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f j) O) (hX : ∀ w ∈ O, w.1 ≠ 0) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffOn ℝ (↑⊤) (transportTailField N h e α v u f) (chartedDomain h O)

theorem NavierStokes.BaseResidual.transportTailField_rate {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox lo hi ⊆ O) (N : ℕ) (e α : ℝ) (v u f : ℕ → SlowBorelBase.Inner → ℝ) (hv : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (v j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f j) O) (hX : ∀ w ∈ O, w.1 ≠ 0) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) (M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (transportTailField N h e α v u f) M (e - 1 + SlowExpansionResidual.slowOrder h (N + 1) - ↑M)

noncomputable def NavierStokes.BaseResidual.radialTailExpression (N : ℕ) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (z : ProblemStatement.SpaceTime) : ℝ

Radial tail expression, given by ∑ i ∈ pressureIndices N, cartesianMonomial h (pressurePower N h i - 1) (fun w => pressureTerm N h C f i w / (2 * w.1)) z.

Equations

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

theorem NavierStokes.BaseResidual.radialTailExpression_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) {z : ProblemStatement.SpaceTime} (hz : z ∈ annularPast) : radialTailExpression N h C f z = radialTailField N h C f z

theorem NavierStokes.BaseResidual.radialTailExpression_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (hv : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.flux j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.axial j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.phi j) O) (hX : ∀ w ∈ O, w.1 ≠ 0) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffOn ℝ (↑⊤) (radialTailExpression N h C f) (chartedDomain h O)

theorem NavierStokes.BaseResidual.radialTailExpression_rate {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox lo hi ⊆ O) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (hv : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.flux j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.axial j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.phi j) O) (hX : ∀ w ∈ O, w.1 ≠ 0) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) (M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (radialTailExpression N h C f) M (SlowExpansionResidual.pressureExponent h - 1 + SlowExpansionResidual.slowOrder h (N + 1) - ↑M)

theorem NavierStokes.BaseResidual.truncationResidual_rate {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) (hlo : 0 < lo) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox lo hi ⊆ O) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (hv : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.flux j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.axial j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f.phi j) O) (hX : ∀ w ∈ O, w.1 ≠ 0) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) (M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => SlowExpansionResidual.truncationResidual N h C f z.1 z.2) M (2 * ↑N * h - 2 - ↑M)

The actual finite residual left by the recurrence has arbitrary increasing order as the truncation index increases. Its rate is derived from the explicit omitted monomials, not supplied as a hypothesis.

noncomputable def NavierStokes.BaseResidual.baseResidual (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

Base residual, given by navierStokesResidual (baseVelocity a h C d) (basePressure a h C d) z.1 z.2 - baseStressForce a h C d z.

Equations

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

theorem NavierStokes.BaseResidual.baseResidual_identity (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) (z : ProblemStatement.SpaceTime) : ProblemStatement.navierStokesResidual (SlowBorelBase.baseVelocity a h C d) (SlowBorelBase.basePressure a h C d) z.1 z.2 = baseStressForce a h C d z + baseResidual a h C d z

theorem NavierStokes.BaseResidual.basePressure_smooth {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (SlowBorelBase.basePressure a h C d) past

theorem NavierStokes.BaseResidual.prefixPressure_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (J : ℕ) (C : ℝ) : ContDiffOn ℝ (↑⊤) (prefixPressure J h C d) past

theorem NavierStokes.BaseResidual.jetRate_neg {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {F : ProblemStatement.SpaceTime → ProblemStatement.Space} {m : ℕ} {r : ℝ} (hF : DiagonalResidual.JetRate l q F m r) : DiagonalResidual.JetRate l q (fun (z : ProblemStatement.SpaceTime) => -F z) m r

def NavierStokes.BaseResidual.FiniteIdentities (h C : ℝ) (d : SlowBorelBase.Coefficients) (f : SlowExpansionResidual.SlowProfiles) : Prop

The finite identity in this interface is the exact identity for the displayed uncut stream prefixes. It contains no asymptotic hypothesis.

Equations

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

theorem NavierStokes.BaseResidual.baseResidual_jetRate {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) (hlo : 0 < lo) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (f : SlowExpansionResidual.SlowProfiles) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox lo hi ⊆ O) (hv : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (f.flux j) O) (hu : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (f.axial j) O) (hf : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (f.phi j) O) (hX : ∀ w ∈ O, w.1 ≠ 0) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) (hfinite : FiniteIdentities h C d f) (m : ℕ) (n : ℝ) (hn : 0 ≤ n) : DiagonalResidual.JetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (baseResidual a h C d) m n

The nonlinear residual estimate for the concrete asymptotic sum. Every rate used in its proof is derived above from smooth coefficients, the chosen scales, and the explicit finite identities.

theorem NavierStokes.BaseResidual.baseResidual_allJetsFlat {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) (hlo : 0 < lo) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (f : SlowExpansionResidual.SlowProfiles) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox lo hi ⊆ O) (hv : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (f.flux j) O) (hu : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (f.axial j) O) (hf : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (f.phi j) O) (hX : ∀ w ∈ O, w.1 ≠ 0) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) (hfinite : FiniteIdentities h C d f) : ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (baseResidual a h C d)

All physical Cartesian space-time jets of the actual nonlinear error are flat along every fixed compact annular approach to q=0.

def NavierStokes.BaseResidual.PolynomialEdgeJets {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (W : Set SlowBorelBase.Inner) (zeta delta : SlowBorelBase.Inner → ℝ) (f : SlowBorelBase.Inner → V) : Prop

Polynomial losses in the two logarithmic edge distances are allowed. The estimate is on the full derivative tensor, including mixed derivatives.

Equations

• NavierStokes.BaseResidual.PolynomialEdgeJets W zeta delta f = ∀ (m : ℕ), ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ w ∈ W, ‖iteratedFDeriv ℝ m f w‖ ≤ C * zeta w * (delta w)⁻¹ ^ N

theorem NavierStokes.BaseResidual.PolynomialEdgeJets.finite {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {W : Set SlowBorelBase.Inner} {zeta delta : SlowBorelBase.Inner → ℝ} {f : SlowBorelBase.Inner → V} (hf : PolynomialEdgeJets W zeta delta f) (hz : ∀ w ∈ W, 0 ≤ zeta w) (hd : ∀ w ∈ W, 0 < delta w ∧ delta w ≤ 1) (M : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ w ∈ W, ∀ m ≤ M, ‖iteratedFDeriv ℝ m f w‖ ≤ C * zeta w * (delta w)⁻¹ ^ N

theorem NavierStokes.BaseResidual.innerLift_blown_le {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SlowBorelBase.Inner → V} (hf : ContDiff ℝ (↑⊤) f) (q : ℝ) (w : SlowBorelBase.Inner) (m : ℕ) : ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => f y.2) (q, w)‖ ≤ ‖iteratedFDeriv ℝ m f w‖

noncomputable def NavierStokes.BaseResidual.positiveScale : Set SlowBorelBase.Chart

Positive scale, given by {y | 0 < y.1}.

Equations

• NavierStokes.BaseResidual.positiveScale = {y : NavierStokes.SlowBorelBase.Chart | 0 < y.1}

theorem NavierStokes.BaseResidual.positiveScale_isOpen : IsOpen positiveScale

theorem NavierStokes.BaseResidual.blown_product_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {F : SlowBorelBase.Chart → ℝ} {G : SlowBorelBase.Chart → V} (hF : ContDiffOn ℝ (↑⊤) F positiveScale) (hG : ContDiffOn ℝ (↑⊤) G positiveScale) {q : ℝ} (hq : 0 < q) (w : SlowBorelBase.Inner) (m : ℕ) {A B : ℝ} (hA : ∀ k ≤ m, ‖SlowBorelBase.blownJet k F (q, w)‖ ≤ A) (hB : ∀ k ≤ m, ‖SlowBorelBase.blownJet k G (q, w)‖ ≤ B) : ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => F y • G y) (q, w)‖ ≤ ‖ContinuousLinearMap.lsmul ℝ ℝ‖ * 2 ^ m * A * B

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

noncomputable def NavierStokes.BaseResidual.firstCutoff (a : ℕ → ℕ) (h : ℝ) : SlowBorelBase.Chart → ℝ

First cutoff, given by powerStage (a 1) (2 * h) (fun _ => 1).

Equations

• NavierStokes.BaseResidual.firstCutoff a h = NavierStokes.SlowBorelBase.powerStage (↑(a 1)) (2 * h) fun (x : NavierStokes.SlowBorelBase.Inner) => 1

theorem NavierStokes.BaseResidual.firstCutoff_finite_bound (a : ℕ → ℕ) (h : ℝ) {K : Set SlowBorelBase.Inner} (hK : IsCompact K) (M : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℝ), 0 < q → ∀ w ∈ K, ∀ m ≤ M, ‖SlowBorelBase.blownJet m (firstCutoff a h) (q, w)‖ ≤ C * q ^ (2 * h)

theorem NavierStokes.BaseResidual.slowSum_split_first {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) (h : ℝ) (f g : ℕ → SlowBorelBase.Inner → V) (zeta : SlowBorelBase.Inner → ℝ) (hg0 : g 0 = 0) (hg1 : g 1 = 0) {O : Set SlowBorelBase.Inner} (hfg : ∀ (j : ℕ), 2 ≤ j → ∀ w ∈ O, f j w = zeta w • g j w) {q : ℝ} (hq : 0 < q) {w : SlowBorelBase.Inner} (hw : w ∈ O) : SlowBorelBase.slowSum a h f (q, w) - f 0 w = firstCutoff a h (q, w) • f 1 w + zeta w • SlowBorelBase.slowSum a h g (q, w)

theorem NavierStokes.BaseResidual.blown_add_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {F G : SlowBorelBase.Chart → V} (hF : ContDiffOn ℝ (↑⊤) F positiveScale) (hG : ContDiffOn ℝ (↑⊤) G positiveScale) {q : ℝ} (hq : 0 < q) (w : SlowBorelBase.Inner) (m : ℕ) : ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => F y + G y) (q, w)‖ ≤ ‖SlowBorelBase.blownJet m F (q, w)‖ + ‖SlowBorelBase.blownJet m G (q, w)‖

theorem NavierStokes.BaseResidual.weighted_slowSum_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f g : ℕ → SlowBorelBase.Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (hg : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (g j)) {K W O : Set SlowBorelBase.Inner} (hK : IsCompact K) (hWK : W ⊆ K) (hO : IsOpen O) (hWO : W ⊆ O) {zeta delta : SlowBorelBase.Inner → ℝ} (hzs : ContDiff ℝ (↑⊤) zeta) (hz : ∀ w ∈ W, 0 ≤ zeta w) (hd : ∀ w ∈ W, 0 < delta w ∧ delta w ≤ 1) (hfirst : PolynomialEdgeJets W zeta delta (f 1)) (hweight : PolynomialEdgeJets W zeta delta zeta) (hg0 : g 0 = 0) (hg1 : g 1 = 0) (hfg : ∀ (j : ℕ), 2 ≤ j → ∀ w ∈ O, f j w = zeta w • g j w) (ha : SlowBorelBase.AdmissibleScales h g K a) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∃ (N : ℕ), ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ W, ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => SlowBorelBase.slowSum a h f y - f 0 y.2) (q, w)‖ ≤ C * q ^ h * zeta w * (delta w)⁻¹ ^ N

Weighted summation of the full coefficient vector. The first coefficient uses polynomial edge bounds; higher coefficients use their genuine smooth quotients by the flat weight and the explicitly chosen cutoff schedule.

noncomputable def NavierStokes.BaseResidual.stressPair (d : SlowBorelBase.Coefficients) (j : ℕ) (w : SlowBorelBase.Inner) : SlowBorelBase.Inner

Both independent slots of the virtual tangential tensor.

Equations

• NavierStokes.BaseResidual.stressPair d j w = (d.stressTheta j w, d.stressAxial j w)

theorem NavierStokes.BaseResidual.stressPair_smooth {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (j : ℕ) : ContDiff ℝ (↑⊤) (stressPair d j)

noncomputable def NavierStokes.BaseResidual.higherStressQuotient (d : SlowBorelBase.Coefficients) (zeta : SlowBorelBase.Inner → ℝ) (j : ℕ) (w : SlowBorelBase.Inner) : SlowBorelBase.Inner

Higher stress quotient, with branches according to j ≤ 1.

Equations

• NavierStokes.BaseResidual.higherStressQuotient d zeta j w = if j ≤ 1 then 0 else (zeta w)⁻¹ • NavierStokes.BaseResidual.stressPair d j w

@[simp]

theorem NavierStokes.BaseResidual.higherStressQuotient_zero (d : SlowBorelBase.Coefficients) (zeta : SlowBorelBase.Inner → ℝ) : higherStressQuotient d zeta 0 = 0

@[simp]

theorem NavierStokes.BaseResidual.higherStressQuotient_one (d : SlowBorelBase.Coefficients) (zeta : SlowBorelBase.Inner → ℝ) : higherStressQuotient d zeta 1 = 0

theorem NavierStokes.BaseResidual.higherStressQuotient_factor (d : SlowBorelBase.Coefficients) (zeta : SlowBorelBase.Inner → ℝ) {j : ℕ} (hj : 2 ≤ j) {w : SlowBorelBase.Inner} (hz : zeta w ≠ 0) : stressPair d j w = zeta w • higherStressQuotient d zeta j w

noncomputable def NavierStokes.BaseResidual.weightedBundle (C : ℝ) (d : SlowBorelBase.Coefficients) (zeta : SlowBorelBase.Inner → ℝ) (j : ℕ) (w : SlowBorelBase.Inner) : SlowBorelBase.Bundle × SlowBorelBase.Inner

A common enlarged bundle controls the actual base fields and the higher-order stress quotients by the same cutoff sequence.

Equations

• NavierStokes.BaseResidual.weightedBundle C d zeta j w = (NavierStokes.SlowBorelBase.coefficientBundle C d j w, NavierStokes.BaseResidual.higherStressQuotient d zeta j w)

theorem NavierStokes.BaseResidual.weightedBundle_smooth {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {zeta : SlowBorelBase.Inner → ℝ} (hq : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (higherStressQuotient d zeta j)) (C : ℝ) (j : ℕ) : ContDiff ℝ (↑⊤) (weightedBundle C d zeta j)

theorem NavierStokes.BaseResidual.weightedBundle_base_scales {a : ℕ → ℕ} {h C : ℝ} {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {zeta : SlowBorelBase.Inner → ℝ} (hq : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (higherStressQuotient d zeta j)) {K : Set SlowBorelBase.Inner} (ha : SlowBorelBase.AdmissibleScales h (weightedBundle C d zeta) K a) : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) K a

theorem NavierStokes.BaseResidual.weightedBundle_quotient_scales {a : ℕ → ℕ} {h C : ℝ} {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {zeta : SlowBorelBase.Inner → ℝ} (hq : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (higherStressQuotient d zeta j)) {K : Set SlowBorelBase.Inner} (ha : SlowBorelBase.AdmissibleScales h (weightedBundle C d zeta) K a) : SlowBorelBase.AdmissibleScales h (higherStressQuotient d zeta) K a

noncomputable def NavierStokes.BaseResidual.normalizedTensor (a : ℕ → ℕ) (h : ℝ) (d : SlowBorelBase.Coefficients) : SlowBorelBase.Chart → SlowBorelBase.Inner

Normalized tensor, given by slowSum a h (stressPair d).

Equations

• NavierStokes.BaseResidual.normalizedTensor a h d = NavierStokes.SlowBorelBase.slowSum a h (NavierStokes.BaseResidual.stressPair d)

theorem NavierStokes.BaseResidual.normalizedTensor_components {a : ℕ → ℕ} (ha : StrictMono a) (h : ℝ) (d : SlowBorelBase.Coefficients) {y : SlowBorelBase.Chart} (hy : 0 < y.1) : normalizedTensor a h d y = (SlowBorelBase.slowSum a h d.stressTheta y, SlowBorelBase.slowSum a h d.stressAxial y)

theorem NavierStokes.BaseResidual.physicalTensor_eq_normalized {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) (d : SlowBorelBase.Coefficients) {p : SlowBorelBase.Chart} (hp : p.1 < 1) : (SlowBorelBase.baseStressTheta a h C d p, SlowBorelBase.baseStressAxial a h C d p) = (SlowBorelBase.physicalChart h p).1 ^ (-CoordinateAlgebra.A h - 1 / 2) • normalizedTensor a h d (SlowBorelBase.physicalChart h p)

Both physical stress slots have exactly the common prefactor used in the manuscript. The normalized tensor is the actual cut sum.

theorem NavierStokes.BaseResidual.normalizedTensor_weighted_bound {a : ℕ → ℕ} {h C : ℝ} (hh : 0 < h) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {K W O : Set SlowBorelBase.Inner} (hK : IsCompact K) (hWK : W ⊆ K) (hO : IsOpen O) (hWO : W ⊆ O) {zeta delta : SlowBorelBase.Inner → ℝ} (hzs : ContDiff ℝ (↑⊤) zeta) (hz : ∀ w ∈ O, 0 < zeta w) (hdelta : ∀ w ∈ W, 0 < delta w ∧ delta w ≤ 1) (hfirst : PolynomialEdgeJets W zeta delta (stressPair d 1)) (hweight : PolynomialEdgeJets W zeta delta zeta) (hq : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (higherStressQuotient d zeta j)) (ha : SlowBorelBase.AdmissibleScales h (weightedBundle C d zeta) K a) (m : ℕ) : ∃ (B : ℝ), 0 < B ∧ ∃ (N : ℕ), ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ W, ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => normalizedTensor a h d y - stressPair d 0 y.2) (q, w)‖ ≤ B * q ^ h * zeta w * (delta w)⁻¹ ^ N

The full normalized two-slot tensor differs from its leading value by O(q^h), with the allowed polynomial losses at both flat edges.

theorem NavierStokes.BaseResidual.exists_weighted_base_scales {h : ℝ} (hh : 0 < h) (C : ℝ) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {K W O : Set SlowBorelBase.Inner} (hK : IsCompact K) (hWK : W ⊆ K) (hO : IsOpen O) (hWO : W ⊆ O) {zeta delta : SlowBorelBase.Inner → ℝ} (hzs : ContDiff ℝ (↑⊤) zeta) (hz : ∀ w ∈ O, 0 < zeta w) (hdelta : ∀ w ∈ W, 0 < delta w ∧ delta w ≤ 1) (hfirst : PolynomialEdgeJets W zeta delta (stressPair d 1)) (hweight : PolynomialEdgeJets W zeta delta zeta) (hq : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (higherStressQuotient d zeta j)) (B : ℕ) : ∃ (a : ℕ → ℕ), B ≤ a 0 ∧ SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) K a ∧ ∀ (m : ℕ), ∃ (D : ℝ), 0 < D ∧ ∃ (N : ℕ), ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ W, ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => normalizedTensor a h d y - stressPair d 0 y.2) (q, w)‖ ≤ D * q ^ h * zeta w * (delta w)⁻¹ ^ N

The common schedule is constructed from coefficient smoothness. The weighted estimate is an output, not part of the admissibility assumptions.

noncomputable def NavierStokes.BaseResidual.logWeightProfile (c a b : ℝ) (w : SlowBorelBase.Inner) : ℝ

Log weight profile, given by weight c a b w.2.

Equations

• NavierStokes.BaseResidual.logWeightProfile c a b w = NavierStokes.ActiveAnnulusWeight.weight c a b w.2

noncomputable def NavierStokes.BaseResidual.weightLeftFactor {a b c : ℝ} (hab : a < b) (_hc : 0 < c) (K : Set ℝ) : ActiveAnnulusWeight.EdgeFactor K c (ActiveAnnulusWeight.leftChart a (logWeightProfile c a b))

Weight left factor, bundling coefficient, order, width, width_pos and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.BaseResidual.weightRightFactor {a b c : ℝ} (hab : a < b) (hc : 0 < c) (K : Set ℝ) : ActiveAnnulusWeight.EdgeFactor K 4 (ActiveAnnulusWeight.rightChart b (logWeightProfile c a b))

Weight right factor, bundling coefficient, order, width, width_pos and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.BaseResidual.swapInner : SlowBorelBase.Inner ≃ₗᵢ[ℝ] SlowBorelBase.Inner

Swap inner, bundling toLinearEquiv, norm_map.

Equations

• NavierStokes.BaseResidual.swapInner = { toLinearEquiv := LinearEquiv.prodComm ℝ ℝ ℝ, norm_map' := NavierStokes.BaseResidual.swapInner._proof_1 }

noncomputable def NavierStokes.BaseResidual.activeWindow (a b : ℝ) : Set SlowBorelBase.Inner

Active window, given by Ioo (Real.exp a) (Real.exp b) ×ˢ Icc (-1) 1.

Equations

• NavierStokes.BaseResidual.activeWindow a b = Set.Ioo (Real.exp a) (Real.exp b) ×ˢ Set.Icc (-1) 1

noncomputable def NavierStokes.BaseResidual.activeZeta (c a b : ℝ) (w : SlowBorelBase.Inner) : ℝ

Active zeta, given by radialWeight c a b w.1.

Equations

• NavierStokes.BaseResidual.activeZeta c a b w = NavierStokes.ActiveAnnulusWeight.radialWeight c a b w.1

noncomputable def NavierStokes.BaseResidual.activeDelta (a b : ℝ) (w : SlowBorelBase.Inner) : ℝ

Active delta, given by edgeDistance a b (Real.log w.1).

Equations

• NavierStokes.BaseResidual.activeDelta a b w = NavierStokes.ActiveAnnulusWeight.edgeDistance a b (Real.log w.1)

theorem NavierStokes.BaseResidual.activeZeta_smooth {c : ℝ} (hc : 0 < c) (a b : ℝ) : ContDiff ℝ (↑⊤) (activeZeta c a b)

theorem NavierStokes.BaseResidual.activeDelta_bounds {a b : ℝ} {w : SlowBorelBase.Inner} (hw : w ∈ activeWindow a b) : 0 < activeDelta a b w ∧ activeDelta a b w ≤ 1

theorem NavierStokes.BaseResidual.activeZeta_edgeJets {a b c : ℝ} (hab : a < b) (hc : 0 < c) : PolynomialEdgeJets (activeWindow a b) (activeZeta c a b) (activeDelta a b) (activeZeta c a b)

The actual two-edge Gaussian weight has the polynomial derivative losses used in the summation theorem. This is derived from its edge factors.

def NavierStokes.BaseResidual.StressZeroCore (d : SlowBorelBase.Coefficients) (r : ℝ) : Prop

A common inner zero region for every actual stress coefficient.

Equations

• NavierStokes.BaseResidual.StressZeroCore d r = ∀ (j : ℕ), ∀ X ∈ Set.Ico 0 r, ∀ eta ∈ Set.Icc (-1) 1, d.stressTheta j (X, eta) = 0 ∧ d.stressAxial j (X, eta) = 0

theorem NavierStokes.BaseResidual.slowSum_zero_of_all {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h q : ℝ) {f : ℕ → SlowBorelBase.Inner → V} {w : SlowBorelBase.Inner} (hf : ∀ (j : ℕ), f j w = 0) : SlowBorelBase.slowSum a h f (q, w) = 0

theorem NavierStokes.BaseResidual.physicalProfile_zero_of_all {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h b : ℝ) {f : ℕ → SlowBorelBase.Inner → V} {p : SlowBorelBase.Chart} (hf : ∀ (j : ℕ), f j (SlowBorelBase.physicalChart h p).2 = 0) : SlowBorelBase.physicalProfile a h b f p = 0

theorem NavierStokes.BaseResidual.physicalUncutPrefix_zero_of_all {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (h b : ℝ) {f : ℕ → SlowBorelBase.Inner → V} (J : ℕ) {p : SlowBorelBase.Chart} (hf : ∀ (j : ℕ), f j (SlowBorelBase.physicalChart h p).2 = 0) : SlowBorelBase.physicalUncutPrefix h b f J p = 0

theorem NavierStokes.BaseResidual.stressForce_zero_at_axis (theta axial : SlowBorelBase.Chart → ℝ) {z : ProblemStatement.SpaceTime} (hs : AxisymmetricFields.radialEnergy z.2 = 0) : stressForce theta axial z = 0

theorem NavierStokes.BaseResidual.stressForce_zero_core {h r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {theta axial : SlowBorelBase.Chart → ℝ} (htheta : ∀ (p : SlowBorelBase.Chart), p.1 < 1 → (SlowBorelBase.physicalChart h p).2.1 ∈ Set.Ioo 0 r → theta p = 0) (haxial : ∀ (p : SlowBorelBase.Chart), p.1 < 1 → (SlowBorelBase.physicalChart h p).2.1 ∈ Set.Ioo 0 r → axial p = 0) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : (SlowBorelBase.cartesianChart h z).2.1 < r) : stressForce theta axial z = 0

theorem NavierStokes.BaseResidual.stressForce_core_germ {h r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {theta axial : SlowBorelBase.Chart → ℝ} (htheta : ∀ (p : SlowBorelBase.Chart), p.1 < 1 → (SlowBorelBase.physicalChart h p).2.1 ∈ Set.Ioo 0 r → theta p = 0) (haxial : ∀ (p : SlowBorelBase.Chart), p.1 < 1 → (SlowBorelBase.physicalChart h p).2.1 ∈ Set.Ioo 0 r → axial p = 0) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : (SlowBorelBase.cartesianChart h z).2.1 < r) : stressForce theta axial =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.BaseResidual.baseStressForce_core_germ {h r C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (a : ℕ → ℕ) {d : SlowBorelBase.Coefficients} (hc : StressZeroCore d r) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : (SlowBorelBase.cartesianChart h z).2.1 < r) : baseStressForce a h C d =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.BaseResidual.prefixStressForce_core_germ {h r C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (J : ℕ) {d : SlowBorelBase.Coefficients} (hc : StressZeroCore d r) {z : ProblemStatement.SpaceTime} (ht : z.1 < 1) (hX : (SlowBorelBase.cartesianChart h z).2.1 < r) : prefixStressForce J h C d =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.BaseResidual.baseStressForce_smooth_past {a : ℕ → ℕ} (ha : StrictMono a) {h r C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hr : 0 < r) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hc : StressZeroCore d r) : ContDiffOn ℝ (↑⊤) (baseStressForce a h C d) past

theorem NavierStokes.BaseResidual.prefixStressForce_smooth_past {h r C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hr : 0 < r) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hc : StressZeroCore d r) (J : ℕ) : ContDiffOn ℝ (↑⊤) (prefixStressForce J h C d) past

theorem NavierStokes.BaseResidual.admissible_mono {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} {f : ℕ → SlowBorelBase.Inner → V} {K K' : Set SlowBorelBase.Inner} (ha : SlowBorelBase.AdmissibleScales h f K a) (hK : K' ⊆ K) : SlowBorelBase.AdmissibleScales h f K' a

theorem NavierStokes.BaseResidual.finiteRate_extend_zero {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {l : Filter ProblemStatement.SpaceTime} {q : ProblemStatement.SpaceTime → ℝ} {F : ProblemStatement.SpaceTime → V} {S : Set ProblemStatement.SpaceTime} {M : ℕ} {r : ℝ} (hF : DiagonalResidual.FiniteJetRate (l ⊓ Filter.principal S) q F M r) (hq : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, 0 < q z) (hz : ∀ᶠ (z : ProblemStatement.SpaceTime) in l, z ∉ S → F =ᶠ[nhds z] fun (x : ProblemStatement.SpaceTime) => 0) : DiagonalResidual.FiniteJetRate l q F M r

theorem NavierStokes.BaseResidual.stress_prefix_rate_axis {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C hi r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h 0 hi) (hr : 0 < r) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hc : StressZeroCore d r) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox 0 hi) a) (J M : ℕ) (hM : M + 1 ≤ J + 3) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => baseStressForce a h C d z - prefixStressForce J h C d z) M (h * (↑J + 1) - CoordinateAlgebra.A h - 1 / 2 - 3 * (↑M + 1))

The stress-force tail estimate also holds on boxes meeting the axis: the apparent reciprocal-radius singularities lie in a common zero region.

theorem NavierStokes.BaseResidual.eqOn_of_off_axis {V : Type} [NormedAddCommGroup V] {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) {F G : ProblemStatement.SpaceTime → V} (hF : ContinuousOn F U) (hG : ContinuousOn G U) (he : ∀ z ∈ U, 0 < AxisymmetricFields.radialEnergy z.2 → F z = G z) : Set.EqOn F G U

Equality of continuous physical fields away from the symmetry axis extends across it. The proof uses an explicit Cartesian perturbation.

noncomputable def NavierStokes.BaseResidual.regularTransportField (N : ℕ) (h e α : ℝ) (beta u f : ℕ → SlowBorelBase.Inner → ℝ) (z : ProblemStatement.SpaceTime) : ℝ

The regular descriptors are actual finite sums of physical monomials.

Equations

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

noncomputable def NavierStokes.BaseResidual.regularRadialField (N : ℕ) (h C : ℝ) (phi u beta : ℕ → SlowBorelBase.Inner → ℝ) (z : ProblemStatement.SpaceTime) : ℝ

Regular radial field, given by ∑ i ∈ pressureIndices N, cartesianMonomial h (pressurePower N h i - 1) (regularPressureTerm N h C phi u beta i) z.

Equations

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

noncomputable def NavierStokes.BaseResidual.regularTruncation (N : ℕ) (h C : ℝ) (phi u beta : ℕ → SlowBorelBase.Inner → ℝ) : ProblemStatement.SpaceTime → ProblemStatement.Space

Regular truncation, constructed using assembleComponents.

Equations

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

theorem NavierStokes.BaseResidual.assembleComponents_smooth {U : Set ProblemStatement.SpaceTime} {R A Z : ProblemStatement.SpaceTime → ℝ} (hR : ContDiffOn ℝ (↑⊤) R U) (hA : ContDiffOn ℝ (↑⊤) A U) (hZ : ContDiffOn ℝ (↑⊤) Z U) : ContDiffOn ℝ (↑⊤) (assembleComponents R A Z) U

theorem NavierStokes.BaseResidual.regularTransportField_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (N : ℕ) (e α : ℝ) (beta u f : ℕ → SlowBorelBase.Inner → ℝ) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hf : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (f j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffOn ℝ (↑⊤) (regularTransportField N h e α beta u f) (chartedDomain h O)

theorem NavierStokes.BaseResidual.regularRadialField_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (N : ℕ) (C : ℝ) (phi u beta : ℕ → SlowBorelBase.Inner → ℝ) (hp : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffOn ℝ (↑⊤) (regularRadialField N h C phi u beta) (chartedDomain h O)

theorem NavierStokes.BaseResidual.regularTruncation_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (N : ℕ) (C : ℝ) (phi u beta : ℕ → SlowBorelBase.Inner → ℝ) (hp : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffOn ℝ (↑⊤) (regularTruncation N h C phi u beta) (chartedDomain h O)

theorem NavierStokes.BaseResidual.regularTruncation_rate {l : Filter ProblemStatement.SpaceTime} {h lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox lo hi ⊆ O) (N : ℕ) (C : ℝ) (phi u beta : ℕ → SlowBorelBase.Inner → ℝ) (hp : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) (M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (regularTruncation N h C phi u beta) M (2 * ↑N * h - 2 - ↑M)

Cancellation of the radial factor loses no power of q, including for all physical derivatives on compact sets meeting the axis.

theorem NavierStokes.BaseResidual.regularTransportField_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (N : ℕ) (e α : ℝ) {v u f beta u' f' : ℕ → SlowBorelBase.Inner → ℝ} (hv : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → v j w = w.1 * beta j w) (hu : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → u j w = u' j w) (hf : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f j w = f' j w) {z : ProblemStatement.SpaceTime} (hz : z ∈ chartedDomain h O) (hs : 0 < AxisymmetricFields.radialEnergy z.2) : regularTransportField N h e α beta u' f' z = transportTailField N h e α v u f z

theorem NavierStokes.BaseResidual.regularRadialField_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (N : ℕ) (C : ℝ) {f : SlowExpansionResidual.SlowProfiles} {phi u beta : ℕ → SlowBorelBase.Inner → ℝ} (hv : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.flux j w = w.1 * beta j w) (hu : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.axial j w = u j w) (hp : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.phi j w = phi j w) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {z : ProblemStatement.SpaceTime} (hz : z ∈ chartedDomain h O) (hs : 0 < AxisymmetricFields.radialEnergy z.2) : regularRadialField N h C phi u beta z = radialTailField N h C f z

theorem NavierStokes.BaseResidual.regularTruncation_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (N : ℕ) (C : ℝ) {f : SlowExpansionResidual.SlowProfiles} {phi u beta : ℕ → SlowBorelBase.Inner → ℝ} (hv : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.flux j w = w.1 * beta j w) (hu : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.axial j w = u j w) (hp : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.phi j w = phi j w) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) {z : ProblemStatement.SpaceTime} (hz : z ∈ chartedDomain h O) (hs : 0 < AxisymmetricFields.radialEnergy z.2) : regularTruncation N h C phi u beta z = SlowExpansionResidual.truncationResidual N h C f z.1 z.2

theorem NavierStokes.BaseResidual.finite_error_rate {l : Filter ProblemStatement.SpaceTime} {h C lo hi r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h lo hi) (hr : 0 < r) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hc : StressZeroCore d r) (f : SlowExpansionResidual.SlowProfiles) (hfinite : FiniteIdentities h C d f) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox lo hi ⊆ O) (N : ℕ) (phi u beta : ℕ → SlowBorelBase.Inner → ℝ) (hp : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ j ≤ N, ContDiffOn ℝ (↑⊤) (beta j) O) (hv : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.flux j w = w.1 * beta j w) (heu : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.axial j w = u j w) (hep : ∀ j ≤ N, ∀ w ∈ O, 0 ≤ w.1 → f.phi j w = phi j w) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) (M : ℕ) : DiagonalResidual.FiniteJetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (fun (z : ProblemStatement.SpaceTime) => ProblemStatement.navierStokesResidual (prefixVelocity N h C d) (prefixPressure N h C d) z.1 z.2 - prefixStressForce N h C d z) M (2 * ↑N * h - 2 - ↑M)

The exact finite physical error has a smooth continuation through the axis, and its physical jet bounds follow from its regular monomials.

theorem NavierStokes.BaseResidual.baseResidual_jetRate_axis {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C hi r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h 0 hi) (hr : 0 < r) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hc : StressZeroCore d r) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox 0 hi) a) (f : SlowExpansionResidual.SlowProfiles) (hfinite : FiniteIdentities h C d f) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox 0 hi ⊆ O) (phi u beta : ℕ → SlowBorelBase.Inner → ℝ) (hp : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (beta j) O) (hv : ∀ (j : ℕ), ∀ w ∈ O, 0 ≤ w.1 → f.flux j w = w.1 * beta j w) (heu : ∀ (j : ℕ), ∀ w ∈ O, 0 ≤ w.1 → f.axial j w = u j w) (hep : ∀ (j : ℕ), ∀ w ∈ O, 0 ≤ w.1 → f.phi j w = phi j w) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) (m : ℕ) (n : ℝ) (hn : 0 ≤ n) : DiagonalResidual.JetRate l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (baseResidual a h C d) m n

The actual nonlinear error is flat in all physical jets on compact similarity boxes, including the symmetry axis. Smooth extensions are used only for the coefficients; their positive-side values are specified here.

theorem NavierStokes.BaseResidual.baseResidual_allJetsFlat_axis {l : Filter ProblemStatement.SpaceTime} {a : ℕ → ℕ} {h C hi r : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (A : PhysicalApproach l h 0 hi) (hr : 0 < r) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hc : StressZeroCore d r) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox 0 hi) a) (f : SlowExpansionResidual.SlowProfiles) (hfinite : FiniteIdentities h C d f) {O : Set SlowBorelBase.Inner} (hO : IsOpen O) (hKO : SlowBorelBase.innerBox 0 hi ⊆ O) (phi u beta : ℕ → SlowBorelBase.Inner → ℝ) (hp : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (phi j) O) (hu : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (u j) O) (hb : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (beta j) O) (hv : ∀ (j : ℕ), ∀ w ∈ O, 0 ≤ w.1 → f.flux j w = w.1 * beta j w) (heu : ∀ (j : ℕ), ∀ w ∈ O, 0 ≤ w.1 → f.axial j w = u j w) (hep : ∀ (j : ℕ), ∀ w ∈ O, 0 ≤ w.1 → f.phi j w = phi j w) (hL : ∀ w ∈ O, CoordinateAlgebra.L h w.2 ≠ 0) : ResidualStability.AllJetsFlat l (fun (z : ProblemStatement.SpaceTime) => (SlowBorelBase.cartesianChart h z).1) (baseResidual a h C d)

def NavierStokes.BaseResidual.HigherInteriorSupport (d : SlowBorelBase.Coefficients) (left right : ℝ) : Prop

Higher-order support is strictly interior to the active annulus. The interval and its distance from the edges may depend on the order.

Equations

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

theorem NavierStokes.BaseResidual.higherStressQuotient_smooth_of_support {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {c left right : ℝ} (hc : 0 < c) (hs : HigherInteriorSupport d left right) (j : ℕ) : ContDiff ℝ (↑⊤) (higherStressQuotient d (activeZeta c left right) j)

theorem NavierStokes.BaseResidual.compact_weighted_jet_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SlowBorelBase.Inner → V} (hf : ContDiff ℝ (↑⊤) f) {zeta : SlowBorelBase.Inner → ℝ} (hz : Continuous zeta) {K : Set SlowBorelBase.Inner} (hK : IsCompact K) (hp : ∀ w ∈ K, 0 < zeta w) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ w ∈ K, ‖iteratedFDeriv ℝ m f w‖ ≤ C * zeta w

noncomputable def NavierStokes.BaseResidual.outerWindow (cut right : ℝ) : Set SlowBorelBase.Inner

Outer window, given by Ico cut (Real.exp right) ×ˢ Icc (-1) 1.

Equations

• NavierStokes.BaseResidual.outerWindow cut right = Set.Ico cut (Real.exp right) ×ˢ Set.Icc (-1) 1

theorem NavierStokes.BaseResidual.edgeJets_of_outer_collar {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : SlowBorelBase.Inner → V} (hf : ContDiff ℝ (↑⊤) f) {c left right inner cut : ℝ} (hc : 0 < c) (hl : Real.exp left < inner) (_hi : inner ≤ cut) (hr : cut < Real.exp right) (hzero : ∀ (w : SlowBorelBase.Inner), w.1 < inner → f w = 0) (ho : PolynomialEdgeJets (outerWindow cut right) (activeZeta c left right) (activeDelta left right) f) : PolynomialEdgeJets (activeWindow left right) (activeZeta c left right) (activeDelta left right) f

Compact middle-region bounds and actual zero germs at the inner edge extend an outer collar estimate to the entire active annulus.

theorem NavierStokes.BaseResidual.terminal_zeta_eq {c left y0 : ℝ} {w : SlowBorelBase.Inner} (hw : 0 < w.1) : SlowFirstOrderEdge.zeta c (Real.exp left) y0 w.1 = activeZeta c left (y0 + 3) w

theorem NavierStokes.BaseResidual.terminal_delta_eq {left y0 : ℝ} {w : SlowBorelBase.Inner} (hw : 0 < w.1) : SlowFirstOrderEdge.edgeDistance (Real.exp left) y0 w.1 = activeDelta left (y0 + 3) w

noncomputable def NavierStokes.BaseResidual.stressSlotInjection : ℝ →L[ℝ] SlowBorelBase.Inner

Stress slot injection, given by (ContinuousLinearMap.id ℝ ℝ).prod 0.

Equations

• NavierStokes.BaseResidual.stressSlotInjection = (ContinuousLinearMap.id ℝ ℝ).prod 0

theorem NavierStokes.BaseResidual.firstOrder_pair_outer_edgeJets (C : ℝ) (d : OutgoingTail.TailData) (y0 : ℝ) {c left width : ℝ} (hc : 0 < c) (hw : 0 < width) (hl : left < y0 + 3 - width) {F : SlowBorelBase.Inner → SlowBorelBase.Inner} (he : ∀ w ∈ outerWindow (Real.exp (y0 + 3 - width)) (y0 + 3), F =ᶠ[nhds w] fun (v : SlowBorelBase.Inner) => (SlowFirstOrderEdge.stressX C d y0 v, 0)) : PolynomialEdgeJets (outerWindow (Real.exp (y0 + 3 - width)) (y0 + 3)) (activeZeta c left (y0 + 3)) (activeDelta left (y0 + 3)) F

The first-order collar bound is imported from the actual backward viscous stress primitive. Only its equality with the coefficient is supplied.

theorem NavierStokes.BaseResidual.exists_weighted_base_scales_from_primitives {h : ℝ} (hh : 0 < h) (C : ℝ) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (tail : OutgoingTail.TailData) (y0 : ℝ) {c left width inner : ℝ} (hc : 0 < c) (hw : 0 < width) (hl : Real.exp left < inner) (hi : inner ≤ Real.exp (y0 + 3 - width)) (hs : HigherInteriorSupport d left (y0 + 3)) (hz : ∀ (w : SlowBorelBase.Inner), w.1 < inner → stressPair d 1 w = 0) (he : ∀ w ∈ outerWindow (Real.exp (y0 + 3 - width)) (y0 + 3), stressPair d 1 =ᶠ[nhds w] fun (v : SlowBorelBase.Inner) => (SlowFirstOrderEdge.stressX C tail y0 v, 0)) {K : Set SlowBorelBase.Inner} (hK : IsCompact K) (hWK : activeWindow left (y0 + 3) ⊆ K) (B : ℕ) : ∃ (a : ℕ → ℕ), B ≤ a 0 ∧ SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) K a ∧ ∀ (m : ℕ), ∃ (D : ℝ), 0 < D ∧ ∃ (N : ℕ), ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ activeWindow left (y0 + 3), ‖SlowBorelBase.blownJet m (fun (v : SlowBorelBase.Chart) => normalizedTensor a h d v - stressPair d 0 v.2) (q, w)‖ ≤ D * q ^ h * activeZeta c left (y0 + 3) w * (activeDelta left (y0 + 3) w)⁻¹ ^ N

A common scale sequence with the full weighted tensor estimate, constructed from support, smoothness, and the actual first-order primitive. No tensor estimate or summation-tail estimate is assumed.