Finite slow expansions and their physical residuals

Finite products are expanded exactly. Terms above the retained slow order and the last axial-viscosity term are displayed as explicit finite remainders.

Radial flux coordinates for the actual axisymmetric residual

Write s = r²/2 and V = r u_r. The convention in AxisymmetricResidual is u_r = -r B, hence B = -V/(2s). All quotient derivatives in this file are genuine Fréchet derivatives, and their hypotheses are local at a point with positive s.

noncomputable def NavierStokes.RadialFluxResidual.radialB (V : AxisymmetricFields.Profile) : AxisymmetricFields.Profile

Radial B, defined pointwise by -V p / (2 * p.2.1).

Equations

• NavierStokes.RadialFluxResidual.radialB V p = -V p / (2 * p.2.1)

theorem NavierStokes.RadialFluxResidual.contDiffAt_radialB {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} {n : WithTop ℕ∞} (hV : ContDiffAt ℝ n V p) (hs : p.2.1 ≠ 0) : ContDiffAt ℝ n (radialB V) p

theorem NavierStokes.RadialFluxResidual.fderiv_radialB_apply {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : DifferentiableAt ℝ V p) (hs : p.2.1 ≠ 0) (v : AxisymmetricFields.ProfilePoint) : (fderiv ℝ (radialB V) p) v = -(fderiv ℝ V p) v / (2 * p.2.1) + V p * v.2.1 / (2 * p.2.1 ^ 2)

theorem NavierStokes.RadialFluxResidual.differentiableAt_radialB {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : DifferentiableAt ℝ V p) (hs : p.2.1 ≠ 0) : DifferentiableAt ℝ (radialB V) p

theorem NavierStokes.RadialFluxResidual.partialT_radialB {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : DifferentiableAt ℝ V p) (hs : p.2.1 ≠ 0) : AxisymmetricResidual.partialT (radialB V) p = radialB (AxisymmetricResidual.partialT V) p

theorem NavierStokes.RadialFluxResidual.partialZ_radialB {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : DifferentiableAt ℝ V p) (hs : p.2.1 ≠ 0) : AxisymmetricFields.partialZ (radialB V) p = radialB (AxisymmetricFields.partialZ V) p

theorem NavierStokes.RadialFluxResidual.partialS_radialB_explicit {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : DifferentiableAt ℝ V p) (hs : p.2.1 ≠ 0) : AxisymmetricFields.partialS (radialB V) p = -AxisymmetricFields.partialS V p / (2 * p.2.1) + V p / (2 * p.2.1 ^ 2)

theorem NavierStokes.RadialFluxResidual.partialS_radialB {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : DifferentiableAt ℝ V p) (hs : p.2.1 ≠ 0) : AxisymmetricFields.partialS (radialB V) p = radialB (AxisymmetricFields.partialS V) p + 2 * radialB (radialB V) p

theorem NavierStokes.RadialFluxResidual.partialS_partialS_radialB {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : ContDiffAt ℝ 2 V p) (hs : p.2.1 ≠ 0) : AxisymmetricFields.partialS (AxisymmetricFields.partialS (radialB V)) p = -AxisymmetricFields.partialS (AxisymmetricFields.partialS V) p / (2 * p.2.1) + AxisymmetricFields.partialS V p / p.2.1 ^ 2 - V p / p.2.1 ^ 3

theorem NavierStokes.RadialFluxResidual.partialZ_partialZ_radialB {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : ContDiffAt ℝ 2 V p) (hs : p.2.1 ≠ 0) : AxisymmetricFields.partialZ (AxisymmetricFields.partialZ (radialB V)) p = radialB (AxisymmetricFields.partialZ (AxisymmetricFields.partialZ V)) p

theorem NavierStokes.RadialFluxResidual.laplaceWeighted_radialB {V : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hV : ContDiffAt ℝ 2 V p) (hs : p.2.1 ≠ 0) : AxisymmetricResidual.laplaceWeighted (radialB V) p = -AxisymmetricFields.partialS (AxisymmetricFields.partialS V) p - AxisymmetricFields.partialZ (AxisymmetricFields.partialZ V) p / (2 * p.2.1)

The 4 B_s connection term cancels the extra radial quotient terms.

theorem NavierStokes.RadialFluxResidual.divergence_coefficient {V : AxisymmetricFields.Profile} (U : AxisymmetricFields.Profile) {p : AxisymmetricFields.ProfilePoint} (hV : DifferentiableAt ℝ V p) (hs : p.2.1 ≠ 0) : AxisymmetricFields.partialZ U p - 2 * radialB V p - 2 * p.2.1 * AxisymmetricFields.partialS (radialB V) p = AxisymmetricFields.partialS V p + AxisymmetricFields.partialZ U p

theorem NavierStokes.RadialFluxResidual.divergence_velocity_at {B F U : AxisymmetricFields.Profile} {t : ℝ} {x : ProblemStatement.Space} (hB : DifferentiableAt ℝ B (AxisymmetricFields.profilePoint t x)) (hF : DifferentiableAt ℝ F (AxisymmetricFields.profilePoint t x)) (hU : DifferentiableAt ℝ U (AxisymmetricFields.profilePoint t x)) : ProblemStatement.spatialDivergence (AxisymmetricResidual.velocity B F U) t x = AxisymmetricFields.partialZ U (AxisymmetricFields.profilePoint t x) - 2 * B (AxisymmetricFields.profilePoint t x) - 2 * AxisymmetricFields.radialEnergy x * AxisymmetricFields.partialS B (AxisymmetricFields.profilePoint t x)

theorem NavierStokes.RadialFluxResidual.divergence_radialB {V F U : AxisymmetricFields.Profile} {t : ℝ} {x : ProblemStatement.Space} (hV : DifferentiableAt ℝ V (AxisymmetricFields.profilePoint t x)) (hF : DifferentiableAt ℝ F (AxisymmetricFields.profilePoint t x)) (hU : DifferentiableAt ℝ U (AxisymmetricFields.profilePoint t x)) (hs : 0 < AxisymmetricFields.radialEnergy x) : ProblemStatement.spatialDivergence (AxisymmetricResidual.velocity (radialB V) F U) t x = AxisymmetricFields.partialS V (AxisymmetricFields.profilePoint t x) + AxisymmetricFields.partialZ U (AxisymmetricFields.profilePoint t x)

Actual Cartesian divergence, needing regularity only at the evaluated profile point. No smooth extension of the quotient across the axis is assumed.

