Finite slow residuals and their radial stress primitives

The finite profiles and all derivatives below are the actual functions from SlowExpansionResidual. The stored radial variable in SlowRecursion is beta = V / X; its conversion to a flux includes the factor X.

The stress operator is the two tangential radial operators in (24). It is not identified with the divergence of an unspecified symmetric tensor.

noncomputable def NavierStokes.SlowResidualMatching.ofBeta (phi axial beta pressure : ℕ → SimilarityProfile.InnerProfile) : SlowExpansionResidual.SlowProfiles

Convert a regular radial quotient to the actual radial flux.

Equations

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

noncomputable def NavierStokes.SlowResidualMatching.hierarchyProfiles {R : ℝ} {U : Set ℂ} {h C : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : SlowRecursion.LocalHierarchy R U h C base) : SlowExpansionResidual.SlowProfiles

The actual functions constructed by the regular-axis recursion.

Equations

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

theorem NavierStokes.SlowResidualMatching.convolution_eq_positiveAxis (F : ℕ → ℕ → ℝ) (n : ℕ) : SlowExpansionResidual.convolution F n = PositiveAxisSystem.convolution n F

theorem NavierStokes.SlowResidualMatching.precedingDiffusion_eq_previous (h b : ℝ) (f : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) : PositiveAxisSystem.precedingDiffusion h b f n w = SlowExpansionResidual.previous (fun (j : ℕ) => SlowExpansionResidual.Z2 h (b + SlowExpansionResidual.slowOrder h j) (f j) w) n

theorem NavierStokes.SlowResidualMatching.angular_convection_ofBeta (h : ℝ) (phi axial beta pressure : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) {w : SimilarityProfile.InnerPoint} (hX : w.1 ≠ 0) : SlowExpansionResidual.convolution (fun (i j : ℕ) => (ofBeta phi axial beta pressure).flux i w * (SimilarityProfile.partialX (phi j) w + phi j w / w.1) + axial i w * SimilarityProfile.Z h (SlowExpansionResidual.angularExponent h + SlowExpansionResidual.slowOrder h j) (phi j) w) n = PositiveAxisSystem.convolution n (PositiveAxisSystem.angularConvection h w.2 w.1 (fun (j : ℕ) => PositiveAxisSystem.actualJet (phi j) w) (fun (j : ℕ) => PositiveAxisSystem.actualJet (axial j) w) fun (j : ℕ) => beta j w)

theorem NavierStokes.SlowResidualMatching.axial_convection_ofBeta (h : ℝ) (phi axial beta pressure : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) : SlowExpansionResidual.convolution (fun (i j : ℕ) => (ofBeta phi axial beta pressure).flux i w * SimilarityProfile.partialX (axial j) w + axial i w * SimilarityProfile.Z h (SlowExpansionResidual.axialExponent h + SlowExpansionResidual.slowOrder h j) (axial j) w) n = PositiveAxisSystem.convolution n (PositiveAxisSystem.axialConvection h w.2 w.1 (fun (j : ℕ) => PositiveAxisSystem.actualJet (axial j) w) fun (j : ℕ) => beta j w)

theorem NavierStokes.SlowResidualMatching.positiveOrder_tangential_coefficients (h C : ℝ) (phi axial beta pressure : ℕ → SimilarityProfile.InnerProfile) (k : SimilarityProfile.InnerProfile) (n : ℕ) {w : SimilarityProfile.InnerPoint} (hX : w.1 ≠ 0) (he : PositiveAxisSystem.PositiveOrderEquations h C w.2 w.1 n (fun (j : ℕ) => PositiveAxisSystem.actualJet (phi j) w) (fun (j : ℕ) => PositiveAxisSystem.actualJet (axial j) w) (fun (j : ℕ) => beta j w) (PositiveAxisSystem.actualJet k w) (PositiveAxisSystem.actualJet (pressure n) w) (PositiveAxisSystem.precedingDiffusion h (PositiveAxisSystem.angularPower h) phi n w) (PositiveAxisSystem.precedingDiffusion h (PositiveAxisSystem.axialPower h) axial n w) (AxisSourceRegularity.previousOmegaDivX h axial beta n w)) : SlowExpansionResidual.angularCoefficient h (ofBeta phi axial beta pressure) n w = 0 ∧ SlowExpansionResidual.axialCoefficient h (ofBeta phi axial beta pressure) n w = 0

The solved angular and axial rows are the literal residual coefficients.

theorem NavierStokes.SlowResidualMatching.hierarchy_tangential_coefficients {R : ℝ} {U : Set ℂ} {h C : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : SlowRecursion.LocalHierarchy R U h C base) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) : SlowExpansionResidual.angularCoefficient h (hierarchyProfiles A) n (X, eta) = 0 ∧ SlowExpansionResidual.axialCoefficient h (hierarchyProfiles A) n (X, eta) = 0

