Positive slow-order tangential stress support

The moments are actual positive-radius integrals. All radial and parameter operators use the actual Frechet derivatives. Compact stress support is a consequence of the repaired moments and the differential equations.

Actual five-row repair at positive slow order

Only the order-n entries of the histories are changed. Endpoint extraction proves that all five actual moment increments are linear, including pressure with the known previous-order radial residual retained.

@[reducible, inline]

abbrev NavierStokes.PositiveOrderMoments.Profile : Type

Profile: an abbreviation for ℝ → ℝ.

Equations

• NavierStokes.PositiveOrderMoments.Profile = (ℝ → ℝ)

@[reducible, inline]

abbrev NavierStokes.PositiveOrderMoments.History : Type

History: an abbreviation for ℕ → Profile.

Equations

• NavierStokes.PositiveOrderMoments.History = (ℕ → NavierStokes.PositiveOrderMoments.Profile)

@[reducible, inline]

abbrev NavierStokes.PositiveOrderMoments.Debt : Type

Debt: an abbreviation for Fin 5 → ℝ.

Equations

• NavierStokes.PositiveOrderMoments.Debt = (Fin 5 → ℝ)

noncomputable def NavierStokes.PositiveOrderMoments.cauchy (n : ℕ) (u v : History) (R : ℝ) : ℝ

Cauchy, given by PositiveAxisSystem.convolution n (fun i j => u i R * v j R).

Equations

• NavierStokes.PositiveOrderMoments.cauchy n u v R = NavierStokes.PositiveAxisSystem.convolution n fun (i j : ℕ) => u i R * v j R

noncomputable def NavierStokes.PositiveOrderMoments.increment (u : History) (n : ℕ) (du : Profile) : History

Increment, given by Function.update u n (fun R => u n R + du R).

Equations

• NavierStokes.PositiveOrderMoments.increment u n du = Function.update u n fun (R : ℝ) => u n R + du R

theorem NavierStokes.PositiveOrderMoments.increment_lower (u : History) {n j : ℕ} (du : Profile) (hj : j < n) : increment u n du j = u j

theorem NavierStokes.PositiveOrderMoments.cauchy_increment {n : ℕ} (hn : 0 < n) (u v : History) (du dv : Profile) (R : ℝ) : cauchy n (increment u n du) (increment v n dv) R = cauchy n u v R + u 0 R * dv R + du R * v 0 R

noncomputable def NavierStokes.PositiveOrderMoments.pressureGradient (n : ℕ) (e : History) (omega : Profile) (R : ℝ) : ℝ

The actual R-pressure equation: Ω is the fixed order-(n-1) source.

Equations

• NavierStokes.PositiveOrderMoments.pressureGradient n e omega R = (NavierStokes.PositiveOrderMoments.cauchy n e e R - omega R) / R

noncomputable def NavierStokes.PositiveOrderMoments.phiHistory (C : ℝ) (e : History) : History

The angular similarity coefficient in (22), reconstructed from E.

Equations

• NavierStokes.PositiveOrderMoments.phiHistory C e j R = C * e j R / R

theorem NavierStokes.PositiveOrderMoments.cauchy_phiHistory (n : ℕ) (C : ℝ) (e : History) (R : ℝ) : cauchy n (phiHistory C e) (phiHistory C e) R = (C / R) ^ 2 * cauchy n e e R

theorem NavierStokes.PositiveOrderMoments.pressureGradient_eq_X_equation (n : ℕ) (C : ℝ) (e : History) (omega : Profile) {R : ℝ} (hC : C ≠ 0) (hR : R ≠ 0) : pressureGradient n e omega R = R * ((C ^ 2)⁻¹ * cauchy n (phiHistory C e) (phiHistory C e) R - omega R / (2 * (R ^ 2 / 2)))

Multiplying the actual X-pressure equation by dX/dR=R gives the pressure row used here. In particular the preceding Ω term is retained exactly.

noncomputable def NavierStokes.PositiveOrderMoments.rowDensity (n : ℕ) (u e : History) (omega : Profile) (R : ℝ) : Debt

The five densities in (23), in the order printed there.

Equations

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

noncomputable def NavierStokes.PositiveOrderMoments.positiveIntegral (f : Profile) : ℝ

Positive integral, given by ∫ R in Ioi (0 : ℝ), f R.

Equations

• NavierStokes.PositiveOrderMoments.positiveIntegral f = ∫ (R : ℝ) in Set.Ioi 0, f R

noncomputable def NavierStokes.PositiveOrderMoments.moments (n : ℕ) (u e : History) (omega : Profile) : Debt

Moments, defined pointwise by positiveIntegral (fun R => rowDensity n u e omega R i).

Equations

• NavierStokes.PositiveOrderMoments.moments n u e omega i = NavierStokes.PositiveOrderMoments.positiveIntegral fun (R : ℝ) => NavierStokes.PositiveOrderMoments.rowDensity n u e omega R i

noncomputable def NavierStokes.PositiveOrderMoments.linearDensity (u₀ e₀ du de : Profile) (R : ℝ) : Debt

Linear density, given by ![R * du R, R ^ 2 * de R, 2 * e₀ R * de R / R, R ^ 2 * (u₀ R * de R + du R * e₀ R), 2 * R * u₀ R * du R - R * e₀ R * de R].

Equations

• NavierStokes.PositiveOrderMoments.linearDensity u₀ e₀ du de R = ![R * du R, R ^ 2 * de R, 2 * e₀ R * de R / R, R ^ 2 * (u₀ R * de R + du R * e₀ R), 2 * R * u₀ R * du R - R * e₀ R * de R]

theorem NavierStokes.PositiveOrderMoments.rowDensity_increment {n : ℕ} (hn : 0 < n) (u e : History) (omega du de : Profile) (R : ℝ) : rowDensity n (increment u n du) (increment e n de) omega R = rowDensity n u e omega R + linearDensity (u 0) (e 0) du de R

There are no quadratic current-order terms when n>0.

noncomputable def NavierStokes.PositiveOrderMoments.weightedDensity (lam A : ℝ) (du de : Profile) (R : ℝ) : Debt

Weighted density, given by ![R * du R, R ^ 2 * de R, (2 * A) * (R ^ (-2 - 2 * lam) * de R), A * (R ^ (1 - 2 * lam) * du R), (-A) * (R ^ (-2 * lam) * de R)].

Equations

• NavierStokes.PositiveOrderMoments.weightedDensity lam A du de R = ![R * du R, R ^ 2 * de R, 2 * A * (R ^ (-2 - 2 * lam) * de R), A * (R ^ (1 - 2 * lam) * du R), -A * (R ^ (-2 * lam) * de R)]

theorem NavierStokes.PositiveOrderMoments.linearDensity_on_patch (lam A a b : ℝ) (ha : 0 < a) (u₀ e₀ du de : Profile) (hu : ∀ R ∈ Set.Ioo a b, u₀ R = 0) (he : ∀ R ∈ Set.Ioo a b, e₀ R = FiveRowRank.background lam A R) (hdu : Function.support du ⊆ Set.Ioo a b) (hde : Function.support de ⊆ Set.Ioo a b) (R : ℝ) : linearDensity u₀ e₀ du de R = weightedDensity lam A du de R

noncomputable def NavierStokes.PositiveOrderMoments.axialDebt (A : ℝ) (d : Debt) : Fin 2 → ℝ

Axial target moments: physical mass and angular transport.

Equations

• NavierStokes.PositiveOrderMoments.axialDebt A d = ![d 0, d 3 / A]

noncomputable def NavierStokes.PositiveOrderMoments.angularDebt (A : ℝ) (d : Debt) : Fin 3 → ℝ

Angular target moments: angular mass, pressure, and axial transport.

Equations

• NavierStokes.PositiveOrderMoments.angularDebt A d = ![d 1, d 2 / (2 * A), -d 4 / A]

noncomputable def NavierStokes.PositiveOrderMoments.repairU (lam A a b : ℝ) (d : Debt) : Profile

Repair U, given by LocalizedMomentRepair.repair (FiveRowRank.axialPowers lam) (FiveRowRank.cellLower a b) (FiveRowRank.cellUpper a b) (axialDebt A d).

Equations

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

noncomputable def NavierStokes.PositiveOrderMoments.repairE (lam A a b : ℝ) (d : Debt) : Profile

Repair E, constructed using LocalizedMomentRepair.repair.

Equations

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

theorem NavierStokes.PositiveOrderMoments.repairU_contDiff (lam A a b : ℝ) (d : Debt) : ContDiff ℝ (↑⊤) (repairU lam A a b d)

theorem NavierStokes.PositiveOrderMoments.repairE_contDiff (lam A a b : ℝ) (d : Debt) : ContDiff ℝ (↑⊤) (repairE lam A a b d)

theorem NavierStokes.PositiveOrderMoments.repairU_tsupport (lam A a b : ℝ) (d : Debt) (hab : a < b) : tsupport (repairU lam A a b d) ⊆ Set.Ioo a b

theorem NavierStokes.PositiveOrderMoments.repairE_tsupport (lam A a b : ℝ) (d : Debt) (hab : a < b) : tsupport (repairE lam A a b d) ⊆ Set.Ioo a b

theorem NavierStokes.PositiveOrderMoments.repairU_moment (lam A a b : ℝ) (d : Debt) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (i : Fin 2) : ∫ (R : ℝ), R ^ FiveRowRank.axialPowers lam i * repairU lam A a b d R = axialDebt A d i

theorem NavierStokes.PositiveOrderMoments.repairE_moment (lam A a b : ℝ) (d : Debt) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (i : Fin 3) : ∫ (R : ℝ), R ^ FiveRowRank.angularPowers lam i * repairE lam A a b d R = angularDebt A d i

theorem NavierStokes.PositiveOrderMoments.positiveIntegral_eq_integral {f : Profile} (hf : ∀ R ≤ 0, f R = 0) : positiveIntegral f = ∫ (R : ℝ), f R

theorem NavierStokes.PositiveOrderMoments.weighted_moments_exact (lam A a b : ℝ) (d : Debt) (hlam : 0 < lam) (hA : A ≠ 0) (ha : 0 < a) (hab : a < b) (i : Fin 5) : (positiveIntegral fun (R : ℝ) => weightedDensity lam A (repairU lam A a b d) (repairE lam A a b d) R i) = d i

theorem NavierStokes.PositiveOrderMoments.repairU_power_integrable (lam A a b p : ℝ) (d : Debt) (ha : 0 < a) (hab : a < b) : MeasureTheory.Integrable (fun (R : ℝ) => R ^ p * repairU lam A a b d R) MeasureTheory.volume

