Globalization of the positive slow profiles

The radial coordinate in this file is the physical similarity radius R, so that X = R² / 2. Smoothness at the axis is represented by genuine smooth even functions of the signed radius. Moment corrections are supported in a fixed positive-radius patch and are reflected with the appropriate parity.

All integrals and differential operators below are the actual ones. In particular the preceding radial source is retained when pressure is recomputed.

@[reducible, inline]

abbrev NavierStokes.GlobalSlowProfiles.Field : Type

Field: an abbreviation for ℝ × ℝ → ℝ.

Equations

• NavierStokes.GlobalSlowProfiles.Field = (ℝ × ℝ → ℝ)

@[reducible, inline]

abbrev NavierStokes.GlobalSlowProfiles.History : Type

History: an abbreviation for ℕ → Field.

Equations

• NavierStokes.GlobalSlowProfiles.History = (ℕ → NavierStokes.GlobalSlowProfiles.Field)

@[reducible, inline]

abbrev NavierStokes.GlobalSlowProfiles.region (S : Set ℝ) : Set (ℝ × ℝ)

Region: an abbreviation for (univ : Set ℝ) ×ˢ S.

Equations

• NavierStokes.GlobalSlowProfiles.region S = Set.univ ×ˢ S

@[reducible, inline]

abbrev NavierStokes.GlobalSlowProfiles.Smooth (S : Set ℝ) (f : Field) : Prop

Smooth: an abbreviation for ContDiffOn ℝ ∞ f (region S).

Equations

• NavierStokes.GlobalSlowProfiles.Smooth S f = ContDiffOn ℝ (↑⊤) f (NavierStokes.GlobalSlowProfiles.region S)

