The physical five-row mean update

The update is the constructed power-moment inverse, transported with the physical length and velocity scales. Each moment carries its own scale.

@[reducible, inline]

abbrev NavierStokes.MeanRankUpdate.Debt : Type

Debt: an abbreviation for FiveRowRank.Debt.

Equations

• NavierStokes.MeanRankUpdate.Debt = NavierStokes.FiveRowRank.Debt

noncomputable def NavierStokes.MeanRankUpdate.scaleField (ell U : ℝ) (f : ℝ → ℝ) : ℝ → ℝ

Scale field, defined pointwise by U * f (r / ell).

Equations

• NavierStokes.MeanRankUpdate.scaleField ell U f r = U * f (r / ell)

noncomputable def NavierStokes.MeanRankUpdate.scaleDebt (ell U : ℝ) (d : Debt) : Debt

Pressure, angular moment, and axial moment have distinct length powers.

Equations

• NavierStokes.MeanRankUpdate.scaleDebt ell U d = ![U ^ 2 * d 0, ell ^ 3 * U ^ 2 * d 1, ell ^ 2 * U ^ 2 * d 2]

noncomputable def NavierStokes.MeanRankUpdate.normalizeDebt (ell U : ℝ) (d : Debt) : Debt

Normalize debt, given by ![d 0 / U ^ 2, d 1 / (ell ^ 3 * U ^ 2), d 2 / (ell ^ 2 * U ^ 2)].

Equations

• NavierStokes.MeanRankUpdate.normalizeDebt ell U d = ![d 0 / U ^ 2, d 1 / (ell ^ 3 * U ^ 2), d 2 / (ell ^ 2 * U ^ 2)]

theorem NavierStokes.MeanRankUpdate.scale_normalizeDebt {ell U : ℝ} (hell : ell ≠ 0) (hU : U ≠ 0) (d : Debt) : scaleDebt ell U (normalizeDebt ell U d) = d

theorem NavierStokes.MeanRankUpdate.normalize_scaleDebt {ell U : ℝ} (hell : ell ≠ 0) (hU : U ≠ 0) (d : Debt) : normalizeDebt ell U (scaleDebt ell U d) = d

theorem NavierStokes.MeanRankUpdate.integral_scaled {ell : ℝ} (hell : 0 < ell) (c : ℝ) (f : ℝ → ℝ) : ∫ (r : ℝ), c * f (r / ell) = ell * c * ∫ (x : ℝ), f x