theorem NavierStokes.RadialFluxResidual.radial_flux_velocity (V F U : AxisymmetricFields.Profile) (t : ℝ) (x : ProblemStatement.Space) (hs : 0 < AxisymmetricFields.radialEnergy x) : x.ofLp 0 * (AxisymmetricResidual.velocity (radialB V) F U (t, x)).ofLp 0 + x.ofLp 1 * (AxisymmetricResidual.velocity (radialB V) F U (t, x)).ofLp 1 = V (AxisymmetricFields.profilePoint t x)

The substitution has exactly the intended physical radial flux.

noncomputable def NavierStokes.RadialFluxResidual.fluxResidual (V F U P : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Flux residual, constructed using partialT.

Equations

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

theorem NavierStokes.RadialFluxResidual.residualRadial_radialB {V : AxisymmetricFields.Profile} (F U P : AxisymmetricFields.Profile) {p : AxisymmetricFields.ProfilePoint} (hV : ContDiffAt ℝ 2 V p) (hs : 0 < p.2.1) : 2 * p.2.1 * AxisymmetricResidual.residualRadial (radialB V) F U P p = fluxResidual V F U P p

The radial residual coefficient in AxisymmetricResidual multiplies (x₀,x₁,0). Thus its product with 2s=r² is r times the cylindrical radial residual, with the positive sign in this identity.

theorem NavierStokes.RadialFluxResidual.physical_radial_flux_residual {V F U P : AxisymmetricFields.Profile} {t : ℝ} {x : ProblemStatement.Space} (hV : ContDiffAt ℝ 2 V (AxisymmetricFields.profilePoint t x)) (hF : ContDiffAt ℝ 2 F (AxisymmetricFields.profilePoint t x)) (hU : ContDiffAt ℝ 2 U (AxisymmetricFields.profilePoint t x)) (hP : DifferentiableAt ℝ P (AxisymmetricFields.profilePoint t x)) (hs : 0 < AxisymmetricFields.radialEnergy x) : x.ofLp 0 * (ProblemStatement.navierStokesResidual (AxisymmetricResidual.velocity (radialB V) F U) (AxisymmetricResidual.pressure P) t x).ofLp 0 + x.ofLp 1 * (ProblemStatement.navierStokesResidual (AxisymmetricResidual.velocity (radialB V) F U) (AxisymmetricResidual.pressure P) t x).ofLp 1 = fluxResidual V F U P (AxisymmetricFields.profilePoint t x)

The actual physical radial residual multiplied by r, expressed without introducing a square root or a radial unit vector. All regularity hypotheses are local at the evaluated point with s > 0.

def NavierStokes.SlowExpansionResidual.slowOrder (h : ℝ) (n : ℕ) : ℝ

The manuscript's slow order λ_n=2nh.

Equations

• NavierStokes.SlowExpansionResidual.slowOrder h n = 2 * ↑n * h

@[simp]

theorem NavierStokes.SlowExpansionResidual.slowOrder_zero (h : ℝ) : slowOrder h 0 = 0

theorem NavierStokes.SlowExpansionResidual.slowOrder_add (h : ℝ) (i j : ℕ) : slowOrder h (i + j) = slowOrder h i + slowOrder h j

theorem NavierStokes.SlowExpansionResidual.slowOrder_succ (h : ℝ) (n : ℕ) : slowOrder h (n + 1) = slowOrder h n + 2 * h

noncomputable def NavierStokes.SlowExpansionResidual.finiteSeries (N : ℕ) (q h b : ℝ) (a : ℕ → ℝ) : ℝ

Finite series, given by ∑ n ∈ Finset.range (N + 1), q ^ (b + slowOrder h n) * a n.

Equations

• NavierStokes.SlowExpansionResidual.finiteSeries N q h b a = ∑ n ∈ Finset.range (N + 1), q ^ (b + NavierStokes.SlowExpansionResidual.slowOrder h n) * a n

noncomputable def NavierStokes.SlowExpansionResidual.pairs (N : ℕ) : Finset (ℕ × ℕ)

Pairs, given by Finset.range (N + 1) ×ˢ Finset.range (N + 1).

Equations

• NavierStokes.SlowExpansionResidual.pairs N = Finset.range (N + 1) ×ˢ Finset.range (N + 1)

def NavierStokes.SlowExpansionResidual.convolution (K : ℕ → ℕ → ℝ) (n : ℕ) : ℝ

Convolution, given by ∑ ij ∈ Finset.antidiagonal n, K ij.1 ij.2.

Equations

• NavierStokes.SlowExpansionResidual.convolution K n = ∑ ij ∈ Finset.antidiagonal n, K ij.1 ij.2

noncomputable def NavierStokes.SlowExpansionResidual.finiteConvolution (N : ℕ) (K : ℕ → ℕ → ℝ) (n : ℕ) : ℝ

Finite convolution, given by ∑ ij ∈ (pairs N).filter (fun ij => ij.1 + ij.2 = n), K ij.1 ij.2.

Equations

• NavierStokes.SlowExpansionResidual.finiteConvolution N K n = ∑ ij ∈ NavierStokes.SlowExpansionResidual.pairs N with ij.1 + ij.2 = n, K ij.1 ij.2

noncomputable def NavierStokes.SlowExpansionResidual.pairTail (N : ℕ) (w : ℕ → ℝ) (K : ℕ → ℕ → ℝ) : ℝ

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

Equations

• NavierStokes.SlowExpansionResidual.pairTail N w K = ∑ ij ∈ NavierStokes.SlowExpansionResidual.pairs N with N < ij.1 + ij.2, w (ij.1 + ij.2) * K ij.1 ij.2

noncomputable def NavierStokes.SlowExpansionResidual.previous (a : ℕ → ℝ) : ℕ → ℝ

Previous as an element of ℕ → ℝ | 0 => 0 | n + 1 => a n.

Equations

• NavierStokes.SlowExpansionResidual.previous a 0 = 0
• NavierStokes.SlowExpansionResidual.previous a n.succ = a n

@[simp]

theorem NavierStokes.SlowExpansionResidual.previous_zero (a : ℕ → ℝ) : previous a 0 = 0

@[simp]

theorem NavierStokes.SlowExpansionResidual.previous_succ (a : ℕ → ℝ) (n : ℕ) : previous a (n + 1) = a n

@[simp]

theorem NavierStokes.SlowExpansionResidual.finiteSeries_order_zero (q h b : ℝ) (a : ℕ → ℝ) : finiteSeries 0 q h b a = q ^ b * a 0

@[simp]

theorem NavierStokes.SlowExpansionResidual.pairTail_order_zero (w : ℕ → ℝ) (K : ℕ → ℕ → ℝ) : pairTail 0 w K = 0

theorem NavierStokes.SlowExpansionResidual.finiteConvolution_eq {N n : ℕ} (hn : n ≤ N) (K : ℕ → ℕ → ℝ) : finiteConvolution N K n = convolution K n

theorem NavierStokes.SlowExpansionResidual.rpow_product_order {q : ℝ} (hq : 0 < q) (h b c : ℝ) (i j : ℕ) : q ^ (b + slowOrder h i) * q ^ (c + slowOrder h j) = q ^ (b + c + slowOrder h (i + j))

theorem NavierStokes.SlowExpansionResidual.finiteSeries_mul {q : ℝ} (hq : 0 < q) (N : ℕ) (h b c : ℝ) (a d : ℕ → ℝ) : finiteSeries N q h b a * finiteSeries N q h c d = ∑ ij ∈ pairs N, q ^ (b + c + slowOrder h (ij.1 + ij.2)) * (a ij.1 * d ij.2)

Exact Cauchy product of two finite slow expansions.

theorem NavierStokes.SlowExpansionResidual.finiteSeries_add (N : ℕ) (q h b : ℝ) (a d : ℕ → ℝ) : (finiteSeries N q h b fun (n : ℕ) => a n + d n) = finiteSeries N q h b a + finiteSeries N q h b d

theorem NavierStokes.SlowExpansionResidual.finiteSeries_scale (N : ℕ) (q h b c : ℝ) (a : ℕ → ℝ) : (finiteSeries N q h b fun (n : ℕ) => c * a n) = c * finiteSeries N q h b a

theorem NavierStokes.SlowExpansionResidual.finiteSeries_mul_q {q : ℝ} (hq : 0 < q) (N : ℕ) (h b : ℝ) (a : ℕ → ℝ) : q * finiteSeries N q h b a = finiteSeries N q h (b + 1) a

theorem NavierStokes.SlowExpansionResidual.finiteSeries_div_qX {q X : ℝ} (hq : 0 < q) (hX : X ≠ 0) (N : ℕ) (h b : ℝ) (a : ℕ → ℝ) : finiteSeries N q h b a / (q * X) = finiteSeries N q h (b - 1) fun (n : ℕ) => a n / X

theorem NavierStokes.SlowExpansionResidual.radialDiffusion_series {q : ℝ} (hq : 0 < q) (N : ℕ) (h b X m : ℝ) (a d : ℕ → ℝ) : 2 * (q * X) * finiteSeries N q h (b - 2) d + 2 * m * finiteSeries N q h (b - 1) a = finiteSeries N q h (b - 1) fun (n : ℕ) => 2 * (X * d n + m * a n)

theorem NavierStokes.SlowExpansionResidual.axialViscosity_shift (N : ℕ) (q h b : ℝ) (a : ℕ → ℝ) : finiteSeries N q h (b - 2 * CoordinateAlgebra.D h) a = ∑ n ∈ Finset.range (N + 1), q ^ (b - 1 + slowOrder h (n + 1)) * a n

theorem NavierStokes.SlowExpansionResidual.pair_sum_low (N : ℕ) (w : ℕ → ℝ) (K : ℕ → ℕ → ℝ) : ∑ n ∈ Finset.range (N + 1), w n * finiteConvolution N K n = ∑ ij ∈ pairs N with ij.1 + ij.2 ≤ N, w (ij.1 + ij.2) * K ij.1 ij.2

theorem NavierStokes.SlowExpansionResidual.pair_sum_split (N : ℕ) (w : ℕ → ℝ) (K : ℕ → ℕ → ℝ) : ∑ ij ∈ pairs N, w (ij.1 + ij.2) * K ij.1 ij.2 = ∑ n ∈ Finset.range (N + 1), w n * convolution K n + pairTail N w K

Low convolution coefficients and the exact omitted pair interactions.

theorem NavierStokes.SlowExpansionResidual.shifted_sum (N : ℕ) (w a : ℕ → ℝ) : ∑ n ∈ Finset.range (N + 1), w (n + 1) * a n = ∑ n ∈ Finset.range (N + 1), w n * previous a n + w (N + 1) * a N

An axial derivative raises slow order by one. The last term is retained here as a literal remainder rather than silently discarded.

noncomputable def NavierStokes.SlowExpansionResidual.recurrence (L : ℕ → ℝ) (K : ℕ → ℕ → ℝ) (A : ℕ → ℝ) (n : ℕ) : ℝ

Recurrence, given by L n + convolution K n - previous A n.

Equations

• NavierStokes.SlowExpansionResidual.recurrence L K A n = L n + NavierStokes.SlowExpansionResidual.convolution K n - NavierStokes.SlowExpansionResidual.previous A n

theorem NavierStokes.SlowExpansionResidual.recurrence_truncation (N : ℕ) (w L A : ℕ → ℝ) (K : ℕ → ℕ → ℝ) : ∑ n ∈ Finset.range (N + 1), w n * L n + ∑ ij ∈ pairs N, w (ij.1 + ij.2) * K ij.1 ij.2 - ∑ n ∈ Finset.range (N + 1), w (n + 1) * A n = ∑ n ∈ Finset.range (N + 1), w n * recurrence L K A n + pairTail N w K - w (N + 1) * A N

Universal finite-order recurrence identity used by the angular, axial, and radial-flux equations.

theorem NavierStokes.SlowExpansionResidual.recurrence_truncation_of_zero (N : ℕ) (w L A : ℕ → ℝ) (K : ℕ → ℕ → ℝ) (hzero : ∀ n ≤ N, recurrence L K A n = 0) : ∑ n ∈ Finset.range (N + 1), w n * L n + ∑ ij ∈ pairs N, w (ij.1 + ij.2) * K ij.1 ij.2 - ∑ n ∈ Finset.range (N + 1), w (n + 1) * A n = pairTail N w K - w (N + 1) * A N

If the retained coefficient equations hold, the physical finite expansion still has these explicit omitted interactions and viscosity term.

def NavierStokes.SlowExpansionResidual.transportLinear (X m : ℝ) (gt gx gxx source : ℕ → ℝ) (n : ℕ) : ℝ

Transport linear, given by gt n - 2 * (X * gxx n + m * gx n) + source n.

Equations

• NavierStokes.SlowExpansionResidual.transportLinear X m gt gx gxx source n = gt n - 2 * (X * gxx n + m * gx n) + source n

noncomputable def NavierStokes.SlowExpansionResidual.transportPair (X α : ℝ) (v u g gx gz : ℕ → ℝ) (i j : ℕ) : ℝ

Transport pair, given by v i * (gx j + α * g j / X) + u i * gz j.

Equations

• NavierStokes.SlowExpansionResidual.transportPair X α v u g gx gz i j = v i * (gx j + α * g j / X) + u i * gz j

theorem NavierStokes.SlowExpansionResidual.transport_series_identity {q X : ℝ} (hq : 0 < q) (hX : X ≠ 0) (N : ℕ) (h e α m : ℝ) (v u g gt gx gxx gz gzz source : ℕ → ℝ) : finiteSeries N q h (e - 1) gt + finiteSeries N q h 0 v * (finiteSeries N q h (e - 1) gx + α * (finiteSeries N q h e g / (q * X))) + finiteSeries N q h (-CoordinateAlgebra.A h) u * finiteSeries N q h (e - CoordinateAlgebra.D h) gz - (2 * (q * X) * finiteSeries N q h (e - 2) gxx + 2 * m * finiteSeries N q h (e - 1) gx + finiteSeries N q h (e - 2 * CoordinateAlgebra.D h) gzz) + finiteSeries N q h (e - 1) source = finiteSeries N q h (e - 1) (recurrence (transportLinear X m gt gx gxx source) (transportPair X α v u g gx gz) gzz) + pairTail N (fun (n : ℕ) => q ^ (e - 1 + slowOrder h n)) (transportPair X α v u g gx gz) - q ^ (e - 1 + slowOrder h (N + 1)) * gzz N

Scalar transport/diffusion for arbitrary finite jets, with all product orders and the final shifted viscosity displayed exactly.

noncomputable def NavierStokes.SlowExpansionResidual.derivativeAlong (v : AxisymmetricFields.ProfilePoint) (f : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Ordinary directional derivative on physical profile space.

Equations

• NavierStokes.SlowExpansionResidual.derivativeAlong v f p = (fderiv ℝ f p) v

theorem NavierStokes.SlowExpansionResidual.derivativeAlong_sum {ι : Type u_1} (s : Finset ι) (f : ι → AxisymmetricFields.Profile) (v p : AxisymmetricFields.ProfilePoint) (hf : ∀ i ∈ s, DifferentiableAt ℝ (f i) p) : derivativeAlong v (fun (y : AxisymmetricFields.ProfilePoint) => ∑ i ∈ s, f i y) p = ∑ i ∈ s, derivativeAlong v (f i) p

theorem NavierStokes.SlowExpansionResidual.secondAlong_sum {ι : Type u_1} (s : Finset ι) (f : ι → AxisymmetricFields.Profile) (v w p : AxisymmetricFields.ProfilePoint) (hf : ∀ i ∈ s, ContDiffAt ℝ 2 (f i) p) : derivativeAlong w (derivativeAlong v fun (y : AxisymmetricFields.ProfilePoint) => ∑ i ∈ s, f i y) p = ∑ i ∈ s, derivativeAlong w (derivativeAlong v (f i)) p

Finite sums commute with actual second derivatives under C² regularity.

noncomputable def NavierStokes.SlowExpansionResidual.finiteProfile (N : ℕ) (h b : ℝ) (f : ℕ → SimilarityProfile.InnerProfile) : AxisymmetricFields.Profile

Finite profile, defined pointwise by ∑ n ∈ Finset.range (N + 1), pullback h (b + slowOrder h n) (f n) p.

Equations

• NavierStokes.SlowExpansionResidual.finiteProfile N h b f p = ∑ n ∈ Finset.range (N + 1), NavierStokes.SimilarityProfile.pullback h (b + NavierStokes.SlowExpansionResidual.slowOrder h n) (f n) p

@[simp]

theorem NavierStokes.SlowExpansionResidual.finiteProfile_order_zero (h b : ℝ) (f : ℕ → SimilarityProfile.InnerProfile) : finiteProfile 0 h b f = SimilarityProfile.pullback h b (f 0)

theorem NavierStokes.SlowExpansionResidual.finiteProfile_value (N : ℕ) (h b : ℝ) (f : ℕ → SimilarityProfile.InnerProfile) (p : AxisymmetricFields.ProfilePoint) : finiteProfile N h b f p = finiteSeries N (SimilarityProfile.q h p) h b fun (n : ℕ) => f n (SimilarityProfile.inner h p)

theorem NavierStokes.SlowExpansionResidual.partialT_finiteProfile {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : ℕ → SimilarityProfile.InnerProfile) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hf : ∀ n ≤ N, DifferentiableAt ℝ (f n) (SimilarityProfile.inner h p)) : AxisymmetricResidual.partialT (finiteProfile N h b f) p = finiteProfile N h (b - 1) (fun (n : ℕ) => SimilarityProfile.T h (b + slowOrder h n) (f n)) p

theorem NavierStokes.SlowExpansionResidual.partialS_finiteProfile {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : ℕ → SimilarityProfile.InnerProfile) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hf : ∀ n ≤ N, DifferentiableAt ℝ (f n) (SimilarityProfile.inner h p)) : AxisymmetricFields.partialS (finiteProfile N h b f) p = finiteProfile N h (b - 1) (fun (n : ℕ) => SimilarityProfile.partialX (f n)) p