theorem NavierStokes.PositiveOrderMoments.repairE_power_integrable (lam A a b p : ℝ) (d : Debt) (ha : 0 < a) (hab : a < b) : MeasureTheory.Integrable (fun (R : ℝ) => R ^ p * repairE lam A a b d R) MeasureTheory.volume

theorem NavierStokes.PositiveOrderMoments.weightedDensity_integrable (lam A a b : ℝ) (d : Debt) (ha : 0 < a) (hab : a < b) (i : Fin 5) : MeasureTheory.Integrable (fun (R : ℝ) => weightedDensity lam A (repairU lam A a b d) (repairE lam A a b d) R i) MeasureTheory.volume

theorem NavierStokes.PositiveOrderMoments.moments_repair (lam A a b : ℝ) (d : Debt) {n : ℕ} (hn : 0 < n) (u e : History) (omega : Profile) (hlam : 0 < lam) (hA : A ≠ 0) (ha : 0 < a) (hab : a < b) (hu : ∀ R ∈ Set.Ioo a b, u 0 R = 0) (he : ∀ R ∈ Set.Ioo a b, e 0 R = FiveRowRank.background lam A R) (hint : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (R : ℝ) => rowDensity n u e omega R i) (Set.Ioi 0) MeasureTheory.volume) : moments n (increment u n (repairU lam A a b d)) (increment e n (repairE lam A a b d)) omega = moments n u e omega + d

Exact affine change of all five actual positive-radius integrals.

theorem NavierStokes.PositiveOrderMoments.moments_repair_target (lam A a b : ℝ) (target : Debt) {n : ℕ} (hn : 0 < n) (u e : History) (omega : Profile) (hlam : 0 < lam) (hA : A ≠ 0) (ha : 0 < a) (hab : a < b) (hu : ∀ R ∈ Set.Ioo a b, u 0 R = 0) (he : ∀ R ∈ Set.Ioo a b, e 0 R = FiveRowRank.background lam A R) (hint : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (R : ℝ) => rowDensity n u e omega R i) (Set.Ioi 0) MeasureTheory.volume) : moments n (increment u n (repairU lam A a b (target - moments n u e omega))) (increment e n (repairE lam A a b (target - moments n u e omega))) omega = target

Arbitrary moment debts are removed, with no size restriction.

theorem NavierStokes.PositiveOrderMoments.exists_smooth_exact_repair (lam A a b : ℝ) (target : Debt) {n : ℕ} (hn : 0 < n) (u e : History) (omega : Profile) (hlam : 0 < lam) (hA : A ≠ 0) (ha : 0 < a) (hab : a < b) (hu : ∀ R ∈ Set.Ioo a b, u 0 R = 0) (he : ∀ R ∈ Set.Ioo a b, e 0 R = FiveRowRank.background lam A R) (hint : ∀ (i : Fin 5), MeasureTheory.IntegrableOn (fun (R : ℝ) => rowDensity n u e omega R i) (Set.Ioi 0) MeasureTheory.volume) : ∃ (du : Profile) (de : Profile), ContDiff ℝ (↑⊤) du ∧ ContDiff ℝ (↑⊤) de ∧ HasCompactSupport du ∧ HasCompactSupport de ∧ tsupport du ⊆ Set.Ioo a b ∧ tsupport de ⊆ Set.Ioo a b ∧ moments n (increment u n du) (increment e n de) omega = target

theorem NavierStokes.PositiveOrderMoments.repairU_zero_before (lam A a b : ℝ) (d : Debt) (hab : a < b) {R : ℝ} (hR : R ≤ a) : repairU lam A a b d R = 0

theorem NavierStokes.PositiveOrderMoments.repairE_zero_before (lam A a b : ℝ) (d : Debt) (hab : a < b) {R : ℝ} (hR : R ≤ a) : repairE lam A a b d R = 0

theorem NavierStokes.PositiveOrderMoments.repairU_zero_outside (lam A a b : ℝ) (d : Debt) (hab : a < b) {R : ℝ} (hR : R ∉ Set.Ioo a b) : repairU lam A a b d R = 0

theorem NavierStokes.PositiveOrderMoments.repairE_zero_outside (lam A a b : ℝ) (d : Debt) (hab : a < b) {R : ℝ} (hR : R ∉ Set.Ioo a b) : repairE lam A a b d R = 0

theorem NavierStokes.PositiveOrderMoments.rowDensity_repair_eq_outside (lam A a b : ℝ) (d : Debt) {n : ℕ} (hn : 0 < n) (u e : History) (omega : Profile) (hab : a < b) {R : ℝ} (hR : R ∉ Set.Ioo a b) : rowDensity n (increment u n (repairU lam A a b d)) (increment e n (repairE lam A a b d)) omega R = rowDensity n u e omega R

theorem NavierStokes.PositiveOrderMoments.rowDensity_repair_exterior (lam A a b : ℝ) (d : Debt) {n : ℕ} (hn : 0 < n) (u e : History) (omega : Profile) (hab : a < b) {B R : ℝ} (hs : ∀ (t : ℝ), B ≤ t → rowDensity n u e omega t = 0) (hR : max B b ≤ R) : rowDensity n (increment u n (repairU lam A a b d)) (increment e n (repairE lam A a b d)) omega R = 0

theorem NavierStokes.PositiveOrderMoments.increment_eq_of_zero (u : History) (n j : ℕ) (du : Profile) (R : ℝ) (hd : du R = 0) : increment u n du j R = u j R

theorem NavierStokes.PositiveOrderMoments.pressureGradient_increment_of_zero {n : ℕ} (hn : 0 < n) (e : History) (omega de : Profile) (R : ℝ) (hd : de R = 0) : pressureGradient n (increment e n de) omega R = pressureGradient n e omega R

theorem NavierStokes.PositiveOrderMoments.pressure_primitive_repair_before_patch (lam A a b : ℝ) (d : Debt) {n : ℕ} (hn : 0 < n) (e : History) (omega : Profile) (hab : a < b) {R : ℝ} (hR0 : 0 ≤ R) (hRa : R ≤ a) : ∫ (t : ℝ) in 0..R, pressureGradient n (increment e n (repairE lam A a b d)) omega t = ∫ (t : ℝ) in 0..R, pressureGradient n e omega t

Recomputing pressure does not disturb the already solved inner region: the complete new pressure source agrees with the old one up to the patch.

theorem NavierStokes.PositiveOrderMoments.mass_primitive_repair_before_patch (lam A a b : ℝ) (d : Debt) (n : ℕ) (u : History) (hab : a < b) {R : ℝ} (hR0 : 0 ≤ R) (hRa : R ≤ a) : ∫ (t : ℝ) in 0..R, t * increment u n (repairU lam A a b d) n t = ∫ (t : ℝ) in 0..R, t * u n t

The physical mass primitive is likewise preserved before the patch.