theorem NavierStokes.MeanRankUpdate.scaleField_smooth (ell U : ℝ) {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (scaleField ell U f)

theorem NavierStokes.MeanRankUpdate.scaleField_tsupport {ell : ℝ} (hell : 0 < ell) (U a b : ℝ) {f : ℝ → ℝ} (hs : tsupport f ⊆ Set.Ioo a b) : tsupport (scaleField ell U f) ⊆ Set.Ioo (ell * a) (ell * b)

theorem NavierStokes.MeanRankUpdate.scaleField_compact {ell : ℝ} (hell : 0 < ell) (U a b : ℝ) {f : ℝ → ℝ} (hs : tsupport f ⊆ Set.Ioo a b) : HasCompactSupport (scaleField ell U f)

theorem NavierStokes.MeanRankUpdate.scaled_angular_mass {ell : ℝ} (hell : 0 < ell) (U : ℝ) (f : ℝ → ℝ) : ∫ (r : ℝ), r ^ 2 * scaleField ell U f r = ell ^ 3 * U * ∫ (x : ℝ), x ^ 2 * f x

theorem NavierStokes.MeanRankUpdate.scaled_axial_mass {ell : ℝ} (hell : 0 < ell) (U : ℝ) (f : ℝ → ℝ) : ∫ (r : ℝ), r * scaleField ell U f r = ell ^ 2 * U * ∫ (x : ℝ), x * f x

theorem NavierStokes.MeanRankUpdate.scaled_pressure_row {ell : ℝ} (hell : 0 < ell) (U : ℝ) (V f : ℝ → ℝ) : ∫ (r : ℝ), 2 * scaleField ell U V r / r * scaleField ell U f r = U ^ 2 * ∫ (x : ℝ), 2 * V x / x * f x

theorem NavierStokes.MeanRankUpdate.scaled_angular_row {ell : ℝ} (hell : 0 < ell) (U : ℝ) (V G f g : ℝ → ℝ) : ∫ (r : ℝ), r ^ 2 * (scaleField ell U G r * scaleField ell U f r + scaleField ell U V r * scaleField ell U g r) = ell ^ 3 * U ^ 2 * ∫ (x : ℝ), x ^ 2 * (G x * f x + V x * g x)

theorem NavierStokes.MeanRankUpdate.scaled_axial_row {ell : ℝ} (hell : 0 < ell) (U : ℝ) (V G f g : ℝ → ℝ) : ∫ (r : ℝ), 2 * r * scaleField ell U G r * scaleField ell U g r - r * scaleField ell U V r * scaleField ell U f r = ell ^ 2 * U ^ 2 * ∫ (x : ℝ), 2 * x * G x * g x - x * V x * f x

theorem NavierStokes.MeanRankUpdate.fiveRows_scaled {ell : ℝ} (hell : 0 < ell) (U : ℝ) {V G f g : ℝ → ℝ} {d : Debt} (h : FiveRowRank.FiveRows V G d f g) : FiveRowRank.FiveRows (scaleField ell U V) (scaleField ell U G) (scaleDebt ell U d) (scaleField ell U f) (scaleField ell U g)

noncomputable def NavierStokes.MeanRankUpdate.angularIncrement (lam C a b ell U : ℝ) (d : Debt) : ℝ → ℝ

Angular increment, given by scaleField ell U (FiveRowRank.deltaV lam C a b (normalizeDebt ell U d)).

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.desiredAxialIncrement (lam C a b ell U : ℝ) (d : Debt) : ℝ → ℝ

Desired axial increment, given by scaleField ell U (FiveRowRank.gamma lam C a b (normalizeDebt ell U d)).

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.background (lam C ell U : ℝ) : ℝ → ℝ

Background, given by scaleField ell U (FiveRowRank.background lam C).

Equations

• NavierStokes.MeanRankUpdate.background lam C ell U = NavierStokes.MeanRankUpdate.scaleField ell U (NavierStokes.FiveRowRank.background lam C)

theorem NavierStokes.MeanRankUpdate.physical_five_rows {lam C a b ell U : ℝ} (hlam : 0 < lam) (hC : C ≠ 0) (ha : 0 < a) (hab : a < b) (hell : 0 < ell) (hU : U ≠ 0) (d : Debt) : FiveRowRank.FiveRows (background lam C ell U) (fun (x : ℝ) => 0) d (angularIncrement lam C a b ell U d) (desiredAxialIncrement lam C a b ell U d)

Equation (35) in physical units, with no assumed rank or inverse.

theorem NavierStokes.MeanRankUpdate.angularIncrement_smooth (lam C a b ell U : ℝ) (d : Debt) : ContDiff ℝ (↑⊤) (angularIncrement lam C a b ell U d)

theorem NavierStokes.MeanRankUpdate.desiredAxialIncrement_smooth (lam C a b ell U : ℝ) (d : Debt) : ContDiff ℝ (↑⊤) (desiredAxialIncrement lam C a b ell U d)

theorem NavierStokes.MeanRankUpdate.angularIncrement_tsupport (lam C a b U : ℝ) {ell : ℝ} (hell : 0 < ell) (hab : a < b) (d : Debt) : tsupport (angularIncrement lam C a b ell U d) ⊆ Set.Ioo (ell * a) (ell * b)

theorem NavierStokes.MeanRankUpdate.desiredAxialIncrement_tsupport (lam C a b U : ℝ) {ell : ℝ} (hell : 0 < ell) (hab : a < b) (d : Debt) : tsupport (desiredAxialIncrement lam C a b ell U d) ⊆ Set.Ioo (ell * a) (ell * b)

theorem NavierStokes.MeanRankUpdate.physical_rows_on_patch {lam C a b ell U : ℝ} (hlam : 0 < lam) (hC : C ≠ 0) (ha : 0 < a) (hab : a < b) (hell : 0 < ell) (hU : U ≠ 0) (d : Debt) (V G : ℝ → ℝ) (hV : ∀ r ∈ Set.Ioo (ell * a) (ell * b), V r = background lam C ell U r) (hG : ∀ r ∈ Set.Ioo (ell * a) (ell * b), G r = 0) : FiveRowRank.FiveRows V G d (angularIncrement lam C a b ell U d) (desiredAxialIncrement lam C a b ell U d)

noncomputable def NavierStokes.MeanRankUpdate.scaleFamily {E : Type u_1} (ell U : E → ℝ) (H : E × ℝ → ℝ) : ℝ × E → ℝ

Scale family, defined pointwise by U p.2 * H (p.2, p.1 / ell p.2).

Equations

• NavierStokes.MeanRankUpdate.scaleFamily ell U H p = U p.2 * H (p.2, p.1 / ell p.2)

theorem NavierStokes.MeanRankUpdate.scaleFamily_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} {ell U : E → ℝ} {H : E × ℝ → ℝ} (hl : ContDiffOn ℝ (↑⊤) ell S) (hU : ContDiffOn ℝ (↑⊤) U S) (hln : ∀ p ∈ S, ell p ≠ 0) (hH : ContDiffOn ℝ (↑⊤) H (S ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (scaleFamily ell U H) (Set.univ ×ˢ S)

noncomputable def NavierStokes.MeanRankUpdate.angularFamily {E : Type u_1} (lam a b : ℝ) (ell U C : E → ℝ) (d : E → Debt) : ℝ × E → ℝ

Angular family, given by scaleFamily ell U (fun p => FiveRowRank.deltaV lam (C p.1) a b (normalizeDebt (ell p.1) (U p.1) (d p.1)) p.2).

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.desiredAxialFamily {E : Type u_1} (lam a b : ℝ) (ell U C : E → ℝ) (d : E → Debt) : ℝ × E → ℝ

Desired axial family, given by scaleFamily ell U (fun p => FiveRowRank.gamma lam (C p.1) a b (normalizeDebt (ell p.1) (U p.1) (d p.1)) p.2).

Equations

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

theorem NavierStokes.MeanRankUpdate.normalizeDebt_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : Set E} {ell U : E → ℝ} {d : E → Debt} (hl : ContDiffOn ℝ (↑⊤) ell S) (hU : ContDiffOn ℝ (↑⊤) U S) (hd : ContDiffOn ℝ (↑⊤) d S) (hln : ∀ p ∈ S, ell p ≠ 0) (hUn : ∀ p ∈ S, U p ≠ 0) : ContDiffOn ℝ (↑⊤) (fun (p : E) => normalizeDebt (ell p) (U p) (d p)) S

theorem NavierStokes.MeanRankUpdate.angularFamily_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (lam a b : ℝ) {S : Set E} {ell U C : E → ℝ} {d : E → Debt} (hl : ContDiffOn ℝ (↑⊤) ell S) (hU : ContDiffOn ℝ (↑⊤) U S) (hC : ContDiffOn ℝ (↑⊤) C S) (hd : ContDiffOn ℝ (↑⊤) d S) (hln : ∀ p ∈ S, ell p ≠ 0) (hUn : ∀ p ∈ S, U p ≠ 0) (hCn : ∀ p ∈ S, C p ≠ 0) : ContDiffOn ℝ (↑⊤) (angularFamily lam a b ell U C d) (Set.univ ×ˢ S)

theorem NavierStokes.MeanRankUpdate.desiredAxialFamily_contDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (lam a b : ℝ) {S : Set E} {ell U C : E → ℝ} {d : E → Debt} (hl : ContDiffOn ℝ (↑⊤) ell S) (hU : ContDiffOn ℝ (↑⊤) U S) (hC : ContDiffOn ℝ (↑⊤) C S) (hd : ContDiffOn ℝ (↑⊤) d S) (hln : ∀ p ∈ S, ell p ≠ 0) (hUn : ∀ p ∈ S, U p ≠ 0) (hCn : ∀ p ∈ S, C p ≠ 0) : ContDiffOn ℝ (↑⊤) (desiredAxialFamily lam a b ell U C d) (Set.univ ×ˢ S)

theorem NavierStokes.MeanRankUpdate.angularFamily_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (lam a b : ℝ) {ell U C : E → ℝ} {d : E → Debt} (hl : ContDiff ℝ (↑⊤) ell) (hU : ContDiff ℝ (↑⊤) U) (hC : ContDiff ℝ (↑⊤) C) (hd : ContDiff ℝ (↑⊤) d) (hln : ∀ (p : E), ell p ≠ 0) (hUn : ∀ (p : E), U p ≠ 0) (hCn : ∀ (p : E), C p ≠ 0) : ContDiff ℝ (↑⊤) (angularFamily lam a b ell U C d)

theorem NavierStokes.MeanRankUpdate.desiredAxialFamily_contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (lam a b : ℝ) {ell U C : E → ℝ} {d : E → Debt} (hl : ContDiff ℝ (↑⊤) ell) (hU : ContDiff ℝ (↑⊤) U) (hC : ContDiff ℝ (↑⊤) C) (hd : ContDiff ℝ (↑⊤) d) (hln : ∀ (p : E), ell p ≠ 0) (hUn : ∀ (p : E), U p ≠ 0) (hCn : ∀ (p : E), C p ≠ 0) : ContDiff ℝ (↑⊤) (desiredAxialFamily lam a b ell U C d)

theorem NavierStokes.MeanRankUpdate.desiredAxialFamily_supported {E : Type u_1} (lam a b : ℝ) {ell U C : E → ℝ} (d : E → Debt) (hab : a < b) (hl : ∀ (s : E), 0 < ell s) {lo hi : ℝ} (hlo : ∀ (s : E), lo ≤ ell s * a) (hhi : ∀ (s : E), ell s * b ≤ hi) : RadialAlias.RadiallySupported lo hi (desiredAxialFamily lam a b ell U C d)

A common radial annulus follows from bounds on the physical length.

theorem NavierStokes.MeanRankUpdate.angularFamily_supported {E : Type u_1} (lam a b : ℝ) {ell U C : E → ℝ} (d : E → Debt) (hab : a < b) (hl : ∀ (s : E), 0 < ell s) {lo hi : ℝ} (hlo : ∀ (s : E), lo ≤ ell s * a) (hhi : ∀ (s : E), ell s * b ≤ hi) : RadialAlias.RadiallySupported lo hi (angularFamily lam a b ell U C d)

noncomputable def NavierStokes.MeanRankUpdate.slowLift {E : Type} (f : ℝ × E → ℝ) : PressureStream.Lift E → ℝ

The slow source is independent of both periodic phase variables.

Equations

• NavierStokes.MeanRankUpdate.slowLift f p = f (p.1, p.2.1)

theorem NavierStokes.MeanRankUpdate.slowLift_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (slowLift f)

theorem NavierStokes.MeanRankUpdate.slowLift_supported {E : Type} {f : ℝ × E → ℝ} {a b : ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (slowLift f)

theorem NavierStokes.MeanRankUpdate.slowLift_shift {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ × E → ℝ) (r : ℝ) (s : E) (Y v : PressureStream.Plane) (c : ℝ) : slowLift f (r, (s, Y) + c • (0, v)) = f (r, s)

theorem NavierStokes.MeanRankUpdate.radial_integral_eq_interval {E : Type} [NormedAddCommGroup E] {a b : ℝ} {f : ℝ × E → ℝ} (hf : Continuous f) (hs : RadialAlias.RadiallySupported a b f) (s : E) : ∫ (r : ℝ) in a..b, f (r, s) = ∫ (r : ℝ), f (r, s)

theorem NavierStokes.MeanRankUpdate.slow_physicalTotal {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (p : PressureStream.Lift E) (hp : a ≤ p.1) : PressureStream.physicalTotal d a M (0, v) (slowLift f) p = ∫ (r : ℝ), f (r, p.2.1)

With a slow source the transported total is the ordinary radial mass.

theorem NavierStokes.MeanRankUpdate.slow_physicalAlias_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∀ (s : E), ∫ (r : ℝ), f (r, s) = 0) (p : PressureStream.Lift E) : RadialPullback.physicalAlias d a b M (0, v) (slowLift f) p = 0

There is exactly zero compactification alias for a zero-mass slow source.

theorem NavierStokes.MeanRankUpdate.slow_streamGamma_eq_desired {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hm : ∀ (s : E), ∫ (r : ℝ), r * f (r, s) = 0) (p : PressureStream.Lift E) : PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (PressureStream.streamPotential d a b M (0, v) (slowLift f)) p = slowLift f p

The actual stream realizes the desired slow axial field, pointwise, including the axis.

theorem NavierStokes.MeanRankUpdate.slow_stream_divergence_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b d M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : PressureStream.Plane) (w : E × PressureStream.Plane) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (p : PressureStream.Lift E) : PressureStream.graphDivergence (PressureStream.physicalSpeed d M) (0, v) w (PressureStream.streamBeta w (PressureStream.streamPotential d a b M (0, v) (slowLift f))) (PressureStream.streamGamma (PressureStream.physicalSpeed d M) (0, v) (PressureStream.streamPotential d a b M (0, v) (slowLift f))) p = 0

The radial companion is the actual axial derivative of the same stream.

noncomputable def NavierStokes.MeanRankUpdate.normalizeDebtLinearMap (ell U : ℝ) : Debt →ₗ[ℝ] Debt

Normalize debt linear map, bundling toFun, map_add, map_smul.

Equations

• NavierStokes.MeanRankUpdate.normalizeDebtLinearMap ell U = { toFun := NavierStokes.MeanRankUpdate.normalizeDebt ell U, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NavierStokes.MeanRankUpdate.scaleFieldLinearMap (ell U : ℝ) : (ℝ → ℝ) →ₗ[ℝ] ℝ → ℝ

Scale field linear map, bundling toFun, map_add, map_smul.

Equations

• NavierStokes.MeanRankUpdate.scaleFieldLinearMap ell U = { toFun := NavierStokes.MeanRankUpdate.scaleField ell U, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def NavierStokes.MeanRankUpdate.angularLinearMap (lam C a b ell U : ℝ) : Debt →ₗ[ℝ] ℝ → ℝ

Angular linear map, given by (scaleFieldLinearMap ell U).comp ((FiveRowRank.deltaVLinearMap lam C a b).comp (normalizeDebtLinearMap ell U)).

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.axialLinearMap (lam C a b ell U : ℝ) : Debt →ₗ[ℝ] ℝ → ℝ

Axial linear map, given by (scaleFieldLinearMap ell U).comp ((FiveRowRank.gammaLinearMap lam C a b).comp (normalizeDebtLinearMap ell U)).

Equations

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

theorem NavierStokes.MeanRankUpdate.debt_eq_sum (d : Debt) : d = ∑ i : Fin 3, d i • Pi.single i 1

theorem NavierStokes.MeanRankUpdate.linearMap_eq_sum {F : Type u_1} [AddCommMonoid F] [Module ℝ F] (L : Debt →ₗ[ℝ] F) (d : Debt) : L d = ∑ i : Fin 3, d i • L (Pi.single i 1)

theorem NavierStokes.MeanRankUpdate.angularIncrement_eq_sum (lam C a b ell U : ℝ) (d : Debt) (r : ℝ) : angularIncrement lam C a b ell U d r = ∑ i : Fin 3, d i * angularIncrement lam C a b ell U (Pi.single i 1) r

The update is a fixed finite linear combination of constructed profiles.

theorem NavierStokes.MeanRankUpdate.desiredAxialIncrement_eq_sum (lam C a b ell U : ℝ) (d : Debt) (r : ℝ) : desiredAxialIncrement lam C a b ell U d r = ∑ i : Fin 3, d i * desiredAxialIncrement lam C a b ell U (Pi.single i 1) r

theorem NavierStokes.MeanRankUpdate.normalizeDebt_rescale {ell U L W : ℝ} (hl : ell ≠ 0) (hU : U ≠ 0) (hL : L ≠ 0) (hW : W ≠ 0) (d : Debt) : normalizeDebt ell U (scaleDebt L W d) = normalizeDebt (ell / L) (U / W) d

theorem NavierStokes.MeanRankUpdate.angularIncrement_rescale {ell U L W : ℝ} (hl : ell ≠ 0) (hU : U ≠ 0) (hL : L ≠ 0) (hW : W ≠ 0) (lam C a b : ℝ) (d : Debt) (r : ℝ) : angularIncrement lam C a b ell U (scaleDebt L W d) (L * r) / W = angularIncrement lam C a b (ell / L) (U / W) d r

theorem NavierStokes.MeanRankUpdate.desiredAxialIncrement_rescale {ell U L W : ℝ} (hl : ell ≠ 0) (hU : U ≠ 0) (hL : L ≠ 0) (hW : W ≠ 0) (lam C a b : ℝ) (d : Debt) (r : ℝ) : desiredAxialIncrement lam C a b ell U (scaleDebt L W d) (L * r) / W = desiredAxialIncrement lam C a b (ell / L) (U / W) d r

theorem NavierStokes.MeanRankUpdate.angularIncrement_q_over_Q {q Q : ℝ} (hq : 0 < q) (hQ : 0 < Q) (A lam C a b : ℝ) (d : Debt) (R : ℝ) : angularIncrement lam C a b (√q) (q ^ (-A)) (scaleDebt (√Q) (Q ^ (-A)) d) (√Q * R) / Q ^ (-A) = angularIncrement lam C a b (√(q / Q)) ((q / Q) ^ (-A)) d R

Normalization from the physical q scale to any comparison band Q.

theorem NavierStokes.MeanRankUpdate.desiredAxialIncrement_q_over_Q {q Q : ℝ} (hq : 0 < q) (hQ : 0 < Q) (A lam C a b : ℝ) (d : Debt) (R : ℝ) : desiredAxialIncrement lam C a b (√q) (q ^ (-A)) (scaleDebt (√Q) (Q ^ (-A)) d) (√Q * R) / Q ^ (-A) = desiredAxialIncrement lam C a b (√(q / Q)) ((q / Q) ^ (-A)) d R

@[reducible, inline]

abbrev NavierStokes.MeanRankUpdate.ModelPoint : Type

Model point: an abbreviation for PhysicalCoordinateBounds.Point.

Equations

• NavierStokes.MeanRankUpdate.ModelPoint = NavierStokes.PhysicalCoordinateBounds.Point

noncomputable def NavierStokes.MeanRankUpdate.shapedAmplitude (B η : ℝ) : ℝ

The fixed shaped amplitude on the untouched patch.

Equations

• NavierStokes.MeanRankUpdate.shapedAmplitude B η = B / (1 + η ^ 2)

theorem NavierStokes.MeanRankUpdate.shapedAmplitude_contDiff (B : ℝ) : ContDiff ℝ (↑⊤) (shapedAmplitude B)

theorem NavierStokes.MeanRankUpdate.shapedAmplitude_ne_zero {B : ℝ} (hB : B ≠ 0) (η : ℝ) : shapedAmplitude B η ≠ 0

noncomputable def NavierStokes.MeanRankUpdate.modelLength (y : ModelPoint) : ℝ

Model length, given by Real.sqrt y.1.

Equations

• NavierStokes.MeanRankUpdate.modelLength y = √y.1

noncomputable def NavierStokes.MeanRankUpdate.modelVelocity (A : ℝ) (y : ModelPoint) : ℝ

Model velocity, given by y.1 ^ (-A).

Equations

• NavierStokes.MeanRankUpdate.modelVelocity A y = y.1 ^ (-A)

noncomputable def NavierStokes.MeanRankUpdate.modelAmplitude (coord B : ℝ) (y : ModelPoint) : ℝ

Model amplitude, given by shapedAmplitude B (y.2.2 / y.1 ^ PhysicalCoordinateBounds.D coord).

Equations

• NavierStokes.MeanRankUpdate.modelAmplitude coord B y = NavierStokes.MeanRankUpdate.shapedAmplitude B (y.2.2 / y.1 ^ NavierStokes.PhysicalCoordinateBounds.D coord)

theorem NavierStokes.MeanRankUpdate.modelLength_contDiffOn : ContDiffOn ℝ (↑⊤) modelLength PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.MeanRankUpdate.modelVelocity_contDiffOn (A : ℝ) : ContDiffOn ℝ (↑⊤) (modelVelocity A) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.MeanRankUpdate.modelAmplitude_contDiffOn (coord B : ℝ) : ContDiffOn ℝ (↑⊤) (modelAmplitude coord B) PhysicalCoordinateBounds.positiveTime

noncomputable def NavierStokes.MeanRankUpdate.angularModel (coord A B lam a b : ℝ) (d : Debt) (y : ModelPoint) : ℝ

Angular model, given by angularFamily lam a b modelLength (modelVelocity A) (modelAmplitude coord B) (fun _ => d) (y.2.1, y).

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.axialModel (coord A B lam a b : ℝ) (d : Debt) (y : ModelPoint) : ℝ

Axial model, given by desiredAxialFamily lam a b modelLength (modelVelocity A) (modelAmplitude coord B) (fun _ => d) (y.2.1, y).

Equations

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

theorem NavierStokes.MeanRankUpdate.angularModel_contDiffOn (coord A B lam a b : ℝ) (hB : B ≠ 0) (d : Debt) : ContDiffOn ℝ (↑⊤) (angularModel coord A B lam a b d) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.MeanRankUpdate.axialModel_contDiffOn (coord A B lam a b : ℝ) (hB : B ≠ 0) (d : Debt) : ContDiffOn ℝ (↑⊤) (axialModel coord A B lam a b d) PhysicalCoordinateBounds.positiveTime

noncomputable def NavierStokes.MeanRankUpdate.modelBox (qlo qhi rlo rhi : ℝ) : Set ModelPoint

Model box, given by Icc qlo qhi ×ˢ (Icc rlo rhi ×ˢ Icc (-1 : ℝ) 1).

Equations

• NavierStokes.MeanRankUpdate.modelBox qlo qhi rlo rhi = Set.Icc qlo qhi ×ˢ Set.Icc rlo rhi ×ˢ Set.Icc (-1) 1

noncomputable def NavierStokes.MeanRankUpdate.modelToInverse (coord : ℝ) (y : ModelPoint) : ModelPoint

Model to inverse, given by (y.1, (y.2.1, y.2.2 * y.1 ^ PhysicalCoordinateBounds.D coord)).

Equations

• NavierStokes.MeanRankUpdate.modelToInverse coord y = (y.1, y.2.1, y.2.2 * y.1 ^ NavierStokes.PhysicalCoordinateBounds.D coord)

theorem NavierStokes.MeanRankUpdate.modelToInverse_contDiffOn (coord : ℝ) : ContDiffOn ℝ (↑⊤) (modelToInverse coord) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.MeanRankUpdate.modelToInverse_slope {q : ℝ} (hq : 0 < q) (coord R η : ℝ) : SimilarityCoordinates.scalarSlope coord (modelToInverse coord (q, R, η)).2.2 (modelToInverse coord (q, R, η)).1 = 1 - coord * η ^ 2

theorem NavierStokes.MeanRankUpdate.modelBox_slope_pos {coord qlo qhi rlo rhi : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) {y : ModelPoint} (hy : y ∈ modelBox qlo qhi rlo rhi) : 0 < SimilarityCoordinates.scalarSlope coord (modelToInverse coord y).2.2 (modelToInverse coord y).1

theorem NavierStokes.MeanRankUpdate.modelBox_image_isCompact {qlo qhi rlo rhi : ℝ} (hqlo : 0 < qlo) (coord : ℝ) : IsCompact (modelToInverse coord '' modelBox qlo qhi rlo rhi)

theorem NavierStokes.MeanRankUpdate.inverseCoordinates_mem_modelBox {coord qlo qhi rlo rhi : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {p : ModelPoint} (hp : p ∈ PhysicalCoordinateBounds.positiveTime) (hq : PhysicalCoordinateBounds.qCoord coord p ∈ Set.Icc qlo qhi) (hR : p.2.1 ∈ Set.Icc rlo rhi) : PhysicalCoordinateBounds.inverseCoordinates coord p ∈ modelToInverse coord '' modelBox qlo qhi rlo rhi

theorem NavierStokes.MeanRankUpdate.inverse_kernel_jet_bound {coord qlo qhi rlo rhi : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) {g : ModelPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) g PhysicalCoordinateBounds.positiveTime) (j : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ p ∈ PhysicalCoordinateBounds.positiveTime, PhysicalCoordinateBounds.qCoord coord p ∈ Set.Icc qlo qhi → p.2.1 ∈ Set.Icc rlo rhi → ‖iteratedFDeriv ℝ j (g ∘ PhysicalCoordinateBounds.inverseCoordinates coord) p‖ ≤ C

Actual inverse-coordinate jets remain bounded on a normalized closed q interval, including both limiting values η=±1.

theorem NavierStokes.MeanRankUpdate.finiteJetBounds_of_orderBounds {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (f : D → ℝ) (S : Set D) (h : ∀ (j : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ S, ‖iteratedFDeriv ℝ j f x‖ ≤ C) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ JetBounds.FiniteJetBound m f S C

theorem NavierStokes.MeanRankUpdate.iteratedFDeriv_comp_linear {D : Type u_1} {F : Type u_2} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : F → ℝ} {S : Set F} (hS : IsOpen S) (hf : ContDiffOn ℝ (↑⊤) f S) (L : D →L[ℝ] F) (j : ℕ) {x : D} (hx : L x ∈ S) : iteratedFDeriv ℝ j (f ∘ ⇑L) x = (iteratedFDeriv ℝ j f (L x)).compContinuousLinearMap fun (x : Fin j) => L

theorem NavierStokes.MeanRankUpdate.iteratedFDeriv_congr_germ {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {f g : D → ℝ} {x : D} (he : f =ᶠ[nhds x] g) (j : ℕ) : iteratedFDeriv ℝ j f x = iteratedFDeriv ℝ j g x

theorem NavierStokes.MeanRankUpdate.meanClass_of_interior_support {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) (f : D → ℝ) (hf : ContDiffOn ℝ (↑⊤) f s.domain) (hb : ∀ (m : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ JetBounds.FiniteJetBound m f s.domain C) {K : Set D} (hK : IsClosed K) (hzero : ∀ x ∈ s.domain, x ∉ K → f x = 0) (hz : ∃ (δ : ℝ), 0 < δ ∧ ∀ x ∈ s.domain, x ∈ K → δ ≤ s.zeta x) : WeightedClasses.MeanClass s 0 fun (x : ℕ) => f

An interior support and genuine finite jet bounds convert! a fixed coefficient to the weighted mean class.

@[reducible, inline]

abbrev NavierStokes.MeanRankUpdate.ChartPoint : Type

Chart point: an abbreviation for PressureStream.Lift PressureStream.Plane.

Equations

• NavierStokes.MeanRankUpdate.ChartPoint = NavierStokes.PressureStream.Lift NavierStokes.PressureStream.Plane

noncomputable def NavierStokes.MeanRankUpdate.chartInput : ChartPoint →L[ℝ] ModelPoint

(R,(T,Z),Y) to the actual inverse-coordinate variables (T,R,Z).

Equations

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

@[simp]

theorem NavierStokes.MeanRankUpdate.chartInput_apply (p : ChartPoint) : chartInput p = (p.2.1.1, p.1, p.2.1.2)

theorem NavierStokes.MeanRankUpdate.chartInput_norm_le_one : ‖chartInput‖ ≤ 1

noncomputable def NavierStokes.MeanRankUpdate.chartQ (coord : ℝ) (p : ChartPoint) : ℝ

Chart Q, given by PhysicalCoordinateBounds.qCoord coord (chartInput p).

Equations

• NavierStokes.MeanRankUpdate.chartQ coord p = NavierStokes.PhysicalCoordinateBounds.qCoord coord (NavierStokes.MeanRankUpdate.chartInput p)

noncomputable def NavierStokes.MeanRankUpdate.chartEta (coord : ℝ) (p : ChartPoint) : ℝ

Chart eta, given by PhysicalCoordinateBounds.etaCoord coord (chartInput p).

Equations

• NavierStokes.MeanRankUpdate.chartEta coord p = NavierStokes.PhysicalCoordinateBounds.etaCoord coord (NavierStokes.MeanRankUpdate.chartInput p)

noncomputable def NavierStokes.MeanRankUpdate.chartKernel (coord : ℝ) (g : ModelPoint → ℝ) : ChartPoint → ℝ

Chart kernel, given by (g ∘ PhysicalCoordinateBounds.inverseCoordinates coord) ∘ chartInput.

Equations

• NavierStokes.MeanRankUpdate.chartKernel coord g = (g ∘ NavierStokes.PhysicalCoordinateBounds.inverseCoordinates coord) ∘ ⇑NavierStokes.MeanRankUpdate.chartInput

noncomputable def NavierStokes.MeanRankUpdate.chartAngular (coord A B lam a b : ℝ) (d : ChartPoint → Debt) (p : ChartPoint) : ℝ

Chart angular, given by angularIncrement lam (shapedAmplitude B (chartEta coord p)) a b (Real.sqrt (chartQ coord p)) (chartQ coord p ^ (-A)) (d p) p.1.

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.chartAxial (coord A B lam a b : ℝ) (d : ChartPoint → Debt) (p : ChartPoint) : ℝ

Chart axial, constructed using desiredAxialIncrement.

Equations

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

theorem NavierStokes.MeanRankUpdate.chartAngular_eq_sum (coord A B lam a b : ℝ) (d : ChartPoint → Debt) (p : ChartPoint) : chartAngular coord A B lam a b d p = ∑ i : Fin 3, d p i * chartKernel coord (angularModel coord A B lam a b (Pi.single i 1)) p

theorem NavierStokes.MeanRankUpdate.chartAxial_eq_sum (coord A B lam a b : ℝ) (d : ChartPoint → Debt) (p : ChartPoint) : chartAxial coord A B lam a b d p = ∑ i : Fin 3, d p i * chartKernel coord (axialModel coord A B lam a b (Pi.single i 1)) p

theorem NavierStokes.MeanRankUpdate.chartKernel_contDiffOn {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {S : Set ChartPoint} (hS : ∀ p ∈ S, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) {g : ModelPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) g PhysicalCoordinateBounds.positiveTime) : ContDiffOn ℝ (↑⊤) (chartKernel coord g) S

theorem NavierStokes.MeanRankUpdate.chartKernel_finiteJetBounds {coord qlo qhi rlo rhi : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) {S : Set ChartPoint} (hT : ∀ p ∈ S, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ S, chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ S, p.1 ∈ Set.Icc rlo rhi) {g : ModelPoint → ℝ} (hg : ContDiffOn ℝ (↑⊤) g PhysicalCoordinateBounds.positiveTime) (m : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ JetBounds.FiniteJetBound m (chartKernel coord g) S C

All stripped jets of the actual inverse-coordinate pullback are uniformly bounded, with no band in either the coefficient or the constant.

noncomputable def NavierStokes.MeanRankUpdate.supportBand (a b qlo qhi : ℝ) : Set ChartPoint

Support band, given by Prod.fst ⁻¹' Icc (Real.sqrt qlo * a) (Real.sqrt qhi * b).

Equations

• NavierStokes.MeanRankUpdate.supportBand a b qlo qhi = Prod.fst ⁻¹' Set.Icc (√qlo * a) (√qhi * b)

theorem NavierStokes.MeanRankUpdate.supportBand_isClosed (a b qlo qhi : ℝ) : IsClosed (supportBand a b qlo qhi)

theorem NavierStokes.MeanRankUpdate.angular_kernel_zero {coord A B lam a b qlo qhi : ℝ} (ha : 0 < a) (hab : a < b) (hqlo : 0 < qlo) (d : Debt) {p : ChartPoint} (hq : chartQ coord p ∈ Set.Icc qlo qhi) (hp : p ∉ supportBand a b qlo qhi) : chartKernel coord (angularModel coord A B lam a b d) p = 0

theorem NavierStokes.MeanRankUpdate.axial_kernel_zero {coord A B lam a b qlo qhi : ℝ} (ha : 0 < a) (hab : a < b) (hqlo : 0 < qlo) (d : Debt) {p : ChartPoint} (hq : chartQ coord p ∈ Set.Icc qlo qhi) (hp : p ∉ supportBand a b qlo qhi) : chartKernel coord (axialModel coord A B lam a b d) p = 0

theorem NavierStokes.MeanRankUpdate.rank_kernels_meanClass (s : WeightedClasses.StripData ChartPoint) {coord A B lam a b qlo qhi rlo rhi : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hqlo : 0 < qlo) (hT : ∀ p ∈ s.domain, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ s.domain, chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ s.domain, p.1 ∈ Set.Icc rlo rhi) (hz : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ s.domain, p ∈ supportBand a b qlo qhi → δ ≤ s.zeta p) (d : Debt) : (WeightedClasses.MeanClass s 0 fun (x : ℕ) => chartKernel coord (angularModel coord A B lam a b d)) ∧ WeightedClasses.MeanClass s 0 fun (x : ℕ) => chartKernel coord (axialModel coord A B lam a b d)

The scalar rank coefficients themselves are proved to lie in M₀. All regularity and all finite jet bounds are derived from the constructed inverse.

theorem NavierStokes.MeanRankUpdate.rank_update_meanClass (s : WeightedClasses.StripData ChartPoint) {coord A B lam a b qlo qhi rlo rhi α : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hqlo : 0 < qlo) (hT : ∀ p ∈ s.domain, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ s.domain, chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ s.domain, p.1 ∈ Set.Icc rlo rhi) (hz : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ s.domain, p ∈ supportBand a b qlo qhi → δ ≤ s.zeta p) {d : ℕ → ChartPoint → Debt} (hd : WeightedClasses.UnweightedClass s α d) : (WeightedClasses.MeanClass s α fun (n : ℕ) => chartAngular coord A B lam a b (d n)) ∧ WeightedClasses.MeanClass s α fun (n : ℕ) => chartAxial coord A B lam a b (d n)

Equation (35) maps the slow defect class S_α to M_α in every finite stripped jet, uniformly over the band index.

noncomputable def NavierStokes.MeanRankUpdate.normalizedDomain (coord qlo qhi rlo rhi : ℝ) : Set ChartPoint

Normalized domain, given by {p | chartInput p ∈ PhysicalCoordinateBounds.positiveTime ∧ chartQ coord p ∈ Ioo qlo qhi ∧ p.1 ∈ Ioo rlo rhi}.

Equations

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

theorem NavierStokes.MeanRankUpdate.normalizedDomain_isOpen {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (qlo qhi rlo rhi : ℝ) : IsOpen (normalizedDomain coord qlo qhi rlo rhi)

noncomputable def NavierStokes.MeanRankUpdate.normalizedStripData (coord qlo qhi rlo rhi cL cR : ℝ) (hc : 0 < coord) (hc1 : coord < 1) (hrlo : 0 < rlo) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) : WeightedClasses.StripData ChartPoint

The concrete logarithmic radial weights, restricted to one normalized physical q/Q strip. The torus variables remain unrestricted.

Equations

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

theorem NavierStokes.MeanRankUpdate.normalizedStrip_weight_margin (coord qlo qhi rlo rhi cL cR a b : ℝ) (hc : 0 < coord) (hc1 : coord < 1) (hrlo : 0 < rlo) (hcL : 0 < cL) (hcR : 0 < cR) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (hleft : rlo < √qlo * a) (hright : √qhi * b < rhi) : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS).domain, p ∈ supportBand a b qlo qhi → δ ≤ (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS).zeta p

theorem NavierStokes.MeanRankUpdate.concrete_rank_update_meanClass (coord qlo qhi rlo rhi cL cR A B lam a b α : ℝ) (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) (hrlo : 0 < rlo) (hcL : 0 < cL) (hcR : 0 < cR) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hleft : rlo < √qlo * a) (hright : √qhi * b < rhi) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) {d : ℕ → ChartPoint → Debt} (hd : WeightedClasses.UnweightedClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α d) : (WeightedClasses.MeanClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α fun (n : ℕ) => chartAngular coord A B lam a b (d n)) ∧ WeightedClasses.MeanClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α fun (n : ℕ) => chartAxial coord A B lam a b (d n)

No coefficient estimate is an input to this concrete S_α → M_α result.

theorem NavierStokes.MeanRankUpdate.chartQ_dilation {coord Q : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hQ : 0 < Q) {p : ChartPoint} (hp : chartInput p ∈ PhysicalCoordinateBounds.positiveTime) : PhysicalCoordinateBounds.qCoord coord ((PhysicalCoordinateBounds.dilation coord Q) (chartInput p)) / Q = chartQ coord p

theorem NavierStokes.MeanRankUpdate.chartEta_dilation {coord Q : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hQ : 0 < Q) {p : ChartPoint} (hp : chartInput p ∈ PhysicalCoordinateBounds.positiveTime) : PhysicalCoordinateBounds.etaCoord coord ((PhysicalCoordinateBounds.dilation coord Q) (chartInput p)) = chartEta coord p

noncomputable def NavierStokes.MeanRankUpdate.normalizedPhysicalAngular (coord A B lam a b Q : ℝ) (d : ChartPoint → Debt) (p : ChartPoint) : ℝ

Normalized physical angular, constructed using angularIncrement.

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.normalizedPhysicalAxial (coord A B lam a b Q : ℝ) (d : ChartPoint → Debt) (p : ChartPoint) : ℝ

Normalized physical axial, constructed using desiredAxialIncrement.

Equations

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

theorem NavierStokes.MeanRankUpdate.normalizedPhysicalAngular_eq_chart {coord Q : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hQ : 0 < Q) (A B lam a b : ℝ) (d : ChartPoint → Debt) {p : ChartPoint} (hp : chartInput p ∈ PhysicalCoordinateBounds.positiveTime) : normalizedPhysicalAngular coord A B lam a b Q d p = chartAngular coord A B lam a b d p

theorem NavierStokes.MeanRankUpdate.normalizedPhysicalAxial_eq_chart {coord Q : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hQ : 0 < Q) (A B lam a b : ℝ) (d : ChartPoint → Debt) {p : ChartPoint} (hp : chartInput p ∈ PhysicalCoordinateBounds.positiveTime) : normalizedPhysicalAxial coord A B lam a b Q d p = chartAxial coord A B lam a b d p

theorem NavierStokes.MeanRankUpdate.meanClass_congr_on {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {s : WeightedClasses.StripData D} {α : ℝ} {f g : ℕ → D → ℝ} (hf : WeightedClasses.MeanClass s α f) (he : ∀ (n : ℕ), ∀ x ∈ s.domain, g n x = f n x) : WeightedClasses.MeanClass s α g

theorem NavierStokes.MeanRankUpdate.concrete_physical_rank_update_meanClass (coord qlo qhi rlo rhi cL cR A B lam a b α : ℝ) (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) (hrlo : 0 < rlo) (hcL : 0 < cL) (hcR : 0 < cR) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hleft : rlo < √qlo * a) (hright : √qhi * b < rhi) (ε S Q : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (hQ : ∀ (n : ℕ), 0 < Q n) {d : ℕ → ChartPoint → Debt} (hd : WeightedClasses.UnweightedClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α d) : (WeightedClasses.MeanClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α fun (n : ℕ) => normalizedPhysicalAngular coord A B lam a b (Q n) (d n)) ∧ WeightedClasses.MeanClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α fun (n : ℕ) => normalizedPhysicalAxial coord A B lam a b (Q n) (d n)

Uniform class bounds for the physical definition, read in any normalized band; the physical correction itself has no chosen band.

theorem NavierStokes.MeanRankUpdate.square_half_power (lam R : ℝ) (hR : 0 < R) : (R ^ 2 / 2) ^ (-(1 / 2 + lam)) = 2 ^ (1 / 2 + lam) * R ^ (-1 - 2 * lam)

theorem NavierStokes.MeanRankUpdate.background_eq_shaped_profile {q r : ℝ} (hq : 0 < q) (hr : 0 < r) (lam U B η : ℝ) : background lam (shapedAmplitude B η * 2 ^ (1 / 2 + lam)) (√q) U r = U * shapedAmplitude B η * (r ^ 2 / (2 * q)) ^ (-(1 / 2 + lam))

The physical radial profile is the manuscript's X^(-1/2-λ) profile, where X = r²/(2q), including the factor of two in its amplitude.

theorem NavierStokes.MeanRankUpdate.physical_rows_on_shaped_patch {lam B a b q : ℝ} (hlam : 0 < lam) (hB : B ≠ 0) (ha : 0 < a) (hab : a < b) (hq : 0 < q) (A η : ℝ) (d : Debt) (V G : ℝ → ℝ) (hV : ∀ r ∈ Set.Ioo (√q * a) (√q * b), V r = q ^ (-A) * shapedAmplitude B η * (r ^ 2 / (2 * q)) ^ (-(1 / 2 + lam))) (hG : ∀ r ∈ Set.Ioo (√q * a) (√q * b), G r = 0) : FiveRowRank.FiveRows V G d (angularIncrement lam (shapedAmplitude B η * 2 ^ (1 / 2 + lam)) a b (√q) (q ^ (-A)) d) (desiredAxialIncrement lam (shapedAmplitude B η * 2 ^ (1 / 2 + lam)) a b (√q) (q ^ (-A)) d)

structure NavierStokes.MeanRankUpdate.SmoothFamily (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E] : Type

Only the input geometry and defect family occur in this record.

• lam : ℝ

  Lam of SmoothFamily, of type ℝ.

• a : ℝ

  A of SmoothFamily, of type ℝ.

• b : ℝ

  B of SmoothFamily, of type ℝ.

• length : E → ℝ

  Length of SmoothFamily, of type E → ℝ.

• velocity : E → ℝ

  Velocity field of SmoothFamily, of type E → ℝ.

• amplitude : E → ℝ

  Amplitude of SmoothFamily, of type E → ℝ.

• debt : E → Debt

  Debt of SmoothFamily, of type E → Debt.

• lam_pos : 0 < self.lam
• a_pos : 0 < self.a
• ordered : self.a < self.b
• length_pos (s : E) : 0 < self.length s
• velocity_ne (s : E) : self.velocity s ≠ 0
• amplitude_ne (s : E) : self.amplitude s ≠ 0
• length_smooth : ContDiff ℝ (↑⊤) self.length
• velocity_smooth : ContDiff ℝ (↑⊤) self.velocity
• amplitude_smooth : ContDiff ℝ (↑⊤) self.amplitude
• debt_smooth : ContDiff ℝ (↑⊤) self.debt

noncomputable def NavierStokes.MeanRankUpdate.SmoothFamily.angular {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) : ℝ × E → ℝ

Angular, given by angularFamily F.lam F.a F.b F.length F.velocity F.amplitude F.debt.

Equations

• F.angular = NavierStokes.MeanRankUpdate.angularFamily F.lam F.a F.b F.length F.velocity F.amplitude F.debt

noncomputable def NavierStokes.MeanRankUpdate.SmoothFamily.desired {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) : ℝ × E → ℝ

Desired, given by desiredAxialFamily F.lam F.a F.b F.length F.velocity F.amplitude F.debt.

Equations

• F.desired = NavierStokes.MeanRankUpdate.desiredAxialFamily F.lam F.a F.b F.length F.velocity F.amplitude F.debt

noncomputable def NavierStokes.MeanRankUpdate.SmoothFamily.potential {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) (power lo hi M : ℝ) (v : PressureStream.Plane) : PressureStream.Lift E → ℝ

Potential, given by PressureStream.streamPotential power lo hi M ((0 : E), v) (slowLift F.desired).

Equations

• F.potential power lo hi M v = NavierStokes.PressureStream.streamPotential power lo hi M (0, v) (NavierStokes.MeanRankUpdate.slowLift F.desired)

noncomputable def NavierStokes.MeanRankUpdate.SmoothFamily.radial {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) (power lo hi M : ℝ) (v : PressureStream.Plane) (w : E × PressureStream.Plane) : PressureStream.Lift E → ℝ

Radial, given by PressureStream.streamBeta w (F.potential power lo hi M v).

Equations

• F.radial power lo hi M v w = NavierStokes.PressureStream.streamBeta w (F.potential power lo hi M v)

noncomputable def NavierStokes.MeanRankUpdate.SmoothFamily.axial {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) (power lo hi M : ℝ) (v : PressureStream.Plane) : PressureStream.Lift E → ℝ

Axial, given by PressureStream.streamGamma (PressureStream.physicalSpeed power M) ((0 : E), v) (F.potential power lo hi M v).

Equations

• F.axial power lo hi M v = NavierStokes.PressureStream.streamGamma (NavierStokes.PressureStream.physicalSpeed power M) (0, v) (F.potential power lo hi M v)

theorem NavierStokes.MeanRankUpdate.SmoothFamily.angular_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) : ContDiff ℝ (↑⊤) F.angular

theorem NavierStokes.MeanRankUpdate.SmoothFamily.desired_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) : ContDiff ℝ (↑⊤) F.desired

theorem NavierStokes.MeanRankUpdate.SmoothFamily.prescribed_five_rows {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) (s : E) : FiveRowRank.FiveRows (background F.lam (F.amplitude s) (F.length s) (F.velocity s)) (fun (x : ℝ) => 0) (F.debt s) (fun (r : ℝ) => F.angular (r, s)) fun (r : ℝ) => F.desired (r, s)

theorem NavierStokes.MeanRankUpdate.SmoothFamily.desired_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {lo hi : ℝ} (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) : RadialAlias.RadiallySupported lo hi F.desired

theorem NavierStokes.MeanRankUpdate.SmoothFamily.desired_mass_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) (s : E) : ∫ (r : ℝ), r * F.desired (r, s) = 0

theorem NavierStokes.MeanRankUpdate.SmoothFamily.desired_zero_outside {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) (s : E) {r : ℝ} (hr : r ∉ Set.Ioo (F.length s * F.a) (F.length s * F.b)) : F.desired (r, s) = 0

theorem NavierStokes.MeanRankUpdate.SmoothFamily.potential_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {power lo hi M : ℝ} (hlo0 : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) : ContDiff ℝ (↑⊤) (F.potential power lo hi M v)

theorem NavierStokes.MeanRankUpdate.SmoothFamily.radial_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {power lo hi M : ℝ} (hlo0 : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (w : E × PressureStream.Plane) (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) : ContDiff ℝ (↑⊤) (F.radial power lo hi M v w)

theorem NavierStokes.MeanRankUpdate.SmoothFamily.axial_exact {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {power lo hi M : ℝ} (hlo0 : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) (p : PressureStream.Lift E) : F.axial power lo hi M v p = F.desired (p.1, p.2.1)

theorem NavierStokes.MeanRankUpdate.SmoothFamily.streamed_five_rows {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {power lo hi M : ℝ} (hlo0 : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) (s : E) (Y : PressureStream.Plane) : FiveRowRank.FiveRows (background F.lam (F.amplitude s) (F.length s) (F.velocity s)) (fun (x : ℝ) => 0) (F.debt s) (fun (r : ℝ) => F.angular (r, s)) fun (r : ℝ) => F.axial power lo hi M v (r, s, Y)

These are the five rows of the actual divergence-free update.

theorem NavierStokes.MeanRankUpdate.SmoothFamily.divergence_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {power lo hi M : ℝ} (hlo0 : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (w : E × PressureStream.Plane) (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) (p : PressureStream.Lift E) : PressureStream.graphDivergence (PressureStream.physicalSpeed power M) (0, v) w (F.radial power lo hi M v w) (F.axial power lo hi M v) p = 0

theorem NavierStokes.MeanRankUpdate.slow_streamPotential_eq_primitive {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {lo hi power M : ℝ} (hlo : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported lo hi f) (hm : ∀ (s : E), ∫ (r : ℝ), r * f (r, s) = 0) (p : PressureStream.Lift E) (hr : lo ≤ p.1) : PressureStream.streamPotential power lo hi M (0, v) (slowLift f) p = (∫ (r : ℝ) in lo..p.1, r * f (r, p.2.1)) / p.1

theorem NavierStokes.MeanRankUpdate.SmoothFamily.potential_zero_outside {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {power lo hi M : ℝ} (hlo0 : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) (p : PressureStream.Lift E) (hnot : p.1 ∉ Set.Ioo (F.length p.2.1 * F.a) (F.length p.2.1 * F.b)) : F.potential power lo hi M v p = 0

noncomputable def NavierStokes.MeanRankUpdate.SmoothFamily.supportSet {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) : Set (PressureStream.Lift E)

Support set, given by {p | p.1 ∈ Icc (F.length p.2.1 * F.a) (F.length p.2.1 * F.b)}.

Equations

• F.supportSet = {p : NavierStokes.PressureStream.Lift E | p.1 ∈ Set.Icc (F.length p.2.1 * F.a) (F.length p.2.1 * F.b)}

theorem NavierStokes.MeanRankUpdate.SmoothFamily.supportSet_isClosed {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) : IsClosed F.supportSet

theorem NavierStokes.MeanRankUpdate.SmoothFamily.radial_zero_outside {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {power lo hi M : ℝ} (hlo0 : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (w : E × PressureStream.Plane) (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) (p : PressureStream.Lift E) (hnot : p ∉ F.supportSet) : F.radial power lo hi M v w p = 0

The radial stream correction remains on the same physical mean patch; varying its endpoints introduces no support outside that patch.

theorem NavierStokes.MeanRankUpdate.SmoothFamily.radial_tsupport {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : SmoothFamily E) {power lo hi M : ℝ} (hlo0 : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (w : E × PressureStream.Plane) (hlo : ∀ (s : E), lo ≤ F.length s * F.a) (hhi : ∀ (s : E), F.length s * F.b ≤ hi) (s : E) (Y : PressureStream.Plane) : (tsupport fun (r : ℝ) => F.radial power lo hi M v w (r, s, Y)) ⊆ Set.Icc (F.length s * F.a) (F.length s * F.b)

noncomputable def NavierStokes.MeanRankUpdate.reservedAngularBase (F : OutgoingProfile.Profile) (XR : ℝ) (c : ℝ → HeatedOutgoing.Coeff) (q U η r : ℝ) : ℝ

Reserved angular base, given by U * HeatedOutgoing.E F XR c ((r / Real.sqrt q) ^ 2 / 2, η).

Equations

• NavierStokes.MeanRankUpdate.reservedAngularBase F XR c q U η r = U * NavierStokes.HeatedOutgoing.E F XR c ((r / √q) ^ 2 / 2, η)

noncomputable def NavierStokes.MeanRankUpdate.reservedAxialBase (F : OutgoingProfile.Profile) (XR q U η r : ℝ) : ℝ

Reserved axial base, given by U * HeatedOutgoing.U F XR ((r / Real.sqrt q) ^ 2 / 2, η).

Equations

• NavierStokes.MeanRankUpdate.reservedAxialBase F XR q U η r = U * NavierStokes.HeatedOutgoing.U F XR ((r / √q) ^ 2 / 2, η)

theorem NavierStokes.MeanRankUpdate.reserved_five_rows (F : OutgoingProfile.Profile) {XR q : ℝ} (hXR : 0 < XR) (hq : 0 < q) (c : ℝ → HeatedOutgoing.Coeff) (A η : ℝ) (d : Debt) : FiveRowRank.FiveRows (reservedAngularBase F XR c q (q ^ (-A)) η) (reservedAxialBase F XR q (q ^ (-A)) η) d (angularIncrement F.data.core.lam (shapedAmplitude (ReservedPatches.radialAmplitude F XR 0) η) (ReservedPatches.radialSupportLeft F XR ReservedPatches.Slot.mean) (ReservedPatches.radialSupportRight F XR ReservedPatches.Slot.mean) (√q) (q ^ (-A)) d) (desiredAxialIncrement F.data.core.lam (shapedAmplitude (ReservedPatches.radialAmplitude F XR 0) η) (ReservedPatches.radialSupportLeft F XR ReservedPatches.Slot.mean) (ReservedPatches.radialSupportRight F XR ReservedPatches.Slot.mean) (√q) (q ^ (-A)) d)

The five-row repair on the actual untouched heated outgoing mean patch.

noncomputable def NavierStokes.MeanRankUpdate.SmoothFamily.ofReserved {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : OutgoingProfile.Profile) (XR : ℝ) (hXR : 0 < XR) (A : ℝ) (q η : E → ℝ) (d : E → Debt) (hq : ContDiff ℝ (↑⊤) q) (hη : ContDiff ℝ (↑⊤) η) (hd : ContDiff ℝ (↑⊤) d) (hqpos : ∀ (s : E), 0 < q s) : SmoothFamily E

Instantiating the actual reserved patch with any smooth physical q>0 and smooth slow defect family supplies all stream input data.

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.scaledPrimitive (f : ℝ → ℝ) (r : ℝ) : ℝ

A smooth formula for r⁻¹∫₀ʳ s f(s) ds, also defined at the axis.

Equations

• NavierStokes.MeanRankUpdate.scaledPrimitive f r = r * ∫ (t : ℝ) in 0..1, t * f (r * t)

theorem NavierStokes.MeanRankUpdate.scaledPrimitive_eq_integral (f : ℝ → ℝ) {r : ℝ} (hr : r ≠ 0) : scaledPrimitive f r = (∫ (s : ℝ) in 0..r, s * f s) / r

theorem NavierStokes.MeanRankUpdate.scaledPrimitive_zero_of_support {l u r : ℝ} (hl : 0 < l) : l < u → ∀ {f : ℝ → ℝ} (hs : tsupport f ⊆ Set.Ioo l u) (hm : ∫ (s : ℝ), s * f s = 0) (hr : r ∉ Set.Ioo l u), scaledPrimitive f r = 0

theorem NavierStokes.MeanRankUpdate.model_compactIntegral_smooth {S : Set ModelPoint} (hS : IsOpen S) {G : ModelPoint → ℝ → ℝ} (hG : ∀ y ∈ S, ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑⊤) (fun (z : ModelPoint × ℝ) => G z.1 z.2) (y, t)) : ContDiffOn ℝ (↑⊤) (fun (y : ModelPoint) => ∫ (t : ℝ) in 0..1, G y t) S

noncomputable def NavierStokes.MeanRankUpdate.primitiveModel (coord A B lam a b : ℝ) (d : Debt) (y : ModelPoint) : ℝ

Primitive model, given by scaledPrimitive (fun r => axialModel coord A B lam a b d (y.1, r, y.2.2)) y.2.1.

Equations

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

theorem NavierStokes.MeanRankUpdate.primitiveModel_contDiffOn (coord A B lam a b : ℝ) (hB : B ≠ 0) (d : Debt) : ContDiffOn ℝ (↑⊤) (primitiveModel coord A B lam a b d) PhysicalCoordinateBounds.positiveTime

theorem NavierStokes.MeanRankUpdate.primitiveModel_zero {coord A B lam a b : ℝ} (hlam : 0 < lam) (hB : B ≠ 0) (ha : 0 < a) (hab : a < b) (d : Debt) {y : ModelPoint} (hy : 0 < y.1) (hr : y.2.1 ∉ Set.Ioo (√y.1 * a) (√y.1 * b)) : primitiveModel coord A B lam a b d y = 0

theorem NavierStokes.MeanRankUpdate.primitive_kernel_zero {coord A B lam a b qlo qhi : ℝ} (hlam : 0 < lam) (hB : B ≠ 0) (ha : 0 < a) (hab : a < b) (hqlo : 0 < qlo) (d : Debt) {p : ChartPoint} (hq : chartQ coord p ∈ Set.Icc qlo qhi) (hp : p ∉ supportBand a b qlo qhi) : chartKernel coord (primitiveModel coord A B lam a b d) p = 0

theorem NavierStokes.MeanRankUpdate.meanClass_sum_basis {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] (s : WeightedClasses.StripData D) {α : ℝ} {d : ℕ → D → Debt} (hd : WeightedClasses.UnweightedClass s α d) (k : Fin 3 → D → ℝ) (hk : ∀ (i : Fin 3), WeightedClasses.MeanClass s 0 fun (x : ℕ) => k i) : WeightedClasses.MeanClass s α fun (n : ℕ) (p : D) => ∑ i : Fin 3, d n p i * k i p

noncomputable def NavierStokes.MeanRankUpdate.chartPotential (coord A B lam a b : ℝ) (d : ChartPoint → Debt) : ChartPoint → ℝ

Chart potential, defined pointwise by ∑ i : Fin 3, d p i * chartKernel coord (primitiveModel coord A B lam a b (Pi.single i 1)) p.

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.chartStreamRadial (coord A B lam a b : ℝ) (w : PressureStream.Plane × PressureStream.Plane) (d : ChartPoint → Debt) : ChartPoint → ℝ

Chart stream radial, given by PressureStream.streamBeta w (chartPotential coord A B lam a b d).

Equations

• NavierStokes.MeanRankUpdate.chartStreamRadial coord A B lam a b w d = NavierStokes.PressureStream.streamBeta w (NavierStokes.MeanRankUpdate.chartPotential coord A B lam a b d)

theorem NavierStokes.MeanRankUpdate.primitive_kernel_meanClass (s : WeightedClasses.StripData ChartPoint) {coord A B lam a b qlo qhi rlo rhi : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hqlo : 0 < qlo) (hT : ∀ p ∈ s.domain, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ s.domain, chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ s.domain, p.1 ∈ Set.Icc rlo rhi) (hz : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ s.domain, p ∈ supportBand a b qlo qhi → δ ≤ s.zeta p) (d : Debt) : WeightedClasses.MeanClass s 0 fun (x : ℕ) => chartKernel coord (primitiveModel coord A B lam a b d)

theorem NavierStokes.MeanRankUpdate.rank_stream_meanClass (s : WeightedClasses.StripData ChartPoint) {coord A B lam a b qlo qhi rlo rhi α : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hqlo : 0 < qlo) (hT : ∀ p ∈ s.domain, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ s.domain, chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ s.domain, p.1 ∈ Set.Icc rlo rhi) (hz : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ s.domain, p ∈ supportBand a b qlo qhi → δ ≤ s.zeta p) (w : PressureStream.Plane × PressureStream.Plane) {d : ℕ → ChartPoint → Debt} (hd : WeightedClasses.UnweightedClass s α d) : (WeightedClasses.MeanClass s α fun (n : ℕ) => chartPotential coord A B lam a b (d n)) ∧ WeightedClasses.MeanClass s α fun (n : ℕ) => chartStreamRadial coord A B lam a b w (d n)

The primitive and its actual slow derivative satisfy the same all-jet weighted class. This proves the radial component bound as well.

theorem NavierStokes.MeanRankUpdate.concrete_rank_stream_meanClass (coord qlo qhi rlo rhi cL cR A B lam a b α : ℝ) (hc : 0 < coord) (hc1 : coord < 1) (hqlo : 0 < qlo) (hrlo : 0 < rlo) (hcL : 0 < cL) (hcR : 0 < cR) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hleft : rlo < √qlo * a) (hright : √qhi * b < rhi) (ε S : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hεone : ∀ (n : ℕ), ε n ≤ 1) (hS : ∀ (n : ℕ), 1 ≤ S n) (w : PressureStream.Plane × PressureStream.Plane) {d : ℕ → ChartPoint → Debt} (hd : WeightedClasses.UnweightedClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α d) : (WeightedClasses.MeanClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α fun (n : ℕ) => chartPotential coord A B lam a b (d n)) ∧ WeightedClasses.MeanClass (normalizedStripData coord qlo qhi rlo rhi cL cR hc hc1 hrlo hcL hcR ε S hε hεone hS) α fun (n : ℕ) => chartStreamRadial coord A B lam a b w (d n)

theorem NavierStokes.MeanRankUpdate.radial_physical_scale_gain (s : WeightedClasses.StripData ChartPoint) {α : ℝ} {β : ℕ → ChartPoint → ℝ} (hβ : WeightedClasses.MeanClass s α β) : WeightedClasses.MeanClass s (α + 1) fun (n : ℕ) (p : ChartPoint) => s.epsilon n * β n p

theorem NavierStokes.MeanRankUpdate.scaledPrimitive_zero_below {l r : ℝ} (hl : 0 ≤ l) {f : ℝ → ℝ} (hf : ∀ x ≤ l, f x = 0) (hr : r ≤ l) : scaledPrimitive f r = 0

theorem NavierStokes.MeanRankUpdate.scaledPrimitive_sum (f : Fin 3 → ℝ → ℝ) (hf : ∀ (i : Fin 3), Continuous (f i)) (d : Debt) (r : ℝ) : scaledPrimitive (fun (x : ℝ) => ∑ i : Fin 3, d i * f i x) r = ∑ i : Fin 3, d i * scaledPrimitive (f i) r

theorem NavierStokes.MeanRankUpdate.chartPotential_eq_scaledPrimitive (coord A B lam a b : ℝ) (d : ChartPoint → Debt) (p : ChartPoint) : chartPotential coord A B lam a b d p = scaledPrimitive (desiredAxialIncrement lam (shapedAmplitude B (chartEta coord p)) a b (√(chartQ coord p)) (chartQ coord p ^ (-A)) (d p)) p.1

theorem NavierStokes.MeanRankUpdate.slow_streamPotential_eq_scaledPrimitive {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {lo hi power M : ℝ} (hlo : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported lo hi f) (hm : ∀ (s : E), ∫ (r : ℝ), r * f (r, s) = 0) (p : PressureStream.Lift E) : PressureStream.streamPotential power lo hi M (0, v) (slowLift f) p = scaledPrimitive (fun (r : ℝ) => f (r, p.2.1)) p.1

The stream is the ordinary zero-axis primitive for a slow zero-mass source. Thus neither its cutoff nor its transport parameter changes it.

theorem NavierStokes.MeanRankUpdate.slow_streamPotential_congr_slice {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (lo hi power M : ℝ) (v : PressureStream.Plane) {f g : ℝ × E → ℝ} (p : PressureStream.Lift E) (he : ∀ (r : ℝ), f (r, p.2.1) = g (r, p.2.1)) : PressureStream.streamPotential power lo hi M (0, v) (slowLift f) p = PressureStream.streamPotential power lo hi M (0, v) (slowLift g) p

theorem NavierStokes.MeanRankUpdate.slow_streamPotential_eq_scaledPrimitive_slice {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {lo hi power M : ℝ} (hlo : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (f : ℝ × E → ℝ) (p : PressureStream.Lift E) (hf : ContDiff ℝ ↑⊤ fun (r : ℝ) => f (r, p.2.1)) (hs : (Function.support fun (r : ℝ) => f (r, p.2.1)) ⊆ Set.Icc lo hi) (hm : ∫ (r : ℝ), r * f (r, p.2.1) = 0) : PressureStream.streamPotential power lo hi M (0, v) (slowLift f) p = scaledPrimitive (fun (r : ℝ) => f (r, p.2.1)) p.1

Only the radial slice is needed for this identity; no extension of the slow data outside its open physical domain is assumed.

noncomputable def NavierStokes.MeanRankUpdate.slowChartDesired (coord A B lam a b : ℝ) (d : PressureStream.Plane → Debt) : ℝ × PressureStream.Plane → ℝ

Slow chart desired, defined pointwise by chartAxial coord A B lam a b (fun z => d z.2.1) (p.1, p.2, 0).

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.actualChartPotential (coord A B lam a b power lo hi M : ℝ) (v : PressureStream.Plane) (d : PressureStream.Plane → Debt) : ChartPoint → ℝ

Actual chart potential, given by PressureStream.streamPotential power lo hi M ((0 : PressureStream.Plane), v) (slowLift (slowChartDesired coord A B lam a b d)).

Equations

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

noncomputable def NavierStokes.MeanRankUpdate.actualChartRadial (coord A B lam a b power lo hi M : ℝ) (v : PressureStream.Plane) (w : PressureStream.Plane × PressureStream.Plane) (d : PressureStream.Plane → Debt) : ChartPoint → ℝ

Actual chart radial, given by PressureStream.streamBeta w (actualChartPotential coord A B lam a b power lo hi M v d).

Equations

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

theorem NavierStokes.MeanRankUpdate.actualChartPotential_eq_chartPotential {coord A B lam a b power lo hi M qlo qhi : ℝ} (hlam : 0 < lam) (hB : B ≠ 0) (ha : 0 < a) (hab : a < b) (hp : 0 < power) (hlo : 0 < lo) (horder : lo < hi) (hqlo : 0 < qlo) (hleft : lo ≤ √qlo * a) (hright : √qhi * b ≤ hi) (v : PressureStream.Plane) (d : PressureStream.Plane → Debt) {p : ChartPoint} (hq : chartQ coord p ∈ Set.Icc qlo qhi) : actualChartPotential coord A B lam a b power lo hi M v d p = chartPotential coord A B lam a b (fun (z : ChartPoint) => d z.2.1) p

theorem NavierStokes.MeanRankUpdate.actual_rank_stream_meanClass (s : WeightedClasses.StripData ChartPoint) {coord A B lam a b power lo hi qlo qhi α : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hp : 0 < power) (hlo : 0 < lo) (horder : lo < hi) (hqlo : 0 < qlo) (hleft : lo ≤ √qlo * a) (hright : √qhi * b ≤ hi) (hT : ∀ p ∈ s.domain, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ s.domain, chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ s.domain, p.1 ∈ Set.Icc lo hi) (hz : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ s.domain, p ∈ supportBand a b qlo qhi → δ ≤ s.zeta p) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (w : PressureStream.Plane × PressureStream.Plane) {d : ℕ → PressureStream.Plane → Debt} (hd : WeightedClasses.UnweightedClass s α fun (n : ℕ) (p : ChartPoint) => d n p.2.1) : (WeightedClasses.MeanClass s α fun (n : ℕ) => actualChartPotential coord A B lam a b power lo hi (M n) (v n) (d n)) ∧ WeightedClasses.MeanClass s α fun (n : ℕ) => actualChartRadial coord A B lam a b power lo hi (M n) (v n) w (d n)

The full slow stream estimate is for the actual PressureStream operator. The proof does not extend data outside the positive-time domain.

theorem NavierStokes.MeanRankUpdate.fderiv_apply_eq_of_line_eq {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {f g : D → ℝ} {x : D} (v : D) (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (he : ∀ (t : ℝ), f (x + t • v) = g (x + t • v)) : (fderiv ℝ f x) v = (fderiv ℝ g x) v

theorem NavierStokes.MeanRankUpdate.slow_streamGamma_eq_desired_slice {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {lo hi power M : ℝ} (hlo : 0 < lo) (horder : lo < hi) (hp : 0 < power) (v : PressureStream.Plane) (f : ℝ × E → ℝ) (p : PressureStream.Lift E) (hf : ContDiff ℝ ↑⊤ fun (r : ℝ) => f (r, p.2.1)) (hs : (Function.support fun (r : ℝ) => f (r, p.2.1)) ⊆ Set.Icc lo hi) (hm : ∫ (r : ℝ), r * f (r, p.2.1) = 0) (hΨ : DifferentiableAt ℝ (PressureStream.streamPotential power lo hi M (0, v) (slowLift f)) p) : PressureStream.streamGamma (PressureStream.physicalSpeed power M) (0, v) (PressureStream.streamPotential power lo hi M (0, v) (slowLift f)) p = f (p.1, p.2.1)

A local differentiability hypothesis suffices for the true slow axial identity; the source need only be smooth along its radial slice.

noncomputable def NavierStokes.MeanRankUpdate.actualChartAxial (coord A B lam a b power lo hi M : ℝ) (v : PressureStream.Plane) (d : PressureStream.Plane → Debt) : ChartPoint → ℝ

Actual chart axial, constructed using PressureStream.streamGamma.

Equations

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

theorem NavierStokes.MeanRankUpdate.actualChartAxial_eq_desired {coord A B lam a b power lo hi M qlo qhi : ℝ} (hlam : 0 < lam) (hB : B ≠ 0) (ha : 0 < a) (hab : a < b) (hp : 0 < power) (hlo : 0 < lo) (horder : lo < hi) (hqlo : 0 < qlo) (hleft : lo ≤ √qlo * a) (hright : √qhi * b ≤ hi) (v : PressureStream.Plane) (d : PressureStream.Plane → Debt) {p : ChartPoint} (hq : chartQ coord p ∈ Set.Icc qlo qhi) (hΨ : DifferentiableAt ℝ (actualChartPotential coord A B lam a b power lo hi M v d) p) : actualChartAxial coord A B lam a b power lo hi M v d p = slowChartDesired coord A B lam a b d (p.1, p.2.1)

theorem NavierStokes.MeanRankUpdate.actual_rank_stream_identities (s : WeightedClasses.StripData ChartPoint) {coord A B lam a b power lo hi qlo qhi α : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hp : 0 < power) (hlo : 0 < lo) (horder : lo < hi) (hqlo : 0 < qlo) (hleft : lo ≤ √qlo * a) (hright : √qhi * b ≤ hi) (hT : ∀ p ∈ s.domain, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ s.domain, chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ s.domain, p.1 ∈ Set.Icc lo hi) (hz : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ s.domain, p ∈ supportBand a b qlo qhi → δ ≤ s.zeta p) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (w : PressureStream.Plane × PressureStream.Plane) {d : ℕ → PressureStream.Plane → Debt} (hd : WeightedClasses.UnweightedClass s α fun (n : ℕ) (p : ChartPoint) => d n p.2.1) (n : ℕ) (p : ChartPoint) : p ∈ s.domain → actualChartAxial coord A B lam a b power lo hi (M n) (v n) (d n) p = slowChartDesired coord A B lam a b (d n) (p.1, p.2.1) ∧ PressureStream.graphDivergence (PressureStream.physicalSpeed power (M n)) (0, v n) w (actualChartRadial coord A B lam a b power lo hi (M n) (v n) w (d n)) (actualChartAxial coord A B lam a b power lo hi (M n) (v n) (d n)) p = 0

Exact slow realization and divergence on the actual normalized physical domain, derived from the input defect class rather than assumed regularity.

theorem NavierStokes.MeanRankUpdate.actual_rank_velocity_meanClass (s : WeightedClasses.StripData ChartPoint) {coord A B lam a b power lo hi qlo qhi α : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (hlam : 0 < lam) (ha : 0 < a) (hab : a < b) (hB : B ≠ 0) (hp : 0 < power) (hlo : 0 < lo) (horder : lo < hi) (hqlo : 0 < qlo) (hleft : lo ≤ √qlo * a) (hright : √qhi * b ≤ hi) (hT : ∀ p ∈ s.domain, chartInput p ∈ PhysicalCoordinateBounds.positiveTime) (hq : ∀ p ∈ s.domain, chartQ coord p ∈ Set.Icc qlo qhi) (hR : ∀ p ∈ s.domain, p.1 ∈ Set.Icc lo hi) (hz : ∃ (δ : ℝ), 0 < δ ∧ ∀ p ∈ s.domain, p ∈ supportBand a b qlo qhi → δ ≤ s.zeta p) (M : ℕ → ℝ) (v : ℕ → PressureStream.Plane) (w : PressureStream.Plane × PressureStream.Plane) {d : ℕ → PressureStream.Plane → Debt} (hd : WeightedClasses.UnweightedClass s α fun (n : ℕ) (p : ChartPoint) => d n p.2.1) : (WeightedClasses.MeanClass s α fun (n : ℕ) => chartAngular coord A B lam a b fun (p : ChartPoint) => d n p.2.1) ∧ (WeightedClasses.MeanClass s α fun (n : ℕ) => actualChartAxial coord A B lam a b power lo hi (M n) (v n) (d n)) ∧ WeightedClasses.MeanClass s α fun (n : ℕ) => actualChartRadial coord A B lam a b power lo hi (M n) (v n) w (d n)

theorem NavierStokes.MeanRankUpdate.slow_streamPotential_phase_independent {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (lo hi power M : ℝ) (v : PressureStream.Plane) (f : ℝ × E → ℝ) (r : ℝ) (s : E) (Y Y' : PressureStream.Plane) : PressureStream.streamPotential power lo hi M (0, v) (slowLift f) (r, s, Y) = PressureStream.streamPotential power lo hi M (0, v) (slowLift f) (r, s, Y')

theorem NavierStokes.MeanRankUpdate.slow_streamBeta_eq_slow_direction {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (lo hi power M : ℝ) (v : PressureStream.Plane) (f : ℝ × E → ℝ) (w : E) (wfast : PressureStream.Plane) (p : PressureStream.Lift E) (hΨ : DifferentiableAt ℝ (PressureStream.streamPotential power lo hi M (0, v) (slowLift f)) p) : PressureStream.streamBeta (w, wfast) (PressureStream.streamPotential power lo hi M (0, v) (slowLift f)) p = PressureStream.streamBeta (w, 0) (PressureStream.streamPotential power lo hi M (0, v) (slowLift f)) p

Arbitrarily large fast parts of the axial graph direction vanish exactly for the slow rank stream. They cannot create a band-dependent loss.