theorem NavierStokes.SlowExpansionResidual.partialZ_finiteProfile {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : ℕ → SimilarityProfile.InnerProfile) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hf : ∀ n ≤ N, DifferentiableAt ℝ (f n) (SimilarityProfile.inner h p)) : AxisymmetricFields.partialZ (finiteProfile N h b f) p = finiteProfile N h (b - CoordinateAlgebra.D h) (fun (n : ℕ) => SimilarityProfile.Z h (b + slowOrder h n) (f n)) p

noncomputable def NavierStokes.SlowExpansionResidual.Z2 (h b : ℝ) (f : SimilarityProfile.InnerProfile) : SimilarityProfile.InnerProfile

Z2, given by Z h (b - CoordinateAlgebra.D h) (Z h b f).

Equations

• NavierStokes.SlowExpansionResidual.Z2 h b f = NavierStokes.SimilarityProfile.Z h (b - NavierStokes.CoordinateAlgebra.D h) (NavierStokes.SimilarityProfile.Z h b f)

theorem NavierStokes.SlowExpansionResidual.partialSS_finiteProfile {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : ℕ → SimilarityProfile.InnerProfile) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hf : ∀ n ≤ N, ContDiffAt ℝ 2 (f n) (SimilarityProfile.inner h p)) : AxisymmetricFields.partialS (AxisymmetricFields.partialS (finiteProfile N h b f)) p = finiteProfile N h (b - 2) (fun (n : ℕ) => SimilarityProfile.partialX (SimilarityProfile.partialX (f n))) p