noncomputable def NavierStokes.GlobalSlowProfiles.dr (F : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

Dr, given by ProfileHistories.radialPartial.

Equations

• NavierStokes.GlobalSlowProfiles.dr = NavierStokes.ProfileHistories.radialPartial

noncomputable def NavierStokes.GlobalSlowProfiles.de (F : ProfileHistories.Field) (p : ProfileHistories.Point) : ℝ

De, given by ProfileHistories.parameterPartial.

Equations

• NavierStokes.GlobalSlowProfiles.de = NavierStokes.ProfileHistories.parameterPartial

structure NavierStokes.GlobalSlowProfiles.Regular (S : Set ℝ) (f : Field) : Prop

Regular data, collecting smooth, even.

• smooth : Smooth S f
• even (eta : ℝ) : eta ∈ S → ∀ (R : ℝ), f (-R, eta) = f (R, eta)

theorem NavierStokes.GlobalSlowProfiles.Regular.const (S : Set ℝ) (c : ℝ) : Regular S fun (x : ℝ × ℝ) => c

theorem NavierStokes.GlobalSlowProfiles.Regular.add {S : Set ℝ} {f g : Field} (hf : Regular S f) (hg : Regular S g) : Regular S (f + g)

theorem NavierStokes.GlobalSlowProfiles.Regular.mul {S : Set ℝ} {f g : Field} (hf : Regular S f) (hg : Regular S g) : Regular S (f * g)

noncomputable def NavierStokes.GlobalSlowProfiles.regularAlgebra (S : Set ℝ) : Subalgebra ℝ Field

Regular algebra, bundling carrier, zero_mem, one_mem, add_mem and the required compatibility proofs.

Equations

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

@[reducible, inline]

abbrev NavierStokes.GlobalSlowProfiles.EvenProfile (S : Set ℝ) : Type

Even profile: an abbreviation for ↥(regularAlgebra S) instance {S : Set ℝ} : CoeFun (EvenProfile S) (fun _ => Field) := ⟨fun f => f.1⟩.

Equations

• NavierStokes.GlobalSlowProfiles.EvenProfile S = ↥(NavierStokes.GlobalSlowProfiles.regularAlgebra S)

@[instance_reducible]

instance NavierStokes.GlobalSlowProfiles.instCoeFunEvenProfileField {S : Set ℝ} : CoeFun (EvenProfile S) fun (x : EvenProfile S) => Field

Equations

• NavierStokes.GlobalSlowProfiles.instCoeFunEvenProfileField = { coe := fun (f : NavierStokes.GlobalSlowProfiles.EvenProfile S) => ↑f }

theorem NavierStokes.GlobalSlowProfiles.EvenProfile.smooth {S : Set ℝ} (f : EvenProfile S) : Smooth S ↑f

theorem NavierStokes.GlobalSlowProfiles.EvenProfile.even {S : Set ℝ} (f : EvenProfile S) {eta : ℝ} (heta : eta ∈ S) (R : ℝ) : ↑f (-R, eta) = ↑f (R, eta)

theorem NavierStokes.GlobalSlowProfiles.slice_smooth {S : Set ℝ} {f : Field} (hf : Smooth S f) {eta : ℝ} (heta : eta ∈ S) : ContDiff ℝ ↑⊤ fun (R : ℝ) => f (R, eta)

@[simp]

theorem NavierStokes.GlobalSlowProfiles.add_apply {S : Set ℝ} (f g : EvenProfile S) (w : ℝ × ℝ) : ↑(f + g) w = ↑f w + ↑g w

@[simp]

theorem NavierStokes.GlobalSlowProfiles.mul_apply {S : Set ℝ} (f g : EvenProfile S) (w : ℝ × ℝ) : ↑(f * g) w = ↑f w * ↑g w

@[simp]

theorem NavierStokes.GlobalSlowProfiles.sub_apply {S : Set ℝ} (f g : EvenProfile S) (w : ℝ × ℝ) : ↑(f - g) w = ↑f w - ↑g w

@[simp]

theorem NavierStokes.GlobalSlowProfiles.neg_apply {S : Set ℝ} (f : EvenProfile S) (w : ℝ × ℝ) : ↑(-f) w = -↑f w

@[simp]

theorem NavierStokes.GlobalSlowProfiles.zero_apply {S : Set ℝ} (w : ℝ × ℝ) : ↑0 w = 0

@[simp]

theorem NavierStokes.GlobalSlowProfiles.one_apply {S : Set ℝ} (w : ℝ × ℝ) : ↑1 w = 1

@[simp]

theorem NavierStokes.GlobalSlowProfiles.sum_apply {ι : Type u_1} {S : Set ℝ} (s : Finset ι) (f : ι → EvenProfile S) (w : ℝ × ℝ) : ↑(∑ i ∈ s, f i) w = ∑ i ∈ s, ↑(f i) w

noncomputable def NavierStokes.GlobalSlowProfiles.boundConstant (S : Set ℝ) (c : ℝ) : EvenProfile S

Bound constant, given by algebraMap ℝ (EvenProfile S) c.

Equations

• NavierStokes.GlobalSlowProfiles.boundConstant S c = (algebraMap ℝ (NavierStokes.GlobalSlowProfiles.EvenProfile S)) c

@[simp]

theorem NavierStokes.GlobalSlowProfiles.constant_apply (S : Set ℝ) (c : ℝ) (w : ℝ × ℝ) : ↑(boundConstant S c) w = c

noncomputable def NavierStokes.GlobalSlowProfiles.radiusSquared (S : Set ℝ) : EvenProfile S

Radius squared, given by ⟨fun w => w.1 ^ 2 / 2, ⟨(contDiffOn_fst.pow 2).div_const 2, fun _ _ _ => by simp only [neg_sq]⟩⟩.

Equations

• NavierStokes.GlobalSlowProfiles.radiusSquared S = ⟨fun (w : ℝ × ℝ) => w.1 ^ 2 / 2, ⋯⟩

noncomputable def NavierStokes.GlobalSlowProfiles.parameter (S : Set ℝ) : EvenProfile S

Parameter, given by ⟨Prod.snd, ⟨contDiffOn_snd, fun _ _ _ => rfl⟩⟩.

Equations

• NavierStokes.GlobalSlowProfiles.parameter S = ⟨Prod.snd, ⋯⟩

noncomputable def NavierStokes.GlobalSlowProfiles.inverse {S : Set ℝ} (f : EvenProfile S) (hf : ∀ w ∈ region S, ↑f w ≠ 0) : EvenProfile S

Inverse, given by ⟨fun w => (f w)⁻¹, ⟨f.smooth.inv hf, fun _ heta R => congrArg Inv.inv (f.even heta R)⟩⟩.

Equations

• NavierStokes.GlobalSlowProfiles.inverse f hf = ⟨fun (w : ℝ × ℝ) => (↑f w)⁻¹, ⋯⟩

theorem NavierStokes.GlobalSlowProfiles.smooth_de {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) : Smooth S (de f)

theorem NavierStokes.GlobalSlowProfiles.parameter_derivative {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {eta : ℝ} (heta : eta ∈ S) (R : ℝ) : HasDerivAt (fun (t : ℝ) => f (R, t)) (de f (R, eta)) eta

noncomputable def NavierStokes.GlobalSlowProfiles.etaDerivative {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) : EvenProfile S

Eta derivative as an element of EvenProfile S.

Equations

• NavierStokes.GlobalSlowProfiles.etaDerivative hS f = ⟨NavierStokes.GlobalSlowProfiles.de ↑f, ⋯⟩

noncomputable def NavierStokes.GlobalSlowProfiles.xDerivative {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) : EvenProfile S

The genuine X derivative, smoothly continued through R = 0.

Equations

• NavierStokes.GlobalSlowProfiles.xDerivative hS f = ⟨fun (w : ℝ × ℝ) => 2 * NavierStokes.BoundaryAxisJets.radialJet (↑f) 1 w.1 w.2, ⋯⟩

theorem NavierStokes.GlobalSlowProfiles.radius_mul_xDerivative {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {eta : ℝ} (heta : eta ∈ S) (R : ℝ) : R * ↑(xDerivative hS f) (R, eta) = dr ↑f (R, eta)

noncomputable def NavierStokes.GlobalSlowProfiles.coreCutoff (inner stop : ℝ) (w : ℝ × ℝ) : ℝ

Literal X-only cutoff. The same two radii will be used at every order.

Equations

• NavierStokes.GlobalSlowProfiles.coreCutoff inner stop w = 1 - NavierStokes.TransportPrimitive.cutoff inner stop (w.1 ^ 2 / 2)

theorem NavierStokes.GlobalSlowProfiles.coreCutoff_smooth (inner stop : ℝ) : ContDiff ℝ (↑⊤) (coreCutoff inner stop)

theorem NavierStokes.GlobalSlowProfiles.coreCutoff_one {inner stop : ℝ} (his : inner < stop) {w : ℝ × ℝ} (hw : w.1 ^ 2 / 2 ≤ inner) : coreCutoff inner stop w = 1

theorem NavierStokes.GlobalSlowProfiles.coreCutoff_zero {inner stop : ℝ} (his : inner < stop) {w : ℝ × ℝ} (hw : stop ≤ w.1 ^ 2 / 2) : coreCutoff inner stop w = 0

noncomputable def NavierStokes.GlobalSlowProfiles.massAverage {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) : EvenProfile S

A normalized mass average. There is no division by the radius.

Equations

• NavierStokes.GlobalSlowProfiles.massAverage hS f = ⟨fun (w : ℝ × ℝ) => 2 * ∫ (t : ℝ) in 0..1, t * ↑f (t * w.1, w.2), ⋯⟩

theorem NavierStokes.GlobalSlowProfiles.massHistory_eq_massAverage {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) (w : ℝ × ℝ) : PositiveOrderMoments.massHistory (↑f) w = w.1 ^ 2 / 2 * ↑(massAverage hS f) w

theorem NavierStokes.GlobalSlowProfiles.parameterMassHistory_eq_massAverage {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {w : ℝ × ℝ} (hw : w.2 ∈ S) : PositiveOrderMoments.parameterMassHistory (↑f) w = w.1 ^ 2 / 2 * ↑(massAverage hS (etaDerivative hS f)) w

structure NavierStokes.GlobalSlowProfiles.Domain (S : Set ℝ) (h : ℝ) : Prop

Domain data, collecting isOpen, denominator.

• isOpen : IsOpen S
• denominator (eta : ℝ) : eta ∈ S → PositiveAxisSystem.ell h eta ≠ 0

noncomputable def NavierStokes.GlobalSlowProfiles.inverseDenominator {S : Set ℝ} {h : ℝ} (d : Domain S h) : EvenProfile S

Inverse denominator, given by inverse (1 - boundConstant S (2 * h) * parameter S ^ 2) (fun w hw => d.denominator w.2 hw.2).

Equations

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

@[simp]

theorem NavierStokes.GlobalSlowProfiles.inverseDenominator_apply {S : Set ℝ} {h : ℝ} (d : Domain S h) (w : ℝ × ℝ) : ↑(inverseDenominator d) w = (PositiveAxisSystem.ell h w.2)⁻¹

noncomputable def NavierStokes.GlobalSlowProfiles.betaFromU {S : Set ℝ} {h : ℝ} (d : Domain S h) (lam : ℝ) (u : EvenProfile S) : EvenProfile S

The normalized divergence reconstruction V = X β.

Equations

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

theorem NavierStokes.GlobalSlowProfiles.betaFromU_eq_fluxHistory {S : Set ℝ} {h : ℝ} (d : Domain S h) (lam : ℝ) (u : EvenProfile S) {w : ℝ × ℝ} (hw : w.2 ∈ S) : w.1 ^ 2 / 2 * ↑(betaFromU d lam u) w = PositiveOrderMoments.fluxHistory h lam (↑u) w

theorem NavierStokes.GlobalSlowProfiles.reconstructed_flux_derivative {S : Set ℝ} {h : ℝ} (d : Domain S h) (lam : ℝ) (u : EvenProfile S) {R eta : ℝ} (heta : eta ∈ S) : HasDerivAt (fun (r : ℝ) => r ^ 2 / 2 * ↑(betaFromU d lam u) (r, eta)) (-R * PositiveOrderMoments.radialZ h (-PositiveAxisSystem.a h + lam) ↑u (R, eta)) R

noncomputable def NavierStokes.GlobalSlowProfiles.timeOp {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) : EvenProfile S

Time op as an element of EvenProfile S.

Equations

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

noncomputable def NavierStokes.GlobalSlowProfiles.axialOp {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) : EvenProfile S

Axial op as an element of EvenProfile S.

Equations

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

noncomputable def NavierStokes.GlobalSlowProfiles.axialOp2 {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) : EvenProfile S

Axial Op2, given by axialOp d (b - SimilarityProfile.D h) (axialOp d b f).

Equations

• NavierStokes.GlobalSlowProfiles.axialOp2 d b f = NavierStokes.GlobalSlowProfiles.axialOp d (b - NavierStokes.SimilarityProfile.D h) (NavierStokes.GlobalSlowProfiles.axialOp d b f)

noncomputable def NavierStokes.GlobalSlowProfiles.shiftedAxial {S : Set ℝ} {h : ℝ} (d : Domain S h) (beta : ℕ → EvenProfile S) : ℕ → EvenProfile S

Shifted axial as an element of ℕ → EvenProfile S | 0 => 0 | k + 1 => axialOp2 d (AxisSourceRegularity.slowOrder h k - 1) (beta k).

Equations

• NavierStokes.GlobalSlowProfiles.shiftedAxial d beta 0 = 0
• NavierStokes.GlobalSlowProfiles.shiftedAxial d beta k.succ = NavierStokes.GlobalSlowProfiles.axialOp2 d (NavierStokes.AxisSourceRegularity.slowOrder h k - 1) (beta k)

noncomputable def NavierStokes.GlobalSlowProfiles.omegaDivX {S : Set ℝ} {h : ℝ} (d : Domain S h) (u beta : ℕ → EvenProfile S) (k : ℕ) : EvenProfile S

The complete radial source divided by X, including both viscous terms.

Equations

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

noncomputable def NavierStokes.GlobalSlowProfiles.previousOmegaDivX {S : Set ℝ} {h : ℝ} (d : Domain S h) (u beta : ℕ → EvenProfile S) : ℕ → EvenProfile S

Previous omega div X as an element of ℕ → EvenProfile S | 0 => 0 | k + 1 => omegaDivX d u beta k.

Equations

• NavierStokes.GlobalSlowProfiles.previousOmegaDivX d u beta 0 = 0
• NavierStokes.GlobalSlowProfiles.previousOmegaDivX d u beta k.succ = NavierStokes.GlobalSlowProfiles.omegaDivX d u beta k

noncomputable def NavierStokes.GlobalSlowProfiles.angularField {S : Set ℝ} (C : ℝ) (phi : EvenProfile S) (w : ℝ × ℝ) : ℝ

Angular field, given by w.1 / C * phi w.

Equations

• NavierStokes.GlobalSlowProfiles.angularField C phi w = w.1 / C * ↑phi w

theorem NavierStokes.GlobalSlowProfiles.angularField_smooth {S : Set ℝ} (C : ℝ) (phi : EvenProfile S) : Smooth S (angularField C phi)

noncomputable def NavierStokes.GlobalSlowProfiles.pressureSource {S : Set ℝ} (C : ℝ) (phi : ℕ → EvenProfile S) (omega : EvenProfile S) (n : ℕ) : EvenProfile S

Pressure source, given by boundConstant S (C ^ 2)⁻¹ * (∑ i ∈ Finset.range (n + 1), phi i * phi (n - i)) - boundConstant S (1 / 2) * omega.

Equations

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

noncomputable def NavierStokes.GlobalSlowProfiles.pressureFromSource {S : Set ℝ} (hS : IsOpen S) (source : EvenProfile S) : EvenProfile S

Pressure from source, given by radiusSquared S * massAverage hS source.

Equations

• NavierStokes.GlobalSlowProfiles.pressureFromSource hS source = NavierStokes.GlobalSlowProfiles.radiusSquared S * NavierStokes.GlobalSlowProfiles.massAverage hS source

theorem NavierStokes.GlobalSlowProfiles.pressureFromSource_eq_primitive {S : Set ℝ} (hS : IsOpen S) (source : EvenProfile S) (w : ℝ × ℝ) : ↑(pressureFromSource hS source) w = ProfileHistories.primitive (fun (p : ProfileHistories.Point) => p.1 * ↑source p) w

theorem NavierStokes.GlobalSlowProfiles.actual_pressureGradient {S : Set ℝ} (C : ℝ) (phi : ℕ → EvenProfile S) (omega : EvenProfile S) (n : ℕ) (w : ℝ × ℝ) : PositiveOrderMoments.jointPressureGradient n (fun (j : ℕ) => angularField C (phi j)) (fun (p : ℝ × ℝ) => p.1 ^ 2 / 2 * ↑omega p) w = w.1 * ↑(pressureSource C phi omega n) w

theorem NavierStokes.GlobalSlowProfiles.pressureFromSource_eq_pressureHistory {S : Set ℝ} (hS : IsOpen S) (C : ℝ) (phi : ℕ → EvenProfile S) (omega : EvenProfile S) (n : ℕ) : ↑(pressureFromSource hS (pressureSource C phi omega n)) = PositiveOrderMoments.pressureHistory n (fun (j : ℕ) => angularField C (phi j)) fun (p : ℝ × ℝ) => p.1 ^ 2 / 2 * ↑omega p

noncomputable def NavierStokes.GlobalSlowProfiles.radialLift {rho : ℝ} {U : Set ℂ} (f : SlowRecursion.AxisFunction rho U) (w : ℝ × ℝ) : ℝ

Pull a local even axis function to the physical similarity radius.

Equations

• NavierStokes.GlobalSlowProfiles.radialLift f w = (↑f (w.1 / √2, ↑w.2)).re

theorem NavierStokes.GlobalSlowProfiles.radialLift_mem {rho R : ℝ} (hrho : 0 < rho) (hR : R ^ 2 / 2 < rho ^ 2) : R / √2 ∈ Set.Ioo (-rho) rho

noncomputable def NavierStokes.GlobalSlowProfiles.cutoffLift {rho : ℝ} {U : Set ℂ} {S : Set ℝ} (hrho : 0 < rho) (hU : IsOpen U) (_hS : IsOpen S) (hSU : ∀ eta ∈ S, ↑eta ∈ U) {inner stop : ℝ} (his : inner < stop) (hsrho : stop < rho ^ 2) (f : SlowRecursion.AxisFunction rho U) : EvenProfile S

Localizing never evaluates derivatives outside the common hierarchy radius: the cutoff is already zero on a neighborhood of that boundary.

Equations

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

theorem NavierStokes.GlobalSlowProfiles.cutoffLift_eq {rho : ℝ} {U : Set ℂ} {S : Set ℝ} (hrho : 0 < rho) (hU : IsOpen U) (hS : IsOpen S) (hSU : ∀ eta ∈ S, ↑eta ∈ U) {inner stop : ℝ} (his : inner < stop) (hsrho : stop < rho ^ 2) (f : SlowRecursion.AxisFunction rho U) {w : ℝ × ℝ} (hw : w.1 ^ 2 / 2 ≤ inner) : ↑(cutoffLift hrho hU hS hSU his hsrho f) w = radialLift f w

theorem NavierStokes.GlobalSlowProfiles.cutoffLift_zero {rho : ℝ} {U : Set ℂ} {S : Set ℝ} (hrho : 0 < rho) (hU : IsOpen U) (hS : IsOpen S) (hSU : ∀ eta ∈ S, ↑eta ∈ U) {inner stop : ℝ} (his : inner < stop) (hsrho : stop < rho ^ 2) (f : SlowRecursion.AxisFunction rho U) {w : ℝ × ℝ} (hw : stop ≤ w.1 ^ 2 / 2) : ↑(cutoffLift hrho hU hS hSU his hsrho f) w = 0

noncomputable def NavierStokes.GlobalSlowProfiles.PatchSupport (a b : ℝ) (f : Field) : Prop

Patch support, given by ∀ eta, tsupport (fun R => f (R, eta)) ⊆ Ioo a b.

Equations

• NavierStokes.GlobalSlowProfiles.PatchSupport a b f = ∀ (eta : ℝ), (tsupport fun (R : ℝ) => f (R, eta)) ⊆ Set.Ioo a b

theorem NavierStokes.GlobalSlowProfiles.patch_zero {a b : ℝ} {f : Field} (hs : PatchSupport a b f) {R eta : ℝ} (hR : R ∉ Set.Ioo a b) : f (R, eta) = 0

noncomputable def NavierStokes.GlobalSlowProfiles.evenCorrection {S : Set ℝ} {f : Field} (hf : Smooth S f) : EvenProfile S

Even correction as an element of EvenProfile S.

Equations

• NavierStokes.GlobalSlowProfiles.evenCorrection hf = ⟨fun (w : ℝ × ℝ) => f w + f (-w.1, w.2), ⋯⟩

noncomputable def NavierStokes.GlobalSlowProfiles.phiCorrection {S : Set ℝ} (_hS : IsOpen S) {a b : ℝ} (ha : 0 < a) {f : Field} (hf : Smooth S f) (hs : PatchSupport a b f) (C : ℝ) : EvenProfile S

Odd angular correction divided by R. The support gap proves smoothness at zero instead of appealing to a formal cancellation.

Equations

• NavierStokes.GlobalSlowProfiles.phiCorrection _hS ha hf hs C = ⟨fun (w : ℝ × ℝ) => C * (f w - f (-w.1, w.2)) / w.1, ⋯⟩

theorem NavierStokes.GlobalSlowProfiles.evenCorrection_nonneg {S : Set ℝ} {a b : ℝ} (ha : 0 < a) {f : Field} (hf : Smooth S f) (hs : PatchSupport a b f) {R eta : ℝ} (hR : 0 ≤ R) : ↑(evenCorrection hf) (R, eta) = f (R, eta)

theorem NavierStokes.GlobalSlowProfiles.phiCorrection_angular_nonneg {S : Set ℝ} (hS : IsOpen S) {a b : ℝ} (ha : 0 < a) {f : Field} (hf : Smooth S f) (hs : PatchSupport a b f) {C : ℝ} (hC : C ≠ 0) {R eta : ℝ} (hR : 0 ≤ R) : angularField C (phiCorrection hS ha hf hs C) (R, eta) = f (R, eta)

theorem NavierStokes.GlobalSlowProfiles.evenCorrection_inner {S : Set ℝ} {a b : ℝ} {f : Field} (hf : Smooth S f) (hs : PatchSupport a b f) {R eta : ℝ} (hR : |R| ≤ a) : ↑(evenCorrection hf) (R, eta) = 0

theorem NavierStokes.GlobalSlowProfiles.phiCorrection_inner {S : Set ℝ} (hS : IsOpen S) {a b : ℝ} (ha : 0 < a) {f : Field} (hf : Smooth S f) (hs : PatchSupport a b f) (C : ℝ) {R eta : ℝ} (hR : |R| ≤ a) : ↑(phiCorrection hS ha hf hs C) (R, eta) = 0

@[reducible, inline]

abbrev NavierStokes.GlobalSlowProfiles.Exterior (B : ℝ) (S : Set ℝ) (f : SlowStressSupport.Field) : Prop

Exterior: an abbreviation for SlowStressSupport.exterior.

Equations

• NavierStokes.GlobalSlowProfiles.Exterior = NavierStokes.SlowStressSupport.exterior

theorem NavierStokes.GlobalSlowProfiles.exterior_xDerivative {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {B : ℝ} (hB : 0 < B) (hf : Exterior B S ↑f) : Exterior B S ↑(xDerivative hS f)

theorem NavierStokes.GlobalSlowProfiles.exterior_etaDerivative {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {B : ℝ} (hf : Exterior B S ↑f) : Exterior B S ↑(etaDerivative hS f)

theorem NavierStokes.GlobalSlowProfiles.exterior_timeOp {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) {B : ℝ} (hB : 0 < B) (hf : Exterior B S ↑f) : Exterior B S ↑(timeOp d b f)

theorem NavierStokes.GlobalSlowProfiles.exterior_axialOp {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) {B : ℝ} (hB : 0 < B) (hf : Exterior B S ↑f) : Exterior B S ↑(axialOp d b f)

theorem NavierStokes.GlobalSlowProfiles.exterior_axialOp2 {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) {B : ℝ} (hB : 0 < B) (hf : Exterior B S ↑f) : Exterior B S ↑(axialOp2 d b f)

theorem NavierStokes.GlobalSlowProfiles.exterior_omegaDivX {S : Set ℝ} {h : ℝ} (d : Domain S h) (u beta : ℕ → EvenProfile S) (k : ℕ) {B : ℝ} (hB : 0 < B) (hb : ∀ j ≤ k, Exterior B S ↑(beta j)) : Exterior B S ↑(omegaDivX d u beta k)

theorem NavierStokes.GlobalSlowProfiles.exterior_previousOmegaDivX {S : Set ℝ} {h : ℝ} (d : Domain S h) (u beta : ℕ → EvenProfile S) (n : ℕ) {B : ℝ} (hB : 0 < B) (hb : ∀ j < n, Exterior B S ↑(beta j)) : Exterior B S ↑(previousOmegaDivX d u beta n)

theorem NavierStokes.GlobalSlowProfiles.exterior_pressureSource {S : Set ℝ} (C : ℝ) (phi : ℕ → EvenProfile S) (omega : EvenProfile S) {n : ℕ} (hn : 0 < n) {B : ℝ} (hp : ∀ (j : ℕ), 0 < j → j ≤ n → Exterior B S ↑(phi j)) (ho : Exterior B S ↑omega) : Exterior B S ↑(pressureSource C phi omega n)

theorem NavierStokes.GlobalSlowProfiles.exterior_evenCorrection {S : Set ℝ} {a b B : ℝ} (ha : 0 < a) (hab : a < b) (hbB : b ≤ B) {f : Field} (hf : Smooth S f) (hs : PatchSupport a b f) : Exterior B S ↑(evenCorrection hf)

theorem NavierStokes.GlobalSlowProfiles.exterior_phiCorrection {S : Set ℝ} (hS : IsOpen S) {a b B : ℝ} (ha : 0 < a) (hab : a < b) (hbB : b ≤ B) {f : Field} (hf : Smooth S f) (hs : PatchSupport a b f) (C : ℝ) : Exterior B S ↑(phiCorrection hS ha hf hs C)

theorem NavierStokes.GlobalSlowProfiles.moments_congr_positive {n : ℕ} {u e u' e' : PositiveOrderMoments.History} {omega omega' : ℝ → ℝ} (hu : ∀ (R : ℝ), 0 < R → ∀ (j : ℕ), u j R = u' j R) (he : ∀ (R : ℝ), 0 < R → ∀ (j : ℕ), e j R = e' j R) (ho : ∀ (R : ℝ), 0 < R → omega R = omega' R) : PositiveOrderMoments.moments n u e omega = PositiveOrderMoments.moments n u' e' omega'

theorem NavierStokes.GlobalSlowProfiles.actual_pressureGradient_smooth {S : Set ℝ} (C : ℝ) (phi : ℕ → EvenProfile S) (omega : EvenProfile S) (n : ℕ) : Smooth S (PositiveOrderMoments.jointPressureGradient n (fun (j : ℕ) => angularField C (phi j)) fun (p : ℝ × ℝ) => p.1 ^ 2 / 2 * ↑omega p)

theorem NavierStokes.GlobalSlowProfiles.exists_repaired_order {S : Set ℝ} (hS : IsOpen S) {C lam a b B : ℝ} (hC : C ≠ 0) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (hbB : b ≤ B) {n : ℕ} (hn : 0 < n) (u phi : ℕ → EvenProfile S) (omega : EvenProfile S) (A : ℝ → ℝ) (hA : ContDiffOn ℝ (↑⊤) A S) (hAn : ∀ eta ∈ S, A eta ≠ 0) (hu0 : ∀ eta ∈ S, ∀ R ∈ Set.Ioo a b, ↑(u 0) (R, eta) = 0) (he0 : ∀ eta ∈ S, ∀ R ∈ Set.Ioo a b, angularField C (phi 0) (R, eta) = FiveRowRank.background lam (A eta) R) (huB : ∀ j ≤ n, Exterior B S ↑(u j)) (hpB : ∀ (j : ℕ), 0 < j → j ≤ n → Exterior B S ↑(phi j)) (hoB : Exterior B S ↑omega) : ∃ (un : EvenProfile S) (phin : EvenProfile S), (∀ (eta R : ℝ), |R| ≤ a → ↑un (R, eta) = ↑(u n) (R, eta)) ∧ (∀ (eta R : ℝ), |R| ≤ a → ↑phin (R, eta) = ↑(phi n) (R, eta)) ∧ Exterior B S ↑un ∧ Exterior B S ↑phin ∧ (∀ (eta R : ℝ), b ≤ R → ↑un (R, eta) = ↑(u n) (R, eta)) ∧ (∀ (eta R : ℝ), b ≤ R → ↑phin (R, eta) = ↑(phi n) (R, eta)) ∧ ∀ eta ∈ S, (PositiveOrderMoments.moments n (PositiveOrderMoments.slice (fun (j : ℕ) => ↑(Function.update u n un j)) eta) (PositiveOrderMoments.slice (fun (j : ℕ) => angularField C (Function.update phi n phin j)) eta) fun (R : ℝ) => R ^ 2 / 2 * ↑omega (R, eta)) = 0

One repair step. Only actual smooth profiles and their compact exterior are inputs; the five zero moments are proved by the explicit linear repair.

theorem NavierStokes.GlobalSlowProfiles.reconstructed_beta_exterior {S : Set ℝ} {h : ℝ} (d : Domain S h) (lam : ℝ) (u : EvenProfile S) {B : ℝ} (hB : 0 < B) (hu : Exterior B S ↑u) (hm : ∀ eta ∈ S, (PositiveOrderMoments.positiveIntegral fun (R : ℝ) => R * ↑u (R, eta)) = 0) : Exterior B S ↑(betaFromU d lam u)

theorem NavierStokes.GlobalSlowProfiles.reconstructed_pressure_exterior {S : Set ℝ} (hS : IsOpen S) (C : ℝ) (u phi : ℕ → EvenProfile S) (omega : EvenProfile S) {n : ℕ} (hn : 0 < n) {B : ℝ} (hB : 0 ≤ B) (hpB : ∀ (j : ℕ), 0 < j → j ≤ n → Exterior B S ↑(phi j)) (hoB : Exterior B S ↑omega) (hm : ∀ eta ∈ S, (PositiveOrderMoments.moments n (PositiveOrderMoments.slice (fun (j : ℕ) => ↑(u j)) eta) (PositiveOrderMoments.slice (fun (j : ℕ) => angularField C (phi j)) eta) fun (R : ℝ) => R ^ 2 / 2 * ↑omega (R, eta)) = 0) : Exterior B S ↑(pressureFromSource hS (pressureSource C phi omega n))

structure NavierStokes.GlobalSlowProfiles.Coefficient (S : Set ℝ) : Type

Coefficient data, collecting phi, axial, beta, pressure.

• phi : EvenProfile S

  Phi of Coefficient, of type EvenProfile S.

• axial : EvenProfile S

  Axial of Coefficient, of type EvenProfile S.

• beta : EvenProfile S

  Beta of Coefficient, of type EvenProfile S.

• pressure : EvenProfile S

  Pressure field of Coefficient, of type EvenProfile S.

structure NavierStokes.GlobalSlowProfiles.Scheme (S : Set ℝ) (h C : ℝ) : Type

The finite order-zero data and a sequence of localized seeds. The constructor schemeFromHierarchy below supplies the seeds from one actual local hierarchy and one common cutoff.

• domain : Domain S h
• nonzero_scale : C ≠ 0
• lam : ℝ

  Lam of Scheme, of type ℝ.

• lam_pos : 0 < self.lam
• a : ℝ

  A of Scheme, of type ℝ.

• b : ℝ

  B of Scheme, of type ℝ.

• B : ℝ

  Bound parameter of Scheme, of type ℝ.

• a_pos : 0 < self.a
• a_lt_b : self.a < self.b
• b_le_B : self.b ≤ self.B
• amplitude : ℝ → ℝ

  Amplitude of Scheme, of type ℝ → ℝ.

• amplitude_smooth : ContDiffOn ℝ (↑⊤) self.amplitude S
• amplitude_ne (eta : ℝ) : eta ∈ S → self.amplitude eta ≠ 0
• base : Coefficient S

  Base of Scheme, of type Coefficient S.

• base_axial_exterior : Exterior self.B S ↑self.base.axial
• base_beta_exterior : Exterior self.B S ↑self.base.beta
• base_axial_patch (eta : ℝ) : eta ∈ S → ∀ R ∈ Set.Ioo self.a self.b, ↑self.base.axial (R, eta) = 0
• base_angular_patch (eta : ℝ) : eta ∈ S → ∀ R ∈ Set.Ioo self.a self.b, angularField C self.base.phi (R, eta) = FiveRowRank.background self.lam (self.amplitude eta) R
• seedAxial : ℕ → EvenProfile S

  Seed axial of Scheme, of type ℕ → EvenProfile S.

• seedPhi : ℕ → EvenProfile S

  Seed phi of Scheme, of type ℕ → EvenProfile S.

• seedAxial_exterior (n : ℕ) : Exterior self.B S ↑(self.seedAxial n)
• seedPhi_exterior (n : ℕ) : Exterior self.B S ↑(self.seedPhi n)

theorem NavierStokes.GlobalSlowProfiles.Scheme.B_pos {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) : 0 < s.B

structure NavierStokes.GlobalSlowProfiles.Admissible {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) : Type

Admissible data, collecting data, axial_exterior, beta_exterior, phi_exterior, pressure_exterior, zero_data and their compatibility conditions.

• data : Coefficient S

  Data of Admissible, of type Coefficient S.

• axial_exterior : Exterior s.B S ↑self.data.axial
• beta_exterior : Exterior s.B S ↑self.data.beta
• phi_exterior : 0 < n → Exterior s.B S ↑self.data.phi
• pressure_exterior : 0 < n → Exterior s.B S ↑self.data.pressure
• zero_data : n = 0 → self.data = s.base
• inner_axial : 0 < n → ∀ (eta R : ℝ), |R| ≤ s.a → ↑self.data.axial (R, eta) = ↑(s.seedAxial n) (R, eta)
• inner_phi : 0 < n → ∀ (eta R : ℝ), |R| ≤ s.a → ↑self.data.phi (R, eta) = ↑(s.seedPhi n) (R, eta)
• outer_axial : 0 < n → ∀ (eta R : ℝ), s.b ≤ R → ↑self.data.axial (R, eta) = ↑(s.seedAxial n) (R, eta)
• outer_phi : 0 < n → ∀ (eta R : ℝ), s.b ≤ R → ↑self.data.phi (R, eta) = ↑(s.seedPhi n) (R, eta)

noncomputable def NavierStokes.GlobalSlowProfiles.previousAxial {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) (previous : (j : ℕ) → j < n → Admissible s j) (j : ℕ) : EvenProfile S

Previous axial, with branches according to hj : j < n.

Equations

• NavierStokes.GlobalSlowProfiles.previousAxial s n previous j = if hj : j < n then (previous j hj).data.axial else s.seedAxial n

noncomputable def NavierStokes.GlobalSlowProfiles.previousPhi {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) (previous : (j : ℕ) → j < n → Admissible s j) (j : ℕ) : EvenProfile S

Previous phi, with branches according to hj : j < n.

Equations

• NavierStokes.GlobalSlowProfiles.previousPhi s n previous j = if hj : j < n then (previous j hj).data.phi else s.seedPhi n

noncomputable def NavierStokes.GlobalSlowProfiles.previousBeta {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) (previous : (j : ℕ) → j < n → Admissible s j) (j : ℕ) : EvenProfile S

Previous beta, with branches according to hj : j < n.

Equations

• NavierStokes.GlobalSlowProfiles.previousBeta s n previous j = if hj : j < n then (previous j hj).data.beta else 0

noncomputable def NavierStokes.GlobalSlowProfiles.previousSource {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) (previous : (j : ℕ) → j < n → Admissible s j) : EvenProfile S

Previous source, given by previousOmegaDivX s.domain (previousAxial s n previous) (previousBeta s n previous) n.

Equations

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

def NavierStokes.GlobalSlowProfiles.StepProperties {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) (previous : (j : ℕ) → j < n → Admissible s j) (out : Admissible s n) : Prop

Step properties, constructed using out.data.beta.

Equations

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

theorem NavierStokes.GlobalSlowProfiles.exists_step {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) (previous : (j : ℕ) → j < n → Admissible s j) : ∃ (out : Admissible s n), StepProperties s n previous out

noncomputable def NavierStokes.GlobalSlowProfiles.step {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) (previous : (j : ℕ) → j < n → Admissible s j) : Admissible s n

Step, given by Classical.choose (exists_step s hn previous).

Equations

• NavierStokes.GlobalSlowProfiles.step s hn previous = Classical.choose ⋯

theorem NavierStokes.GlobalSlowProfiles.step_spec {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) (previous : (j : ℕ) → j < n → Admissible s j) : StepProperties s n previous (step s hn previous)

noncomputable def NavierStokes.GlobalSlowProfiles.recursionStep {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) : ((j : ℕ) → j < n → Admissible s j) → Admissible s n

Recursion step used in global slow profiles.

Equations

• One or more equations did not get rendered due to their size.
• NavierStokes.GlobalSlowProfiles.recursionStep s n.succ previous = NavierStokes.GlobalSlowProfiles.step s ⋯ previous

noncomputable def NavierStokes.GlobalSlowProfiles.sequence {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) : Admissible s n

A single coherent infinite sequence, constructed by well-founded recursion; all coefficient indices used in the radial source are smaller.

Equations

• NavierStokes.GlobalSlowProfiles.sequence s n = ⋯.fix (NavierStokes.GlobalSlowProfiles.recursionStep s) n

noncomputable def NavierStokes.GlobalSlowProfiles.profiles {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) : Coefficient S

Profiles, given by (sequence s n).data.

Equations

• NavierStokes.GlobalSlowProfiles.profiles s n = (NavierStokes.GlobalSlowProfiles.sequence s n).data

theorem NavierStokes.GlobalSlowProfiles.sequence_succ {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) : sequence s (n + 1) = step s ⋯ fun (j : ℕ) (x : j < n.succ) => sequence s j

theorem NavierStokes.GlobalSlowProfiles.profiles_zero {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) : profiles s 0 = s.base

theorem NavierStokes.GlobalSlowProfiles.profiles_axial_exterior {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) : Exterior s.B S ↑(profiles s n).axial

theorem NavierStokes.GlobalSlowProfiles.profiles_beta_exterior {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) : Exterior s.B S ↑(profiles s n).beta

theorem NavierStokes.GlobalSlowProfiles.profiles_phi_exterior {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) : Exterior s.B S ↑(profiles s n).phi

theorem NavierStokes.GlobalSlowProfiles.profiles_pressure_exterior {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) : Exterior s.B S ↑(profiles s n).pressure

theorem NavierStokes.GlobalSlowProfiles.profiles_inner_axial {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : |R| ≤ s.a) : ↑(profiles s n).axial (R, eta) = ↑(s.seedAxial n) (R, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_inner_phi {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : |R| ≤ s.a) : ↑(profiles s n).phi (R, eta) = ↑(s.seedPhi n) (R, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_outer_axial {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : s.b ≤ R) : ↑(profiles s n).axial (R, eta) = ↑(s.seedAxial n) (R, eta)

Positive-order repairs preserve the actual seed beyond the repair patch. This property is retained in the predicate used to select each step.

theorem NavierStokes.GlobalSlowProfiles.profiles_outer_phi {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : s.b ≤ R) : ↑(profiles s n).phi (R, eta) = ↑(s.seedPhi n) (R, eta)

theorem NavierStokes.GlobalSlowProfiles.omegaDivX_congr_prefix {S : Set ℝ} {h : ℝ} (d : Domain S h) {u beta u' beta' : ℕ → EvenProfile S} (k : ℕ) (hu : ∀ j ≤ k, u j = u' j) (hb : ∀ j ≤ k, beta j = beta' j) : omegaDivX d u beta k = omegaDivX d u' beta' k

theorem NavierStokes.GlobalSlowProfiles.previousOmegaDivX_congr_prefix {S : Set ℝ} {h : ℝ} (d : Domain S h) {u beta u' beta' : ℕ → EvenProfile S} (n : ℕ) (hu : ∀ j < n, u j = u' j) (hb : ∀ j < n, beta j = beta' j) : previousOmegaDivX d u beta n = previousOmegaDivX d u' beta' n

theorem NavierStokes.GlobalSlowProfiles.pressureSource_congr_prefix {S : Set ℝ} (C : ℝ) {phi phi' : ℕ → EvenProfile S} (omega : EvenProfile S) (n : ℕ) (hp : ∀ j ≤ n, phi j = phi' j) : pressureSource C phi omega n = pressureSource C phi' omega n

theorem NavierStokes.GlobalSlowProfiles.cauchy_congr_prefix {u e u' e' : PositiveOrderMoments.History} (n : ℕ) (R : ℝ) (hu : ∀ j ≤ n, u j R = u' j R) (he : ∀ j ≤ n, e j R = e' j R) : PositiveOrderMoments.cauchy n u e R = PositiveOrderMoments.cauchy n u' e' R

theorem NavierStokes.GlobalSlowProfiles.moments_congr_prefix {n : ℕ} {u e u' e' : PositiveOrderMoments.History} {omega omega' : ℝ → ℝ} (hu : ∀ (R : ℝ), 0 < R → ∀ j ≤ n, u j R = u' j R) (he : ∀ (R : ℝ), 0 < R → ∀ j ≤ n, e j R = e' j R) (ho : ∀ (R : ℝ), 0 < R → omega R = omega' R) : PositiveOrderMoments.moments n u e omega = PositiveOrderMoments.moments n u' e' omega'

theorem NavierStokes.GlobalSlowProfiles.sequence_step_spec {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) : StepProperties s n (fun (j : ℕ) (x : j < n) => sequence s j) (sequence s n)

theorem NavierStokes.GlobalSlowProfiles.previousSource_sequence {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) : (previousSource s n fun (j : ℕ) (x : j < n) => sequence s j) = previousOmegaDivX ⋯ (fun (j : ℕ) => (profiles s j).axial) (fun (j : ℕ) => (profiles s j).beta) n

theorem NavierStokes.GlobalSlowProfiles.updated_sequence_axial {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) {j : ℕ} (hj : j ≤ n) : Function.update (previousAxial s n fun (k : ℕ) (x : k < n) => sequence s k) n (profiles s n).axial j = (profiles s j).axial

theorem NavierStokes.GlobalSlowProfiles.updated_sequence_phi {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) {j : ℕ} (hj : j ≤ n) : Function.update (previousPhi s n fun (k : ℕ) (x : k < n) => sequence s k) n (profiles s n).phi j = (profiles s j).phi

theorem NavierStokes.GlobalSlowProfiles.profiles_moments {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {eta : ℝ} (heta : eta ∈ S) : (PositiveOrderMoments.moments n (PositiveOrderMoments.slice (fun (j : ℕ) => ↑(profiles s j).axial) eta) (PositiveOrderMoments.slice (fun (j : ℕ) => angularField C (profiles s j).phi) eta) fun (R : ℝ) => R ^ 2 / 2 * ↑(previousOmegaDivX ⋯ (fun (j : ℕ) => (profiles s j).axial) (fun (j : ℕ) => (profiles s j).beta) n) (R, eta)) = 0

All five actual total rows hold at every positive order of the same infinite sequence. The source is recomputed from that sequence's lower fields.

theorem NavierStokes.GlobalSlowProfiles.profiles_beta_eq {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) : (profiles s n).beta = betaFromU ⋯ (AxisSourceRegularity.slowOrder h n) (profiles s n).axial

theorem NavierStokes.GlobalSlowProfiles.profiles_pressure_eq {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) : (profiles s n).pressure = pressureFromSource ⋯ (pressureSource C (fun (j : ℕ) => (profiles s j).phi) (previousOmegaDivX ⋯ (fun (j : ℕ) => (profiles s j).axial) (fun (j : ℕ) => (profiles s j).beta) n) n)

structure NavierStokes.GlobalSlowProfiles.BaseData (S : Set ℝ) (C lam a b B : ℝ) : Type

Data required from the actual order-zero construction. No positive-order equations, moments, or extension properties are assumed here.

• fields : Coefficient S

  Fields of BaseData, of type Coefficient S.

• axial_exterior : Exterior B S ↑self.fields.axial
• beta_exterior : Exterior B S ↑self.fields.beta
• amplitude : ℝ → ℝ

  Amplitude of BaseData, of type ℝ → ℝ.

• amplitude_smooth : ContDiffOn ℝ (↑⊤) self.amplitude S
• amplitude_ne (eta : ℝ) : eta ∈ S → self.amplitude eta ≠ 0
• axial_patch (eta : ℝ) : eta ∈ S → ∀ R ∈ Set.Ioo a b, ↑self.fields.axial (R, eta) = 0
• angular_patch (eta : ℝ) : eta ∈ S → ∀ R ∈ Set.Ioo a b, angularField C self.fields.phi (R, eta) = FiveRowRank.background lam (self.amplitude eta) R

noncomputable def NavierStokes.GlobalSlowProfiles.schemeFromHierarchy {rho : ℝ} {U : Set ℂ} {S : Set ℝ} {h C lam inner stop a b B : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : SlowRecursion.LocalHierarchy rho U h C base) (hrho : 0 < rho) (hU : IsOpen U) (d : Domain S h) (hSU : ∀ eta ∈ S, ↑eta ∈ U) (hC : C ≠ 0) (hlam : 0 < lam) (his : inner < stop) (hsrho : stop < rho ^ 2) (hsa : stop < a ^ 2 / 2) (ha : 0 < a) (hab : a < b) (hbB : b ≤ B) (B0 : BaseData S C lam a b B) : Scheme S h C

The common cutoff is chosen strictly inside the hierarchy's proved radius; the moment patch begins beyond that cutoff.

Equations

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

noncomputable def NavierStokes.GlobalSlowProfiles.xProfile {S : Set ℝ} (f : EvenProfile S) (w : ℝ × ℝ) : ℝ

The actual squared-radius profile. We use ordinary derivatives only at positive X; the axis jets are the right jets of this descent.

Equations

• NavierStokes.GlobalSlowProfiles.xProfile f w = ↑f (√(2 * w.1), w.2)

theorem NavierStokes.GlobalSlowProfiles.xProfile_radius {S : Set ℝ} (f : EvenProfile S) {R : ℝ} (hR : 0 ≤ R) (eta : ℝ) : xProfile f (R ^ 2 / 2, eta) = ↑f (R, eta)

theorem NavierStokes.GlobalSlowProfiles.xProfile_contDiffAt {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : ContDiffAt ℝ (↑⊤) (xProfile f) w

theorem NavierStokes.GlobalSlowProfiles.partialX_hasDerivAt {f : Field} {w : ℝ × ℝ} (hf : DifferentiableAt ℝ f w) : HasDerivAt (fun (X : ℝ) => f (X, w.2)) (SimilarityProfile.partialX f w) w.1

theorem NavierStokes.GlobalSlowProfiles.partialEta_hasDerivAt {f : Field} {w : ℝ × ℝ} (hf : DifferentiableAt ℝ f w) : HasDerivAt (fun (eta : ℝ) => f (w.1, eta)) (SimilarityProfile.partialEta f w) w.2

theorem NavierStokes.GlobalSlowProfiles.xProfile_partialEta {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : SimilarityProfile.partialEta (xProfile f) w = xProfile (etaDerivative hS f) w

theorem NavierStokes.GlobalSlowProfiles.xProfile_partialX {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : SimilarityProfile.partialX (xProfile f) w = xProfile (xDerivative hS f) w

theorem NavierStokes.GlobalSlowProfiles.xProfile_partialX_germ {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : SimilarityProfile.partialX (xProfile f) =ᶠ[nhds w] xProfile (xDerivative hS f)

theorem NavierStokes.GlobalSlowProfiles.xProfile_partialXX {S : Set ℝ} (hS : IsOpen S) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : SimilarityProfile.partialX (SimilarityProfile.partialX (xProfile f)) w = xProfile (xDerivative hS (xDerivative hS f)) w

@[simp]

theorem NavierStokes.GlobalSlowProfiles.xProfile_add {S : Set ℝ} (f g : EvenProfile S) (w : ℝ × ℝ) : xProfile (f + g) w = xProfile f w + xProfile g w

@[simp]

theorem NavierStokes.GlobalSlowProfiles.xProfile_sub {S : Set ℝ} (f g : EvenProfile S) (w : ℝ × ℝ) : xProfile (f - g) w = xProfile f w - xProfile g w

@[simp]

theorem NavierStokes.GlobalSlowProfiles.xProfile_mul {S : Set ℝ} (f g : EvenProfile S) (w : ℝ × ℝ) : xProfile (f * g) w = xProfile f w * xProfile g w

@[simp]

theorem NavierStokes.GlobalSlowProfiles.xProfile_constant (S : Set ℝ) (c : ℝ) (w : ℝ × ℝ) : xProfile (boundConstant S c) w = c

theorem NavierStokes.GlobalSlowProfiles.xProfile_radiusSquared (S : Set ℝ) {w : ℝ × ℝ} (hX : 0 ≤ w.1) : xProfile (radiusSquared S) w = w.1

theorem NavierStokes.GlobalSlowProfiles.xProfile_timeOp {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : xProfile (timeOp d b f) w = SimilarityProfile.T h b (xProfile f) w

theorem NavierStokes.GlobalSlowProfiles.xProfile_axialOp {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : xProfile (axialOp d b f) w = SimilarityProfile.Z h b (xProfile f) w

theorem NavierStokes.GlobalSlowProfiles.xProfile_axialOp_germ {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : xProfile (axialOp d b f) =ᶠ[nhds w] SimilarityProfile.Z h b (xProfile f)

theorem NavierStokes.GlobalSlowProfiles.xProfile_axialOp2 {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (f : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : xProfile (axialOp2 d b f) w = AxisSourceRegularity.Z2 h b (xProfile f) w

theorem NavierStokes.GlobalSlowProfiles.xProfile_previousOmegaDivX {S : Set ℝ} {h : ℝ} (d : Domain S h) (u beta : ℕ → EvenProfile S) (n : ℕ) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : xProfile (previousOmegaDivX d u beta n) w = AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => xProfile (u j)) (fun (j : ℕ) => xProfile (beta j)) n w

theorem NavierStokes.GlobalSlowProfiles.cutoffLift_xProfile {rho : ℝ} {U : Set ℂ} {S : Set ℝ} (hrho : 0 < rho) (hU : IsOpen U) (hS : IsOpen S) (hSU : ∀ eta ∈ S, ↑eta ∈ U) {inner stop : ℝ} (his : inner < stop) (hsrho : stop < rho ^ 2) (f : SlowRecursion.AxisFunction rho U) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (hi : w.1 ≤ inner) : xProfile (cutoffLift hrho hU hS hSU his hsrho f) w = SlowRecursion.profile f w

structure NavierStokes.GlobalSlowProfiles.Localization {S : Set ℝ} {h C rho : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} (s : Scheme S h C) (A : SlowRecursion.LocalHierarchy rho U h C base) (inner : ℝ) : Prop

A transparent interface supplied by the common cutoff constructor.

• radius_pos : 0 < rho
• parameter_open : IsOpen U
• parameter_embedding (eta : ℝ) : eta ∈ S → ↑eta ∈ U
• inner_pos : 0 < inner
• inner_radius : inner < rho ^ 2
• inner_patch : inner < s.a ^ 2 / 2
• axial_seed (n : ℕ) (w : ℝ × ℝ) : 0 ≤ w.1 → w.1 ≤ inner → xProfile (s.seedAxial n) w = SlowRecursion.profile (A.coefficients n 1) w
• phi_seed (n : ℕ) (w : ℝ × ℝ) : 0 ≤ w.1 → w.1 ≤ inner → xProfile (s.seedPhi n) w = SlowRecursion.profile (A.coefficients n 0) w

theorem NavierStokes.GlobalSlowProfiles.localizationFromHierarchy {rho : ℝ} {U : Set ℂ} {S : Set ℝ} {h C lam inner stop a b B : ℝ} {base : Fin 5 → SimilarityProfile.InnerProfile} (A : SlowRecursion.LocalHierarchy rho U h C base) (hrho : 0 < rho) (hU : IsOpen U) (d : Domain S h) (hSU : ∀ eta ∈ S, ↑eta ∈ U) (hC : C ≠ 0) (hlam : 0 < lam) (hi : 0 < inner) (his : inner < stop) (hsrho : stop < rho ^ 2) (hsa : stop < a ^ 2 / 2) (ha : 0 < a) (hab : a < b) (hbB : b ≤ B) (B0 : BaseData S C lam a b B) : Localization (schemeFromHierarchy A hrho hU d hSU hC hlam his hsrho hsa ha hab hbB B0) A inner

theorem NavierStokes.GlobalSlowProfiles.actual_previousOmega_congr_germ (h : ℝ) {u beta u' beta' : ℕ → Field} (n : ℕ) {w : ℝ × ℝ} (hu : ∀ j < n, u j =ᶠ[nhds w] u' j) (hb : ∀ j < n, beta j =ᶠ[nhds w] beta' j) : AxisSourceRegularity.previousOmegaDivX h u beta n w = AxisSourceRegularity.previousOmegaDivX h u' beta' n w

structure NavierStokes.GlobalSlowProfiles.BaseAgreement {S : Set ℝ} {h C rho : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} (s : Scheme S h C) (A : SlowRecursion.LocalHierarchy rho U h C base) (inner : ℝ) : Prop

Agreement of the finite order-zero input with the same local hierarchy. These are identities on an inner region, not positive-order hypotheses.

• phi (w : ℝ × ℝ) : 0 ≤ w.1 → w.1 < inner → w.2 ∈ S → xProfile s.base.phi w = SlowRecursion.profile (A.coefficients 0 0) w
• axial (w : ℝ × ℝ) : 0 ≤ w.1 → w.1 < inner → w.2 ∈ S → xProfile s.base.axial w = SlowRecursion.profile (A.coefficients 0 1) w
• beta (w : ℝ × ℝ) : 0 ≤ w.1 → w.1 < inner → w.2 ∈ S → xProfile s.base.beta w = SlowRecursion.profile (A.coefficients 0 4) w

theorem NavierStokes.GlobalSlowProfiles.profiles_x_inner_axial {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (hi : w.1 ≤ inner) : xProfile (profiles s n).axial w = SlowRecursion.profile (A.coefficients n 1) w

theorem NavierStokes.GlobalSlowProfiles.profiles_x_inner_phi {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (hi : w.1 ≤ inner) : xProfile (profiles s n).phi w = SlowRecursion.profile (A.coefficients n 0) w

theorem NavierStokes.GlobalSlowProfiles.local_profile_smoothAt {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (n : ℕ) (i : Fin 5) {w : ℝ × ℝ} (hX : 0 < w.1) (hi : w.1 < rho ^ 2) (heta : w.2 ∈ S) : ContDiffAt ℝ (↑⊤) (SlowRecursion.profile (A.coefficients n i)) w

theorem NavierStokes.GlobalSlowProfiles.massHistory_of_composition {S : Set ℝ} (u : EvenProfile S) (g : Field) {R eta : ℝ} (hR : 0 ≤ R) (hg : ContinuousOn (fun (X : ℝ) => g (X, eta)) (Set.Icc 0 (R ^ 2 / 2))) (hu : ∀ r ∈ Set.Icc 0 R, ↑u (r, eta) = g (r ^ 2 / 2, eta)) : PositiveOrderMoments.massHistory ↑u (R, eta) = ProfileHistories.primitive g (R ^ 2 / 2, eta)

An actual substitution in the mass integral, with no axis differentiability assumption on the squared-radius function.

theorem NavierStokes.GlobalSlowProfiles.local_mass {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : 0 ≤ R) (hi : R ^ 2 / 2 ≤ inner) (heta : eta ∈ S) : PositiveOrderMoments.massHistory ↑(profiles s n).axial (R, eta) = R ^ 2 / 2 * (SlowRecursion.profile (A.coefficients n 1) (R ^ 2 / 2, eta) + SlowRecursion.profile (A.coefficients n 2) (R ^ 2 / 2, eta))

theorem NavierStokes.GlobalSlowProfiles.local_parameterMass {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : 0 < R) (hi : R ^ 2 / 2 ≤ inner) (heta : eta ∈ S) : PositiveOrderMoments.parameterMassHistory ↑(profiles s n).axial (R, eta) = R ^ 2 / 2 * (SimilarityProfile.partialEta (SlowRecursion.profile (A.coefficients n 1)) (R ^ 2 / 2, eta) + SimilarityProfile.partialEta (SlowRecursion.profile (A.coefficients n 2)) (R ^ 2 / 2, eta))

theorem NavierStokes.GlobalSlowProfiles.profiles_radial_inner_beta_pos {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : 0 < R) (hi : R ^ 2 / 2 ≤ inner) (heta : eta ∈ S) : ↑(profiles s n).beta (R, eta) = SlowRecursion.profile (A.coefficients n 4) (R ^ 2 / 2, eta)

noncomputable def NavierStokes.GlobalSlowProfiles.localExtension {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (n : ℕ) (i : Fin 5) : EvenProfile S

Local extension, constructed using cutoffLift.

Equations

• NavierStokes.GlobalSlowProfiles.localExtension L n i = NavierStokes.GlobalSlowProfiles.cutoffLift ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (A.coefficients n i)

theorem NavierStokes.GlobalSlowProfiles.localExtension_xProfile {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (n : ℕ) (i : Fin 5) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (hi : w.1 ≤ inner) : xProfile (localExtension L n i) w = SlowRecursion.profile (A.coefficients n i) w

theorem NavierStokes.GlobalSlowProfiles.localExtension_radial {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (n : ℕ) (i : Fin 5) {R eta : ℝ} (hR : 0 ≤ R) (hi : R ^ 2 / 2 ≤ inner) : ↑(localExtension L n i) (R, eta) = SlowRecursion.profile (A.coefficients n i) (R ^ 2 / 2, eta)

theorem NavierStokes.GlobalSlowProfiles.localExtension_germ {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (n : ℕ) (i : Fin 5) {w : ℝ × ℝ} (hX : 0 < w.1) (hi : w.1 < inner) : xProfile (localExtension L n i) =ᶠ[nhds w] SlowRecursion.profile (A.coefficients n i)

theorem NavierStokes.GlobalSlowProfiles.localExtension_axis {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) {n : ℕ} (hn : 0 < n) (i : Fin 5) {eta : ℝ} (heta : eta ∈ S) : ↑(localExtension L n i) (0, eta) = 0

theorem NavierStokes.GlobalSlowProfiles.profiles_radial_inner_beta_axis {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) {n : ℕ} (hn : 0 < n) {eta : ℝ} (heta : eta ∈ S) : ↑(profiles s n).beta (0, eta) = ↑(localExtension L n 4) (0, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_x_inner_beta {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (hi : w.1 ≤ inner) (heta : w.2 ∈ S) : xProfile (profiles s n).beta w = SlowRecursion.profile (A.coefficients n 4) w

theorem NavierStokes.GlobalSlowProfiles.profiles_x_phi_germ {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) (n : ℕ) {w : ℝ × ℝ} (hX : 0 < w.1) (hi : w.1 < inner) (heta : w.2 ∈ S) : xProfile (profiles s n).phi =ᶠ[nhds w] SlowRecursion.profile (A.coefficients n 0)

theorem NavierStokes.GlobalSlowProfiles.profiles_x_axial_germ {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) (n : ℕ) {w : ℝ × ℝ} (hX : 0 < w.1) (hi : w.1 < inner) (heta : w.2 ∈ S) : xProfile (profiles s n).axial =ᶠ[nhds w] SlowRecursion.profile (A.coefficients n 1)

theorem NavierStokes.GlobalSlowProfiles.profiles_x_beta_germ {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) (n : ℕ) {w : ℝ × ℝ} (hX : 0 < w.1) (hi : w.1 < inner) (heta : w.2 ∈ S) : xProfile (profiles s n).beta =ᶠ[nhds w] SlowRecursion.profile (A.coefficients n 4)

theorem NavierStokes.GlobalSlowProfiles.profiles_source_local {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) (n : ℕ) {w : ℝ × ℝ} (hX : 0 < w.1) (hi : w.1 < inner) (heta : w.2 ∈ S) : xProfile (previousOmegaDivX ⋯ (fun (j : ℕ) => (profiles s j).axial) (fun (j : ℕ) => (profiles s j).beta) n) w = AxisSourceRegularity.previousOmegaDivX h (fun (j : ℕ) => SlowRecursion.profile (A.coefficients j 1)) (fun (j : ℕ) => SlowRecursion.profile (A.coefficients j 4)) n w

theorem NavierStokes.GlobalSlowProfiles.profiles_pressureSource_local {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : 0 < R) (hi : R ^ 2 / 2 < inner) (heta : eta ∈ S) : ↑(pressureSource C (fun (j : ℕ) => (profiles s j).phi) (previousOmegaDivX ⋯ (fun (j : ℕ) => (profiles s j).axial) (fun (j : ℕ) => (profiles s j).beta) n) n) (R, eta) = SimilarityProfile.partialX (SlowRecursion.profile (A.coefficients n 3)) (R ^ 2 / 2, eta)

theorem NavierStokes.GlobalSlowProfiles.localExtension_radial_derivative {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (n : ℕ) (i : Fin 5) {R eta : ℝ} (hR : 0 < R) (hi : R ^ 2 / 2 < inner) (heta : eta ∈ S) : ProfileHistories.radialPartial ↑(localExtension L n i) (R, eta) = R * SimilarityProfile.partialX (SlowRecursion.profile (A.coefficients n i)) (R ^ 2 / 2, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_radial_inner_pressure {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (hR : 0 ≤ R) (hi : R ^ 2 / 2 < inner) (heta : eta ∈ S) : ↑(profiles s n).pressure (R, eta) = SlowRecursion.profile (A.coefficients n 3) (R ^ 2 / 2, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_x_inner_pressure {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (hi : w.1 < inner) (heta : w.2 ∈ S) : xProfile (profiles s n).pressure w = SlowRecursion.profile (A.coefficients n 3) w

theorem NavierStokes.GlobalSlowProfiles.pressureFromSource_hasDerivAt {S : Set ℝ} (hS : IsOpen S) (q : EvenProfile S) {R eta : ℝ} (heta : eta ∈ S) : HasDerivAt (fun (r : ℝ) => ↑(pressureFromSource hS q) (r, eta)) (R * ↑q (R, eta)) R

theorem NavierStokes.GlobalSlowProfiles.profiles_x_pressure_derivative {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : SimilarityProfile.partialX (xProfile (profiles s n).pressure) w = xProfile (pressureSource C (fun (j : ℕ) => (profiles s j).phi) (previousOmegaDivX ⋯ (fun (j : ℕ) => (profiles s j).axial) (fun (j : ℕ) => (profiles s j).beta) n) n) w

theorem NavierStokes.GlobalSlowProfiles.radialZ_eq_axialOp {S : Set ℝ} {h : ℝ} (d : Domain S h) (b : ℝ) (u : EvenProfile S) {w : ℝ × ℝ} (heta : w.2 ∈ S) : PositiveOrderMoments.radialZ h b (↑u) w = ↑(axialOp d b u) w

theorem NavierStokes.GlobalSlowProfiles.betaFromU_x_divergence {S : Set ℝ} {h : ℝ} (d : Domain S h) (lam : ℝ) (u : EvenProfile S) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : SimilarityProfile.partialX (AxisSourceRegularity.axisFactor (xProfile (betaFromU d lam u))) w + SimilarityProfile.Z h (-PositiveAxisSystem.a h + lam) (xProfile u) w = 0

noncomputable def NavierStokes.GlobalSlowProfiles.asSlowProfiles {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) : SlowExpansionResidual.SlowProfiles

As slow profiles, constructed using SlowResidualMatching.ofBeta.

Equations

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

theorem NavierStokes.GlobalSlowProfiles.profiles_divergenceCoefficient {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : SlowExpansionResidual.divergenceCoefficient h (asSlowProfiles s) n w = 0

Exact global divergence at every positive order.

theorem NavierStokes.GlobalSlowProfiles.profiles_pressureCoefficient {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hX : 0 < w.1) (heta : w.2 ∈ S) : SlowExpansionResidual.pressureCoefficient h C (asSlowProfiles s) n w = 0

Exact global pressure row, with the actual preceding radial residual.

noncomputable def NavierStokes.GlobalSlowProfiles.component {S : Set ℝ} (q : Coefficient S) (i : Fin 4) : EvenProfile S

Component, given by ![q.phi, q.axial, q.beta, q.pressure] i.

Equations

• NavierStokes.GlobalSlowProfiles.component q i = ![q.phi, q.axial, q.beta, q.pressure] i

noncomputable def NavierStokes.GlobalSlowProfiles.localIndex (i : Fin 4) : Fin 5

Local index, given by ![0, 1, 4, 3] i.

Equations

• NavierStokes.GlobalSlowProfiles.localIndex i = ![0, 1, 4, 3] i

theorem NavierStokes.GlobalSlowProfiles.profiles_inner_eq {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) (i : Fin 4) {w : ℝ × ℝ} (hX : 0 ≤ w.1) (hi : w.1 < inner) (heta : w.2 ∈ S) : xProfile (component (profiles s n) i) w = SlowRecursion.profile (A.coefficients n (localIndex i)) w

Every repaired coefficient agrees with the original local hierarchy on one common inner domain, including the axis.

theorem NavierStokes.GlobalSlowProfiles.profiles_axis_zero {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) (i : Fin 4) {eta : ℝ} (heta : eta ∈ S) : ↑(component (profiles s n) i) (0, eta) = 0

theorem NavierStokes.GlobalSlowProfiles.profiles_inner_smooth {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) (i : Fin 4) : ContDiffOn ℝ (↑⊤) (xProfile (component (profiles s n) i)) (Set.Ico 0 inner ×ˢ S)

Joint smoothness up to the axis is inherited from actual local equality.

theorem NavierStokes.GlobalSlowProfiles.profiles_axis_mixed_jets {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) (i : Fin 4) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : iteratedFDerivWithin ℝ m (xProfile (component (profiles s n) i)) (Set.Ici 0 ×ˢ Set.univ) (0, eta) = iteratedFDerivWithin ℝ m (SlowRecursion.profile (A.coefficients n (localIndex i))) (Set.Ici 0 ×ˢ Set.univ) (0, eta)

All actual mixed right jets, not just the zero-order values, agree at the axis. The derivative is taken relative to the closed half-plane.

theorem NavierStokes.GlobalSlowProfiles.profiles_axis_right_jets {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) (i : Fin 4) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : iteratedDerivWithin m (fun (X : ℝ) => xProfile (component (profiles s n) i) (X, eta)) (Set.Ici 0) 0 = iteratedDerivWithin m (fun (X : ℝ) => SlowRecursion.profile (A.coefficients n (localIndex i)) (X, eta)) (Set.Ici 0) 0

theorem NavierStokes.GlobalSlowProfiles.profiles_inner_tangential {S : Set ℝ} {h C rho inner : ℝ} {U : Set ℂ} {base : Fin 5 → SimilarityProfile.InnerProfile} {s : Scheme S h C} {A : SlowRecursion.LocalHierarchy rho U h C base} (L : Localization s A inner) (B0 : BaseAgreement s A inner) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (hX : 0 < w.1) (hi : w.1 < inner) (heta : w.2 ∈ S) : SlowExpansionResidual.angularCoefficient h (asSlowProfiles s) n w = 0 ∧ SlowExpansionResidual.axialCoefficient h (asSlowProfiles s) n w = 0

Germ locality transfers the two solved tangential equations. No agreement outside the fixed inner region is required.

theorem NavierStokes.GlobalSlowProfiles.compactSupport_of_even_exterior {S : Set ℝ} (f : EvenProfile S) {B : ℝ} (hf : Exterior B S ↑f) {eta : ℝ} (heta : eta ∈ S) : HasCompactSupport fun (R : ℝ) => ↑f (R, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_compactSupport {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) (i : Fin 4) {eta : ℝ} (heta : eta ∈ S) : HasCompactSupport fun (R : ℝ) => ↑(component (profiles s n) i) (R, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_angular_compactSupport {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {eta : ℝ} (heta : eta ∈ S) : HasCompactSupport fun (R : ℝ) => angularField C (profiles s n).phi (R, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_flux_compactSupport {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) (n : ℕ) {eta : ℝ} (heta : eta ∈ S) : HasCompactSupport fun (R : ℝ) => R ^ 2 / 2 * ↑(profiles s n).beta (R, eta)

theorem NavierStokes.GlobalSlowProfiles.profiles_pressureHistory {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) : ↑(profiles s n).pressure = PositiveOrderMoments.pressureHistory n (fun (j : ℕ) => angularField C (profiles s j).phi) fun (w : ℝ × ℝ) => w.1 ^ 2 / 2 * ↑(previousOmegaDivX ⋯ (fun (j : ℕ) => (profiles s j).axial) (fun (j : ℕ) => (profiles s j).beta) n) w

The radial pressure is literally the forward primitive used by the moment module, with the actual preceding radial source retained.

theorem NavierStokes.GlobalSlowProfiles.profiles_fluxHistory {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {w : ℝ × ℝ} (heta : w.2 ∈ S) : w.1 ^ 2 / 2 * ↑(profiles s n).beta w = PositiveOrderMoments.fluxHistory h (AxisSourceRegularity.slowOrder h n) (↑(profiles s n).axial) w

theorem NavierStokes.GlobalSlowProfiles.profiles_radial_divergence {S : Set ℝ} {h C : ℝ} (s : Scheme S h C) {n : ℕ} (hn : 0 < n) {R eta : ℝ} (heta : eta ∈ S) : HasDerivAt (fun (r : ℝ) => r ^ 2 / 2 * ↑(profiles s n).beta (r, eta)) (-R * PositiveOrderMoments.radialZ h (-PositiveAxisSystem.a h + AxisSourceRegularity.slowOrder h n) ↑(profiles s n).axial (R, eta)) R

The genuine radial divergence identity holds at every signed radius, including the axis, on the original open parameter domain.