theorem NavierStokes.SlowResidualMatching.omegaCoefficient_eq_omega (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (w : SimilarityProfile.InnerPoint) : SlowExpansionResidual.omegaCoefficient h f n w = AxisSourceRegularity.omega h f.axial f.flux n w

theorem NavierStokes.SlowResidualMatching.previousOmega_ofBeta (h : ℝ) (phi axial beta pressure : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) (hX : w.1 ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) (hb : ∀ j < n, ContDiffAt ℝ 2 (beta j) w) : SlowExpansionResidual.previous (fun (j : ℕ) => SlowExpansionResidual.omegaCoefficient h (ofBeta phi axial beta pressure) j w) n / w.1 = AxisSourceRegularity.previousOmegaDivX h axial beta n w

theorem NavierStokes.SlowResidualMatching.positiveOrder_pressure_coefficient (h C : ℝ) (phi axial beta pressure : ℕ → SimilarityProfile.InnerProfile) (k : SimilarityProfile.InnerProfile) (n : ℕ) {w : SimilarityProfile.InnerPoint} (hX : w.1 ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) (hb : ∀ j < n, ContDiffAt ℝ 2 (beta j) w) (he : PositiveAxisSystem.PositiveOrderEquations h C w.2 w.1 n (fun (j : ℕ) => PositiveAxisSystem.actualJet (phi j) w) (fun (j : ℕ) => PositiveAxisSystem.actualJet (axial j) w) (fun (j : ℕ) => beta j w) (PositiveAxisSystem.actualJet k w) (PositiveAxisSystem.actualJet (pressure n) w) (PositiveAxisSystem.precedingDiffusion h (PositiveAxisSystem.angularPower h) phi n w) (PositiveAxisSystem.precedingDiffusion h (PositiveAxisSystem.axialPower h) axial n w) (AxisSourceRegularity.previousOmegaDivX h axial beta n w)) : SlowExpansionResidual.pressureCoefficient h C (ofBeta phi axial beta pressure) n w = 0

theorem NavierStokes.SlowResidualMatching.partialX_congr_germ {f g : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hfg : f =ᶠ[nhds w] g) : SimilarityProfile.partialX f =ᶠ[nhds w] SimilarityProfile.partialX g

theorem NavierStokes.SlowResidualMatching.Z_congr_germ (h b : ℝ) {f g : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hfg : f =ᶠ[nhds w] g) : SimilarityProfile.Z h b f =ᶠ[nhds w] SimilarityProfile.Z h b g

theorem NavierStokes.SlowResidualMatching.Z2_congr_germ (h b : ℝ) {f g : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hfg : f =ᶠ[nhds w] g) : SlowExpansionResidual.Z2 h b f w = SlowExpansionResidual.Z2 h b g w

theorem NavierStokes.SlowResidualMatching.T_congr_germ (h b : ℝ) {f g : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hfg : f =ᶠ[nhds w] g) : SimilarityProfile.T h b f w = SimilarityProfile.T h b g w

theorem NavierStokes.SlowResidualMatching.transportCoefficient_congr_germ (h e α m : ℝ) {v u f s v' u' f' s' : ℕ → SimilarityProfile.InnerProfile} (n : ℕ) {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) (hs : s n w = s' n w) : SlowExpansionResidual.transportCoefficient h e α m v u f s n w = SlowExpansionResidual.transportCoefficient h e α m v' u' f' s' n w

A finite residual coefficient depends only on the germs of the coefficients through its own order. No global equality is required.

theorem NavierStokes.SlowResidualMatching.angularCoefficient_congr_germ (h : ℝ) {f g : SlowExpansionResidual.SlowProfiles} (n : ℕ) {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) (hf : ∀ j ≤ n, f.phi j =ᶠ[nhds w] g.phi j) : SlowExpansionResidual.angularCoefficient h f n w = SlowExpansionResidual.angularCoefficient h g n w

theorem NavierStokes.SlowResidualMatching.axialCoefficient_congr_germ (h : ℝ) {f g : SlowExpansionResidual.SlowProfiles} (n : ℕ) {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 : f.pressure n =ᶠ[nhds w] g.pressure n) : SlowExpansionResidual.axialCoefficient h f n w = SlowExpansionResidual.axialCoefficient h g n w

theorem NavierStokes.SlowResidualMatching.omegaCoefficient_congr_germ (h : ℝ) {f g : SlowExpansionResidual.SlowProfiles} (n : ℕ) {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) : SlowExpansionResidual.omegaCoefficient h f n w = SlowExpansionResidual.omegaCoefficient h g n w

theorem NavierStokes.SlowResidualMatching.slowOrder_mono {h : ℝ} (hh : 0 ≤ h) : Monotone (SlowExpansionResidual.slowOrder h)

Monotonicity of slow orders is the precise reason every omitted pair has at least the next power of q.

noncomputable def NavierStokes.SlowResidualMatching.pairTailSize (N : ℕ) (K : ℕ → ℕ → ℝ) : ℝ

Pair tail size, given by ∑ ij ∈ (pairs N).filter (fun ij => N < ij.1 + ij.2), |K ij.1 ij.2|.

Equations

• NavierStokes.SlowResidualMatching.pairTailSize N K = ∑ ij ∈ NavierStokes.SlowExpansionResidual.pairs N with N < ij.1 + ij.2, |K ij.1 ij.2|

theorem NavierStokes.SlowResidualMatching.pairTailSize_nonneg (N : ℕ) (K : ℕ → ℕ → ℝ) : 0 ≤ pairTailSize N K

theorem NavierStokes.SlowResidualMatching.pairTail_bound {q h : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) (hh : 0 ≤ h) (N : ℕ) (b : ℝ) (K : ℕ → ℕ → ℝ) : |SlowExpansionResidual.pairTail N (fun (n : ℕ) => q ^ (b + SlowExpansionResidual.slowOrder h n)) K| ≤ pairTailSize N K * q ^ (b + SlowExpansionResidual.slowOrder h (N + 1))

noncomputable def NavierStokes.SlowResidualMatching.transportKernel (h e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : ℕ → ℕ → ℝ

Transport kernel, constructed using transportPair.

Equations

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

noncomputable def NavierStokes.SlowResidualMatching.transportTailSize (N : ℕ) (h e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : ℝ

Transport tail size, given by pairTailSize N (transportKernel h e α v u f w) + |Z2 h (e + slowOrder h N) (f N) w|.

Equations

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

theorem NavierStokes.SlowResidualMatching.transportTailSize_nonneg (N : ℕ) (h e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : 0 ≤ transportTailSize N h e α v u f w

theorem NavierStokes.SlowResidualMatching.transportTail_bound {q h : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) (hh : 0 ≤ h) (N : ℕ) (e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : |SlowExpansionResidual.transportTail N q h e α v u f w| ≤ transportTailSize N h e α v u f w * q ^ (e - 1 + SlowExpansionResidual.slowOrder h (N + 1))

Both the omitted quadratic interactions and the last axial viscosity are bounded, with their true next-order power.

noncomputable def NavierStokes.SlowResidualMatching.pressureTailSize (N : ℕ) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (w : SimilarityProfile.InnerPoint) : ℝ

Pressure tail size, constructed using transportTailSize.

Equations

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

theorem NavierStokes.SlowResidualMatching.pressureTailSize_nonneg (N : ℕ) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (w : SimilarityProfile.InnerPoint) : 0 ≤ pressureTailSize N h C f w

theorem NavierStokes.SlowResidualMatching.pressureTail_bound {q h : ℝ} (hq : 0 < q) (hq1 : q ≤ 1) (hh : 0 ≤ h) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (w : SimilarityProfile.InnerPoint) : |SlowExpansionResidual.pressureTail N q h C f w| ≤ pressureTailSize N h C f w * q ^ (SlowExpansionResidual.pressureExponent h + SlowExpansionResidual.slowOrder h (N + 1))

The radial remainder retains the last radial acceleration as well as the omitted swirl products. Its exponent is not silently equated with the stronger tangential exponent.

noncomputable def NavierStokes.SlowResidualMatching.radiusPoint (w : SimilarityProfile.InnerPoint) : SimilarityProfile.InnerPoint

The change from cylindrical radius R to the regular variable X.

Equations

• NavierStokes.SlowResidualMatching.radiusPoint w = (w.1 ^ 2 / 2, w.2)

noncomputable def NavierStokes.SlowResidualMatching.fromRadius (F : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : ℝ

From radius, given by F (Real.sqrt (2 * w.1), w.2).

Equations

• NavierStokes.SlowResidualMatching.fromRadius F w = F (√(2 * w.1), w.2)

noncomputable def NavierStokes.SlowResidualMatching.toRadius (f : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : ℝ

To radius, given by f (radiusPoint w).

Equations

• NavierStokes.SlowResidualMatching.toRadius f w = f (NavierStokes.SlowResidualMatching.radiusPoint w)

noncomputable def NavierStokes.SlowResidualMatching.swirlRadius (C : ℝ) (f : SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : ℝ

Swirl radius, given by w.1 / C * toRadius f w.

Equations

• NavierStokes.SlowResidualMatching.swirlRadius C f w = w.1 / C * NavierStokes.SlowResidualMatching.toRadius f w

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

theorem NavierStokes.SlowResidualMatching.fromRadius_smoothAt {F : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hX : 0 < w.1) (hF : ContDiffAt ℝ (↑⊤) F (√(2 * w.1), w.2)) : ContDiffAt ℝ (↑⊤) (fromRadius F) w

theorem NavierStokes.SlowResidualMatching.partialX_fromRadius {F : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hX : 0 < w.1) (hF : DifferentiableAt ℝ F (√(2 * w.1), w.2)) : SimilarityProfile.partialX (fromRadius F) w = SimilarityProfile.partialX F (√(2 * w.1), w.2) / √(2 * w.1)

theorem NavierStokes.SlowResidualMatching.primitive_stress_smoothAt {S : Set ℝ} (hS : IsOpen S) {F : SimilarityProfile.InnerProfile} (hF : SlowStressSupport.Smooth S F) (m : ℕ) {w : SimilarityProfile.InnerPoint} (hR : 0 < w.1) (heta : w.2 ∈ S) : ContDiffAt ℝ (↑⊤) (SlowStressSupport.stress m F) w

At a positive radius the primitive stress is smooth without an axis vanishing assumption. The latter is needed only to extend through R=0.

theorem NavierStokes.SlowResidualMatching.primitive_stress_radial_identity {S : Set ℝ} (hS : IsOpen S) {F : SimilarityProfile.InnerProfile} (hF : SlowStressSupport.Smooth S F) (m : ℕ) {w : SimilarityProfile.InnerPoint} (hR : 0 < w.1) (heta : w.2 ∈ S) : ↑m * w.1 ^ (m - 1) * SlowStressSupport.stress m F w + w.1 ^ m * SimilarityProfile.partialX (SlowStressSupport.stress m F) w = -F w

noncomputable def NavierStokes.SlowResidualMatching.thetaDensity (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (w : SimilarityProfile.InnerPoint) : ℝ

Literal R²-weighted angular residual.

Equations

• NavierStokes.SlowResidualMatching.thetaDensity h C f n w = w.1 ^ 3 / C * NavierStokes.SlowExpansionResidual.angularCoefficient h f n (NavierStokes.SlowResidualMatching.radiusPoint w)

noncomputable def NavierStokes.SlowResidualMatching.zDensity (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (w : SimilarityProfile.InnerPoint) : ℝ

Literal R-weighted axial residual.

Equations

• NavierStokes.SlowResidualMatching.zDensity h f n w = w.1 * NavierStokes.SlowExpansionResidual.axialCoefficient h f n (NavierStokes.SlowResidualMatching.radiusPoint w)

noncomputable def NavierStokes.SlowResidualMatching.thetaStress (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) : SimilarityProfile.InnerProfile

Theta stress, given by fromRadius (SlowStressSupport.stress 2 (thetaDensity h C f n)).

Equations

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

noncomputable def NavierStokes.SlowResidualMatching.zStress (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) : SimilarityProfile.InnerProfile

Z stress, given by fromRadius (SlowStressSupport.stress 1 (zDensity h f n)).

Equations

• NavierStokes.SlowResidualMatching.zStress h f n = NavierStokes.SlowResidualMatching.fromRadius (NavierStokes.SlowStressSupport.stress 1 (NavierStokes.SlowResidualMatching.zDensity h f n))

theorem NavierStokes.SlowResidualMatching.thetaStress_smoothAt {S : Set ℝ} (hS : IsOpen S) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (hF : SlowStressSupport.Smooth S (thetaDensity h C f n)) {w : SimilarityProfile.InnerPoint} (hX : 0 < w.1) (heta : w.2 ∈ S) : ContDiffAt ℝ (↑⊤) (thetaStress h C f n) w

theorem NavierStokes.SlowResidualMatching.zStress_smoothAt {S : Set ℝ} (hS : IsOpen S) (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (hF : SlowStressSupport.Smooth S (zDensity h f n)) {w : SimilarityProfile.InnerPoint} (hX : 0 < w.1) (heta : w.2 ∈ S) : ContDiffAt ℝ (↑⊤) (zStress h f n) w

theorem NavierStokes.SlowResidualMatching.thetaStress_identity {S : Set ℝ} (hS : IsOpen S) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (hF : SlowStressSupport.Smooth S (thetaDensity h C f n)) {w : SimilarityProfile.InnerPoint} (hX : 0 < w.1) (heta : w.2 ∈ S) : √(2 * w.1) * SimilarityProfile.partialX (thetaStress h C f n) w + 2 * thetaStress h C f n w / √(2 * w.1) = -(√(2 * w.1) / C * SlowExpansionResidual.angularCoefficient h f n w)

The angular primitive has exactly the required unweighted divergence.

theorem NavierStokes.SlowResidualMatching.zStress_identity {S : Set ℝ} (hS : IsOpen S) (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (hF : SlowStressSupport.Smooth S (zDensity h f n)) {w : SimilarityProfile.InnerPoint} (hX : 0 < w.1) (heta : w.2 ∈ S) : √(2 * w.1) * SimilarityProfile.partialX (zStress h f n) w + zStress h f n w / √(2 * w.1) = -SlowExpansionResidual.axialCoefficient h f n w

noncomputable def NavierStokes.SlowResidualMatching.physicalThetaStress (N : ℕ) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) : SimilarityProfile.PhysicalProfile

Physical theta stress, given by finiteProfile N h (angularExponent h) (thetaStress h C f).

Equations

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

noncomputable def NavierStokes.SlowResidualMatching.physicalZStress (N : ℕ) (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) : SimilarityProfile.PhysicalProfile

Physical Z stress, given by finiteProfile N h (angularExponent h) (zStress h f).

Equations

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

theorem NavierStokes.SlowResidualMatching.radialDivergence_sum {ι : Type u_1} (s : Finset ι) (k : ℝ) (F : ι → SimilarityProfile.PhysicalProfile) (p : SimilarityProfile.PhysicalPoint) (hF : ∀ i ∈ s, DifferentiableAt ℝ (F i) p) : LeadingStress.radialDivergence k (fun (y : SimilarityProfile.PhysicalPoint) => ∑ i ∈ s, F i y) p = ∑ i ∈ s, LeadingStress.radialDivergence k (F i) p

theorem NavierStokes.SlowResidualMatching.physicalThetaStress_divergence {S : Set ℝ} (hS : IsOpen S) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (hF : ∀ n ≤ N, SlowStressSupport.Smooth S (thetaDensity h C f n)) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (heta : (SimilarityProfile.inner h p).2 ∈ S) : LeadingStress.radialDivergence 2 (physicalThetaStress N h C f) p = -(√(2 * p.2.1) * C⁻¹ * SlowExpansionResidual.finiteSeries N (SimilarityProfile.q h p) h (SlowExpansionResidual.angularExponent h - 1) fun (n : ℕ) => SlowExpansionResidual.angularCoefficient h f n (SimilarityProfile.inner h p))

theorem NavierStokes.SlowResidualMatching.physicalZStress_divergence {S : Set ℝ} (hS : IsOpen S) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : SlowExpansionResidual.SlowProfiles) (hF : ∀ n ≤ N, SlowStressSupport.Smooth S (zDensity h f n)) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (heta : (SimilarityProfile.inner h p).2 ∈ S) : LeadingStress.radialDivergence 1 (physicalZStress N h f) p = -SlowExpansionResidual.finiteSeries N (SimilarityProfile.q h p) h (SlowExpansionResidual.axialExponent h - 1) fun (n : ℕ) => SlowExpansionResidual.axialCoefficient h f n (SimilarityProfile.inner h p)

noncomputable def NavierStokes.SlowResidualMatching.tangentialStressForce (theta axial : SimilarityProfile.PhysicalProfile) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.Space

The two radial tangential operators appearing in the manuscript. They are written as an actual Cartesian vector; no unspecified tensor is used.

Equations

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

noncomputable def NavierStokes.SlowResidualMatching.retainedRadialForce (N : ℕ) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.Space

The pressure recurrence contributes this separate radial vector.

Equations

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

theorem NavierStokes.SlowResidualMatching.navierStokesResidual_eq_stress_add_tails {S : Set ℝ} (hS : IsOpen S) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (hTheta : ∀ n ≤ N, SlowStressSupport.Smooth S (thetaDensity h C f n)) (hZ : ∀ n ≤ N, SlowStressSupport.Smooth S (zDensity h f n)) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) (heta : (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x)).2 ∈ S) (hv : ∀ n ≤ N, ContDiffAt ℝ 2 (f.flux n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hphi : ∀ n ≤ N, ContDiffAt ℝ 2 (f.phi n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hu : ∀ n ≤ N, ContDiffAt ℝ 2 (f.axial n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hp : ∀ n ≤ N, DifferentiableAt ℝ (f.pressure n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) : ProblemStatement.navierStokesResidual (SlowExpansionResidual.slowVelocity N h C f) (SlowExpansionResidual.slowPressureField N h f) t x = tangentialStressForce (physicalThetaStress N h C f) (physicalZStress N h f) t x + retainedRadialForce N h C f t x + SlowExpansionResidual.truncationResidual N h C f t x

Exact finite field matching. All nonlinear interactions not in the retained coefficients, the final axial viscosities, and the final radial acceleration remain in the explicitly defined truncationResidual.

theorem NavierStokes.SlowResidualMatching.navierStokesResidual_eq_stress_add_truncation {S : Set ℝ} (hS : IsOpen S) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (hTheta : ∀ n ≤ N, SlowStressSupport.Smooth S (thetaDensity h C f n)) (hZ : ∀ n ≤ N, SlowStressSupport.Smooth S (zDensity h f n)) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) (heta : (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x)).2 ∈ S) (hv : ∀ n ≤ N, ContDiffAt ℝ 2 (f.flux n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hphi : ∀ n ≤ N, ContDiffAt ℝ 2 (f.phi n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hu : ∀ n ≤ N, ContDiffAt ℝ 2 (f.axial n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hp : ∀ n ≤ N, DifferentiableAt ℝ (f.pressure n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hpressure : ∀ n ≤ N, SlowExpansionResidual.pressureCoefficient h C f n (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x)) = 0) : ProblemStatement.navierStokesResidual (SlowExpansionResidual.slowVelocity N h C f) (SlowExpansionResidual.slowPressureField N h f) t x = tangentialStressForce (physicalThetaStress N h C f) (physicalZStress N h f) t x + SlowExpansionResidual.truncationResidual N h C f t x

If the pressure was recomputed from its actual radial recurrence, the finite residual consists of the tangential stress force and the explicit tails.

theorem NavierStokes.SlowResidualMatching.toRadius_differentiableAt {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : DifferentiableAt ℝ (toRadius f) w

theorem NavierStokes.SlowResidualMatching.toRadius_contDiffAt_two {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ 2 f (radiusPoint w)) : ContDiffAt ℝ 2 (toRadius f) w

theorem NavierStokes.SlowResidualMatching.partialX_toRadius {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : SimilarityProfile.partialX (toRadius f) w = w.1 * SimilarityProfile.partialX f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.partialEta_toRadius {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : SimilarityProfile.partialEta (toRadius f) w = SimilarityProfile.partialEta f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.partialX_swirlRadius (C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : SimilarityProfile.partialX (swirlRadius C f) w = f (radiusPoint w) / C + w.1 ^ 2 / C * SimilarityProfile.partialX f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.partialEta_swirlRadius (C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : SimilarityProfile.partialEta (swirlRadius C f) w = w.1 / C * SimilarityProfile.partialEta f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.partialXX_toRadius {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ 2 f (radiusPoint w)) : SimilarityProfile.partialX (SimilarityProfile.partialX (toRadius f)) w = SimilarityProfile.partialX f (radiusPoint w) + w.1 ^ 2 * SimilarityProfile.partialX (SimilarityProfile.partialX f) (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.timeOp_toRadius (h b : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : SlowStressSupport.timeOp h b (toRadius f) w = SimilarityProfile.T h b f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.axialOp_toRadius (h b : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : SlowStressSupport.axialOp h b (toRadius f) w = SimilarityProfile.Z h b f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.timeOp_swirlRadius (h b C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : SlowStressSupport.timeOp h b (swirlRadius C f) w = w.1 / C * SimilarityProfile.T h (b - 1 / 2) f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.axialOp_swirlRadius (h b C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ f (radiusPoint w)) : SlowStressSupport.axialOp h b (swirlRadius C f) w = w.1 / C * SimilarityProfile.Z h (b - 1 / 2) f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.axialOp_congr_germ (h b : ℝ) {f g : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hfg : f =ᶠ[nhds w] g) : SlowStressSupport.axialOp h b f w = SlowStressSupport.axialOp h b g w

theorem NavierStokes.SlowResidualMatching.axialOp2_toRadius (h b : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ 2 f (radiusPoint w)) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowStressSupport.axialOp2 h b (toRadius f) w = SlowExpansionResidual.Z2 h b f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.axialOp2_swirlRadius (h b C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ 2 f (radiusPoint w)) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowStressSupport.axialOp2 h b (swirlRadius C f) w = w.1 / C * SlowExpansionResidual.Z2 h (b - 1 / 2) f (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.partialXX_swirlRadius (C : ℝ) {f : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hf : ContDiffAt ℝ 2 f (radiusPoint w)) : SimilarityProfile.partialX (SimilarityProfile.partialX (swirlRadius C f)) w = 3 * w.1 / C * SimilarityProfile.partialX f (radiusPoint w) + w.1 ^ 3 / C * SimilarityProfile.partialX (SimilarityProfile.partialX f) (radiusPoint w)

@[reducible, inline]

abbrev NavierStokes.SlowResidualMatching.TailIndex : Type

An explicit finite index for all omitted transport terms. none is the last axial-viscosity coefficient.

Equations

• NavierStokes.SlowResidualMatching.TailIndex = Option (ℕ × ℕ)

noncomputable def NavierStokes.SlowResidualMatching.transportIndices (N : ℕ) : Finset TailIndex

Transport indices, given by insert none (((pairs N).filter (fun ij => N < ij.1 + ij.2)).image some).

Equations

• NavierStokes.SlowResidualMatching.transportIndices N = insert none (Finset.image some ({ij ∈ NavierStokes.SlowExpansionResidual.pairs N | N < ij.1 + ij.2}))

noncomputable def NavierStokes.SlowResidualMatching.transportPower (N : ℕ) (h e : ℝ) : TailIndex → ℝ

Transport power as an element of TailIndex → ℝ | none => e - 1 + slowOrder h (N + 1) | some ij => e - 1 + slowOrder h (ij.1 + ij.2).

Equations

• NavierStokes.SlowResidualMatching.transportPower N h e none = e - 1 + NavierStokes.SlowExpansionResidual.slowOrder h (N + 1)
• NavierStokes.SlowResidualMatching.transportPower N h e (some ij) = e - 1 + NavierStokes.SlowExpansionResidual.slowOrder h (ij.1 + ij.2)

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

Transport term as an element of TailIndex → InnerProfile | none => fun w => -Z2 h (e + slowOrder h N) (f N) w | some ij => fun w => transportKernel h e α v u f w ij.1 ij.2.

Equations

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

theorem NavierStokes.SlowResidualMatching.mem_transportIndices_some (N : ℕ) (ij : ℕ × ℕ) : some ij ∈ transportIndices N ↔ ij ∈ SlowExpansionResidual.pairs N ∧ N < ij.1 + ij.2

theorem NavierStokes.SlowResidualMatching.transportTail_eq_finite_monomials (N : ℕ) (q h e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : SlowExpansionResidual.transportTail N q h e α v u f w = ∑ i ∈ transportIndices N, q ^ transportPower N h e i * transportTerm N h e α v u f i w

This equality is an identity of actual functions, suitable for taking any fixed number of derivatives in q and the inner variables.

theorem NavierStokes.SlowResidualMatching.transportPower_lower {h : ℝ} (hh : 0 ≤ h) (N : ℕ) (e : ℝ) {i : TailIndex} (hi : i ∈ transportIndices N) : e - 1 + SlowExpansionResidual.slowOrder h (N + 1) ≤ transportPower N h e i

theorem NavierStokes.SlowResidualMatching.transportKernel_smoothAt (h e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (i j : ℕ) {w : SimilarityProfile.InnerPoint} (hv : ContDiffAt ℝ (↑⊤) (v i) w) (hu : ContDiffAt ℝ (↑⊤) (u i) w) (hf : ContDiffAt ℝ (↑⊤) (f j) w) (hX : w.1 ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (fun (y : SimilarityProfile.InnerPoint) => transportKernel h e α v u f y i j) w

theorem NavierStokes.SlowResidualMatching.transportTerm_smoothOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (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) {i : TailIndex} (hi : i ∈ transportIndices N) : ContDiffOn ℝ (↑⊤) (transportTerm N h e α v u f i) O

theorem NavierStokes.SlowResidualMatching.transportCoefficient_smoothAt (h e α m : ℝ) (v u f source : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) {w : SimilarityProfile.InnerPoint} (hv : ∀ j ≤ n, ContDiffAt ℝ (↑⊤) (v j) w) (hu : ∀ j ≤ n, ContDiffAt ℝ (↑⊤) (u j) w) (hf : ∀ j ≤ n, ContDiffAt ℝ (↑⊤) (f j) w) (hs : ContDiffAt ℝ (↑⊤) (source n) w) (hX : w.1 ≠ 0) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : ContDiffAt ℝ (↑⊤) (SlowExpansionResidual.transportCoefficient h e α m v u f source n) w

@[reducible, inline]

abbrev NavierStokes.SlowResidualMatching.PressureIndex : Type

Pressure index: an abbreviation for Sum TailIndex TailIndex.

Equations

• NavierStokes.SlowResidualMatching.PressureIndex = (NavierStokes.SlowResidualMatching.TailIndex ⊕ NavierStokes.SlowResidualMatching.TailIndex)

noncomputable def NavierStokes.SlowResidualMatching.pressureIndices (N : ℕ) : Finset PressureIndex

Pressure indices, given by ((transportIndices N).image Sum.inl) ∪ ((transportIndices N).image Sum.inr).

Equations

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

noncomputable def NavierStokes.SlowResidualMatching.pressurePower (N : ℕ) (h : ℝ) : PressureIndex → ℝ

Pressure power used in slow residual matching.

Equations

• NavierStokes.SlowResidualMatching.pressurePower N h (Sum.inl i) = NavierStokes.SlowResidualMatching.transportPower N h 0 i
• NavierStokes.SlowResidualMatching.pressurePower N h (Sum.inr none) = NavierStokes.SlowExpansionResidual.pressureExponent h + NavierStokes.SlowExpansionResidual.slowOrder h (N + 1)
• NavierStokes.SlowResidualMatching.pressurePower N h (Sum.inr (some ij)) = NavierStokes.SlowExpansionResidual.pressureExponent h + NavierStokes.SlowExpansionResidual.slowOrder h (ij.1 + ij.2)

noncomputable def NavierStokes.SlowResidualMatching.pressureTerm (N : ℕ) (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) : PressureIndex → SimilarityProfile.InnerProfile

Pressure term used in slow residual matching.

Equations

• NavierStokes.SlowResidualMatching.pressureTerm N h C f (Sum.inl i) = NavierStokes.SlowResidualMatching.transportTerm N h 0 (-(1 / 2)) f.flux f.axial f.flux i
• NavierStokes.SlowResidualMatching.pressureTerm N h C f (Sum.inr none) = NavierStokes.SlowExpansionResidual.omegaCoefficient h f N
• NavierStokes.SlowResidualMatching.pressureTerm N h C f (Sum.inr (some ij)) = fun (w : NavierStokes.SimilarityProfile.InnerPoint) => -(2 * w.1 * C⁻¹ ^ 2) * (f.phi ij.1 w * f.phi ij.2 w)

theorem NavierStokes.SlowResidualMatching.pressure_indices_disjoint (N : ℕ) : Disjoint (Finset.image Sum.inl (transportIndices N)) (Finset.image Sum.inr (transportIndices N))

theorem NavierStokes.SlowResidualMatching.pressureTail_eq_finite_monomials (N : ℕ) (q h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (w : SimilarityProfile.InnerPoint) : SlowExpansionResidual.pressureTail N q h C f w = ∑ i ∈ pressureIndices N, q ^ pressurePower N h i * pressureTerm N h C f i w

theorem NavierStokes.SlowResidualMatching.pressurePower_lower {h : ℝ} (hh : 0 ≤ h) (N : ℕ) {i : PressureIndex} (hi : i ∈ pressureIndices N) : SlowExpansionResidual.pressureExponent h + SlowExpansionResidual.slowOrder h (N + 1) ≤ pressurePower N h i

theorem NavierStokes.SlowResidualMatching.pressureTerm_smoothOn {O : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (N : ℕ) (h 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) {i : PressureIndex} (hi : i ∈ pressureIndices N) : ContDiffOn ℝ (↑⊤) (pressureTerm N h C f i) O

theorem NavierStokes.SlowResidualMatching.radialTail_eq_finite_monomials {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowExpansionResidual.SlowProfiles) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hs : 0 < p.2.1) : SlowExpansionResidual.pressureTail N (SimilarityProfile.q h p) h C f (SimilarityProfile.inner h p) / (2 * p.2.1) = ∑ i ∈ pressureIndices N, SimilarityProfile.q h p ^ (pressurePower N h i - 1) * (pressureTerm N h C f i (SimilarityProfile.inner h p) / (2 * (SimilarityProfile.inner h p).1))

Division by the physical radial energy is converted to a single q power and an ordinary smooth inner coefficient away from X=0.

theorem NavierStokes.SlowResidualMatching.common_tail_power_lower {h : ℝ} (hh : 0 ≤ h) (N : ℕ) : SlowExpansionResidual.pressureExponent h - 1 + SlowExpansionResidual.slowOrder h (N + 1) = 2 * ↑N * h - 2 ∧ SlowExpansionResidual.pressureExponent h - 1 + SlowExpansionResidual.slowOrder h (N + 1) ≤ SlowExpansionResidual.angularExponent h - 1 + SlowExpansionResidual.slowOrder h (N + 1) ∧ SlowExpansionResidual.pressureExponent h - 1 + SlowExpansionResidual.slowOrder h (N + 1) ≤ SlowExpansionResidual.axialExponent h - 1 + SlowExpansionResidual.slowOrder h (N + 1)

theorem NavierStokes.SlowResidualMatching.finite_monomial_inner_jet_bound {ι : Type u_1} (s : Finset ι) (b : ι → ℝ) (F : ι → SimilarityProfile.InnerProfile) (bmin : ℝ) {O K : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O) (hF : ∀ i ∈ s, ContDiffOn ℝ (↑⊤) (F i) O) (hb : ∀ i ∈ s, bmin ≤ b i) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ K, ‖iteratedFDeriv ℝ m (fun (y : SimilarityProfile.InnerPoint) => ∑ i ∈ s, q ^ b i * F i y) w‖ ≤ C * q ^ bmin

Compact coefficient jets give a uniform bound for every fixed inner derivative of a finite sum of actual powers. The exponent is unchanged by inner differentiation.

theorem NavierStokes.SlowResidualMatching.transportTail_inner_jet_bound {O K : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O) {h : ℝ} (hh : 0 ≤ h) (N : ℕ) (e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (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 : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ K, ‖iteratedFDeriv ℝ m (SlowExpansionResidual.transportTail N q h e α v u f) w‖ ≤ C * q ^ (e - 1 + SlowExpansionResidual.slowOrder h (N + 1))

theorem NavierStokes.SlowResidualMatching.pressureTail_inner_jet_bound {O K : Set SimilarityProfile.InnerPoint} (hO : IsOpen O) (hK : IsCompact K) (hKO : K ⊆ O) {h : ℝ} (hh : 0 ≤ h) (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 : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℝ), 0 < q → q ≤ 1 → ∀ w ∈ K, ‖iteratedFDeriv ℝ m (SlowExpansionResidual.pressureTail N q h C₀ f) w‖ ≤ C * q ^ (SlowExpansionResidual.pressureExponent h + SlowExpansionResidual.slowOrder h (N + 1))

theorem NavierStokes.SlowResidualMatching.orderExponent_eq_axial (h : ℝ) (n : ℕ) : SlowStressSupport.orderExponent h n = SlowExpansionResidual.axialExponent h + SlowExpansionResidual.slowOrder h n

theorem NavierStokes.SlowResidualMatching.orderExponent_sub_half (h : ℝ) (n : ℕ) : SlowStressSupport.orderExponent h n - 1 / 2 = SlowExpansionResidual.angularExponent h + SlowExpansionResidual.slowOrder h n

theorem NavierStokes.SlowResidualMatching.previous_of_pos (a : ℕ → ℝ) {n : ℕ} (hn : 0 < n) : SlowExpansionResidual.previous a n = a (n - 1)

theorem NavierStokes.SlowResidualMatching.angular_radius_pair (h C : ℝ) (hC : C ≠ 0) (f : SlowExpansionResidual.SlowProfiles) (i j : ℕ) {w : SimilarityProfile.InnerPoint} (hR : w.1 ≠ 0) (hf : DifferentiableAt ℝ (f.phi j) (radiusPoint w)) : w.1 * toRadius (f.flux i) w * SimilarityProfile.partialX (swirlRadius C (f.phi j)) w + toRadius (f.flux i) w * swirlRadius C (f.phi j) w + w.1 ^ 2 * toRadius (f.axial i) w * SlowStressSupport.axialOp h (SlowStressSupport.orderExponent h j) (swirlRadius C (f.phi j)) w = w.1 ^ 3 / C * transportKernel h (SlowExpansionResidual.angularExponent h) 1 f.flux f.axial f.phi (radiusPoint w) i j

theorem NavierStokes.SlowResidualMatching.axial_radius_pair (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (i j : ℕ) {w : SimilarityProfile.InnerPoint} (hf : DifferentiableAt ℝ (f.axial j) (radiusPoint w)) : toRadius (f.flux i) w * SimilarityProfile.partialX (toRadius (f.axial j)) w + w.1 * toRadius (f.axial i) w * SlowStressSupport.axialOp h (SlowStressSupport.orderExponent h j) (toRadius (f.axial j)) w = w.1 * transportKernel h (SlowExpansionResidual.axialExponent h) 0 f.flux f.axial f.axial (radiusPoint w) i j

theorem NavierStokes.SlowResidualMatching.angularWeighted_eq_thetaDensity (h C : ℝ) (hC : C ≠ 0) (f : SlowExpansionResidual.SlowProfiles) {n : ℕ} (hn : 0 < n) {w : SimilarityProfile.InnerPoint} (hR : w.1 ≠ 0) (hf : ∀ j ≤ n, ContDiffAt ℝ 2 (f.phi j) (radiusPoint w)) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowStressSupport.angularWeighted h n (fun (j : ℕ) => toRadius (f.flux j)) (fun (j : ℕ) => toRadius (f.axial j)) (fun (j : ℕ) => swirlRadius C (f.phi j)) w = thetaDensity h C f n w

The canonical R-coordinate weighted angular residual is exactly the coefficient used by the finite Cartesian expansion.

theorem NavierStokes.SlowResidualMatching.axialWeighted_eq_zDensity (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) {n : ℕ} (hn : 0 < n) {w : SimilarityProfile.InnerPoint} (hf : ∀ j ≤ n, ContDiffAt ℝ 2 (f.axial j) (radiusPoint w)) (hp : DifferentiableAt ℝ (f.pressure n) (radiusPoint w)) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowStressSupport.axialWeighted h n (fun (j : ℕ) => toRadius (f.flux j)) (fun (j : ℕ) => toRadius (f.axial j)) (toRadius (f.pressure n)) w = zDensity h f n w

The canonical weighted axial residual uses the same pressure derivative and preceding viscosity as the finite Cartesian expansion.

theorem NavierStokes.SlowResidualMatching.radius_divergence (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) {w : SimilarityProfile.InnerPoint} (hv : DifferentiableAt ℝ (f.flux n) (radiusPoint w)) (hu : DifferentiableAt ℝ (f.axial n) (radiusPoint w)) (hd : SlowExpansionResidual.divergenceCoefficient h f n (radiusPoint w) = 0) : SlowStressSupport.dr (toRadius (f.flux n)) w = -w.1 * SlowStressSupport.axialOp h (SlowStressSupport.orderExponent h n) (toRadius (f.axial n)) w

theorem NavierStokes.SlowResidualMatching.partialX_toRadius_zero {f : SimilarityProfile.InnerProfile} {eta : ℝ} (hf : DifferentiableAt ℝ (toRadius f) (0, eta)) : SimilarityProfile.partialX (toRadius f) (0, eta) = 0

theorem NavierStokes.SlowResidualMatching.thetaDensity_eq_angularDensity {S : Set ℝ} (hS : IsOpen S) (h C : ℝ) (hC : C ≠ 0) (f : SlowExpansionResidual.SlowProfiles) {n : ℕ} (hn : 0 < n) (hv : ∀ j ≤ n, SlowStressSupport.Smooth S (toRadius (f.flux j))) (hu : ∀ j ≤ n, SlowStressSupport.Smooth S (toRadius (f.axial j))) (he : ∀ j ≤ n, SlowStressSupport.Smooth S (swirlRadius C (f.phi j))) (hf : ∀ (w : SimilarityProfile.InnerPoint), w.2 ∈ S → w.1 ≠ 0 → ∀ j ≤ n, ContDiffAt ℝ 2 (f.phi j) (radiusPoint w)) (hL : ∀ eta ∈ S, CoordinateAlgebra.L h eta ≠ 0) (hdiv : ∀ (w : SimilarityProfile.InnerPoint), w.2 ∈ S → ∀ j ≤ n, SlowStressSupport.dr (toRadius (f.flux j)) w = -w.1 * SlowStressSupport.axialOp h (SlowStressSupport.orderExponent h j) (toRadius (f.axial j)) w) : Set.EqOn (thetaDensity h C f n) (SlowStressSupport.angularDensity h n (fun (j : ℕ) => toRadius (f.flux j)) (fun (j : ℕ) => toRadius (f.axial j)) fun (j : ℕ) => swirlRadius C (f.phi j)) (SlowStressSupport.region S)

The primitive source is the canonical conservative density, including the axis. At the axis the equality uses the actual radial parity.

theorem NavierStokes.SlowResidualMatching.zDensity_eq_axialDensity {S : Set ℝ} (hS : IsOpen S) (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) {n : ℕ} (hn : 0 < n) (hv : ∀ j ≤ n, SlowStressSupport.Smooth S (toRadius (f.flux j))) (hu : ∀ j ≤ n, SlowStressSupport.Smooth S (toRadius (f.axial j))) (hp : SlowStressSupport.Smooth S (toRadius (f.pressure n))) (hf : ∀ (w : SimilarityProfile.InnerPoint), w.2 ∈ S → w.1 ≠ 0 → ∀ j ≤ n, ContDiffAt ℝ 2 (f.axial j) (radiusPoint w)) (hp' : ∀ (w : SimilarityProfile.InnerPoint), w.2 ∈ S → w.1 ≠ 0 → DifferentiableAt ℝ (f.pressure n) (radiusPoint w)) (hL : ∀ eta ∈ S, CoordinateAlgebra.L h eta ≠ 0) (hdiv : ∀ (w : SimilarityProfile.InnerPoint), w.2 ∈ S → ∀ j ≤ n, SlowStressSupport.dr (toRadius (f.flux j)) w = -w.1 * SlowStressSupport.axialOp h (SlowStressSupport.orderExponent h j) (toRadius (f.axial j)) w) : Set.EqOn (zDensity h f n) (SlowStressSupport.axialDensity h n (fun (j : ℕ) => toRadius (f.flux j)) (fun (j : ℕ) => toRadius (f.axial j)) (toRadius (f.pressure n))) (SlowStressSupport.region S)

theorem NavierStokes.SlowResidualMatching.primitive_stress_congr_slice (m : ℕ) {F G : SimilarityProfile.InnerProfile} {R eta : ℝ} (hFG : ∀ (r : ℝ), F (r, eta) = G (r, eta)) : SlowStressSupport.stress m F (R, eta) = SlowStressSupport.stress m G (R, eta)

theorem NavierStokes.SlowResidualMatching.thetaStress_eq_canonical {S : Set ℝ} (h C : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (hEq : Set.EqOn (thetaDensity h C f n) (SlowStressSupport.angularDensity h n (fun (j : ℕ) => toRadius (f.flux j)) (fun (j : ℕ) => toRadius (f.axial j)) fun (j : ℕ) => swirlRadius C (f.phi j)) (SlowStressSupport.region S)) {w : SimilarityProfile.InnerPoint} (hw : w.2 ∈ S) : thetaStress h C f n w = fromRadius (SlowStressSupport.angularStress h n (fun (j : ℕ) => toRadius (f.flux j)) (fun (j : ℕ) => toRadius (f.axial j)) fun (j : ℕ) => swirlRadius C (f.phi j)) w

Equality of the actual negative integrals, not just their derivatives.

theorem NavierStokes.SlowResidualMatching.zStress_eq_canonical {S : Set ℝ} (h : ℝ) (f : SlowExpansionResidual.SlowProfiles) (n : ℕ) (hEq : Set.EqOn (zDensity h f n) (SlowStressSupport.axialDensity h n (fun (j : ℕ) => toRadius (f.flux j)) (fun (j : ℕ) => toRadius (f.axial j)) (toRadius (f.pressure n))) (SlowStressSupport.region S)) {w : SimilarityProfile.InnerPoint} (hw : w.2 ∈ S) : zStress h f n w = fromRadius (SlowStressSupport.axialStress h n (fun (j : ℕ) => toRadius (f.flux j)) (fun (j : ℕ) => toRadius (f.axial j)) (toRadius (f.pressure n))) w

theorem NavierStokes.SlowResidualMatching.inner_smoothAt_of_radial {S : Set ℝ} (hS : IsOpen S) {F E : SimilarityProfile.InnerProfile} (hF : SlowStressSupport.Smooth S F) (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ S, F (R, eta) = E (R ^ 2 / 2, eta)) {w : SimilarityProfile.InnerPoint} (hX : 0 < w.1) (heta : w.2 ∈ S) : ContDiffAt ℝ (↑⊤) E w

theorem NavierStokes.SlowResidualMatching.axialOp2_congr_germ (h b : ℝ) {f g : SimilarityProfile.InnerProfile} {w : SimilarityProfile.InnerPoint} (hfg : f =ᶠ[nhds w] g) : SlowStressSupport.axialOp2 h b f w = SlowStressSupport.axialOp2 h b g w

theorem NavierStokes.SlowResidualMatching.axialOp2_radial_eq_Z2 {S : Set ℝ} (hS : IsOpen S) (h b : ℝ) {F E : SimilarityProfile.InnerProfile} (hF : SlowStressSupport.Smooth S F) (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ S, F (R, eta) = E (R ^ 2 / 2, eta)) {w : SimilarityProfile.InnerPoint} (hR : 0 < w.1) (heta : w.2 ∈ S) (hL : CoordinateAlgebra.L h w.2 ≠ 0) : SlowStressSupport.axialOp2 h b F w = SlowExpansionResidual.Z2 h b E (radiusPoint w)

theorem NavierStokes.SlowResidualMatching.deriv_deriv_pullback_z {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : SimilarityProfile.InnerProfile} {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) (hf : ContDiffAt ℝ 2 f (SimilarityProfile.inner h p)) : deriv (deriv fun (z : ℝ) => SimilarityProfile.pullback h b f (p.1, p.2.1, z)) p.2.2 = SimilarityProfile.pullback h (b - 2 * CoordinateAlgebra.D h) (SlowExpansionResidual.Z2 h b f) p

theorem NavierStokes.SlowResidualMatching.normalized_axial_viscosity {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {F E : SimilarityProfile.InnerProfile} (hF : SlowStressSupport.Smooth (Set.Ioo (-1) 1) F) (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, F (R, eta) = E (R ^ 2 / 2, eta)) {eta R : ℝ} (heta : eta ∈ Set.Ioo (-1) 1) (hR : 0 < R) : deriv (deriv (RenormalizedHeatMoment.uTheta h E (eta ^ 2) R)) eta = SlowStressSupport.axialOp2 h (-CoordinateAlgebra.A h) F (R, eta)

At the normalized physical point q=1, the literal second axial derivative is exactly the canonical R-coordinate operator.

theorem NavierStokes.SlowResidualMatching.lowerAngularViscosityMoment_of_renormalized {h C T B : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hT : 0 < T) (hB : 0 ≤ B) {F E : SimilarityProfile.InnerProfile} (hF : SlowStressSupport.Smooth (Set.Ioo (-1) 1) F) (hFE : ∀ (R : ℝ), 0 < R → ∀ eta ∈ Set.Ioo (-1) 1, F (R, eta) = E (R ^ 2 / 2, eta)) (he : ∀ eta ∈ Set.Ioo (-1) 1, ∀ (X : ℝ), T ≤ X → E (X, eta) = C * X ^ (-RenormalizedHeatMoment.A h) * RadialHeatProfile.profile (1 + h) (2 * (1 - eta ^ 2) / X)) (hm : ∀ eta ∈ Set.Ioo (-1) 1, RenormalizedHeatMoment.xMoment h C E eta = 0) (hExt : SlowStressSupport.exterior B (Set.Ioo (-1) 1) (SlowStressSupport.axialOp2 h (SlowStressSupport.orderExponent h 0) F)) : SlowStressSupport.LowerAngularViscosityMoment (Set.Ioo (-1) 1) B h F

The order-one angular viscosity moment follows from the restored renormalized heat moment. Only the stated exterior support is used to replace the positive half-line integral by its finite radial integral.

theorem NavierStokes.SlowResidualMatching.hierarchy_profile_smoothAt {R : ℝ} {U : Set ℂ} {h C : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : SlowRecursion.LocalHierarchy R U h C base) (hR : 0 < R) (hU : IsOpen U) (n : ℕ) (i : Fin 5) {w : SimilarityProfile.InnerPoint} (hX : w.1 ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑w.2 ∈ U) : ContDiffAt ℝ (↑⊤) (SlowRecursion.profile (A.coefficients n i)) w

theorem NavierStokes.SlowResidualMatching.hierarchy_pressure_coefficient {R : ℝ} {U : Set ℂ} {h C : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : SlowRecursion.LocalHierarchy R U h C base) (hR : 0 < R) (hU : IsOpen U) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) (hL : CoordinateAlgebra.L h eta ≠ 0) : SlowExpansionResidual.pressureCoefficient h C (hierarchyProfiles A) n (X, eta) = 0

theorem NavierStokes.SlowResidualMatching.repaired_tangential_coefficients {R : ℝ} {U : Set ℂ} {h C : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : SlowRecursion.LocalHierarchy R U h C base) (f : SlowExpansionResidual.SlowProfiles) {n : ℕ} (hn : 0 < n) {X eta : ℝ} (hX : X ∈ Set.Ioo 0 (R ^ 2)) (heta : ↑eta ∈ U) (hv : ∀ j ≤ n, f.flux j =ᶠ[nhds (X, eta)] (hierarchyProfiles A).flux j) (hu : ∀ j ≤ n, f.axial j =ᶠ[nhds (X, eta)] (hierarchyProfiles A).axial j) (hphi : ∀ j ≤ n, f.phi j =ᶠ[nhds (X, eta)] (hierarchyProfiles A).phi j) (hp : f.pressure n =ᶠ[nhds (X, eta)] (hierarchyProfiles A).pressure n) : SlowExpansionResidual.angularCoefficient h f n (X, eta) = 0 ∧ SlowExpansionResidual.axialCoefficient h f n (X, eta) = 0

A repaired family that retains the finite input germs retains the actual solved angular and axial equations in the inner region.