theorem NavierStokes.SlowExpansionResidual.partialZZ_finiteProfile {h b : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : ℕ → SimilarityProfile.InnerProfile) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hf : ∀ n ≤ N, ContDiffAt ℝ 2 (f n) (SimilarityProfile.inner h p)) : AxisymmetricFields.partialZ (AxisymmetricFields.partialZ (finiteProfile N h b f)) p = finiteProfile N h (b - 2 * CoordinateAlgebra.D h) (fun (n : ℕ) => Z2 h (b + slowOrder h n) (f n)) p

noncomputable def NavierStokes.SlowExpansionResidual.transportResidual (α m : ℝ) (V U G source : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Transport residual, constructed using AxisymmetricResidual.partialT.

Equations

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

noncomputable def NavierStokes.SlowExpansionResidual.transportCoefficient (h e α m : ℝ) (v u f source : ℕ → SimilarityProfile.InnerProfile) (n : ℕ) (w : SimilarityProfile.InnerPoint) : ℝ

Transport coefficient, constructed using recurrence.

Equations

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

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

Transport tail, constructed using pairTail.

Equations

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

@[simp]

theorem NavierStokes.SlowExpansionResidual.transportTail_order_zero (q h e α : ℝ) (v u f : ℕ → SimilarityProfile.InnerProfile) (w : SimilarityProfile.InnerPoint) : transportTail 0 q h e α v u f w = -q ^ (e - 1 + 2 * h) * Z2 h e (f 0) w

theorem NavierStokes.SlowExpansionResidual.q_mul_X {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) : SimilarityProfile.q h p * (SimilarityProfile.inner h p).1 = p.2.1

theorem NavierStokes.SlowExpansionResidual.transport_finiteProfile {h e : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (α m : ℝ) (v u f source : ℕ → SimilarityProfile.InnerProfile) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hf : ∀ n ≤ N, ContDiffAt ℝ 2 (f n) (SimilarityProfile.inner h p)) : transportResidual α m (finiteProfile N h 0 v) (finiteProfile N h (-CoordinateAlgebra.A h) u) (finiteProfile N h e f) (finiteProfile N h (e - 1) source) p = (finiteSeries N (SimilarityProfile.q h p) h (e - 1) fun (n : ℕ) => transportCoefficient h e α m v u f source n (SimilarityProfile.inner h p)) + transportTail N (SimilarityProfile.q h p) h e α v u f (SimilarityProfile.inner h p)

The finite transport recurrence is obtained from genuine derivatives of the reconstructed profiles, rather than from formal coefficient placeholders.

theorem NavierStokes.SlowExpansionResidual.finiteProfile_smoothAt {h e : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : ℕ → SimilarityProfile.InnerProfile) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hf : ∀ n ≤ N, ContDiffAt ℝ 2 (f n) (SimilarityProfile.inner h p)) : ContDiffAt ℝ 2 (finiteProfile N h e f) p

