Pressure and divergence reconstruction with the exact compactification error

The radial primitives are the actual transport integrals. Slow parameters are retained separately from the two auxiliary torus coordinates. The pressure correction uses a constructed smooth bump of integral one.

@[reducible, inline]

abbrev NavierStokes.PressureStream.Plane : Type

Plane: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.PressureStream.Plane = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.PressureStream.Lift (S : Type) : Type

Lift: an abbreviation for ℝ × (S × Plane).

Equations

• NavierStokes.PressureStream.Lift S = (ℝ × S × NavierStokes.PressureStream.Plane)

noncomputable def NavierStokes.PressureStream.meanBump (a b : ℝ) (hab : a < b) : ContDiffBump ((a + b) / 2)

A concrete bump strictly inside the radial interval.

Equations

• NavierStokes.PressureStream.meanBump a b hab = { rIn := (b - a) / 8, rOut := (b - a) / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def NavierStokes.PressureStream.rho (a b : ℝ) (hab : a < b) : ℝ → ℝ

The actual radial density has integral one, with no normalization premise.

Equations

• NavierStokes.PressureStream.rho a b hab = (NavierStokes.PressureStream.meanBump a b hab).normed MeasureTheory.volume

theorem NavierStokes.PressureStream.rho_contDiff (a b : ℝ) (hab : a < b) : ContDiff ℝ (↑⊤) (rho a b hab)

theorem NavierStokes.PressureStream.rho_integrable (a b : ℝ) (hab : a < b) : MeasureTheory.Integrable (rho a b hab) MeasureTheory.volume

theorem NavierStokes.PressureStream.rho_integral (a b : ℝ) (hab : a < b) : ∫ (r : ℝ), rho a b hab r = 1

theorem NavierStokes.PressureStream.rho_nonneg (a b : ℝ) (hab : a < b) (r : ℝ) : 0 ≤ rho a b hab r

theorem NavierStokes.PressureStream.rho_support (a b : ℝ) (hab : a < b) : Function.support (rho a b hab) ⊆ Set.Icc a b

theorem NavierStokes.PressureStream.rho_hasCompactSupport (a b : ℝ) (hab : a < b) : HasCompactSupport (rho a b hab)

noncomputable def NavierStokes.PressureStream.torusInner {S : Type} (f : Lift S → ℝ) (p : (ℝ × S) × ℝ) : ℝ

Torus inner, given by ∫ x in (0 : ℝ)..1, f (p.1.1, (p.1.2, (x, p.2))).

Equations

• NavierStokes.PressureStream.torusInner f p = ∫ (x : ℝ) in 0..1, f (p.1.1, p.1.2, x, p.2)

noncomputable def NavierStokes.PressureStream.torusAverage {S : Type} (f : Lift S → ℝ) (p : ℝ × S) : ℝ

The bar averages only the auxiliary torus, preserving every slow parameter.

Equations

• NavierStokes.PressureStream.torusAverage f p = ∫ (y : ℝ) in 0..1, NavierStokes.PressureStream.torusInner f (p, y)

theorem NavierStokes.PressureStream.torusInner_contDiff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (torusInner f)

theorem NavierStokes.PressureStream.torusAverage_contDiff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (torusAverage f)

theorem NavierStokes.PressureStream.torusAverage_zero_of_forall {S : Type} {f : Lift S → ℝ} {p : ℝ × S} (hzero : ∀ (Y : Plane), f (p.1, p.2, Y) = 0) : torusAverage f p = 0

theorem NavierStokes.PressureStream.torusAverage_supported {S : Type} {a b : ℝ} {f : Lift S → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (torusAverage f)

theorem NavierStokes.PressureStream.torusAverage_sub_slow {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (g : ℝ × S → ℝ) (p : ℝ × S) : torusAverage (fun (q : Lift S) => f q - g (q.1, q.2.1)) p = torusAverage f p - g p

noncomputable def NavierStokes.PressureStream.pressureMass {S : Type} (f : Lift S → ℝ) (s : S) : ℝ

Pressure mass, given by ∫ r, torusAverage f (r, s).

Equations

• NavierStokes.PressureStream.pressureMass f s = ∫ (r : ℝ), NavierStokes.PressureStream.torusAverage f (r, s)

theorem NavierStokes.PressureStream.torusAverage_slice_integrable {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (s : S) : MeasureTheory.Integrable (fun (r : ℝ) => torusAverage f (r, s)) MeasureTheory.volume

theorem NavierStokes.PressureStream.pressureMass_eq_interval {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (s : S) : pressureMass f s = ∫ (r : ℝ) in a..b, torusAverage f (r, s)

theorem NavierStokes.PressureStream.pressureMass_contDiff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (pressureMass f)

noncomputable def NavierStokes.PressureStream.pressureSource {S : Type} (a b : ℝ) (hab : a < b) (f : Lift S → ℝ) (p : Lift S) : ℝ

Pressure source, given by f p - rho a b hab p.1 * pressureMass f p.2.1.

Equations

• NavierStokes.PressureStream.pressureSource a b hab f p = f p - NavierStokes.PressureStream.rho a b hab p.1 * NavierStokes.PressureStream.pressureMass f p.2.1

theorem NavierStokes.PressureStream.pressureSource_contDiff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (hab : a < b) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (pressureSource a b hab f)

theorem NavierStokes.PressureStream.pressureSource_supported {S : Type} {a b : ℝ} (hab : a < b) {f : Lift S → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (pressureSource a b hab f)

theorem NavierStokes.PressureStream.torusAverage_pressureSource {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (hab : a < b) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (p : ℝ × S) : torusAverage (pressureSource a b hab f) p = torusAverage f p - rho a b hab p.1 * pressureMass f p.2

theorem NavierStokes.PressureStream.pressureSource_mass_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {a b : ℝ} (hab : a < b) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (s : S) : pressureMass (pressureSource a b hab f) s = 0

The corrected pressure source has zero integrated torus mean, derived from the integral-one bump rather than imposed as a hypothesis.

noncomputable def NavierStokes.PressureStream.radialVector {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (k : ℝ → ℝ) (v : E) (p : ℝ × E) : ℝ × E

Radial vector, given by (1, k p.1 • v).

Equations

• NavierStokes.PressureStream.radialVector k v p = (1, k p.1 • v)

noncomputable def NavierStokes.PressureStream.graphDr {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (k : ℝ → ℝ) (v : E) (f : ℝ × E → ℝ) (p : ℝ × E) : ℝ

The exact radial graph derivative. The directions are fixed; only its radial speed is allowed to vary with the slow radius.

Equations

• NavierStokes.PressureStream.graphDr k v f p = (fderiv ℝ f p) (NavierStokes.PressureStream.radialVector k v p)

noncomputable def NavierStokes.PressureStream.graphDz {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (w : E) (f : ℝ × E → ℝ) (p : ℝ × E) : ℝ

A fixed axial graph direction may include both slow and torus directions.

Equations

• NavierStokes.PressureStream.graphDz w f p = (fderiv ℝ f p) (0, w)

theorem NavierStokes.PressureStream.graphDz_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (w : E) : ContDiff ℝ (↑⊤) (graphDz w f)

theorem NavierStokes.PressureStream.graphDr_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → ℝ} {k : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hk : ContDiff ℝ (↑⊤) k) (v : E) : ContDiff ℝ (↑⊤) (graphDr k v f)

theorem NavierStokes.PressureStream.radialVector_hasFDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℝ → ℝ} (v : E) {p : ℝ × E} (hk : DifferentiableAt ℝ k p.1) : HasFDerivAt (radialVector k v) (ContinuousLinearMap.prod 0 ((fderiv ℝ k p.1 ∘SL ContinuousLinearMap.fst ℝ ℝ E).smulRight v)) p

theorem NavierStokes.PressureStream.radialVector_cross_derivative {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℝ → ℝ} (v w : E) {p : ℝ × E} (hk : DifferentiableAt ℝ k p.1) : (fderiv ℝ (radialVector k v) p) (0, w) = 0

theorem NavierStokes.PressureStream.graphDr_graphDz_comm {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → ℝ} {k : ℝ → ℝ} (v w : E) {p : ℝ × E} (hf : ContDiffAt ℝ 2 f p) (hk : DifferentiableAt ℝ k p.1) : graphDr k v (graphDz w f) p = graphDz w (graphDr k v f) p

Exact commutation is proved from symmetry of the second derivative and the vanishing cross derivative of the radial vector field.

noncomputable def NavierStokes.PressureStream.divideRadius {E : Type} (f : ℝ × E → ℝ) (p : ℝ × E) : ℝ

Divide radius, given by f p / p.1.

Equations

• NavierStokes.PressureStream.divideRadius f p = f p / p.1

theorem NavierStokes.PressureStream.divideRadius_supported {E : Type} {a b : ℝ} {f : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (divideRadius f)

theorem NavierStokes.PressureStream.divideRadius_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (ha : 0 < a) {f : ℝ × E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (divideRadius f)

Division by radius is harmless for a smooth field supported away from the axis.

theorem NavierStokes.PressureStream.graphDr_neg {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → ℝ} {k : ℝ → ℝ} (v : E) {p : ℝ × E} (hf : DifferentiableAt ℝ f p) : graphDr k v (fun (q : ℝ × E) => -f q) p = -graphDr k v f p

theorem NavierStokes.PressureStream.graphDz_add {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ × E → ℝ} (w : E) {p : ℝ × E} (hf : DifferentiableAt ℝ f p) (hg : DifferentiableAt ℝ g p) : graphDz w (fun (q : ℝ × E) => f q + g q) p = graphDz w f p + graphDz w g p

theorem NavierStokes.PressureStream.divideRadius_hasFDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → ℝ} {p : ℝ × E} (hf : DifferentiableAt ℝ f p) (hr : p.1 ≠ 0) : HasFDerivAt (divideRadius f) (f p • -(p.1 ^ 2)⁻¹ • ContinuousLinearMap.fst ℝ ℝ E + p.1⁻¹ • fderiv ℝ f p) p

theorem NavierStokes.PressureStream.graphDz_divideRadius {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → ℝ} (w : E) {p : ℝ × E} (hf : DifferentiableAt ℝ f p) (hr : p.1 ≠ 0) : graphDz w (divideRadius f) p = graphDz w f p / p.1

theorem NavierStokes.PressureStream.graphDr_divideRadius {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × E → ℝ} (k : ℝ → ℝ) (v : E) {p : ℝ × E} (hf : DifferentiableAt ℝ f p) (hr : p.1 ≠ 0) : graphDr k v (divideRadius f) p + divideRadius f p / p.1 = graphDr k v f p / p.1

noncomputable def NavierStokes.PressureStream.streamBeta {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (w : E) (Ψ : ℝ × E → ℝ) : ℝ × E → ℝ

Stream beta, defined pointwise by -graphDz w Ψ p.

Equations

• NavierStokes.PressureStream.streamBeta w Ψ p = -NavierStokes.PressureStream.graphDz w Ψ p

noncomputable def NavierStokes.PressureStream.streamGamma {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (k : ℝ → ℝ) (v : E) (Ψ : ℝ × E → ℝ) : ℝ × E → ℝ

Stream gamma, defined pointwise by graphDr k v Ψ p + divideRadius Ψ p.

Equations

• NavierStokes.PressureStream.streamGamma k v Ψ p = NavierStokes.PressureStream.graphDr k v Ψ p + NavierStokes.PressureStream.divideRadius Ψ p

noncomputable def NavierStokes.PressureStream.graphDivergence {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (k : ℝ → ℝ) (v w : E) (β γ : ℝ × E → ℝ) (p : ℝ × E) : ℝ

Graph divergence, given by graphDr k v β p + β p / p.1 + graphDz w γ p.

Equations

• NavierStokes.PressureStream.graphDivergence k v w β γ p = NavierStokes.PressureStream.graphDr k v β p + β p / p.1 + NavierStokes.PressureStream.graphDz w γ p

theorem NavierStokes.PressureStream.stream_divergence_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {Ψ : ℝ × E → ℝ} {k : ℝ → ℝ} (v w : E) {p : ℝ × E} (hΨ : ContDiffAt ℝ 2 Ψ p) (hk : DifferentiableAt ℝ k p.1) (hr : p.1 ≠ 0) : graphDivergence k v w (streamBeta w Ψ) (streamGamma k v Ψ) p = 0

The cylindrical divergence of the actual stream realization is exactly zero.

theorem NavierStokes.PressureStream.graphDr_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported a b f) (k : ℝ → ℝ) (v : E) : RadialAlias.RadiallySupported a b (graphDr k v f)

theorem NavierStokes.PressureStream.graphDz_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported a b f) (w : E) : RadialAlias.RadiallySupported a b (graphDz w f)

theorem NavierStokes.PressureStream.graphDr_contDiff_of_support {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (ha : 0 < a) {f : ℝ × E → ℝ} {k : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hk : ∀ (r : ℝ), r ≠ 0 → ContDiffAt ℝ (↑⊤) k r) (v : E) : ContDiff ℝ (↑⊤) (graphDr k v f)

noncomputable def NavierStokes.PressureStream.physicalSpeed (d M r : ℝ) : ℝ

Physical speed, given by RadialPullback.radialJacobian d r * M.

Equations

• NavierStokes.PressureStream.physicalSpeed d M r = NavierStokes.RadialPullback.radialJacobian d r * M

theorem NavierStokes.PressureStream.physicalSpeed_smooth (d M : ℝ) {r : ℝ} (hr : r ≠ 0) : ContDiffAt ℝ (↑⊤) (physicalSpeed d M) r

theorem NavierStokes.PressureStream.graphDr_eq_physical {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (d M : ℝ) (v : E) (f : ℝ × E → ℝ) (p : ℝ × E) : graphDr (physicalSpeed d M) v f p = RadialPullback.physicalGraphDeriv d M v f p

noncomputable def NavierStokes.PressureStream.meanPressure {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (hab : a < b) (v : Plane) (f : Lift S → ℝ) : Lift S → ℝ

Formula (33), with the exact physical shifted primitive.

Equations

• NavierStokes.PressureStream.meanPressure d a b M hab v f = NavierStokes.RadialPullback.physicalCompact d a b M (0, v) (NavierStokes.PressureStream.pressureSource a b hab f)

noncomputable def NavierStokes.PressureStream.pressureAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] (d a b M : ℝ) (hab : a < b) (v : Plane) (f : Lift S → ℝ) : Lift S → ℝ

Pressure alias, given by RadialPullback.physicalAlias d a b M (0, v) (pressureSource a b hab f).

Equations

• NavierStokes.PressureStream.pressureAlias d a b M hab v f = NavierStokes.RadialPullback.physicalAlias d a b M (0, v) (NavierStokes.PressureStream.pressureSource a b hab f)

theorem NavierStokes.PressureStream.meanPressure_contDiff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : ContDiff ℝ (↑⊤) (meanPressure d a b M hab v f)

theorem NavierStokes.PressureStream.meanPressure_supported {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) : RadialAlias.RadiallySupported a b (meanPressure d a b M hab v f)

theorem NavierStokes.PressureStream.meanPressure_radial_residual {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (p : Lift S) (hp : a ≤ p.1) : graphDr (physicalSpeed d M) (0, v) (meanPressure d a b M hab v f) p - f p = -rho a b hab p.1 * pressureMass f p.2.1 - pressureAlias d a b M hab v f p

The pressure residual retains the entire cutoff alias with its minus sign.

noncomputable def NavierStokes.PressureStream.weightedSource {E : Type} (γd : ℝ × E → ℝ) (p : ℝ × E) : ℝ

Weighted source, given by p.1 * γd p.

Equations

• NavierStokes.PressureStream.weightedSource γd p = p.1 * γd p

theorem NavierStokes.PressureStream.weightedSource_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) : ContDiff ℝ (↑⊤) (weightedSource γd)

theorem NavierStokes.PressureStream.weightedSource_supported {E : Type} {a b : ℝ} {γd : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported a b γd) : RadialAlias.RadiallySupported a b (weightedSource γd)

noncomputable def NavierStokes.PressureStream.streamPotential {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (d a b M : ℝ) (v : E) (γd : ℝ × E → ℝ) : ℝ × E → ℝ

The actual physical stream r⁻¹ Ic(r γd).

Equations

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

theorem NavierStokes.PressureStream.streamPotential_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : E) {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) : ContDiff ℝ (↑⊤) (streamPotential d a b M v γd)

theorem NavierStokes.PressureStream.streamPotential_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : E) {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) : RadialAlias.RadiallySupported a b (streamPotential d a b M v γd)

theorem NavierStokes.PressureStream.streamBeta_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v w : E) {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) : ContDiff ℝ (↑⊤) (streamBeta w (streamPotential d a b M v γd))

theorem NavierStokes.PressureStream.streamGamma_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : E) {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) : ContDiff ℝ (↑⊤) (streamGamma (physicalSpeed d M) v (streamPotential d a b M v γd))

theorem NavierStokes.PressureStream.streamGamma_eq_desired_sub_alias {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : E) {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) (p : ℝ × E) (hp : a ≤ p.1) : streamGamma (physicalSpeed d M) v (streamPotential d a b M v γd) p = γd p - RadialPullback.physicalAlias d a b M v (weightedSource γd) p / p.1

The constructed axial increment is the desired field minus the exact compactification defect divided by radius.

theorem NavierStokes.PressureStream.reconstructed_divergence_zero_of_ne {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v w : E) {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) (p : ℝ × E) (hp : p.1 ≠ 0) : graphDivergence (physicalSpeed d M) v w (streamBeta w (streamPotential d a b M v γd)) (streamGamma (physicalSpeed d M) v (streamPotential d a b M v γd)) p = 0

noncomputable def NavierStokes.PressureStream.TorusPeriodicLift {S : Type} (f : Lift S → ℝ) : Prop

Torus periodic lift, given by ∀ r : ℝ, ∀ s : S, FourierAlias.TorusPeriodic (fun Y => f (r, (s, Y))).

Equations

• NavierStokes.PressureStream.TorusPeriodicLift f = ∀ (r : ℝ) (s : S), NavierStokes.FourierAlias.TorusPeriodic fun (Y : NavierStokes.TorusInverse.Plane) => f (r, s, Y)

theorem NavierStokes.PressureStream.torusAverage_congr_slice {S : Type} {f g : Lift S → ℝ} (p : ℝ × S) (h : ∀ (Y : Plane), f (p.1, p.2, Y) = g (p.1, p.2, Y)) : torusAverage f p = torusAverage g p

theorem NavierStokes.PressureStream.torusAverage_divideRadius {S : Type} (f : Lift S → ℝ) (p : ℝ × S) : torusAverage (divideRadius f) p = torusAverage f p / p.1

theorem NavierStokes.PressureStream.torusAverage_weightedSource {S : Type} (f : Lift S → ℝ) (p : ℝ × S) : torusAverage (weightedSource f) p = p.1 * torusAverage f p

theorem NavierStokes.PressureStream.pressureSource_periodic {S : Type} {a b : ℝ} (hab : a < b) {f : Lift S → ℝ} (hp : TorusPeriodicLift f) : TorusPeriodicLift (pressureSource a b hab f)

theorem NavierStokes.PressureStream.weightedSource_periodic {S : Type} {f : Lift S → ℝ} (hp : TorusPeriodicLift f) : TorusPeriodicLift (weightedSource f)

theorem NavierStokes.PressureStream.torusMean_shifted_integral {S : Type} [NormedAddCommGroup S] {a b : ℝ} (hab : a ≤ b) {f : Lift S → ℝ} (hf : Continuous f) (hp : TorusPeriodicLift f) {φ : ℝ → ℝ} (hφ : Continuous φ) (v : Plane) (s : S) : (FourierAlias.torusMean fun (Y : TorusInverse.Plane) => ∫ (r : ℝ) in a..b, f (r, s, Y + φ r • v)) = ∫ (r : ℝ) in a..b, torusAverage f (r, s)

Fubini and translation invariance give the mean of a genuinely shifted physical radial integral, retaining all slow parameters.

theorem NavierStokes.PressureStream.physicalAlias_slice_continuous {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (p : ℝ × S) : Continuous fun (Y : Plane) => RadialPullback.physicalAlias d a b M (0, v) f (p.1, p.2, Y)

theorem NavierStokes.PressureStream.torusAverage_physicalAlias {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hp : TorusPeriodicLift f) (p : ℝ × S) : torusAverage (RadialPullback.physicalAlias d a b M (0, v) f) p = RadialPullback.radialJacobian d p.1 * deriv (TransportPrimitive.interiorCutoff (a ^ d) (b ^ d)) (RadialPullback.powerChart d a p.1) * pressureMass f p.2

The exact alias mean is the radial mean mass times its cutoff derivative. The source need not have zero torus mean at each radius.

theorem NavierStokes.PressureStream.pressureAlias_mean_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hp : TorusPeriodicLift f) (p : ℝ × S) : torusAverage (pressureAlias d a b M hab v f) p = 0

theorem NavierStokes.PressureStream.torusAverage_physicalCompact {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hp : TorusPeriodicLift f) (p : ℝ × S) (hr : a ≤ p.1) : torusAverage (RadialPullback.physicalCompact d a b M (0, v) f) p = (∫ (r : ℝ) in a..p.1, torusAverage f (r, p.2)) - TransportPrimitive.interiorCutoff (a ^ d) (b ^ d) (p.1 ^ d) * pressureMass f p.2

Taking the torus mean of the physical compact primitive gives the ordinary radial compact primitive, with its exact mean-mass term.

theorem NavierStokes.PressureStream.torusAverage_physicalCompact_of_mass_zero {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hp : TorusPeriodicLift f) (p : ℝ × S) (hm : pressureMass f p.2 = 0) : torusAverage (RadialPullback.physicalCompact d a b M (0, v) f) p = ∫ (r : ℝ) in a..p.1, torusAverage f (r, p.2)

Zero integrated bar mass removes the compactification term from the bar exactly. This is an identity on the whole radial line.

theorem NavierStokes.PressureStream.meanPressure_bar_eq_integral {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hp : TorusPeriodicLift f) (p : ℝ × S) : torusAverage (meanPressure d a b M hab v f) p = ∫ (r : ℝ) in a..p.1, torusAverage f (r, p.2) - rho a b hab r * pressureMass f p.2

theorem NavierStokes.PressureStream.meanPressure_bar_hasDerivAt {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (hp : TorusPeriodicLift f) (s : S) (r : ℝ) : HasDerivAt (fun (R : ℝ) => torusAverage (meanPressure d a b M hab v f) (R, s)) (torusAverage f (r, s) - rho a b hab r * pressureMass f s) r

The derivative of the actual mean pressure, needed for weighted moment integration. It is derived from the integral reconstruction.

theorem NavierStokes.PressureStream.streamBeta_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {Ψ : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported a b Ψ) (w : E) : RadialAlias.RadiallySupported a b (streamBeta w Ψ)

theorem NavierStokes.PressureStream.streamGamma_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {Ψ : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported a b Ψ) (k : ℝ → ℝ) (v : E) : RadialAlias.RadiallySupported a b (streamGamma k v Ψ)

theorem NavierStokes.PressureStream.reconstructed_divergence_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v w : E) {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) (p : ℝ × E) : graphDivergence (physicalSpeed d M) v w (streamBeta w (streamPotential d a b M v γd)) (streamGamma (physicalSpeed d M) v (streamPotential d a b M v γd)) p = 0

The support proof handles the axis as well as the positive annulus.

theorem NavierStokes.PressureStream.streamGamma_eq_desired_sub_alias_global {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : E) {γd : ℝ × E → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) (p : ℝ × E) : streamGamma (physicalSpeed d M) v (streamPotential d a b M v γd) p = γd p - RadialPullback.physicalAlias d a b M v (weightedSource γd) p / p.1

noncomputable def NavierStokes.PressureStream.physicalTotal {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (d a M : ℝ) (v : E) (g : ℝ × E → ℝ) (p : ℝ × E) : ℝ

The total physical radial integral, written in normalized transport coordinates.

Equations

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

theorem NavierStokes.PressureStream.physicalTotal_eq_integral {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : E) {g : ℝ × E → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hs : RadialAlias.RadiallySupported a b g) (p : ℝ × E) (hp : a ≤ p.1) : physicalTotal d a M v g p = ∫ (r : ℝ) in a..b, g (r, p.2 + (M * (r ^ d - p.1 ^ d)) • v)

theorem NavierStokes.PressureStream.meanPressure_radial_residual_global {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (p : Lift S) : graphDr (physicalSpeed d M) (0, v) (meanPressure d a b M hab v f) p - f p = -rho a b hab p.1 * pressureMass f p.2.1 - pressureAlias d a b M hab v f p

theorem NavierStokes.PressureStream.meanPressure_radial_residual_cutoff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported a b f) (p : Lift S) : graphDr (physicalSpeed d M) (0, v) (meanPressure d a b M hab v f) p - f p = -rho a b hab p.1 * pressureMass f p.2.1 - deriv (RadialPullback.physicalCutoff d a b) p.1 * physicalTotal d a M (0, v) (pressureSource a b hab f) p

Formula (33), with the physical cutoff derivative and total primitive fully displayed. No radial-cutoff commutator is discarded.

theorem NavierStokes.PressureStream.torusAverage_sub {S : Type} [NormedAddCommGroup S] {f g : Lift S → ℝ} (hf : Continuous f) (hg : Continuous g) (p : ℝ × S) : torusAverage (fun (q : Lift S) => f q - g q) p = torusAverage f p - torusAverage g p

theorem NavierStokes.PressureStream.torusAverage_slice_contDiff {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {f : Lift S → ℝ} (hf : ContDiff ℝ (↑⊤) f) (s : S) : ContDiff ℝ ↑⊤ fun (r : ℝ) => torusAverage f (r, s)

theorem NavierStokes.PressureStream.torusAverage_slice_hasCompactSupport {S : Type} {a b : ℝ} {f : Lift S → ℝ} (hs : RadialAlias.RadiallySupported a b f) (s : S) : HasCompactSupport fun (r : ℝ) => torusAverage f (r, s)

theorem NavierStokes.PressureStream.streamGamma_bar_eq_desired {S : Type} [NormedAddCommGroup S] [NormedSpace ℝ S] {d a b M : ℝ} (ha : 0 < a) (hab : a < b) (hd : 0 < d) (v : Plane) {γd : Lift S → ℝ} (hγ : ContDiff ℝ (↑⊤) γd) (hs : RadialAlias.RadiallySupported a b γd) (hp : TorusPeriodicLift γd) (hm : ∀ (s : S), ∫ (r : ℝ), r * torusAverage γd (r, s) = 0) (p : ℝ × S) : torusAverage (streamGamma (physicalSpeed d M) (0, v) (streamPotential d a b M (0, v) γd)) p = torusAverage γd p

Zero weighted bar mass yields precisely the prescribed axial bar, although the full axial field includes the nonzero compactification alias.