The actual compact signed-stress primitive

A positive normalized bump is constructed in a chosen interior slow patch. Subtracting its exact weighted moment makes the negative radial primitive compact. The physical construction is normalized by the physical scale.

structure NavierStokes.SignedStressPrimitive.Patch : Type

Patch data, collecting a, b, left, right, a_pos, a_lt_left and their compatibility conditions.

• a : ℝ

  A of Patch, of type ℝ.

• b : ℝ

  B of Patch, of type ℝ.

• left : ℝ

  Left of Patch, of type ℝ.

• right : ℝ

  Right of Patch, of type ℝ.

• a_pos : 0 < self.a
• a_lt_left : self.a < self.left
• left_lt_right : self.left < self.right
• right_lt_b : self.right < self.b

theorem NavierStokes.SignedStressPrimitive.Patch.a_lt_b (P : Patch) : P.a < P.b

theorem NavierStokes.SignedStressPrimitive.Patch.left_pos (P : Patch) : 0 < P.left

noncomputable def NavierStokes.SignedStressPrimitive.density (P : Patch) : ℝ → ℝ

Density, given by PressureStream.rho P.left P.right P.left_lt_right.

Equations

• NavierStokes.SignedStressPrimitive.density P = NavierStokes.PressureStream.rho P.left P.right ⋯

theorem NavierStokes.SignedStressPrimitive.density_contDiff (P : Patch) : ContDiff ℝ (↑⊤) (density P)

theorem NavierStokes.SignedStressPrimitive.density_support (P : Patch) : Function.support (density P) ⊆ Set.Icc P.left P.right

theorem NavierStokes.SignedStressPrimitive.density_integral (P : Patch) : ∫ (r : ℝ), density P r = 1

theorem NavierStokes.SignedStressPrimitive.density_nonneg (P : Patch) (r : ℝ) : 0 ≤ density P r

noncomputable def NavierStokes.SignedStressPrimitive.densityLift (P : Patch) (z : ℝ × ℝ) : ℝ

Density lift, given by density P z.1.

Equations

• NavierStokes.SignedStressPrimitive.densityLift P z = NavierStokes.SignedStressPrimitive.density P z.1

theorem NavierStokes.SignedStressPrimitive.densityLift_contDiff (P : Patch) : ContDiff ℝ (↑⊤) (densityLift P)

theorem NavierStokes.SignedStressPrimitive.densityLift_supported (P : Patch) : RadialAlias.RadiallySupported P.left P.right (densityLift P)

noncomputable def NavierStokes.SignedStressPrimitive.cutoff (P : Patch) (r : ℝ) : ℝ

Cutoff, given by TransportPrimitive.pastIntegral 0 (0 : ℝ) (densityLift P) (r, 0).

Equations

• NavierStokes.SignedStressPrimitive.cutoff P r = NavierStokes.TransportPrimitive.pastIntegral 0 0 (NavierStokes.SignedStressPrimitive.densityLift P) (r, 0)

theorem NavierStokes.SignedStressPrimitive.cutoff_contDiff (P : Patch) : ContDiff ℝ (↑⊤) (cutoff P)

theorem NavierStokes.SignedStressPrimitive.cutoff_total (P : Patch) (r : ℝ) : TransportPrimitive.totalIntegral 0 0 (densityLift P) (r, 0) = 1

theorem NavierStokes.SignedStressPrimitive.cutoff_zero (P : Patch) {r : ℝ} (hr : r ≤ P.left) : cutoff P r = 0

theorem NavierStokes.SignedStressPrimitive.cutoff_one (P : Patch) {r : ℝ} (hr : P.right ≤ r) : cutoff P r = 1

theorem NavierStokes.SignedStressPrimitive.cutoff_hasDerivAt (P : Patch) (r : ℝ) : HasDerivAt (cutoff P) (density P r) r

theorem NavierStokes.SignedStressPrimitive.cutoff_deriv (P : Patch) (r : ℝ) : deriv (cutoff P) r = density P r

noncomputable def NavierStokes.SignedStressPrimitive.inversePower (P : Patch) (e : ℕ) (r : ℝ) : ℝ

Inverse power, given by ((RadialPullback.positiveRadius (P.a / 4) r) ^ e)⁻¹.

Equations

• NavierStokes.SignedStressPrimitive.inversePower P e r = (NavierStokes.RadialPullback.positiveRadius (P.a / 4) r ^ e)⁻¹

theorem NavierStokes.SignedStressPrimitive.inversePower_contDiff (P : Patch) (e : ℕ) : ContDiff ℝ (↑⊤) (inversePower P e)

theorem NavierStokes.SignedStressPrimitive.inversePower_nonneg (P : Patch) (e : ℕ) (r : ℝ) : 0 ≤ inversePower P e r

theorem NavierStokes.SignedStressPrimitive.inversePower_eq (P : Patch) (e : ℕ) {r : ℝ} (hr : P.a ≤ r) : inversePower P e r = (r ^ e)⁻¹

noncomputable def NavierStokes.SignedStressPrimitive.momentDensity (P : Patch) (e : ℕ) (r : ℝ) : ℝ

Moment density, given by inversePower P e r * density P r.

Equations

• NavierStokes.SignedStressPrimitive.momentDensity P e r = NavierStokes.SignedStressPrimitive.inversePower P e r * NavierStokes.SignedStressPrimitive.density P r

theorem NavierStokes.SignedStressPrimitive.momentDensity_contDiff (P : Patch) (e : ℕ) : ContDiff ℝ (↑⊤) (momentDensity P e)

theorem NavierStokes.SignedStressPrimitive.momentDensity_nonneg (P : Patch) (e : ℕ) (r : ℝ) : 0 ≤ momentDensity P e r