theorem NavierStokes.SlowExpansionResidual.finiteProfile_differentiableAt {h e : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : ℕ → SimilarityProfile.InnerProfile) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hf : ∀ n ≤ N, DifferentiableAt ℝ (f n) (SimilarityProfile.inner h p)) : DifferentiableAt ℝ (finiteProfile N h e f) p

theorem NavierStokes.SlowExpansionResidual.derivativeAlong_scale (c : ℝ) {f : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hf : DifferentiableAt ℝ f p) (v : AxisymmetricFields.ProfilePoint) : derivativeAlong v (fun (y : AxisymmetricFields.ProfilePoint) => c * f y) p = c * derivativeAlong v f p

theorem NavierStokes.SlowExpansionResidual.secondAlong_scale (c : ℝ) {f : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hf : ContDiffAt ℝ 2 f p) (v w : AxisymmetricFields.ProfilePoint) : derivativeAlong w (derivativeAlong v fun (y : AxisymmetricFields.ProfilePoint) => c * f y) p = c * derivativeAlong w (derivativeAlong v f) p

theorem NavierStokes.SlowExpansionResidual.transportResidual_scale (c α m : ℝ) (V U : AxisymmetricFields.Profile) {G : AxisymmetricFields.Profile} {p : AxisymmetricFields.ProfilePoint} (hG : ContDiffAt ℝ 2 G p) : transportResidual α m V U (fun (y : AxisymmetricFields.ProfilePoint) => c * G y) (fun (x : AxisymmetricFields.ProfilePoint) => 0) p = c * transportResidual α m V U G (fun (x : AxisymmetricFields.ProfilePoint) => 0) p

noncomputable def NavierStokes.SlowExpansionResidual.angularExponent (h : ℝ) : ℝ

Angular exponent, given by -CoordinateAlgebra.A h - 1 / 2.

Equations

• NavierStokes.SlowExpansionResidual.angularExponent h = -NavierStokes.CoordinateAlgebra.A h - 1 / 2

noncomputable def NavierStokes.SlowExpansionResidual.axialExponent (h : ℝ) : ℝ

Axial exponent, given by -CoordinateAlgebra.A h.

Equations

• NavierStokes.SlowExpansionResidual.axialExponent h = -NavierStokes.CoordinateAlgebra.A h

noncomputable def NavierStokes.SlowExpansionResidual.pressureExponent (h : ℝ) : ℝ

Pressure exponent, given by -2 * CoordinateAlgebra.A h.

Equations

• NavierStokes.SlowExpansionResidual.pressureExponent h = -2 * NavierStokes.CoordinateAlgebra.A h

structure NavierStokes.SlowExpansionResidual.SlowProfiles : Type

Slow profiles data, collecting phi, axial, flux, pressure.

• phi : ℕ → SimilarityProfile.InnerProfile

  Phi of SlowProfiles, of type ℕ → InnerProfile.

• axial : ℕ → SimilarityProfile.InnerProfile

  Axial of SlowProfiles, of type ℕ → InnerProfile.

• flux : ℕ → SimilarityProfile.InnerProfile

  Flux of SlowProfiles, of type ℕ → InnerProfile.

• pressure : ℕ → SimilarityProfile.InnerProfile

  Pressure field of SlowProfiles, of type ℕ → InnerProfile.

noncomputable def NavierStokes.SlowExpansionResidual.slowFlux (N : ℕ) (h : ℝ) (f : SlowProfiles) : AxisymmetricFields.Profile