theorem NavierStokes.PositiveOrderMoments.axialDebt_contDiffOn {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {S : Set P} {A : P → ℝ} {d : P → Debt} (hA : ContDiffOn ℝ (↑⊤) A S) (hd : ContDiffOn ℝ (↑⊤) d S) (hAn : ∀ p ∈ S, A p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (p : P) => axialDebt (A p) (d p)) S

theorem NavierStokes.PositiveOrderMoments.angularDebt_contDiffOn {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] {S : Set P} {A : P → ℝ} {d : P → Debt} (hA : ContDiffOn ℝ (↑⊤) A S) (hd : ContDiffOn ℝ (↑⊤) d S) (hAn : ∀ p ∈ S, A p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (p : P) => angularDebt (A p) (d p)) S

theorem NavierStokes.PositiveOrderMoments.repairU_joint_contDiffOn {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (lam a b : ℝ) {S : Set P} {A : P → ℝ} {d : P → Debt} (hA : ContDiffOn ℝ (↑⊤) A S) (hd : ContDiffOn ℝ (↑⊤) d S) (hAn : ∀ p ∈ S, A p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (z : P × ℝ) => repairU lam (A z.1) a b (d z.1) z.2) (S ×ˢ Set.univ)

theorem NavierStokes.PositiveOrderMoments.repairE_joint_contDiffOn {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (lam a b : ℝ) {S : Set P} {A : P → ℝ} {d : P → Debt} (hA : ContDiffOn ℝ (↑⊤) A S) (hd : ContDiffOn ℝ (↑⊤) d S) (hAn : ∀ p ∈ S, A p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (z : P × ℝ) => repairE lam (A z.1) a b (d z.1) z.2) (S ×ˢ Set.univ)

@[reducible, inline]

abbrev NavierStokes.PositiveOrderMoments.JointProfile : Type

Joint profile: an abbreviation for ℝ × ℝ → ℝ.

Equations

• NavierStokes.PositiveOrderMoments.JointProfile = (ℝ × ℝ → ℝ)

@[reducible, inline]

abbrev NavierStokes.PositiveOrderMoments.JointHistory : Type

Joint history: an abbreviation for ℕ → JointProfile.

Equations

• NavierStokes.PositiveOrderMoments.JointHistory = (ℕ → NavierStokes.PositiveOrderMoments.JointProfile)

noncomputable def NavierStokes.PositiveOrderMoments.slice (f : JointHistory) (eta : ℝ) : History

Slice, defined pointwise by f j (R, eta).

Equations

• NavierStokes.PositiveOrderMoments.slice f eta j R = f j (R, eta)

noncomputable def NavierStokes.PositiveOrderMoments.jointIncrement (u : JointHistory) (n : ℕ) (du : JointProfile) : JointHistory

Joint increment, given by Function.update u n (fun w => u n w + du w).

Equations

• NavierStokes.PositiveOrderMoments.jointIncrement u n du = Function.update u n fun (w : ℝ × ℝ) => u n w + du w

theorem NavierStokes.PositiveOrderMoments.slice_jointIncrement (u : JointHistory) (n : ℕ) (du : JointProfile) (eta : ℝ) : slice (jointIncrement u n du) eta = increment (slice u eta) n fun (R : ℝ) => du (R, eta)

theorem NavierStokes.PositiveOrderMoments.jointIncrement_lower (u : JointHistory) {n j : ℕ} (du : JointProfile) (hj : j < n) : jointIncrement u n du j = u j

theorem NavierStokes.PositiveOrderMoments.jointIncrement_contDiffOn {S : Set (ℝ × ℝ)} {n : ℕ} {u : JointHistory} {du : JointProfile} (hu : ∀ j ≤ n, ContDiffOn ℝ (↑⊤) (u j) S) (hdu : ContDiffOn ℝ (↑⊤) du S) (j : ℕ) (hj : j ≤ n) : ContDiffOn ℝ (↑⊤) (jointIncrement u n du j) S

noncomputable def NavierStokes.PositiveOrderMoments.globalDomain : ProfileHistories.RadialDomain

Global domain, bundling carrier, isOpen, scale_mem.

Equations

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

theorem NavierStokes.PositiveOrderMoments.primitive_contDiff {F : JointProfile} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (ProfileHistories.primitive F)

theorem NavierStokes.PositiveOrderMoments.primitive_hasDerivAt {F : JointProfile} (hF : ContDiff ℝ (↑⊤) F) (w : ℝ × ℝ) : HasDerivAt (fun (R : ℝ) => ProfileHistories.primitive F (R, w.2)) (F w) w.1

theorem NavierStokes.PositiveOrderMoments.positiveIntegral_eq_primitive {f : Profile} {B R : ℝ} (hB : 0 ≤ B) (hR : B ≤ R) (hf : ∀ (t : ℝ), B ≤ t → f t = 0) : positiveIntegral f = ∫ (t : ℝ) in 0..R, f t

Compact positive-radius sources identify the actual primitive with the positive-radius total integral, without imposing values at negative radii.

noncomputable def NavierStokes.PositiveOrderMoments.jointPressureGradient (n : ℕ) (e : JointHistory) (omega : JointProfile) (w : ℝ × ℝ) : ℝ

Joint pressure gradient, given by pressureGradient n (slice e w.2) (fun R => omega (R, w.2)) w.1.

Equations

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

noncomputable def NavierStokes.PositiveOrderMoments.pressureHistory (n : ℕ) (e : JointHistory) (omega : JointProfile) : JointProfile

Pressure is recomputed from its actual radial gradient, with zero axis datum.

Equations

• NavierStokes.PositiveOrderMoments.pressureHistory n e omega = NavierStokes.ProfileHistories.primitive (NavierStokes.PositiveOrderMoments.jointPressureGradient n e omega)

theorem NavierStokes.PositiveOrderMoments.pressureHistory_axis (n : ℕ) (e : JointHistory) (omega : JointProfile) (eta : ℝ) : pressureHistory n e omega (0, eta) = 0

theorem NavierStokes.PositiveOrderMoments.pressureHistory_contDiff {n : ℕ} {e : JointHistory} {omega : JointProfile} (hq : ContDiff ℝ (↑⊤) (jointPressureGradient n e omega)) : ContDiff ℝ (↑⊤) (pressureHistory n e omega)

theorem NavierStokes.PositiveOrderMoments.pressureHistory_hasDerivAt {n : ℕ} {e : JointHistory} {omega : JointProfile} (hq : ContDiff ℝ (↑⊤) (jointPressureGradient n e omega)) (w : ℝ × ℝ) : HasDerivAt (fun (R : ℝ) => pressureHistory n e omega (R, w.2)) (pressureGradient n (slice e w.2) (fun (R : ℝ) => omega (R, w.2)) w.1) w.1

theorem NavierStokes.PositiveOrderMoments.pressureHistory_exterior {n : ℕ} {e : JointHistory} {omega : JointProfile} {B : ℝ} (hB : 0 ≤ B) (hs : ∀ (eta R : ℝ), B ≤ R → jointPressureGradient n e omega (R, eta) = 0) (hm : ∀ (eta : ℝ), (positiveIntegral fun (R : ℝ) => jointPressureGradient n e omega (R, eta)) = 0) {R eta : ℝ} (hR : B ≤ R) : pressureHistory n e omega (R, eta) = 0

theorem NavierStokes.PositiveOrderMoments.pressureHistory_exterior_of_moments {n : ℕ} {u e : JointHistory} {omega : JointProfile} {B : ℝ} (hB : 0 ≤ B) (hs : ∀ (eta R : ℝ), B ≤ R → jointPressureGradient n e omega (R, eta) = 0) (hm : ∀ (eta : ℝ), (moments n (slice u eta) (slice e eta) fun (R : ℝ) => omega (R, eta)) = 0) {R eta : ℝ} (hR : B ≤ R) : pressureHistory n e omega (R, eta) = 0

The third repaired row is the actual pressure-exterior condition.

noncomputable def NavierStokes.PositiveOrderMoments.weightedAxial (u : JointProfile) (w : ℝ × ℝ) : ℝ

Weighted axial, given by w.1 * u w.

Equations

• NavierStokes.PositiveOrderMoments.weightedAxial u w = w.1 * u w

noncomputable def NavierStokes.PositiveOrderMoments.massHistory (u : JointProfile) : JointProfile

Mass history, given by ProfileHistories.primitive (weightedAxial u).

Equations

• NavierStokes.PositiveOrderMoments.massHistory u = NavierStokes.ProfileHistories.primitive (NavierStokes.PositiveOrderMoments.weightedAxial u)

noncomputable def NavierStokes.PositiveOrderMoments.parameterMassHistory (u : JointProfile) : JointProfile

Parameter mass history, given by ProfileHistories.primitive (ProfileHistories.parameterPartial (weightedAxial u)).

Equations

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

noncomputable def NavierStokes.PositiveOrderMoments.fluxHistory (h lam : ℝ) (u : JointProfile) (w : ℝ × ℝ) : ℝ

The R-coordinate version of (21), with both histories given by actual integrals.

Equations

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

noncomputable def NavierStokes.PositiveOrderMoments.radialZ (h power : ℝ) (u : JointProfile) (w : ℝ × ℝ) : ℝ

Radial Z as an element of ℝ.

Equations

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

theorem NavierStokes.PositiveOrderMoments.weightedAxial_contDiff {u : JointProfile} (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (weightedAxial u)

theorem NavierStokes.PositiveOrderMoments.parameterPartial_contDiff {F : JointProfile} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (ProfileHistories.parameterPartial F)

theorem NavierStokes.PositiveOrderMoments.weightedAxial_parameterPartial {u : JointProfile} (hu : ContDiff ℝ (↑⊤) u) (w : ℝ × ℝ) : ProfileHistories.parameterPartial (weightedAxial u) w = w.1 * ProfileHistories.parameterPartial u w

theorem NavierStokes.PositiveOrderMoments.massHistory_parameterPartial {u : JointProfile} (hu : ContDiff ℝ (↑⊤) u) (w : ℝ × ℝ) : ProfileHistories.parameterPartial (massHistory u) w = parameterMassHistory u w

theorem NavierStokes.PositiveOrderMoments.fluxHistory_hasDerivAt (h lam : ℝ) {u : JointProfile} (hu : ContDiff ℝ (↑⊤) u) (w : ℝ × ℝ) : HasDerivAt (fun (R : ℝ) => fluxHistory h lam u (R, w.2)) (-w.1 * radialZ h (-PositiveAxisSystem.a h + lam) u w) w.1

Genuine radial differentiation of the integral formula gives incompressibility.

theorem NavierStokes.PositiveOrderMoments.fluxHistory_exterior (h lam : ℝ) {u : JointProfile} (hu : ContDiff ℝ (↑⊤) u) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ (eta R : ℝ), B ≤ R → u (R, eta) = 0) (hm : ∀ (eta : ℝ), (positiveIntegral fun (R : ℝ) => R * u (R, eta)) = 0) {R eta : ℝ} (hR : B ≤ R) : fluxHistory h lam u (R, eta) = 0

The first repaired row is exactly the mass condition making the recomputed radial flux vanish outside the source. Parameter differentiation is justified by the actual smooth history theorem.

theorem NavierStokes.PositiveOrderMoments.fluxHistory_exterior_of_moments (h lam : ℝ) {n : ℕ} {u e : JointHistory} {omega : JointProfile} (hu : ContDiff ℝ (↑⊤) (u n)) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ (eta R : ℝ), B ≤ R → u n (R, eta) = 0) (hm : ∀ (eta : ℝ), (moments n (slice u eta) (slice e eta) fun (R : ℝ) => omega (R, eta)) = 0) {R eta : ℝ} (hR : B ≤ R) : fluxHistory h lam (u n) (R, eta) = 0

The first row of the actual five-moment system gives the required mass condition for the recomputed divergence flux.

theorem NavierStokes.PositiveOrderMoments.pressure_weighted_identity {q : JointProfile} (hq : ContDiff ℝ (↑⊤) q) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ (eta R : ℝ), B ≤ R → q (R, eta) = 0) (hm : ∀ (eta : ℝ), (positiveIntegral fun (R : ℝ) => q (R, eta)) = 0) (eta : ℝ) : (positiveIntegral fun (R : ℝ) => R * ProfileHistories.primitive q (R, eta)) = -(1 / 2) * positiveIntegral fun (R : ℝ) => R ^ 2 * q (R, eta)

The pressure integration-by-parts identity underlying the fifth row is proved for the actual pressure primitive, including its exterior boundary.

noncomputable def NavierStokes.PositiveOrderMoments.parameterDomain (S : Set ℝ) (hS : IsOpen S) : ProfileHistories.RadialDomain

Open parameter domains retain all radial histories while keeping the original parameter domain; no extension across its endpoints is needed.

Equations

• NavierStokes.PositiveOrderMoments.parameterDomain S hS = { carrier := Set.univ ×ˢ S, isOpen := ⋯, scale_mem := ⋯ }

theorem NavierStokes.PositiveOrderMoments.pressureHistory_contDiffOn {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {e : JointHistory} {omega : JointProfile} (hq : ContDiffOn ℝ (↑⊤) (jointPressureGradient n e omega) (Set.univ ×ˢ S)) : ContDiffOn ℝ (↑⊤) (pressureHistory n e omega) (Set.univ ×ˢ S)

The pressure reconstruction needs smoothness only on the working parameter domain.

theorem NavierStokes.PositiveOrderMoments.pressureHistory_hasDerivAt_on {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {e : JointHistory} {omega : JointProfile} (hq : ContDiffOn ℝ (↑⊤) (jointPressureGradient n e omega) (Set.univ ×ˢ S)) {R eta : ℝ} (heta : eta ∈ S) : HasDerivAt (fun (r : ℝ) => pressureHistory n e omega (r, eta)) (jointPressureGradient n e omega (R, eta)) R

theorem NavierStokes.PositiveOrderMoments.pressureHistory_exterior_on {S : Set ℝ} {n : ℕ} {u e : JointHistory} {omega : JointProfile} {B : ℝ} (hB : 0 ≤ B) (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → jointPressureGradient n e omega (R, eta) = 0) (hm : ∀ eta ∈ S, (moments n (slice u eta) (slice e eta) fun (R : ℝ) => omega (R, eta)) = 0) {R eta : ℝ} (hR : B ≤ R) (heta : eta ∈ S) : pressureHistory n e omega (R, eta) = 0

theorem NavierStokes.PositiveOrderMoments.weightedAxial_parameterPartial_on {S : Set ℝ} (hS : IsOpen S) {u : JointProfile} (hu : ContDiffOn ℝ (↑⊤) u (Set.univ ×ˢ S)) {w : ℝ × ℝ} (hw : w.2 ∈ S) : ProfileHistories.parameterPartial (weightedAxial u) w = w.1 * ProfileHistories.parameterPartial u w

theorem NavierStokes.PositiveOrderMoments.massHistory_parameterPartial_on {S : Set ℝ} (hS : IsOpen S) {u : JointProfile} (hu : ContDiffOn ℝ (↑⊤) u (Set.univ ×ˢ S)) {w : ℝ × ℝ} (hw : w.2 ∈ S) : ProfileHistories.parameterPartial (massHistory u) w = parameterMassHistory u w

theorem NavierStokes.PositiveOrderMoments.fluxHistory_contDiffOn (h lam : ℝ) {S : Set ℝ} (hS : IsOpen S) {u : JointProfile} (hu : ContDiffOn ℝ (↑⊤) u (Set.univ ×ˢ S)) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) : ContDiffOn ℝ (↑⊤) (fluxHistory h lam u) (Set.univ ×ˢ S)

theorem NavierStokes.PositiveOrderMoments.fluxHistory_hasDerivAt_on (h lam : ℝ) {S : Set ℝ} (hS : IsOpen S) {u : JointProfile} (hu : ContDiffOn ℝ (↑⊤) u (Set.univ ×ˢ S)) {w : ℝ × ℝ} (hw : w.2 ∈ S) : HasDerivAt (fun (R : ℝ) => fluxHistory h lam u (R, w.2)) (-w.1 * radialZ h (-PositiveAxisSystem.a h + lam) u w) w.1

The actual radial divergence equation holds on an open parameter domain, without any smooth extension past that domain.

theorem NavierStokes.PositiveOrderMoments.fluxHistory_exterior_on (h lam : ℝ) {S : Set ℝ} (hS : IsOpen S) {u : JointProfile} (hu : ContDiffOn ℝ (↑⊤) u (Set.univ ×ˢ S)) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → u (R, eta) = 0) (hm : ∀ eta ∈ S, (positiveIntegral fun (R : ℝ) => R * u (R, eta)) = 0) {R eta : ℝ} (hR : B ≤ R) (heta : eta ∈ S) : fluxHistory h lam u (R, eta) = 0

theorem NavierStokes.PositiveOrderMoments.positiveIntegral_contDiffOn {S : Set ℝ} (hS : IsOpen S) {F : JointProfile} (hF : ContDiffOn ℝ (↑⊤) F (Set.univ ×ˢ S)) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → F (R, eta) = 0) : ContDiffOn ℝ (↑⊤) (fun (eta : ℝ) => positiveIntegral fun (R : ℝ) => F (R, eta)) S