theorem NavierStokes.SignedStressPrimitive.momentDensity_support (P : Patch) (e : ℕ) : Function.support (momentDensity P e) ⊆ Set.Icc P.left P.right

theorem NavierStokes.SignedStressPrimitive.weighted_momentDensity (P : Patch) (e : ℕ) (r : ℝ) : r ^ e * momentDensity P e r = density P r

theorem NavierStokes.SignedStressPrimitive.momentDensity_moment (P : Patch) (e : ℕ) : ∫ (r : ℝ), r ^ e * momentDensity P e r = 1

theorem NavierStokes.SignedStressPrimitive.momentDensity_positive_moment (P : Patch) (e : ℕ) : ∫ (r : ℝ) in Set.Ioi 0, r ^ e * momentDensity P e r = 1

theorem NavierStokes.SignedStressPrimitive.momentDensity_tsupport (P : Patch) (e : ℕ) : tsupport (momentDensity P e) ⊆ Set.Ioo P.a P.b

noncomputable def NavierStokes.SignedStressPrimitive.weightedSource {E : Type} (e : ℕ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Weighted source, given by z.1 ^ e * F z.

Equations

• NavierStokes.SignedStressPrimitive.weightedSource e F z = z.1 ^ e * F z

noncomputable def NavierStokes.SignedStressPrimitive.mass {E : Type} (e : ℕ) (F : ℝ × E → ℝ) : E → ℝ

Mass, given by IntegratedMeanBalances.radialMoment e F.

Equations

• NavierStokes.SignedStressPrimitive.mass e F = NavierStokes.IntegratedMeanBalances.radialMoment e F

noncomputable def NavierStokes.SignedStressPrimitive.bumpCorrection {E : Type} (P : Patch) (e : ℕ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Bump correction, given by momentDensity P e z.1 * mass e F z.2.

Equations

• NavierStokes.SignedStressPrimitive.bumpCorrection P e F z = NavierStokes.SignedStressPrimitive.momentDensity P e z.1 * NavierStokes.SignedStressPrimitive.mass e F z.2

noncomputable def NavierStokes.SignedStressPrimitive.adjusted {E : Type} (P : Patch) (e : ℕ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Adjusted, given by F z - bumpCorrection P e F z.

Equations

• NavierStokes.SignedStressPrimitive.adjusted P e F z = F z - NavierStokes.SignedStressPrimitive.bumpCorrection P e F z

noncomputable def NavierStokes.SignedStressPrimitive.primitive {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) (F : ℝ × E → ℝ) : ℝ × E → ℝ

Primitive, given by TransportPrimitive.compactIntegral (cutoff P) 0 0 (weightedSource e F).

Equations

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

noncomputable def NavierStokes.SignedStressPrimitive.sigma {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Sigma, given by -inversePower P e z.1 * primitive P e F z.

Equations

• NavierStokes.SignedStressPrimitive.sigma P e F z = -NavierStokes.SignedStressPrimitive.inversePower P e z.1 * NavierStokes.SignedStressPrimitive.primitive P e F z

theorem NavierStokes.SignedStressPrimitive.weightedSource_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (weightedSource e F)

theorem NavierStokes.SignedStressPrimitive.weightedSource_continuous {E : Type} [NormedAddCommGroup E] (e : ℕ) {F : ℝ × E → ℝ} (hF : Continuous F) : Continuous (weightedSource e F)

theorem NavierStokes.SignedStressPrimitive.weightedSource_supported {E : Type} (e : ℕ) {P : Patch} {F : ℝ × E → ℝ} (hF : RadialAlias.RadiallySupported P.a P.b F) : RadialAlias.RadiallySupported P.a P.b (weightedSource e F)

theorem NavierStokes.SignedStressPrimitive.mass_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {P : Patch} (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) : ContDiff ℝ (↑⊤) (mass e F)

theorem NavierStokes.SignedStressPrimitive.bumpCorrection_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) : ContDiff ℝ (↑⊤) (bumpCorrection P e F)

theorem NavierStokes.SignedStressPrimitive.bumpCorrection_supported {E : Type} (P : Patch) (e : ℕ) (F : ℝ × E → ℝ) : RadialAlias.RadiallySupported P.left P.right (bumpCorrection P e F)

theorem NavierStokes.SignedStressPrimitive.bumpCorrection_moment {E : Type} (P : Patch) (e : ℕ) (F : ℝ × E → ℝ) (p : E) : mass e (bumpCorrection P e F) p = mass e F p

theorem NavierStokes.SignedStressPrimitive.adjusted_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) : ContDiff ℝ (↑⊤) (adjusted P e F)

theorem NavierStokes.SignedStressPrimitive.primitive_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) : ContDiff ℝ (↑⊤) (primitive P e F)

theorem NavierStokes.SignedStressPrimitive.primitive_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : Continuous F) (hs : RadialAlias.RadiallySupported P.a P.b F) : RadialAlias.RadiallySupported P.a P.b (primitive P e F)

theorem NavierStokes.SignedStressPrimitive.sigma_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) : ContDiff ℝ (↑⊤) (sigma P e F)

theorem NavierStokes.SignedStressPrimitive.sigma_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : Continuous F) (hs : RadialAlias.RadiallySupported P.a P.b F) : RadialAlias.RadiallySupported P.a P.b (sigma P e F)

theorem NavierStokes.SignedStressPrimitive.total_weightedSource {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : Continuous F) (hs : RadialAlias.RadiallySupported P.a P.b F) (z : ℝ × E) : TransportPrimitive.totalIntegral 0 0 (weightedSource e F) z = mass e F z.2