Slow flux, given by finiteProfile N h 0 f.flux.

Equations

• NavierStokes.SlowExpansionResidual.slowFlux N h f = NavierStokes.SlowExpansionResidual.finiteProfile N h 0 f.flux

noncomputable def NavierStokes.SlowExpansionResidual.slowSwirl (N : ℕ) (h C : ℝ) (f : SlowProfiles) : AxisymmetricFields.Profile

Slow swirl, defined pointwise by C⁻¹ * finiteProfile N h (angularExponent h) f.phi p.

Equations

• NavierStokes.SlowExpansionResidual.slowSwirl N h C f p = C⁻¹ * NavierStokes.SlowExpansionResidual.finiteProfile N h (NavierStokes.SlowExpansionResidual.angularExponent h) f.phi p

noncomputable def NavierStokes.SlowExpansionResidual.slowAxial (N : ℕ) (h : ℝ) (f : SlowProfiles) : AxisymmetricFields.Profile

Slow axial, given by finiteProfile N h (axialExponent h) f.axial.

Equations

• NavierStokes.SlowExpansionResidual.slowAxial N h f = NavierStokes.SlowExpansionResidual.finiteProfile N h (NavierStokes.SlowExpansionResidual.axialExponent h) f.axial

noncomputable def NavierStokes.SlowExpansionResidual.slowPressure (N : ℕ) (h : ℝ) (f : SlowProfiles) : AxisymmetricFields.Profile

Slow pressure, given by finiteProfile N h (pressureExponent h) f.pressure.

Equations

• NavierStokes.SlowExpansionResidual.slowPressure N h f = NavierStokes.SlowExpansionResidual.finiteProfile N h (NavierStokes.SlowExpansionResidual.pressureExponent h) f.pressure

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

Axial pressure source, given by Z h (pressureExponent h + slowOrder h n) (f.pressure n).

Equations

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

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

Angular coefficient, given by transportCoefficient h (angularExponent h) 1 2 f.flux f.axial f.phi (fun _ _ => 0) n.

Equations

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

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

Axial coefficient, given by transportCoefficient h (axialExponent h) 0 1 f.flux f.axial f.axial (axialPressureSource h f) n.

Equations

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

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

Omega coefficient, given by transportCoefficient h 0 (-(1 / 2)) 0 f.flux f.axial f.flux (fun _ _ => 0) n.

Equations

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

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

Divergence coefficient, given by partialX (f.flux n) w + Z h (axialExponent h + slowOrder h n) (f.axial n) w.

Equations

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

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

Pressure coefficient, constructed using partialX.

Equations

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

@[simp]

theorem NavierStokes.SlowExpansionResidual.finiteProfile_zero (N : ℕ) (h b : ℝ) : (finiteProfile N h b fun (x : ℕ) (x_1 : SimilarityProfile.InnerPoint) => 0) = fun (x : AxisymmetricFields.ProfilePoint) => 0

theorem NavierStokes.SlowExpansionResidual.angular_finite_expansion {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowProfiles) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hf : ∀ n ≤ N, ContDiffAt ℝ 2 (f.phi n) (SimilarityProfile.inner h p)) : transportResidual 1 2 (slowFlux N h f) (slowAxial N h f) (slowSwirl N h C f) (fun (x : AxisymmetricFields.ProfilePoint) => 0) p = C⁻¹ * ((finiteSeries N (SimilarityProfile.q h p) h (angularExponent h - 1) fun (n : ℕ) => angularCoefficient h f n (SimilarityProfile.inner h p)) + transportTail N (SimilarityProfile.q h p) h (angularExponent h) 1 f.flux f.axial f.phi (SimilarityProfile.inner h p))

The physical angular equation for the finite swirl expansion.

theorem NavierStokes.SlowExpansionResidual.axial_finite_expansion {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : SlowProfiles) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hf : ∀ n ≤ N, ContDiffAt ℝ 2 (f.axial n) (SimilarityProfile.inner h p)) (hπ : ∀ n ≤ N, DifferentiableAt ℝ (f.pressure n) (SimilarityProfile.inner h p)) : transportResidual 0 1 (slowFlux N h f) (slowAxial N h f) (slowAxial N h f) (AxisymmetricFields.partialZ (slowPressure N h f)) p = (finiteSeries N (SimilarityProfile.q h p) h (axialExponent h - 1) fun (n : ℕ) => axialCoefficient h f n (SimilarityProfile.inner h p)) + transportTail N (SimilarityProfile.q h p) h (axialExponent h) 0 f.flux f.axial f.axial (SimilarityProfile.inner h p)

The axial equation includes the complete axial pressure derivative.

theorem NavierStokes.SlowExpansionResidual.omega_finite_expansion {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : SlowProfiles) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hf : ∀ n ≤ N, ContDiffAt ℝ 2 (f.flux n) (SimilarityProfile.inner h p)) : transportResidual (-(1 / 2)) 0 (slowFlux N h f) (slowAxial N h f) (slowFlux N h f) (fun (x : AxisymmetricFields.ProfilePoint) => 0) p = (finiteSeries N (SimilarityProfile.q h p) h (-1) fun (n : ℕ) => omegaCoefficient h f n (SimilarityProfile.inner h p)) + transportTail N (SimilarityProfile.q h p) h 0 (-(1 / 2)) f.flux f.axial f.flux (SimilarityProfile.inner h p)

The radial acceleration flux Ω, before centrifugal and pressure terms.

theorem NavierStokes.SlowExpansionResidual.divergence_finite_expansion {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (f : SlowProfiles) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hv : ∀ n ≤ N, DifferentiableAt ℝ (f.flux n) (SimilarityProfile.inner h p)) (hu : ∀ n ≤ N, DifferentiableAt ℝ (f.axial n) (SimilarityProfile.inner h p)) : AxisymmetricFields.partialS (slowFlux N h f) p + AxisymmetricFields.partialZ (slowAxial N h f) p = finiteSeries N (SimilarityProfile.q h p) h (-1) fun (n : ℕ) => divergenceCoefficient h f n (SimilarityProfile.inner h p)

Equation (21) is the exact divergence coefficient at every retained order.