Smoothness of the actual total moment follows from common compact radial support and the proved smooth history theorem.

noncomputable def NavierStokes.PositiveOrderMoments.jointRowDensity (n : ℕ) (u e : JointHistory) (omega : JointProfile) (w : ℝ × ℝ) : Debt

Joint row density, given by rowDensity n (slice u w.2) (slice e w.2) (fun R => omega (R, w.2)) w.1.

Equations

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

theorem NavierStokes.PositiveOrderMoments.cauchy_eq_zero_of_left (n : ℕ) (u v : History) (R : ℝ) (hu : ∀ j ≤ n, u j R = 0) : cauchy n u v R = 0

theorem NavierStokes.PositiveOrderMoments.cauchy_self_eq_zero_of_positive {n : ℕ} (hn : 0 < n) (e : History) (R : ℝ) (he : ∀ (j : ℕ), 0 < j → j ≤ n → e j R = 0) : cauchy n e e R = 0

theorem NavierStokes.PositiveOrderMoments.jointCauchy_contDiffOn {S : Set (ℝ × ℝ)} {n : ℕ} {u v : JointHistory} (hu : ∀ j ≤ n, ContDiffOn ℝ (↑⊤) (u j) S) (hv : ∀ j ≤ n, ContDiffOn ℝ (↑⊤) (v j) S) : ContDiffOn ℝ (↑⊤) (fun (w : ℝ × ℝ) => cauchy n (slice u w.2) (slice v w.2) w.1) S

theorem NavierStokes.PositiveOrderMoments.jointRowDensity_contDiffOn {S : Set (ℝ × ℝ)} {n : ℕ} {u e : JointHistory} {omega : JointProfile} (hu : ∀ j ≤ n, ContDiffOn ℝ (↑⊤) (u j) S) (he : ∀ j ≤ n, ContDiffOn ℝ (↑⊤) (e j) S) (hq : ContDiffOn ℝ (↑⊤) (jointPressureGradient n e omega) S) (i : Fin 5) : ContDiffOn ℝ (↑⊤) (fun (w : ℝ × ℝ) => jointRowDensity n u e omega w i) S

theorem NavierStokes.PositiveOrderMoments.jointRowDensity_exterior {n : ℕ} (hn : 0 < n) (u e : JointHistory) (omega : JointProfile) (w : ℝ × ℝ) (hu : ∀ j ≤ n, u j w = 0) (he : ∀ (j : ℕ), 0 < j → j ≤ n → e j w = 0) (hw : omega w = 0) : jointRowDensity n u e omega w = 0

The order-zero angular tail need not be compact: every summand of the positive-order self-convolution contains a strictly positive index.

theorem NavierStokes.PositiveOrderMoments.moments_contDiffOn {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {u e : JointHistory} {omega : JointProfile} (hd : ∀ (i : Fin 5), ContDiffOn ℝ (↑⊤) (fun (w : ℝ × ℝ) => jointRowDensity n u e omega w i) (Set.univ ×ˢ S)) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → jointRowDensity n u e omega (R, eta) = 0) : ContDiffOn ℝ (↑⊤) (fun (eta : ℝ) => moments n (slice u eta) (slice e eta) fun (R : ℝ) => omega (R, eta)) S

This statement derives smoothness of the five genuine integral debts; the density hypotheses can be checked componentwise from the known fields.

theorem NavierStokes.PositiveOrderMoments.moments_contDiffOn_of_histories {S : Set ℝ} (hS : IsOpen S) {n : ℕ} (hn : 0 < n) {u e : JointHistory} {omega : JointProfile} (hu : ∀ j ≤ n, ContDiffOn ℝ (↑⊤) (u j) (Set.univ ×ˢ S)) (he : ∀ j ≤ n, ContDiffOn ℝ (↑⊤) (e j) (Set.univ ×ˢ S)) (hq : ContDiffOn ℝ (↑⊤) (jointPressureGradient n e omega) (Set.univ ×ˢ S)) {B : ℝ} (hB : 0 ≤ B) (hU : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → ∀ j ≤ n, u j (R, eta) = 0) (hE : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → ∀ (j : ℕ), 0 < j → j ≤ n → e j (R, eta) = 0) (hOmega : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → omega (R, eta) = 0) : ContDiffOn ℝ (↑⊤) (fun (eta : ℝ) => moments n (slice u eta) (slice e eta) fun (R : ℝ) => omega (R, eta)) S

theorem NavierStokes.PositiveOrderMoments.exact_corrections_joint_contDiffOn (lam a b : ℝ) {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {u e : JointHistory} {omega : JointProfile} {A : ℝ → ℝ} (hA : ContDiffOn ℝ (↑⊤) A S) (hAn : ∀ eta ∈ S, A eta ≠ 0) (hd : ∀ (i : Fin 5), ContDiffOn ℝ (↑⊤) (fun (w : ℝ × ℝ) => jointRowDensity n u e omega w i) (Set.univ ×ˢ S)) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → jointRowDensity n u e omega (R, eta) = 0) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × ℝ) => (repairU lam (A z.1) a b (-moments n (slice u z.1) (slice e z.1) fun (R : ℝ) => omega (R, z.1)) z.2, repairE lam (A z.1) a b (-moments n (slice u z.1) (slice e z.1) fun (R : ℝ) => omega (R, z.1)) z.2)) (S ×ˢ Set.univ)

In particular, the exact zero-moment corrections vary smoothly with η when their debts are the actual profile integrals, not prescribed surrogates.

theorem NavierStokes.PositiveOrderMoments.positive_integrableOn_of_compact {f : Profile} {B : ℝ} (hf : ContinuousOn f (Set.Icc 0 B)) (hs : ∀ (R : ℝ), B ≤ R → f R = 0) : MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume

theorem NavierStokes.PositiveOrderMoments.jointRowDensity_integrableOn {S : Set ℝ} {n : ℕ} {u e : JointHistory} {omega : JointProfile} (hd : ∀ (i : Fin 5), ContinuousOn (fun (w : ℝ × ℝ) => jointRowDensity n u e omega w i) (Set.univ ×ˢ S)) {B : ℝ} (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → jointRowDensity n u e omega (R, eta) = 0) {eta : ℝ} (heta : eta ∈ S) (i : Fin 5) : MeasureTheory.IntegrableOn (fun (R : ℝ) => rowDensity n (slice u eta) (slice e eta) (fun (r : ℝ) => omega (r, eta)) R i) (Set.Ioi 0) MeasureTheory.volume

The integrability requirements of the repair theorem follow from the same common compact support and smoothness used for the parameter jets.

theorem NavierStokes.PositiveOrderMoments.exists_parameterized_exact_repair (lam a b : ℝ) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) {S : Set ℝ} (hS : IsOpen S) {n : ℕ} (hn : 0 < n) (u e : JointHistory) (omega : JointProfile) (A : ℝ → ℝ) (hA : ContDiffOn ℝ (↑⊤) A S) (hAn : ∀ eta ∈ S, A eta ≠ 0) (hU₀ : ∀ eta ∈ S, ∀ R ∈ Set.Ioo a b, u 0 (R, eta) = 0) (hE₀ : ∀ eta ∈ S, ∀ R ∈ Set.Ioo a b, e 0 (R, eta) = FiveRowRank.background lam (A eta) R) (hd : ∀ (i : Fin 5), ContDiffOn ℝ (↑⊤) (fun (w : ℝ × ℝ) => jointRowDensity n u e omega w i) (Set.univ ×ˢ S)) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → jointRowDensity n u e omega (R, eta) = 0) : ∃ (du : JointProfile) (de : JointProfile), ContDiffOn ℝ (↑⊤) du (Set.univ ×ˢ S) ∧ ContDiffOn ℝ (↑⊤) de (Set.univ ×ˢ S) ∧ (∀ (eta : ℝ), (tsupport fun (R : ℝ) => du (R, eta)) ⊆ Set.Ioo a b) ∧ (∀ (eta : ℝ), (tsupport fun (R : ℝ) => de (R, eta)) ⊆ Set.Ioo a b) ∧ ∀ eta ∈ S, (moments n (increment (slice u eta) n fun (R : ℝ) => du (R, eta)) (increment (slice e eta) n fun (R : ℝ) => de (R, eta)) fun (R : ℝ) => omega (R, eta)) = 0