theorem NavierStokes.SignedStressPrimitive.past_zero_eq_integral {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (ha : 0 ≤ a) {F : ℝ × E → ℝ} (hF : Continuous F) (hs : RadialAlias.RadiallySupported a b F) (z : ℝ × E) : TransportPrimitive.pastIntegral 0 0 F z = ∫ (r : ℝ) in 0..z.1, F (r, z.2)

theorem NavierStokes.SignedStressPrimitive.cutoff_eq_integral (P : Patch) (r : ℝ) : cutoff P r = ∫ (s : ℝ) in 0..r, density P s

theorem NavierStokes.SignedStressPrimitive.primitive_eq_integral {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (z : ℝ × E) : primitive P e F z = ∫ (r : ℝ) in 0..z.1, r ^ e * adjusted P e F (r, z.2)

theorem NavierStokes.SignedStressPrimitive.weighted_sigma_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : Continuous F) (hs : RadialAlias.RadiallySupported P.a P.b F) (z : ℝ × E) : z.1 ^ e * sigma P e F z = -primitive P e F z

theorem NavierStokes.SignedStressPrimitive.sigma_eq_negative_primitive {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (z : ℝ × E) : sigma P e F z = (-∫ (r : ℝ) in 0..z.1, r ^ e * adjusted P e F (r, z.2)) / z.1 ^ e

theorem NavierStokes.SignedStressPrimitive.adjusted_supported {E : Type} (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hs : RadialAlias.RadiallySupported P.a P.b F) : RadialAlias.RadiallySupported P.a P.b (adjusted P e F)

theorem NavierStokes.SignedStressPrimitive.adjusted_moment_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (p : E) : mass e (adjusted P e F) p = 0

theorem NavierStokes.SignedStressPrimitive.adjusted_positive_moment_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (p : E) : ∫ (r : ℝ) in Set.Ioi 0, r ^ e * adjusted P e F (r, p) = 0

theorem NavierStokes.SignedStressPrimitive.primitive_hasDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (p : E) (r : ℝ) : HasDerivAt (fun (t : ℝ) => primitive P e F (t, p)) (r ^ e * adjusted P e F (r, p)) r

theorem NavierStokes.SignedStressPrimitive.weighted_sigma_hasDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (p : E) (r : ℝ) : HasDerivAt (fun (t : ℝ) => t ^ e * sigma P e F (t, p)) (-r ^ e * adjusted P e F (r, p)) r

The sign is the one required to cancel the adjusted residual by divergence.

theorem NavierStokes.SignedStressPrimitive.sigma_slice_compact {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : ℝ × E → ℝ} (hF : Continuous F) (hs : RadialAlias.RadiallySupported P.a P.b F) (p : E) : HasCompactSupport fun (r : ℝ) => sigma P e F (r, p)

theorem NavierStokes.SignedStressPrimitive.angular_divergence {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (p : E) {r : ℝ} (hr : 0 < r) : IntegratedMeanBalances.radialDivergence 2 (fun (t : ℝ) => sigma P 2 F (t, p)) r = -adjusted P 2 F (r, p)

theorem NavierStokes.SignedStressPrimitive.axial_divergence {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (p : E) {r : ℝ} (hr : 0 < r) : IntegratedMeanBalances.radialDivergence 1 (fun (t : ℝ) => sigma P 1 F (t, p)) r = -adjusted P 1 F (r, p)

theorem NavierStokes.SignedStressPrimitive.sigma_finiteJets_uniform {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (p m : ℕ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (F : ℝ × E → ℝ), ContDiff ℝ (↑⊤) F → RadialAlias.RadiallySupported P.a P.b F → ∀ (A : ℝ), 0 ≤ A → (∀ i ≤ m, ∀ r ∈ Set.Ioo P.a P.b, ∀ (y : E), ‖iteratedFDeriv ℝ i F (r, y)‖ ≤ A * WeightedRadialPrimitive.logWeight cL cR P.a P.b p r) → ∀ (z : ℝ × E), z.1 ∈ Set.Ioo P.a P.b → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (sigma P e F) z‖ ≤ K * A * WeightedRadialPrimitive.logWeight cL cR P.a P.b p z.1

All fixed-order constants come from the proved weighted integral estimate and bounded radial multipliers on a fixed positive annulus.

theorem NavierStokes.SignedStressPrimitive.meanClass_sigma {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) (α : ℝ) (F : ℕ → ℝ × E → ℝ) (hF : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) (hs : ∀ (n : ℕ), RadialAlias.RadiallySupported P.a P.b (F n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) α F) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) α fun (n : ℕ) => sigma P e (F n)

theorem NavierStokes.SignedStressPrimitive.momentDensity_meanClass {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) 0 fun (x : ℕ) (z : ℝ × E) => momentDensity P e z.1

The constructed interior bump carries the full edge weight, because its support lies in a fixed compact subset of the active annulus.

theorem NavierStokes.SignedStressPrimitive.fderiv_lift {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (D : E → ℝ) (hD : ContDiff ℝ (↑⊤) D) (z : ℝ × E) (v : E) : (fderiv ℝ (fun (y : ℝ × E) => D y.2) z) (0, v) = (fderiv ℝ D z.2) v

theorem NavierStokes.SignedStressPrimitive.bump_improvedClass_of_moment_identity {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) (α : ℝ) (F : ℕ → ℝ × E → ℝ) (D : ℕ → E → ℝ) (v : E) (hD : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (D n)) (hclass : WeightedClasses.UnweightedClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) α fun (n : ℕ) (z : ℝ × E) => D n z.2) (hmoment : ∀ (n : ℕ) (p : E), mass e (F n) p = ε n * (fderiv ℝ (D n) p) v) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) (α + 1) fun (n : ℕ) => bumpCorrection P e (F n)

The improved bump order follows from a proved residual-moment identity: one slow derivative comes with one additional factor of epsilon.

noncomputable def NavierStokes.SignedStressPrimitive.barSigma {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) (F : PressureStream.Lift E → ℝ) : ℝ × E → ℝ

Bar sigma, given by sigma P e (PressureStream.torusAverage F).

Equations

• NavierStokes.SignedStressPrimitive.barSigma P e F = NavierStokes.SignedStressPrimitive.sigma P e (NavierStokes.PressureStream.torusAverage F)

theorem NavierStokes.SignedStressPrimitive.barSigma_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : PressureStream.Lift E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) : ContDiff ℝ (↑⊤) (barSigma P e F)

theorem NavierStokes.SignedStressPrimitive.barSigma_eq_primitive {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {F : PressureStream.Lift E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : RadialAlias.RadiallySupported P.a P.b F) (z : ℝ × E) : barSigma P e F z = (-∫ (r : ℝ) in 0..z.1, r ^ e * adjusted P e (PressureStream.torusAverage F) (r, z.2)) / z.1 ^ e

theorem NavierStokes.SignedStressPrimitive.sigma_slow_mul {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) (k : E → ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : sigma P e (fun (y : ℝ × E) => k y.2 * F y) z = k z.2 * sigma P e F z

Slow coefficients are constant along the ordinary radial integration.

theorem NavierStokes.SignedStressPrimitive.mass_slow_mul {E : Type} (e : ℕ) (k : E → ℝ) (F : ℝ × E → ℝ) (p : E) : mass e (fun (y : ℝ × E) => k y.2 * F y) p = k p * mass e F p

theorem NavierStokes.SignedStressPrimitive.bump_slow_mul {E : Type} (P : Patch) (e : ℕ) (k : E → ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : bumpCorrection P e (fun (y : ℝ × E) => k y.2 * F y) z = k z.2 * bumpCorrection P e F z

noncomputable def NavierStokes.SignedStressPrimitive.lengthScale {E : Type} (q : E → ℝ) (p : E) : ℝ

The physical radial length is sqrt q, as in the chart R = r / sqrt Q.

Equations

• NavierStokes.SignedStressPrimitive.lengthScale q p = √(q p)

noncomputable def NavierStokes.SignedStressPrimitive.nativeSource {E : Type} (q : E → ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Native source, given by F (lengthScale q z.2 * z.1, z.2).

Equations

• NavierStokes.SignedStressPrimitive.nativeSource q F z = F (NavierStokes.SignedStressPrimitive.lengthScale q z.2 * z.1, z.2)

noncomputable def NavierStokes.SignedStressPrimitive.physicalDensity {E : Type} (P : Patch) (e : ℕ) (q : E → ℝ) (z : ℝ × E) : ℝ

Physical density, given by momentDensity P e (z.1 / lengthScale q z.2) / lengthScale q z.2 ^ (e + 1).

Equations

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

noncomputable def NavierStokes.SignedStressPrimitive.physicalBump {E : Type} (P : Patch) (e : ℕ) (q : E → ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Physical bump, given by physicalDensity P e q z * mass e F z.2.

Equations

• NavierStokes.SignedStressPrimitive.physicalBump P e q F z = NavierStokes.SignedStressPrimitive.physicalDensity P e q z * NavierStokes.SignedStressPrimitive.mass e F z.2

noncomputable def NavierStokes.SignedStressPrimitive.physicalAdjusted {E : Type} (P : Patch) (e : ℕ) (q : E → ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Physical adjusted, given by F z - physicalBump P e q F z.

Equations

• NavierStokes.SignedStressPrimitive.physicalAdjusted P e q F z = F z - NavierStokes.SignedStressPrimitive.physicalBump P e q F z

noncomputable def NavierStokes.SignedStressPrimitive.physicalSigma {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) (q : E → ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Physical sigma, given by lengthScale q z.2 * sigma P e (nativeSource q F) (z.1 / lengthScale q z.2, z.2).

Equations

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

def NavierStokes.SignedStressPrimitive.PhysicalSupport {E : Type} (P : Patch) (q : E → ℝ) (F : ℝ × E → ℝ) : Prop

Radial support stated directly using the physical q, with no band index.

Equations

• NavierStokes.SignedStressPrimitive.PhysicalSupport P q F = ∀ (z : ℝ × E), F z ≠ 0 → z.1 / NavierStokes.SignedStressPrimitive.lengthScale q z.2 ∈ Set.Icc P.a P.b

theorem NavierStokes.SignedStressPrimitive.lengthScale_pos {E : Type} {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (p : E) : 0 < lengthScale q p

theorem NavierStokes.SignedStressPrimitive.lengthScale_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) : ContDiff ℝ (↑⊤) (lengthScale q)

theorem NavierStokes.SignedStressPrimitive.nativeSource_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (nativeSource q F)

theorem NavierStokes.SignedStressPrimitive.nativeSource_supported {E : Type} (P : Patch) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hs : PhysicalSupport P q F) : RadialAlias.RadiallySupported P.a P.b (nativeSource q F)

theorem NavierStokes.SignedStressPrimitive.integral_dilate_weighted (e : ℕ) (f : ℝ → ℝ) {s : ℝ} (hs : 0 < s) : ∫ (r : ℝ), r ^ e * f (s * r) = (∫ (r : ℝ), r ^ e * f r) / s ^ (e + 1)

theorem NavierStokes.SignedStressPrimitive.interval_dilate_weighted (e : ℕ) (f : ℝ → ℝ) {s : ℝ} (hs : 0 < s) (x : ℝ) : ∫ (r : ℝ) in 0..x, r ^ e * f (s * r) = (∫ (r : ℝ) in 0..s * x, r ^ e * f r) / s ^ (e + 1)

theorem NavierStokes.SignedStressPrimitive.nativeSource_mass {E : Type} (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (F : ℝ × E → ℝ) (p : E) : mass e (nativeSource q F) p = mass e F p / lengthScale q p ^ (e + 1)

theorem NavierStokes.SignedStressPrimitive.physicalDensity_moment {E : Type} (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (p : E) : ∫ (r : ℝ), r ^ e * physicalDensity P e q (r, p) = 1

theorem NavierStokes.SignedStressPrimitive.physicalDensity_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) : ContDiff ℝ (↑⊤) (physicalDensity P e q)

theorem NavierStokes.SignedStressPrimitive.physical_mass_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) : ContDiff ℝ (↑⊤) (mass e F)

theorem NavierStokes.SignedStressPrimitive.physicalBump_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) : ContDiff ℝ (↑⊤) (physicalBump P e q F)

theorem NavierStokes.SignedStressPrimitive.physicalSigma_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) : ContDiff ℝ (↑⊤) (physicalSigma P e q F)

theorem NavierStokes.SignedStressPrimitive.physicalSigma_supported {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) : PhysicalSupport P q (physicalSigma P e q F)

theorem NavierStokes.SignedStressPrimitive.native_adjusted_eq {E : Type} (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (F : ℝ × E → ℝ) (z : ℝ × E) : adjusted P e (nativeSource q F) z = physicalAdjusted P e q F (lengthScale q z.2 * z.1, z.2)

theorem NavierStokes.SignedStressPrimitive.physicalSigma_eq_negative_primitive {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) (z : ℝ × E) : physicalSigma P e q F z = (-∫ (r : ℝ) in 0..z.1, r ^ e * physicalAdjusted P e q F (r, z.2)) / z.1 ^ e

The physical sigma is exactly the requested negative primitive from zero. No fixed-Q chart enters this definition or identity.

theorem NavierStokes.SignedStressPrimitive.physicalDensity_support {E : Type} (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (p : E) : (Function.support fun (r : ℝ) => physicalDensity P e q (r, p)) ⊆ Set.Icc (lengthScale q p * P.left) (lengthScale q p * P.right)

theorem NavierStokes.SignedStressPrimitive.physicalDensity_positive_moment {E : Type} (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (p : E) : ∫ (r : ℝ) in Set.Ioi 0, r ^ e * physicalDensity P e q (r, p) = 1

theorem NavierStokes.SignedStressPrimitive.physicalBump_moment {E : Type} (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (F : ℝ × E → ℝ) (p : E) : mass e (physicalBump P e q F) p = mass e F p

theorem NavierStokes.SignedStressPrimitive.physicalAdjusted_moment_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) (p : E) : mass e (physicalAdjusted P e q F) p = 0

theorem NavierStokes.SignedStressPrimitive.physicalSigma_slice_compact {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) (p : E) : HasCompactSupport fun (r : ℝ) => physicalSigma P e q F (r, p)

theorem NavierStokes.SignedStressPrimitive.physicalAdjusted_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) : ContDiff ℝ (↑⊤) (physicalAdjusted P e q F)

theorem NavierStokes.SignedStressPrimitive.physical_weighted_sigma_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) (p : E) (r : ℝ) : r ^ e * physicalSigma P e q F (r, p) = -∫ (t : ℝ) in 0..r, t ^ e * physicalAdjusted P e q F (t, p)

theorem NavierStokes.SignedStressPrimitive.physical_weighted_sigma_hasDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) (p : E) (r : ℝ) : HasDerivAt (fun (t : ℝ) => t ^ e * physicalSigma P e q F (t, p)) (-r ^ e * physicalAdjusted P e q F (r, p)) r

theorem NavierStokes.SignedStressPrimitive.physical_angular_divergence {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) (p : E) {r : ℝ} (hr : 0 < r) : IntegratedMeanBalances.radialDivergence 2 (fun (t : ℝ) => physicalSigma P 2 q F (t, p)) r = -physicalAdjusted P 2 q F (r, p)

theorem NavierStokes.SignedStressPrimitive.physical_axial_divergence {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P q F) (p : E) {r : ℝ} (hr : 0 < r) : IntegratedMeanBalances.radialDivergence 1 (fun (t : ℝ) => physicalSigma P 1 q F (t, p)) r = -physicalAdjusted P 1 q F (r, p)

theorem NavierStokes.SignedStressPrimitive.physical_torusAverage_supported {E : Type} (P : Patch) {q : E → ℝ} {F : PressureStream.Lift E → ℝ} (hs : PhysicalSupport P (fun (p : E × PressureStream.Plane) => q p.1) F) : PhysicalSupport P q (PressureStream.torusAverage F)

Taking the torus bar preserves support described by the physical q.

noncomputable def NavierStokes.SignedStressPrimitive.physicalBarSigma {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) (q : E → ℝ) (F : PressureStream.Lift E → ℝ) : ℝ × E → ℝ

Physical bar sigma, given by physicalSigma P e q (PressureStream.torusAverage F).

Equations

• NavierStokes.SignedStressPrimitive.physicalBarSigma P e q F = NavierStokes.SignedStressPrimitive.physicalSigma P e q (NavierStokes.PressureStream.torusAverage F)

theorem NavierStokes.SignedStressPrimitive.physicalBarSigma_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : PressureStream.Lift E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P (fun (p : E × PressureStream.Plane) => q p.1) F) : ContDiff ℝ (↑⊤) (physicalBarSigma P e q F)

theorem NavierStokes.SignedStressPrimitive.physicalBarSigma_eq_negative_primitive {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) {F : PressureStream.Lift E → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hs : PhysicalSupport P (fun (p : E × PressureStream.Plane) => q p.1) F) (z : ℝ × E) : physicalBarSigma P e q F z = (-∫ (r : ℝ) in 0..z.1, r ^ e * physicalAdjusted P e q (PressureStream.torusAverage F) (r, z.2)) / z.1 ^ e

noncomputable def NavierStokes.SignedStressPrimitive.normalizedResidual {E : Type} (q : E → ℝ) (A : ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Residual units in the q-chart: q^(2A+1/2) times the physical residual.

Equations

• NavierStokes.SignedStressPrimitive.normalizedResidual q A F z = q z.2 ^ (2 * A + 1 / 2) * NavierStokes.SignedStressPrimitive.nativeSource q F z

noncomputable def NavierStokes.SignedStressPrimitive.qChartTensor {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) (q : E → ℝ) (A : ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Q chart tensor, given by q z.2 ^ (2 * A) * physicalSigma P e q F (lengthScale q z.2 * z.1, z.2).

Equations

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

noncomputable def NavierStokes.SignedStressPrimitive.qChartBump {E : Type} (P : Patch) (e : ℕ) (q : E → ℝ) (A : ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Q chart bump, given by q z.2 ^ (2 * A + 1 / 2) * physicalBump P e q F (lengthScale q z.2 * z.1, z.2).

Equations

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

theorem NavierStokes.SignedStressPrimitive.qChartBump_eq {E : Type} (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (A : ℝ) (F : ℝ × E → ℝ) : qChartBump P e q A F = bumpCorrection P e (normalizedResidual q A F)

theorem NavierStokes.SignedStressPrimitive.tensor_units_identity {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (A : ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : q z.2 ^ (2 * A) * physicalSigma P e q F z = sigma P e (normalizedResidual q A F) (z.1 / lengthScale q z.2, z.2)

theorem NavierStokes.SignedStressPrimitive.qChartTensor_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (A : ℝ) (F : ℝ × E → ℝ) : qChartTensor P e q A F = sigma P e (normalizedResidual q A F)

Exact chart tensor units, with no preferred band in the physical definition.

theorem NavierStokes.SignedStressPrimitive.normalizedResidual_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) (A : ℝ) {F : ℝ × E → ℝ} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ (↑⊤) (normalizedResidual q A F)

theorem NavierStokes.SignedStressPrimitive.normalizedResidual_supported {E : Type} (P : Patch) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) (A : ℝ) {F : ℝ × E → ℝ} (hs : PhysicalSupport P q F) : RadialAlias.RadiallySupported P.a P.b (normalizedResidual q A F)

theorem NavierStokes.SignedStressPrimitive.meanClass_qChartTensor {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) {q : E → ℝ} (hq : ContDiff ℝ (↑⊤) q) (hpos : ∀ (p : E), 0 < q p) (A α : ℝ) (F : ℕ → ℝ × E → ℝ) (hF : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (F n)) (hs : ∀ (n : ℕ), PhysicalSupport P q (F n)) (hclass : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) α fun (n : ℕ) => normalizedResidual q A (F n)) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) α fun (n : ℕ) => qChartTensor P e q A (F n)

The actual physical stress has the claimed all-jet tensor class after conversion to q-chart units, directly from the normalized residual class.

theorem NavierStokes.SignedStressPrimitive.fixedQ_tensor_identity {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {q : E → ℝ} (hq : ∀ (p : E), 0 < q p) {Q : ℝ} (hQ : 0 < Q) (A : ℝ) (F : ℝ × E → ℝ) (R : ℝ) (p : E) : Q ^ (2 * A) * physicalSigma P e q F (√Q * R, p) = (Q / q p) ^ (2 * A) * sigma P e (normalizedResidual q A F) (√Q / √(q p) * R, p)

A fixed-Q chart is an exact reparametrization of the physical-q stress; the physical stress itself was defined without Q.

theorem NavierStokes.SignedStressPrimitive.fixedQ_density_identity {E : Type} (P : Patch) (e : ℕ) (q : E → ℝ) (Q R : ℝ) (p : E) : √Q ^ (e + 1) * physicalDensity P e q (√Q * R, p) = (√Q / √(q p)) ^ (e + 1) * momentDensity P e (√Q / √(q p) * R)

theorem NavierStokes.SignedStressPrimitive.angular_bump_identity (P : Patch) (ε : ℝ) {v radialFlux axialFlux virtualFlux : IntegratedMeanBalances.MeanField} (hv : IntegratedMeanBalances.SmoothShell P.a P.b v) (hr : IntegratedMeanBalances.SmoothShell P.a P.b radialFlux) (hz : IntegratedMeanBalances.SmoothShell P.a P.b axialFlux) (hT : IntegratedMeanBalances.SmoothShell P.a P.b virtualFlux) (hmass : IntegratedMeanBalances.radialMoment 2 v = 0) (z : IntegratedMeanBalances.MeanPoint) : bumpCorrection P 2 (IntegratedMeanBalances.angularBalance ε v radialFlux axialFlux virtualFlux) z = momentDensity P 2 z.1 * (ε * (fderiv ℝ (IntegratedMeanBalances.radialMoment 2 axialFlux) z.2) (0, 1))

The removed angular moment is the actual defect derivative in (34).

noncomputable def NavierStokes.SignedStressPrimitive.axialMomentPotential (axialFlux gr ρ : IntegratedMeanBalances.MeanField) (p : IntegratedMeanBalances.MeanParameter) : ℝ

Axial moment potential, given by axialDefect axialFlux gr p + pressureCoefficient ρ p * pressureTotal gr p.

Equations

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

theorem NavierStokes.SignedStressPrimitive.axialMomentPotential_contDiff (P : Patch) {axialFlux gr ρ : IntegratedMeanBalances.MeanField} (hz : IntegratedMeanBalances.SmoothShell P.a P.b axialFlux) (hg : IntegratedMeanBalances.SmoothShell P.a P.b gr) (hρ : IntegratedMeanBalances.SmoothShell P.a P.b ρ) : ContDiff ℝ (↑⊤) (axialMomentPotential axialFlux gr ρ)

theorem NavierStokes.SignedStressPrimitive.axial_bump_identity (P : Patch) (ε : ℝ) {γ radialFlux axialFlux pressure virtualFlux gr ρ : IntegratedMeanBalances.MeanField} (hγ : IntegratedMeanBalances.SmoothShell P.a P.b γ) (hr : IntegratedMeanBalances.SmoothShell P.a P.b radialFlux) (hz : IntegratedMeanBalances.SmoothShell P.a P.b axialFlux) (hp : IntegratedMeanBalances.SmoothShell P.a P.b pressure) (hT : IntegratedMeanBalances.SmoothShell P.a P.b virtualFlux) (hg : IntegratedMeanBalances.SmoothShell P.a P.b gr) (hρ : IntegratedMeanBalances.SmoothShell P.a P.b ρ) (hmass : IntegratedMeanBalances.radialMoment 1 γ = 0) (hderiv : ∀ (r : ℝ) (p : IntegratedMeanBalances.MeanParameter), deriv (fun (s : ℝ) => pressure (s, p)) r = gr (r, p) - ρ (r, p) * IntegratedMeanBalances.pressureTotal gr p) (z : IntegratedMeanBalances.MeanPoint) : bumpCorrection P 1 (IntegratedMeanBalances.axialBalance ε γ radialFlux axialFlux pressure virtualFlux) z = momentDensity P 1 z.1 * (ε * (fderiv ℝ (axialMomentPotential axialFlux gr ρ) z.2) (0, 1))

The pressure coefficient remains inside the actual slow derivative.

theorem NavierStokes.SignedStressPrimitive.axial_bump_constructed_pressure_identity (P : Patch) {d M : ℝ} (hd : 0 < d) (ε : ℝ) (v : ℝ × ℝ) {f : PressureStream.Lift IntegratedMeanBalances.MeanParameter → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hs : RadialAlias.RadiallySupported P.a P.b f) (hper : PressureStream.TorusPeriodicLift f) {γ radialFlux axialFlux virtualFlux : IntegratedMeanBalances.MeanField} (hγ : IntegratedMeanBalances.SmoothShell P.a P.b γ) (hr : IntegratedMeanBalances.SmoothShell P.a P.b radialFlux) (hz : IntegratedMeanBalances.SmoothShell P.a P.b axialFlux) (hT : IntegratedMeanBalances.SmoothShell P.a P.b virtualFlux) (hmass : IntegratedMeanBalances.radialMoment 1 γ = 0) (z : IntegratedMeanBalances.MeanPoint) : bumpCorrection P 1 (IntegratedMeanBalances.axialBalance ε γ radialFlux axialFlux (IntegratedMeanBalances.reconstructedMeanPressure d P.a P.b M ⋯ v f) virtualFlux) z = momentDensity P 1 z.1 * (ε * (fderiv ℝ (axialMomentPotential axialFlux (IntegratedMeanBalances.averagedRadialSource f) (IntegratedMeanBalances.normalizedMeanDensity P.a P.b ⋯)) z.2) (0, 1))

The axial bump identity with pressure supplied by the actual torus-averaged compact pressure constructor, so no pressure moment or derivative is assumed.

theorem NavierStokes.SignedStressPrimitive.angular_bump_improvedClass (P : Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) (α : ℝ) (v radialFlux axialFlux virtualFlux : ℕ → IntegratedMeanBalances.MeanField) (hv : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (v n)) (hr : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (radialFlux n)) (hz : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (axialFlux n)) (hT : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (virtualFlux n)) (hmass : ∀ (n : ℕ), IntegratedMeanBalances.radialMoment 2 (v n) = 0) (hclass : WeightedClasses.UnweightedClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) α fun (n : ℕ) (z : IntegratedMeanBalances.MeanPoint) => IntegratedMeanBalances.radialMoment 2 (axialFlux n) z.2) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) (α + 1) fun (n : ℕ) => bumpCorrection P 2 (IntegratedMeanBalances.angularBalance (ε n) (v n) (radialFlux n) (axialFlux n) (virtualFlux n))

theorem NavierStokes.SignedStressPrimitive.axial_bump_improvedClass (P : Patch) {cL cR : ℝ} (hcL : 0 < cL) (hcR : 0 < cR) (ε slow : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hε1 : ∀ (n : ℕ), ε n ≤ 1) (hslow : ∀ (n : ℕ), 1 ≤ slow n) (α : ℝ) (γ radialFlux axialFlux pressure virtualFlux gr ρ : ℕ → IntegratedMeanBalances.MeanField) (hγ : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (γ n)) (hr : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (radialFlux n)) (hz : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (axialFlux n)) (hp : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (pressure n)) (hT : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (virtualFlux n)) (hg : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (gr n)) (hρ : ∀ (n : ℕ), IntegratedMeanBalances.SmoothShell P.a P.b (ρ n)) (hmass : ∀ (n : ℕ), IntegratedMeanBalances.radialMoment 1 (γ n) = 0) (hderiv : ∀ (n : ℕ) (r : ℝ) (p : IntegratedMeanBalances.MeanParameter), deriv (fun (s : ℝ) => pressure n (s, p)) r = gr n (r, p) - ρ n (r, p) * IntegratedMeanBalances.pressureTotal (gr n) p) (hclass : WeightedClasses.UnweightedClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) α fun (n : ℕ) (z : IntegratedMeanBalances.MeanPoint) => axialMomentPotential (axialFlux n) (gr n) (ρ n) z.2) : WeightedClasses.MeanClass (WeightedRadialPrimitive.logStripData P.a P.b cL cR ⋯ hcL hcR ε slow hε hε1 hslow) (α + 1) fun (n : ℕ) => bumpCorrection P 1 (IntegratedMeanBalances.axialBalance (ε n) (γ n) (radialFlux n) (axialFlux n) (pressure n) (virtualFlux n))

theorem NavierStokes.SignedStressPrimitive.compact_jet_bounds {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {K : Set X} (hK : IsCompact K) {f : X → Y} (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ j ≤ m, ∀ x ∈ K, ‖iteratedFDeriv ℝ j f x‖ ≤ C

theorem NavierStokes.SignedStressPrimitive.compact_change_jet_bound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {K : Set X} (hK : IsCompact K) {a : X → ℝ} (ha : ContDiff ℝ (↑⊤) a) {φ : X → X} (hφ : ContDiff ℝ (↑⊤) φ) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (f : X → ℝ), ContDiff ℝ (↑⊤) f → ∀ x ∈ K, ∀ (B : ℝ), 0 ≤ B → (∀ i ≤ m, ‖iteratedFDeriv ℝ i f (φ x)‖ ≤ B) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (fun (y : X) => a y * f (φ y)) x‖ ≤ C * B

Smooth coordinate changes and multipliers have actual finite-jet operator bounds on compact sets; the bound is uniform over every input function.

noncomputable def NavierStokes.SignedStressPrimitive.changeChart {E : Type} (ρ : E → ℝ) (A : ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Change chart, given by ρ z.2 ^ (-2 * A) * F (z.1 / Real.sqrt (ρ z.2), z.2).

Equations

• NavierStokes.SignedStressPrimitive.changeChart ρ A F z = ρ z.2 ^ (-2 * A) * F (z.1 / √(ρ z.2), z.2)

noncomputable def NavierStokes.SignedStressPrimitive.inverseChangeChart {E : Type} (ρ : E → ℝ) (A : ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : ℝ

Inverse change chart, given by ρ z.2 ^ (2 * A) * F (Real.sqrt (ρ z.2) * z.1, z.2).

Equations

• NavierStokes.SignedStressPrimitive.inverseChangeChart ρ A F z = ρ z.2 ^ (2 * A) * F (√(ρ z.2) * z.1, z.2)

theorem NavierStokes.SignedStressPrimitive.changeChart_inverse {E : Type} {ρ : E → ℝ} (hρ : ∀ (p : E), 0 < ρ p) (A : ℝ) (F : ℝ × E → ℝ) : changeChart ρ A (inverseChangeChart ρ A F) = F ∧ inverseChangeChart ρ A (changeChart ρ A F) = F

theorem NavierStokes.SignedStressPrimitive.chart_change_finiteJets {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : E → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (hpos : ∀ (p : E), 0 < ρ p) (A : ℝ) {K : Set (ℝ × E)} (hK : IsCompact K) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (F : ℝ × E → ℝ), ContDiff ℝ (↑⊤) F → ∀ z ∈ K, ∀ (B : ℝ), 0 ≤ B → ((∀ i ≤ m, ‖iteratedFDeriv ℝ i F (z.1 / √(ρ z.2), z.2)‖ ≤ B) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (changeChart ρ A F) z‖ ≤ C * B) ∧ ((∀ i ≤ m, ‖iteratedFDeriv ℝ i F (√(ρ z.2) * z.1, z.2)‖ ≤ B) → ∀ j ≤ m, ‖iteratedFDeriv ℝ j (inverseChangeChart ρ A F) z‖ ≤ C * B)

Both directions of the q/Q chart comparison have uniform finite-jet operator bounds. The positive ratio and all its derivatives are bounded by compactness, rather than postulated bounds on the transformed stress.

theorem NavierStokes.SignedStressPrimitive.fixedQ_tensor_common_ratio {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {ρ : E → ℝ} (hρ : ∀ (p : E), 0 < ρ p) {Q : ℝ} (hQ : 0 < Q) (A : ℝ) (F : ℝ × E → ℝ) (z : ℝ × E) : Q ^ (2 * A) * physicalSigma P e (fun (p : E) => Q * ρ p) F (√Q * z.1, z.2) = changeChart ρ A (sigma P e (normalizedResidual (fun (p : E) => Q * ρ p) A F)) z

theorem NavierStokes.SignedStressPrimitive.fixedQ_density_common_ratio {E : Type} (P : Patch) (e : ℕ) {ρ : E → ℝ} (hρ : ∀ (p : E), 0 < ρ p) {Q : ℝ} (hQ : 0 < Q) (z : ℝ × E) : √Q ^ (e + 1) * physicalDensity P e (fun (p : E) => Q * ρ p) (√Q * z.1, z.2) = physicalDensity P e ρ z

theorem NavierStokes.SignedStressPrimitive.fixedQ_density_finiteJets {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : Patch) (e : ℕ) {ρ : E → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (hpos : ∀ (p : E), 0 < ρ p) {K : Set (ℝ × E)} (hK : IsCompact K) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (Q : ℝ), 0 < Q → ∀ i ≤ m, ∀ z ∈ K, ‖iteratedFDeriv ℝ i (fun (y : ℝ × E) => √Q ^ (e + 1) * physicalDensity P e (fun (p : E) => Q * ρ p) (√Q * y.1, y.2)) z‖ ≤ C

For a fixed smooth positive ratio q/Q, every derivative of the length-normalized physical bump is bounded independently of the band Q.