theorem NavierStokes.SlowExpansionResidual.pressure_series_identity {q X : ℝ} (hq : 0 < q) (hX : X ≠ 0) (N : ℕ) (h C tail : ℝ) (phi px omega : ℕ → ℝ) : finiteSeries N q h (-1) omega + tail + 2 * (q * X) * (finiteSeries N q h (pressureExponent h - 1) px - (C⁻¹ * finiteSeries N q h (angularExponent h) phi) ^ 2) = (2 * X * finiteSeries N q h (pressureExponent h) fun (n : ℕ) => px n - C⁻¹ ^ 2 * convolution (fun (i j : ℕ) => phi i * phi j) n + previous omega n / (2 * X)) + (tail + q ^ (pressureExponent h + slowOrder h (N + 1)) * omega N - 2 * X * C⁻¹ ^ 2 * pairTail N (fun (n : ℕ) => q ^ (pressureExponent h + slowOrder h n)) fun (i j : ℕ) => phi i * phi j)

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

Pressure tail, constructed using transportTail.

Equations

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

theorem NavierStokes.SlowExpansionResidual.pressure_finite_expansion {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowProfiles) {p : AxisymmetricFields.ProfilePoint} (hp : p.1 < 1) (hs : 0 < p.2.1) (hv : ∀ n ≤ N, ContDiffAt ℝ 2 (f.flux n) (SimilarityProfile.inner h p)) (hπ : ∀ n ≤ N, DifferentiableAt ℝ (f.pressure n) (SimilarityProfile.inner h p)) : RadialFluxResidual.fluxResidual (slowFlux N h f) (slowSwirl N h C f) (slowAxial N h f) (slowPressure N h f) p = (2 * (SimilarityProfile.inner h p).1 * finiteSeries N (SimilarityProfile.q h p) h (pressureExponent h) fun (n : ℕ) => pressureCoefficient h C f n (SimilarityProfile.inner h p)) + pressureTail N (SimilarityProfile.q h p) h C f (SimilarityProfile.inner h p)

The pressure row of (22), including the shifted radial acceleration and the exact finite pressure remainder.

theorem NavierStokes.SlowExpansionResidual.divergenceCoefficient_eq_zero_iff (h : ℝ) (f : SlowProfiles) (n : ℕ) (w : SimilarityProfile.InnerPoint) : divergenceCoefficient h f n w = 0 ↔ SimilarityProfile.partialX (f.flux n) w = -SimilarityProfile.Z h (axialExponent h + slowOrder h n) (f.axial n) w

The first differential equation in (21), with the actual inner derivative.

theorem NavierStokes.SlowExpansionResidual.angularCoefficient_eq_zero_iff (h : ℝ) (f : SlowProfiles) (n : ℕ) (w : SimilarityProfile.InnerPoint) : angularCoefficient h f n w = 0 ↔ 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX (f.phi n)) w + 2 * SimilarityProfile.partialX (f.phi n) w) = SimilarityProfile.T h (angularExponent h + slowOrder h n) (f.phi n) w + convolution (fun (i j : ℕ) => f.flux i w * (SimilarityProfile.partialX (f.phi j) w + f.phi j w / w.1) + f.axial i w * SimilarityProfile.Z h (angularExponent h + slowOrder h j) (f.phi j) w) n - previous (fun (j : ℕ) => Z2 h (angularExponent h + slowOrder h j) (f.phi j) w) n

The angular row of (22). previous makes the missing order -1 equal zero.

theorem NavierStokes.SlowExpansionResidual.axialCoefficient_eq_zero_iff (h : ℝ) (f : SlowProfiles) (n : ℕ) (w : SimilarityProfile.InnerPoint) : axialCoefficient h f n w = 0 ↔ 2 * (w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX (f.axial n)) w + SimilarityProfile.partialX (f.axial n) w) = SimilarityProfile.T h (axialExponent h + slowOrder h n) (f.axial n) w + convolution (fun (i j : ℕ) => f.flux i w * SimilarityProfile.partialX (f.axial j) w + f.axial i w * SimilarityProfile.Z h (axialExponent h + slowOrder h j) (f.axial j) w) n + SimilarityProfile.Z h (pressureExponent h + slowOrder h n) (f.pressure n) w - previous (fun (j : ℕ) => Z2 h (axialExponent h + slowOrder h j) (f.axial j) w) n

The axial row of (22), including the pressure derivative and viscosity shift.

theorem NavierStokes.SlowExpansionResidual.omegaCoefficient_eq (h : ℝ) (f : SlowProfiles) (n : ℕ) (w : SimilarityProfile.InnerPoint) : omegaCoefficient h f n w = SimilarityProfile.T h (slowOrder h n) (f.flux n) w + convolution (fun (i j : ℕ) => f.flux i w * (SimilarityProfile.partialX (f.flux j) w - f.flux j w / (2 * w.1)) + f.axial i w * SimilarityProfile.Z h (slowOrder h j) (f.flux j) w) n - 2 * w.1 * SimilarityProfile.partialX (SimilarityProfile.partialX (f.flux n)) w - previous (fun (j : ℕ) => Z2 h (slowOrder h j) (f.flux j) w) n

The radial acceleration coefficient appearing in the pressure row of (22).

theorem NavierStokes.SlowExpansionResidual.pressureCoefficient_eq_zero_iff (h C : ℝ) (f : SlowProfiles) (n : ℕ) (w : SimilarityProfile.InnerPoint) : pressureCoefficient h C f n w = 0 ↔ SimilarityProfile.partialX (f.pressure n) w = C⁻¹ ^ 2 * convolution (fun (i j : ℕ) => f.phi i w * f.phi j w) n - previous (fun (j : ℕ) => omegaCoefficient h f j w) n / (2 * w.1)

The pressure row of (22), including the preceding radial acceleration.

theorem NavierStokes.SlowExpansionResidual.residualAngular_radialB (V F U : AxisymmetricFields.Profile) {p : AxisymmetricFields.ProfilePoint} (hs : p.2.1 ≠ 0) : AxisymmetricResidual.residualAngular (RadialFluxResidual.radialB V) F U p = -transportResidual 1 2 V U F (fun (x : AxisymmetricFields.ProfilePoint) => 0) p

The angular coefficient in Cartesian coordinates has the opposite sign because it multiplies (y,-x,0) in the residual formula.

theorem NavierStokes.SlowExpansionResidual.residualAxial_radialB (V U P : AxisymmetricFields.Profile) {p : AxisymmetricFields.ProfilePoint} (hs : p.2.1 ≠ 0) : AxisymmetricResidual.residualAxial (RadialFluxResidual.radialB V) U P p = transportResidual 0 1 V U U (AxisymmetricFields.partialZ P) p

noncomputable def NavierStokes.SlowExpansionResidual.slowVelocity (N : ℕ) (h C : ℝ) (f : SlowProfiles) : ProblemStatement.VelocityField