A single explicit smooth family repairs all five rows on the parameter domain. Its debts are the actual finite-profile integrals; only order n is changed, and the known Ω term remains untouched.

@[reducible, inline]

abbrev NavierStokes.SlowStressSupport.Field : Type

Field: an abbreviation for ℝ × ℝ → ℝ.

Equations

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

@[reducible, inline]

abbrev NavierStokes.SlowStressSupport.History : Type

History: an abbreviation for ℕ → Field.

Equations

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

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

Dr, given by ProfileHistories.radialPartial.

Equations

• NavierStokes.SlowStressSupport.dr = NavierStokes.ProfileHistories.radialPartial

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

De, given by ProfileHistories.parameterPartial.

Equations

• NavierStokes.SlowStressSupport.de = NavierStokes.ProfileHistories.parameterPartial

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

noncomputable def NavierStokes.SlowStressSupport.exterior (B : ℝ) (S : Set ℝ) (f : Field) : Prop

Exterior, given by ∀ eta ∈ S, ∀ R, B ≤ R → f (R, eta) = 0.

Equations

• NavierStokes.SlowStressSupport.exterior B S f = ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → f (R, eta) = 0

noncomputable def NavierStokes.SlowStressSupport.weighted (m : ℕ) (f : Field) (w : ℝ × ℝ) : ℝ

Weighted, given by w.1 ^ m * f w.

Equations

• NavierStokes.SlowStressSupport.weighted m f w = w.1 ^ m * f w

noncomputable def NavierStokes.SlowStressSupport.moment (B : ℝ) (m : ℕ) (f : Field) (eta : ℝ) : ℝ

Moment, given by ∫ R in (0 : ℝ)..B, R ^ m * f (R, eta).

Equations

• NavierStokes.SlowStressSupport.moment B m f eta = ∫ (R : ℝ) in 0..B, R ^ m * f (R, eta)

noncomputable def NavierStokes.SlowStressSupport.timeOp (h b : ℝ) (f : Field) (w : ℝ × ℝ) : ℝ

Time op, given by (-b * f w + PositiveAxisSystem.dScale h * w.2 * de f w + w.1 / 2 * dr f w) / PositiveAxisSystem.ell h w.2.

Equations

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

noncomputable def NavierStokes.SlowStressSupport.axialOp (h b : ℝ) (f : Field) (w : ℝ × ℝ) : ℝ

Axial op, given by (2 * w.2 * b * f w + PositiveAxisSystem.edge w.2 * de f w - w.2 * w.1 * dr f w) / PositiveAxisSystem.ell h w.2.

Equations

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

noncomputable def NavierStokes.SlowStressSupport.axialOp2 (h b : ℝ) (f : Field) : Field

Axial Op2, given by axialOp h (b - PositiveAxisSystem.dScale h) (axialOp h b f).

Equations

• NavierStokes.SlowStressSupport.axialOp2 h b f = NavierStokes.SlowStressSupport.axialOp h (b - NavierStokes.PositiveAxisSystem.dScale h) (NavierStokes.SlowStressSupport.axialOp h b f)

theorem NavierStokes.SlowStressSupport.smooth_dr {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) : Smooth S (dr f)

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

theorem NavierStokes.SlowStressSupport.smooth_weighted {S : Set ℝ} {f : Field} (hf : Smooth S f) (m : ℕ) : Smooth S (weighted m f)

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