Slow velocity, given by AxisymmetricResidual.velocity (RadialFluxResidual.radialB (slowFlux N h f)) (slowSwirl N h C f) (slowAxial N h f).

Equations

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

noncomputable def NavierStokes.SlowExpansionResidual.slowPressureField (N : ℕ) (h : ℝ) (f : SlowProfiles) : ProblemStatement.PressureField

Slow pressure field, given by AxisymmetricResidual.pressure (slowPressure N h f).

Equations

• NavierStokes.SlowExpansionResidual.slowPressureField N h f = NavierStokes.AxisymmetricResidual.pressure (NavierStokes.SlowExpansionResidual.slowPressure N h f)

theorem NavierStokes.SlowExpansionResidual.slowVelocity_components (N : ℕ) (h C : ℝ) (f : SlowProfiles) (t : ℝ) (x : ProblemStatement.Space) : slowVelocity N h C f (t, x) = AxisymmetricResidual.pack (x.ofLp 0 * (slowFlux N h f (AxisymmetricFields.profilePoint t x) / (2 * AxisymmetricFields.radialEnergy x)) - x.ofLp 1 * slowSwirl N h C f (AxisymmetricFields.profilePoint t x)) (x.ofLp 1 * (slowFlux N h f (AxisymmetricFields.profilePoint t x) / (2 * AxisymmetricFields.radialEnergy x)) + x.ofLp 0 * slowSwirl N h C f (AxisymmetricFields.profilePoint t x)) (slowAxial N h f (AxisymmetricFields.profilePoint t x))

Cartesian realization of the radial-flux and swirl ansatz.

theorem NavierStokes.SlowExpansionResidual.slowVelocity_radial_flux (N : ℕ) (h C : ℝ) (f : SlowProfiles) (t : ℝ) (x : ProblemStatement.Space) (hs : 0 < AxisymmetricFields.radialEnergy x) : x.ofLp 0 * (slowVelocity N h C f (t, x)).ofLp 0 + x.ofLp 1 * (slowVelocity N h C f (t, x)).ofLp 1 = slowFlux N h f (AxisymmetricFields.profilePoint t x)

theorem NavierStokes.SlowExpansionResidual.divergence_slowVelocity {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowProfiles) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) (hv : ∀ n ≤ N, DifferentiableAt ℝ (f.flux n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hf : ∀ n ≤ N, DifferentiableAt ℝ (f.phi n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hu : ∀ n ≤ N, DifferentiableAt ℝ (f.axial n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) : ProblemStatement.spatialDivergence (slowVelocity N h C f) t x = finiteSeries N (SimilarityProfile.q h (AxisymmetricFields.profilePoint t x)) h (-1) fun (n : ℕ) => divergenceCoefficient h f n (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))

The finite field's divergence is exactly its finite divergence-coefficient sum. This assertion uses the actual Euclidean divergence, away from the axis.

theorem NavierStokes.SlowExpansionResidual.finiteSeries_eq_zero (N : ℕ) (q h e : ℝ) (a : ℕ → ℝ) (ha : ∀ n ≤ N, a n = 0) : finiteSeries N q h e a = 0

theorem NavierStokes.SlowExpansionResidual.divergence_slowVelocity_eq_zero {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowProfiles) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) (hv : ∀ n ≤ N, DifferentiableAt ℝ (f.flux n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hf : ∀ n ≤ N, DifferentiableAt ℝ (f.phi n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hu : ∀ n ≤ N, DifferentiableAt ℝ (f.axial n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hdiv : ∀ n ≤ N, divergenceCoefficient h f n (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x)) = 0) : ProblemStatement.spatialDivergence (slowVelocity N h C f) t x = 0

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

Angular expansion as an element of ℝ.

Equations

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

noncomputable def NavierStokes.SlowExpansionResidual.axialExpansion (N : ℕ) (q h : ℝ) (f : SlowProfiles) (w : SimilarityProfile.InnerPoint) : ℝ

Axial expansion, constructed using finiteSeries.

Equations

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

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

Radial flux expansion, given by 2 * w.1 * finiteSeries N q h (pressureExponent h) (fun n => pressureCoefficient h C f n w) + pressureTail N q h C f w.

Equations

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

theorem NavierStokes.SlowExpansionResidual.navierStokesResidual_slowVelocity {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowProfiles) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) (hv : ∀ n ≤ N, ContDiffAt ℝ 2 (f.flux n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hf : ∀ 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))) (hπ : ∀ n ≤ N, DifferentiableAt ℝ (f.pressure n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) : ProblemStatement.navierStokesResidual (slowVelocity N h C f) (slowPressureField N h f) t x = have q := SimilarityProfile.q h (AxisymmetricFields.profilePoint t x); have w := SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x); AxisymmetricResidual.pack (x.ofLp 0 * (radialFluxExpansion N q h C f w / (2 * AxisymmetricFields.radialEnergy x)) - x.ofLp 1 * angularExpansion N q h C f w) (x.ofLp 1 * (radialFluxExpansion N q h C f w / (2 * AxisymmetricFields.radialEnergy x)) + x.ofLp 0 * angularExpansion N q h C f w) (axialExpansion N q h f w)

Reconstruction of the full Cartesian Navier--Stokes residual of the finite slow expansion. Every derivative on the left is the genuine spatial or temporal Fréchet derivative from ProblemStatement.

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

The explicit forcing left by truncation once all retained coefficient equations hold. This includes omitted quadratic interactions and the final axial-viscosity and radial-acceleration terms.

Equations

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

theorem NavierStokes.SlowExpansionResidual.navierStokesResidual_slowVelocity_of_coefficients {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (N : ℕ) (C : ℝ) (f : SlowProfiles) {t : ℝ} {x : ProblemStatement.Space} (ht : t < 1) (hs : 0 < AxisymmetricFields.radialEnergy x) (hv : ∀ n ≤ N, ContDiffAt ℝ 2 (f.flux n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hf : ∀ 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))) (hπ : ∀ n ≤ N, DifferentiableAt ℝ (f.pressure n) (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x))) (hA : ∀ n ≤ N, angularCoefficient h f n (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x)) = 0) (hZ : ∀ n ≤ N, axialCoefficient h f n (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x)) = 0) (hR : ∀ n ≤ N, pressureCoefficient h C f n (SimilarityProfile.inner h (AxisymmetricFields.profilePoint t x)) = 0) : ProblemStatement.navierStokesResidual (slowVelocity N h C f) (slowPressureField N h f) t x = truncationResidual N h C f t x

Solving all retained coefficient equations produces precisely the displayed truncation forcing; it does not make that forcing disappear.