theorem NavierStokes.SlowStressSupport.radial_hasDerivAt {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {w : ℝ × ℝ} (hw : w.2 ∈ S) : HasDerivAt (fun (R : ℝ) => f (R, w.2)) (dr f w) w.1

theorem NavierStokes.SlowStressSupport.parameter_hasDerivAt {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {w : ℝ × ℝ} (hw : w.2 ∈ S) : HasDerivAt (fun (eta : ℝ) => f (w.1, eta)) (de f w) w.2

theorem NavierStokes.SlowStressSupport.dr_mul {S : Set ℝ} (hS : IsOpen S) {f g : Field} (hf : Smooth S f) (hg : Smooth S g) {w : ℝ × ℝ} (hw : w.2 ∈ S) : dr (fun (p : ProfileHistories.Point) => f p * g p) w = dr f w * g w + f w * dr g w

theorem NavierStokes.SlowStressSupport.de_mul {S : Set ℝ} (hS : IsOpen S) {f g : Field} (hf : Smooth S f) (hg : Smooth S g) {w : ℝ × ℝ} (hw : w.2 ∈ S) : de (fun (p : ProfileHistories.Point) => f p * g p) w = de f w * g w + f w * de g w

theorem NavierStokes.SlowStressSupport.de_weighted {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (m : ℕ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : de (weighted m f) w = w.1 ^ m * de f w

theorem NavierStokes.SlowStressSupport.exterior_partial {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {B : ℝ} (hs : exterior B S f) (v : ℝ × ℝ) : exterior B S fun (w : ℝ × ℝ) => (fderiv ℝ f w) v

theorem NavierStokes.SlowStressSupport.exterior_dr {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {B : ℝ} (hs : exterior B S f) : exterior B S (dr f)

theorem NavierStokes.SlowStressSupport.exterior_de {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {B : ℝ} (hs : exterior B S f) : exterior B S (de f)

theorem NavierStokes.SlowStressSupport.moment_eq_positive {S : Set ℝ} {f : Field} {B : ℝ} (hB : 0 ≤ B) (hs : exterior B S f) {eta : ℝ} (heta : eta ∈ S) (m : ℕ) : moment B m f eta = PositiveOrderMoments.positiveIntegral fun (R : ℝ) => R ^ m * f (R, eta)

theorem NavierStokes.SlowStressSupport.moment_hasDerivAt {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (B : ℝ) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : HasDerivAt (moment B m f) (moment B m (de f) eta) eta

theorem NavierStokes.SlowStressSupport.moment_de_zero {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (B : ℝ) (m : ℕ) (hm : ∀ eta ∈ S, moment B m f eta = 0) {eta : ℝ} (heta : eta ∈ S) : moment B m (de f) eta = 0

theorem NavierStokes.SlowStressSupport.moment_dr {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (B : ℝ) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : moment B (m + 1) (dr f) eta = B ^ (m + 1) * f (B, eta) - ↑(m + 1) * moment B m f eta

Radial integration by parts includes the genuine boundary at the axis.

theorem NavierStokes.SlowStressSupport.moment_add {S : Set ℝ} {f g : Field} (hf : Smooth S f) (hg : Smooth S g) (B : ℝ) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : moment B m (fun (w : ℝ × ℝ) => f w + g w) eta = moment B m f eta + moment B m g eta

theorem NavierStokes.SlowStressSupport.moment_sub {S : Set ℝ} {f g : Field} (hf : Smooth S f) (hg : Smooth S g) (B : ℝ) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : moment B m (fun (w : ℝ × ℝ) => f w - g w) eta = moment B m f eta - moment B m g eta

theorem NavierStokes.SlowStressSupport.smooth_axialOp {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (h b : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) : Smooth S (axialOp h b f)

theorem NavierStokes.SlowStressSupport.exterior_axialOp {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {B : ℝ} (hs : exterior B S f) (h b : ℝ) : exterior B S (axialOp h b f)

theorem NavierStokes.SlowStressSupport.axialOp_mul {S : Set ℝ} (hS : IsOpen S) {f g : Field} (hf : Smooth S f) (hg : Smooth S g) (h b c : ℝ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : axialOp h (b + c) (fun (p : ℝ × ℝ) => f p * g p) w = axialOp h b f w * g w + f w * axialOp h c g w

theorem NavierStokes.SlowStressSupport.moment_axialOp {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (h b B : ℝ) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : moment B m (axialOp h b f) eta = (2 * eta * b * moment B m f eta + PositiveAxisSystem.edge eta * moment B m (de f) eta - eta * (B ^ (m + 1) * f (B, eta) - ↑(m + 1) * moment B m f eta)) / PositiveAxisSystem.ell h eta

The weighted axial derivative is the actual derivative of the weighted moment, with its exact scaling coefficient and radial boundary term.

theorem NavierStokes.SlowStressSupport.moment_timeOp {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (h b B : ℝ) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : moment B m (timeOp h b f) eta = (-b * moment B m f eta + PositiveAxisSystem.dScale h * eta * moment B m (de f) eta + (B ^ (m + 1) * f (B, eta) - ↑(m + 1) * moment B m f eta) / 2) / PositiveAxisSystem.ell h eta

theorem NavierStokes.SlowStressSupport.moment_axialOp_zero {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (h b B : ℝ) (m : ℕ) (hb : ∀ eta ∈ S, f (B, eta) = 0) (hm : ∀ eta ∈ S, moment B m f eta = 0) {eta : ℝ} (heta : eta ∈ S) : moment B m (axialOp h b f) eta = 0

theorem NavierStokes.SlowStressSupport.moment_timeOp_zero {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (h b B : ℝ) (m : ℕ) (hb : ∀ eta ∈ S, f (B, eta) = 0) (hm : ∀ eta ∈ S, moment B m f eta = 0) {eta : ℝ} (heta : eta ∈ S) : moment B m (timeOp h b f) eta = 0

theorem NavierStokes.SlowStressSupport.moment_axialOp2_zero {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (h b B : ℝ) (m : ℕ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (hs : exterior B S f) (hm : ∀ eta ∈ S, moment B m f eta = 0) {eta : ℝ} (heta : eta ∈ S) : moment B m (axialOp2 h b f) eta = 0

noncomputable def NavierStokes.SlowStressSupport.orderExponent (h : ℝ) (n : ℕ) : ℝ

Order exponent, given by -PositiveAxisSystem.a h + SlowExpansionResidual.slowOrder h n.

Equations

• NavierStokes.SlowStressSupport.orderExponent h n = -NavierStokes.PositiveAxisSystem.a h + NavierStokes.SlowExpansionResidual.slowOrder h n

noncomputable def NavierStokes.SlowStressSupport.pressureExponent (h : ℝ) (n : ℕ) : ℝ

Pressure exponent, given by -2 * PositiveAxisSystem.a h + SlowExpansionResidual.slowOrder h n.

Equations

• NavierStokes.SlowStressSupport.pressureExponent h n = -2 * NavierStokes.PositiveAxisSystem.a h + NavierStokes.SlowExpansionResidual.slowOrder h n

theorem NavierStokes.SlowStressSupport.orderExponent_pair (h : ℝ) {i j n : ℕ} (hij : i + j = n) : orderExponent h i + orderExponent h j = pressureExponent h n

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

At a fixed convolution order the physical power is independent of the split.

noncomputable def NavierStokes.SlowStressSupport.conv (n : ℕ) (u v : History) (w : ℝ × ℝ) : ℝ

Conv, given by ∑ i ∈ Finset.range (n + 1), u i w * v (n - i) w.

Equations

• NavierStokes.SlowStressSupport.conv n u v w = ∑ i ∈ Finset.range (n + 1), u i w * v (n - i) w

theorem NavierStokes.SlowStressSupport.conv_eq_actual (n : ℕ) (u v : History) (w : ℝ × ℝ) : conv n u v w = PositiveOrderMoments.cauchy n (PositiveOrderMoments.slice u w.2) (PositiveOrderMoments.slice v w.2) w.1

theorem NavierStokes.SlowStressSupport.conv_eq_antidiagonal (n : ℕ) (u v : History) (w : ℝ × ℝ) : conv n u v w = SlowExpansionResidual.convolution (fun (i j : ℕ) => u i w * v j w) n

theorem NavierStokes.SlowStressSupport.smooth_conv {S : Set ℝ} {n : ℕ} {u v : History} (hu : ∀ j ≤ n, Smooth S (u j)) (hv : ∀ j ≤ n, Smooth S (v j)) : Smooth S (conv n u v)

theorem NavierStokes.SlowStressSupport.dr_conv {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {u v : History} (hu : ∀ j ≤ n, Smooth S (u j)) (hv : ∀ j ≤ n, Smooth S (v j)) {w : ℝ × ℝ} (hw : w.2 ∈ S) : dr (conv n u v) w = ∑ j ∈ Finset.range (n + 1), (dr (u j) w * v (n - j) w + u j w * dr (v (n - j)) w)

theorem NavierStokes.SlowStressSupport.de_conv {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {u v : History} (hu : ∀ j ≤ n, Smooth S (u j)) (hv : ∀ j ≤ n, Smooth S (v j)) {w : ℝ × ℝ} (hw : w.2 ∈ S) : de (conv n u v) w = ∑ j ∈ Finset.range (n + 1), (de (u j) w * v (n - j) w + u j w * de (v (n - j)) w)

theorem NavierStokes.SlowStressSupport.axialOp_conv {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {u v : History} (hu : ∀ j ≤ n, Smooth S (u j)) (hv : ∀ j ≤ n, Smooth S (v j)) (h : ℝ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : axialOp h (pressureExponent h n) (conv n u v) w = ∑ j ∈ Finset.range (n + 1), (axialOp h (orderExponent h j) (u j) w * v (n - j) w + u j w * axialOp h (orderExponent h (n - j)) (v (n - j)) w)

theorem NavierStokes.SlowStressSupport.dr_weighted {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (m : ℕ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : dr (weighted m f) w = ↑m * w.1 ^ (m - 1) * f w + w.1 ^ m * dr f w

theorem NavierStokes.SlowStressSupport.dr_sub {S : Set ℝ} (hS : IsOpen S) {f g : Field} (hf : Smooth S f) (hg : Smooth S g) {w : ℝ × ℝ} (hw : w.2 ∈ S) : dr (fun (p : ProfileHistories.Point) => f p - g p) w = dr f w - dr g w

theorem NavierStokes.SlowStressSupport.axialOp_add {S : Set ℝ} (hS : IsOpen S) {f g : Field} (hf : Smooth S f) (hg : Smooth S g) (h b : ℝ) {w : ℝ × ℝ} (hw : w.2 ∈ S) : axialOp h b (fun (p : ℝ × ℝ) => f p + g p) w = axialOp h b f w + axialOp h b g w

noncomputable def NavierStokes.SlowStressSupport.angularViscousFlux (e : Field) (w : ℝ × ℝ) : ℝ

Angular viscous flux, given by w.1 ^ 2 * dr e w - w.1 * e w.

Equations

• NavierStokes.SlowStressSupport.angularViscousFlux e w = w.1 ^ 2 * NavierStokes.SlowStressSupport.dr e w - w.1 * e w

noncomputable def NavierStokes.SlowStressSupport.axialViscousFlux (u : Field) (w : ℝ × ℝ) : ℝ

Axial viscous flux, given by w.1 * dr u w.

Equations

• NavierStokes.SlowStressSupport.axialViscousFlux u w = w.1 * NavierStokes.SlowStressSupport.dr u w

theorem NavierStokes.SlowStressSupport.dr_angularViscousFlux {S : Set ℝ} (hS : IsOpen S) {e : Field} (he : Smooth S e) {w : ℝ × ℝ} (hw : w.2 ∈ S) : dr (angularViscousFlux e) w = w.1 ^ 2 * dr (dr e) w + w.1 * dr e w - e w

theorem NavierStokes.SlowStressSupport.dr_axialViscousFlux {S : Set ℝ} (hS : IsOpen S) {u : Field} (hu : Smooth S u) {w : ℝ × ℝ} (hw : w.2 ∈ S) : dr (axialViscousFlux u) w = w.1 * dr (dr u) w + dr u w

noncomputable def NavierStokes.SlowStressSupport.angularWeighted (h : ℝ) (n : ℕ) (v u e : History) (w : ℝ × ℝ) : ℝ

Angular weighted, constructed using w.1.

Equations

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

noncomputable def NavierStokes.SlowStressSupport.axialWeighted (h : ℝ) (n : ℕ) (v u : History) (p : Field) (w : ℝ × ℝ) : ℝ

Axial weighted, constructed using w.1.

Equations

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

noncomputable def NavierStokes.SlowStressSupport.angularDensity (h : ℝ) (n : ℕ) (v u e : History) (w : ℝ × ℝ) : ℝ

Angular density, constructed using w.1.

Equations

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

noncomputable def NavierStokes.SlowStressSupport.axialDensity (h : ℝ) (n : ℕ) (v u : History) (p : Field) (w : ℝ × ℝ) : ℝ

Axial density, constructed using w.1.

Equations

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

theorem NavierStokes.SlowStressSupport.angularWeighted_eq_density {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u e : History} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (he : ∀ j ≤ n, Smooth S (e j)) (h : ℝ) {w : ℝ × ℝ} (hw : w.2 ∈ S) (hdiv : ∀ j ≤ n, dr (v j) w = -w.1 * axialOp h (orderExponent h j) (u j) w) : angularWeighted h n v u e w = angularDensity h n v u e w

Incompressibility converts the actual angular advection terms to conservative form; the convolution exponents are checked, not assumed.

theorem NavierStokes.SlowStressSupport.axialWeighted_eq_density {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u : History} {p : Field} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (hp : Smooth S p) (h : ℝ) {w : ℝ × ℝ} (hw : w.2 ∈ S) (hdiv : ∀ j ≤ n, dr (v j) w = -w.1 * axialOp h (orderExponent h j) (u j) w) : axialWeighted h n v u p w = axialDensity h n v u p w

theorem NavierStokes.SlowStressSupport.smooth_timeOp {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (h b : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) : Smooth S (timeOp h b f)

theorem NavierStokes.SlowStressSupport.smooth_axialOp2 {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (h b : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) : Smooth S (axialOp2 h b f)

theorem NavierStokes.SlowStressSupport.smooth_angularViscousFlux {S : Set ℝ} (hS : IsOpen S) {e : Field} (he : Smooth S e) : Smooth S (angularViscousFlux e)

theorem NavierStokes.SlowStressSupport.smooth_axialViscousFlux {S : Set ℝ} (hS : IsOpen S) {u : Field} (hu : Smooth S u) : Smooth S (axialViscousFlux u)

theorem NavierStokes.SlowStressSupport.moment_weighted_zero (B : ℝ) (m : ℕ) (f : Field) (eta : ℝ) : moment B 0 (weighted m f) eta = moment B m f eta

theorem NavierStokes.SlowStressSupport.moment_dr_boundary {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) (B : ℝ) {eta : ℝ} (heta : eta ∈ S) : moment B 0 (dr f) eta = f (B, eta) - f (0, eta)

theorem NavierStokes.SlowStressSupport.moment_five {S : Set ℝ} {f g k l p : Field} (hf : Smooth S f) (hg : Smooth S g) (hk : Smooth S k) (hl : Smooth S l) (hp : Smooth S p) (B : ℝ) (m : ℕ) {eta : ℝ} (heta : eta ∈ S) : moment B m (fun (w : ℝ × ℝ) => f w + g w + k w - l w - p w) eta = moment B m f eta + moment B m g eta + moment B m k eta - moment B m l eta - moment B m p eta

theorem NavierStokes.SlowStressSupport.exterior_conv_left {S : Set ℝ} {B : ℝ} {n : ℕ} {u v : History} (hu : ∀ j ≤ n, exterior B S (u j)) : exterior B S (conv n u v)

theorem NavierStokes.SlowStressSupport.angular_integral_balance {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u e : History} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (he : ∀ j ≤ n, Smooth S (e j)) (h B : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (hev : exterior B S (e n)) (hvv : ∀ j ≤ n, exterior B S (v j)) (hem : ∀ eta ∈ S, moment B 2 (e n) eta = 0) (hum : ∀ eta ∈ S, moment B 2 (conv n u e) eta = 0) (hug : exterior B S (conv n u e)) {eta : ℝ} (heta : eta ∈ S) : moment B 0 (angularDensity h n v u e) eta = -moment B 2 (axialOp2 h (orderExponent h (n - 1)) (e (n - 1))) eta

The integrated angular equation, with the previous axial-viscosity term still displayed. The other four terms cancel by the repaired moments and the actual radial boundary terms.

theorem NavierStokes.SlowStressSupport.axial_integral_balance {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u : History} {p : Field} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (hp : Smooth S p) (h B : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (huv : exterior B S (u n)) (hvv : ∀ j ≤ n, exterior B S (v j)) (haxis : ∀ eta ∈ S, conv n v u (0, eta) = 0) (hum : ∀ eta ∈ S, moment B 1 (u n) eta = 0) (hflux : ∀ eta ∈ S, moment B 1 (fun (w : ℝ × ℝ) => conv n u u w + p w) eta = 0) (hfluxB : ∀ eta ∈ S, conv n u u (B, eta) + p (B, eta) = 0) {eta : ℝ} (heta : eta ∈ S) : moment B 0 (axialDensity h n v u p) eta = -moment B 1 (axialOp2 h (orderExponent h (n - 1)) (u (n - 1))) eta

theorem NavierStokes.SlowStressSupport.axial_flux_moment_from_fifth {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {u : History} {p : Field} (hu : ∀ j ≤ n, Smooth S (u j)) (hp : Smooth S p) (B : ℝ) (hpB : ∀ eta ∈ S, p (B, eta) = 0) (hrow : ∀ eta ∈ S, moment B 1 (conv n u u) eta - 1 / 2 * moment B 2 (dr p) eta = 0) {eta : ℝ} (heta : eta ∈ S) : moment B 1 (fun (w : ℝ × ℝ) => conv n u u w + p w) eta = 0

Pressure integration by parts turns the fifth repaired row into the zero total axial momentum flux. The pressure derivative is an actual one.

theorem NavierStokes.SlowStressSupport.actual_row_integral_zero {n : ℕ} {u e : History} {omega : Field} {S : Set ℝ} {B : ℝ} (hB : 0 ≤ B) (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → PositiveOrderMoments.jointRowDensity n u e omega (R, eta) = 0) (hm : ∀ eta ∈ S, (PositiveOrderMoments.moments n (PositiveOrderMoments.slice u eta) (PositiveOrderMoments.slice e eta) fun (R : ℝ) => omega (R, eta)) = 0) {eta : ℝ} (heta : eta ∈ S) (i : Fin 5) : ∫ (R : ℝ) in 0..B, PositiveOrderMoments.jointRowDensity n u e omega (R, eta) i = 0

theorem NavierStokes.SlowStressSupport.repaired_moment_data {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {u e : History} {omega : Field} (hu : ∀ j ≤ n, Smooth S (u j)) (hq : Smooth S (PositiveOrderMoments.jointPressureGradient n e omega)) {B : ℝ} (hB : 0 ≤ B) (hs : ∀ eta ∈ S, ∀ (R : ℝ), B ≤ R → PositiveOrderMoments.jointRowDensity n u e omega (R, eta) = 0) (hm : ∀ eta ∈ S, (PositiveOrderMoments.moments n (PositiveOrderMoments.slice u eta) (PositiveOrderMoments.slice e eta) fun (R : ℝ) => omega (R, eta)) = 0) {eta : ℝ} (heta : eta ∈ S) : moment B 1 (u n) eta = 0 ∧ moment B 2 (e n) eta = 0 ∧ moment B 2 (conv n u e) eta = 0 ∧ moment B 1 (fun (w : ℝ × ℝ) => conv n u u w + PositiveOrderMoments.pressureHistory n e omega w) eta = 0

All moment hypotheses used in the integrated balances follow from the five repaired rows. Pressure is the actual forward primitive of its source.

theorem NavierStokes.SlowStressSupport.angular_integral_zero {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u e : History} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (he : ∀ j ≤ n, Smooth S (e j)) (h B : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (hev : exterior B S (e n)) (hvv : ∀ j ≤ n, exterior B S (v j)) (hem : ∀ eta ∈ S, moment B 2 (e n) eta = 0) (hum : ∀ eta ∈ S, moment B 2 (conv n u e) eta = 0) (hug : exterior B S (conv n u e)) (heprev : exterior B S (e (n - 1))) (hmprev : ∀ eta ∈ S, moment B 2 (e (n - 1)) eta = 0) {eta : ℝ} (heta : eta ∈ S) : moment B 0 (angularDensity h n v u e) eta = 0

theorem NavierStokes.SlowStressSupport.axial_integral_zero {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u : History} {p : Field} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (hp : Smooth S p) (h B : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (huv : exterior B S (u n)) (hvv : ∀ j ≤ n, exterior B S (v j)) (haxis : ∀ eta ∈ S, conv n v u (0, eta) = 0) (hum : ∀ eta ∈ S, moment B 1 (u n) eta = 0) (hflux : ∀ eta ∈ S, moment B 1 (fun (w : ℝ × ℝ) => conv n u u w + p w) eta = 0) (hfluxB : ∀ eta ∈ S, conv n u u (B, eta) + p (B, eta) = 0) (huprev : exterior B S (u (n - 1))) (hmprev : ∀ eta ∈ S, moment B 1 (u (n - 1)) eta = 0) {eta : ℝ} (heta : eta ∈ S) : moment B 0 (axialDensity h n v u p) eta = 0

noncomputable def NavierStokes.SlowStressSupport.stress (m : ℕ) (F : Field) (w : ℝ × ℝ) : ℝ

The negative weighted radial primitive. The definition is zero on nonpositive radii; vanishing of the source near the axis makes this smooth.

Equations

• NavierStokes.SlowStressSupport.stress m F w = if 0 < w.1 then -NavierStokes.ProfileHistories.primitive F w / w.1 ^ m else 0

theorem NavierStokes.SlowStressSupport.stress_of_pos (m : ℕ) (F : Field) {w : ℝ × ℝ} (hw : 0 < w.1) : stress m F w = -ProfileHistories.primitive F w / w.1 ^ m

theorem NavierStokes.SlowStressSupport.stress_inner (m : ℕ) {F : Field} {S : Set ℝ} {a : ℝ} (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, F (R, eta) = 0) {R eta : ℝ} (hR : R ≤ a) (heta : eta ∈ S) : stress m F (R, eta) = 0

theorem NavierStokes.SlowStressSupport.stress_exterior (m : ℕ) {F : Field} {S : Set ℝ} {B : ℝ} (hB : 0 ≤ B) (hs : exterior B S F) (hm : ∀ eta ∈ S, moment B 0 F eta = 0) {R eta : ℝ} (hR : B ≤ R) (heta : eta ∈ S) : stress m F (R, eta) = 0

theorem NavierStokes.SlowStressSupport.stress_smooth {S : Set ℝ} (hS : IsOpen S) {F : Field} (hF : Smooth S F) (m : ℕ) {a : ℝ} (ha : 0 < a) (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, F (R, eta) = 0) : Smooth S (stress m F)

theorem NavierStokes.SlowStressSupport.stress_weighted_hasDerivAt {S : Set ℝ} (hS : IsOpen S) {F : Field} (hF : Smooth S F) (m : ℕ) {R eta : ℝ} (hR : 0 < R) (heta : eta ∈ S) : HasDerivAt (fun (r : ℝ) => r ^ m * stress m F (r, eta)) (-F (R, eta)) R

The defining primitive has the exact negative weighted derivative.

theorem NavierStokes.SlowStressSupport.stress_radial_identity {S : Set ℝ} (hS : IsOpen S) {F : Field} (hF : Smooth S F) (m : ℕ) {a : ℝ} (ha : 0 < a) (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, F (R, eta) = 0) {w : ℝ × ℝ} (hR : 0 < w.1) (heta : w.2 ∈ S) : ↑m * w.1 ^ (m - 1) * stress m F w + w.1 ^ m * dr (stress m F) w = -F w

theorem NavierStokes.SlowStressSupport.stress_slice_support (m : ℕ) {F : Field} {S : Set ℝ} {a B : ℝ} (hB : 0 ≤ B) (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, F (R, eta) = 0) (hs : exterior B S F) (hm : ∀ eta ∈ S, moment B 0 F eta = 0) {eta : ℝ} (heta : eta ∈ S) : (Function.support fun (R : ℝ) => stress m F (R, eta)) ⊆ Set.Icc a B

noncomputable def NavierStokes.SlowStressSupport.radialSupport (S : Set ℝ) (a b : ℝ) (f : Field) : Prop

Radial support, given by ∀ eta ∈ S, ∀ R, R ∉ Icc a b → f (R, eta) = 0.

Equations

• NavierStokes.SlowStressSupport.radialSupport S a b f = ∀ eta ∈ S, ∀ R ∉ Set.Icc a b, f (R, eta) = 0

theorem NavierStokes.SlowStressSupport.support_eventually_zero {S : Set ℝ} (hS : IsOpen S) {a b : ℝ} {f : Field} (hs : radialSupport S a b f) {w : ℝ × ℝ} (hw : w.2 ∈ S) (hR : w.1 ∉ Set.Icc a b) : f =ᶠ[nhds w] fun (x : ℝ × ℝ) => 0

theorem NavierStokes.SlowStressSupport.jet_eq_zero_of_eventually {f : Field} {w : ℝ × ℝ} (hf : f =ᶠ[nhds w] fun (x : ℝ × ℝ) => 0) (k : ℕ) : iteratedFDeriv ℝ k f w = 0

theorem NavierStokes.SlowStressSupport.interior_quotient_smooth {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {a b l r : ℝ} (hs : radialSupport S a b f) (hab : Set.Icc a b ⊆ Set.Ioo l r) {zeta : ℝ → ℝ} (hz : ContDiffOn ℝ (↑⊤) zeta (Set.Ioo l r)) (hz0 : ∀ R ∈ Set.Ioo l r, zeta R ≠ 0) : Smooth S fun (w : ℝ × ℝ) => f w / zeta w.1

theorem NavierStokes.SlowStressSupport.interior_weighted_jets {S K : Set ℝ} (hS : IsOpen S) (hK : IsCompact K) (hKS : K ⊆ S) {f : Field} (hf : Smooth S f) {a b l r : ℝ} (hs : radialSupport S a b f) (hab : Set.Icc a b ⊆ Set.Ioo l r) {zeta : ℝ → ℝ} (hz : ContinuousOn zeta (Set.Ioo l r)) (hz0 : ∀ R ∈ Set.Ioo l r, 0 < zeta R) (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ R ∈ Set.Ioo l r, ∀ eta ∈ K, ‖iteratedFDeriv ℝ k f (R, eta)‖ ≤ C * zeta R

Every actual derivative tensor has a weighted bound because its support lies in one fixed compact subinterval of the positive-weight region. No stress norm bound is an input. The constant may depend on the derivative order.

theorem NavierStokes.SlowStressSupport.stress_radialSupport (m : ℕ) {F : Field} {S : Set ℝ} {a B : ℝ} (hB : 0 ≤ B) (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, F (R, eta) = 0) (hs : exterior B S F) (hm : ∀ eta ∈ S, moment B 0 F eta = 0) : radialSupport S a B (stress m F)

theorem NavierStokes.SlowStressSupport.stress_weighted_jets {S K : Set ℝ} (hS : IsOpen S) (hK : IsCompact K) (hKS : K ⊆ S) {F : Field} (hF : Smooth S F) (m : ℕ) {a B l r : ℝ} (ha : 0 < a) (hB : 0 ≤ B) (hab : Set.Icc a B ⊆ Set.Ioo l r) (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, F (R, eta) = 0) (hs : exterior B S F) (hm : ∀ eta ∈ S, moment B 0 F eta = 0) {zeta : ℝ → ℝ} (hz : ContDiffOn ℝ (↑⊤) zeta (Set.Ioo l r)) (hz0 : ∀ R ∈ Set.Ioo l r, 0 < zeta R) : (Smooth S fun (w : ℝ × ℝ) => stress m F w / zeta w.1) ∧ ∀ (k : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ R ∈ Set.Ioo l r, ∀ eta ∈ K, ‖iteratedFDeriv ℝ k (stress m F) (R, eta)‖ ≤ C * zeta R

A fixed interior support interval gives all weighted stress jets on every compact parameter subinterval, as well as a smooth normalized stress.

theorem NavierStokes.SlowStressSupport.smooth_angularDensity {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u e : History} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (he : ∀ j ≤ n, Smooth S (e j)) (h : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) : Smooth S (angularDensity h n v u e)

theorem NavierStokes.SlowStressSupport.smooth_axialDensity {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u : History} {p : Field} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (hp : Smooth S p) (h : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) : Smooth S (axialDensity h n v u p)

theorem NavierStokes.SlowStressSupport.exterior_weighted {S : Set ℝ} {B : ℝ} {f : Field} (hf : exterior B S f) (m : ℕ) : exterior B S (weighted m f)

theorem NavierStokes.SlowStressSupport.exterior_timeOp {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {B : ℝ} (hs : exterior B S f) (h b : ℝ) : exterior B S (timeOp h b f)

theorem NavierStokes.SlowStressSupport.exterior_axialOp2 {S : Set ℝ} (hS : IsOpen S) {f : Field} (hf : Smooth S f) {B : ℝ} (hs : exterior B S f) (h b : ℝ) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) : exterior B S (axialOp2 h b f)

theorem NavierStokes.SlowStressSupport.exterior_angularDensity {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u e : History} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (he : ∀ j ≤ n, Smooth S (e j)) (h B : ℝ) (hV : ∀ j ≤ n, exterior B S (v j)) (hU : ∀ j ≤ n, exterior B S (u j)) (hE : exterior B S (e n)) (hprev : exterior B S (axialOp2 h (orderExponent h (n - 1)) (e (n - 1)))) : exterior B S (angularDensity h n v u e)

theorem NavierStokes.SlowStressSupport.exterior_axialDensity {S : Set ℝ} (hS : IsOpen S) {n : ℕ} {v u : History} {p : Field} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (hp : Smooth S p) (h B : ℝ) (hV : ∀ j ≤ n, exterior B S (v j)) (hU : ∀ j ≤ n, exterior B S (u j)) (hP : exterior B S p) (hprev : exterior B S (axialOp2 h (orderExponent h (n - 1)) (u (n - 1)))) : exterior B S (axialDensity h n v u p)

noncomputable def NavierStokes.SlowStressSupport.angularStress (h : ℝ) (n : ℕ) (v u e : History) : Field

Angular stress, given by stress 2 (angularDensity h n v u e).

Equations

• NavierStokes.SlowStressSupport.angularStress h n v u e = NavierStokes.SlowStressSupport.stress 2 (NavierStokes.SlowStressSupport.angularDensity h n v u e)

noncomputable def NavierStokes.SlowStressSupport.axialStress (h : ℝ) (n : ℕ) (v u : History) (p : Field) : Field

Axial stress, given by stress 1 (axialDensity h n v u p).

Equations

• NavierStokes.SlowStressSupport.axialStress h n v u p = NavierStokes.SlowStressSupport.stress 1 (NavierStokes.SlowStressSupport.axialDensity h n v u p)

theorem NavierStokes.SlowStressSupport.angular_stress_support {S : Set ℝ} (hS : IsOpen S) {n : ℕ} (hn : 2 ≤ n) {v u e : History} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (he : ∀ j ≤ n, Smooth S (e j)) (h a B : ℝ) (ha : 0 < a) (hB : 0 ≤ B) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (hV : ∀ j ≤ n, exterior B S (v j)) (hU : ∀ j ≤ n, exterior B S (u j)) (hE : ∀ (j : ℕ), 0 < j → j ≤ n → exterior B S (e j)) (hem : ∀ eta ∈ S, moment B 2 (e n) eta = 0) (hum : ∀ eta ∈ S, moment B 2 (conv n u e) eta = 0) (hprev : ∀ eta ∈ S, moment B 2 (e (n - 1)) eta = 0) (hdiv : ∀ (w : ℝ × ℝ), w.2 ∈ S → ∀ j ≤ n, dr (v j) w = -w.1 * axialOp h (orderExponent h j) (u j) w) (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, angularWeighted h n v u e (R, eta) = 0) : Smooth S (angularStress h n v u e) ∧ radialSupport S a B (angularStress h n v u e) ∧ ∀ eta ∈ S, ∀ (R : ℝ), 0 < R → HasDerivAt (fun (r : ℝ) => r ^ 2 * angularStress h n v u e (r, eta)) (-angularWeighted h n v u e (R, eta)) R

For n≥2 all the angular hypotheses below are supplied by ordinary positive-order moments and compact positive-order profiles.

theorem NavierStokes.SlowStressSupport.axial_stress_support {S : Set ℝ} (hS : IsOpen S) {n : ℕ} (hn : 0 < n) {v u : History} {p : Field} (hv : ∀ j ≤ n, Smooth S (v j)) (hu : ∀ j ≤ n, Smooth S (u j)) (hp : Smooth S p) (h a B : ℝ) (ha : 0 < a) (hB : 0 ≤ B) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (hV : ∀ j ≤ n, exterior B S (v j)) (hU : ∀ j ≤ n, exterior B S (u j)) (hP : exterior B S p) (haxis : ∀ eta ∈ S, ∀ j ≤ n, v j (0, eta) = 0) (hum : ∀ eta ∈ S, moment B 1 (u n) eta = 0) (hflux : ∀ eta ∈ S, moment B 1 (fun (w : ℝ × ℝ) => conv n u u w + p w) eta = 0) (hprev : ∀ eta ∈ S, moment B 1 (u (n - 1)) eta = 0) (hdiv : ∀ (w : ℝ × ℝ), w.2 ∈ S → ∀ j ≤ n, dr (v j) w = -w.1 * axialOp h (orderExponent h j) (u j) w) (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, axialWeighted h n v u p (R, eta) = 0) : Smooth S (axialStress h n v u p) ∧ radialSupport S a B (axialStress h n v u p) ∧ ∀ eta ∈ S, ∀ (R : ℝ), 0 < R → HasDerivAt (fun (r : ℝ) => r * axialStress h n v u p (r, eta)) (-axialWeighted h n v u p (R, eta)) R

noncomputable def NavierStokes.SlowStressSupport.LowerAngularViscosityMoment (S : Set ℝ) (B h : ℝ) (e₀ : Field) : Prop

The order-one angular input is a moment of the actual axial viscosity, not a condition on the total residual. It is supplied by differentiating the restored renormalized order-zero physical angular moment.

Equations

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

theorem NavierStokes.SlowStressSupport.order_one_angular_stress_support {S : Set ℝ} (hS : IsOpen S) {v u e : History} (hv : ∀ j ≤ 1, Smooth S (v j)) (hu : ∀ j ≤ 1, Smooth S (u j)) (he : ∀ j ≤ 1, Smooth S (e j)) (h a B : ℝ) (ha : 0 < a) (hB : 0 ≤ B) (hell : ∀ eta ∈ S, PositiveAxisSystem.ell h eta ≠ 0) (hV : ∀ j ≤ 1, exterior B S (v j)) (hU : ∀ j ≤ 1, exterior B S (u j)) (hE : exterior B S (e 1)) (hem : ∀ eta ∈ S, moment B 2 (e 1) eta = 0) (hum : ∀ eta ∈ S, moment B 2 (conv 1 u e) eta = 0) (hvisc : LowerAngularViscosityMoment S B h (e 0)) (hviscExterior : exterior B S (axialOp2 h (orderExponent h 0) (e 0))) (hdiv : ∀ (w : ℝ × ℝ), w.2 ∈ S → ∀ j ≤ 1, dr (v j) w = -w.1 * axialOp h (orderExponent h j) (u j) w) (hinner : ∀ eta ∈ S, ∀ R ∈ Set.Icc 0 a, angularWeighted h 1 v u e (R, eta) = 0) : Smooth S (angularStress h 1 v u e) ∧ radialSupport S a B (angularStress h 1 v u e) ∧ ∀ eta ∈ S, ∀ (R : ℝ), 0 < R → HasDerivAt (fun (r : ℝ) => r ^ 2 * angularStress h 1 v u e (r, eta)) (-angularWeighted h 1 v u e (R, eta)) R

noncomputable def NavierStokes.SlowStressSupport.logFlatWeight (l r cL cR R : ℝ) : ℝ

A concrete two-edge weight of the form prescribed in (20).

Equations

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

theorem NavierStokes.SlowStressSupport.logFlatWeight_pos {l r : ℝ} (hl : 0 < l) (cL cR : ℝ) {R : ℝ} (hR : R ∈ Set.Ioo l r) : 0 < logFlatWeight l r cL cR R

theorem NavierStokes.SlowStressSupport.logFlatWeight_contDiffOn {l r cL cR : ℝ} (hl : 0 < l) (hcL : 0 < cL) (hcR : 0 < cR) : ContDiffOn ℝ (↑⊤) (logFlatWeight l r cL cR) (Set.Ioo l r)

theorem NavierStokes.SlowStressSupport.logarithmic_weighted_jets {S K : Set ℝ} (hS : IsOpen S) (hK : IsCompact K) (hKS : K ⊆ S) {f : Field} (hf : Smooth S f) {a b l r cL cR : ℝ} (hs : radialSupport S a b f) (hab : Set.Icc a b ⊆ Set.Ioo l r) (hl : 0 < l) (hcL : 0 < cL) (hcR : 0 < cR) : (Smooth S fun (w : ℝ × ℝ) => f w / logFlatWeight l r cL cR w.1) ∧ ∀ (k : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ R ∈ Set.Ioo l r, ∀ eta ∈ K, ‖iteratedFDeriv ℝ k f (R, eta)‖ ≤ C * logFlatWeight l r cL cR R

In particular the prescribed logarithmic Gaussian weight controls every jet, with inverse-edge loss zero, for a field supported strictly inside both fixed edges. The constants are obtained from compactness.