Direct angular means in the physical diagonal

The angular velocity is retained as a direct field. It is not replaced by an axial primitive. Axisymmetry proves its divergence equation, and an annular zero germ removes the coordinate singularity on the axis.

@[reducible, inline]

abbrev NavierStokes.DirectAngularDiagonal.Slow : Type

Slow: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.DirectAngularDiagonal.Slow = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.DirectAngularDiagonal.CylPoint : Type

Cyl point: an abbreviation for ℝ × (ℝ × ℝ).

Equations

• NavierStokes.DirectAngularDiagonal.CylPoint = (ℝ × ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.DirectAngularDiagonal.Coefficient : Type

Coefficient: an abbreviation for CylPoint → ℝ.

Equations

• NavierStokes.DirectAngularDiagonal.Coefficient = (NavierStokes.DirectAngularDiagonal.CylPoint → ℝ)

noncomputable def NavierStokes.DirectAngularDiagonal.radius (w : ProblemStatement.SpaceTime) : ℝ

Radius, given by PolarCharts.radius (PhysicalGraphBounds.radialProjection w).

Equations

• NavierStokes.DirectAngularDiagonal.radius w = NavierStokes.PolarCharts.radius (NavierStokes.PhysicalGraphBounds.radialProjection w)

noncomputable def NavierStokes.DirectAngularDiagonal.slowPoint (w : ProblemStatement.SpaceTime) : Slow

Slow point, given by (w.1, w.2 2).

Equations

• NavierStokes.DirectAngularDiagonal.slowPoint w = (w.1, w.2.ofLp 2)

noncomputable def NavierStokes.DirectAngularDiagonal.cylPoint (w : ProblemStatement.SpaceTime) : CylPoint

Cyl point, given by (w.1, (radius w, w.2 2)).

Equations

• NavierStokes.DirectAngularDiagonal.cylPoint w = (w.1, NavierStokes.DirectAngularDiagonal.radius w, w.2.ofLp 2)

noncomputable def NavierStokes.DirectAngularDiagonal.slowOfCyl (p : CylPoint) : Slow

Slow of cyl, given by (p.1, p.2.2).

Equations

• NavierStokes.DirectAngularDiagonal.slowOfCyl p = (p.1, p.2.2)

noncomputable def NavierStokes.DirectAngularDiagonal.physicalDomain (U : Set Slow) : Set ProblemStatement.SpaceTime

Physical domain, given by slowPoint ⁻¹' U.

Equations

• NavierStokes.DirectAngularDiagonal.physicalDomain U = NavierStokes.DirectAngularDiagonal.slowPoint ⁻¹' U

noncomputable def NavierStokes.DirectAngularDiagonal.positiveDomain (U : Set Slow) : Set CylPoint

Positive domain, given by {p | slowOfCyl p ∈ U ∧ 0 < p.2.1}.

Equations

• NavierStokes.DirectAngularDiagonal.positiveDomain U = {p : NavierStokes.DirectAngularDiagonal.CylPoint | NavierStokes.DirectAngularDiagonal.slowOfCyl p ∈ U ∧ 0 < p.2.1}

theorem NavierStokes.DirectAngularDiagonal.slowPoint_smooth : ContDiff ℝ (↑⊤) slowPoint

theorem NavierStokes.DirectAngularDiagonal.physicalDomain_open {U : Set Slow} (hU : IsOpen U) : IsOpen (physicalDomain U)

theorem NavierStokes.DirectAngularDiagonal.positiveDomain_open {U : Set Slow} (hU : IsOpen U) : IsOpen (positiveDomain U)

theorem NavierStokes.DirectAngularDiagonal.radius_nonneg (w : ProblemStatement.SpaceTime) : 0 ≤ radius w

theorem NavierStokes.DirectAngularDiagonal.radius_continuous : Continuous radius

noncomputable def NavierStokes.DirectAngularDiagonal.profileToCyl (p : AxisymmetricFields.ProfilePoint) : CylPoint

Profile to cyl, given by (p.1, (Real.sqrt (2 * p.2.1), p.2.2)).

Equations

• NavierStokes.DirectAngularDiagonal.profileToCyl p = (p.1, √(2 * p.2.1), p.2.2)

noncomputable def NavierStokes.DirectAngularDiagonal.rate (b : Coefficient) (p : AxisymmetricFields.ProfilePoint) : ℝ

Rate, given by b (profileToCyl p) / Real.sqrt (2 * p.2.1).

Equations

• NavierStokes.DirectAngularDiagonal.rate b p = b (NavierStokes.DirectAngularDiagonal.profileToCyl p) / √(2 * p.2.1)

noncomputable def NavierStokes.DirectAngularDiagonal.angularField (b : Coefficient) (w : ProblemStatement.SpaceTime) : ProblemStatement.Space

Literal angular velocity with physical tangential magnitude b.

Equations

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

noncomputable def NavierStokes.DirectAngularDiagonal.rotationField (F : AxisymmetricFields.Profile) (w : ProblemStatement.SpaceTime) : ProblemStatement.Space

Rotation field, constructed using AxisymmetricResidual.pack.

Equations

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

theorem NavierStokes.DirectAngularDiagonal.profileToCyl_profilePoint (w : ProblemStatement.SpaceTime) : profileToCyl (AxisymmetricFields.profilePoint w.1 w.2) = cylPoint w

theorem NavierStokes.DirectAngularDiagonal.angularField_eq_rotationField (b : Coefficient) : angularField b = rotationField (rate b)

theorem NavierStokes.DirectAngularDiagonal.divergence_rotationField {F : AxisymmetricFields.Profile} {w : ProblemStatement.SpaceTime} (hF : DifferentiableAt ℝ F (AxisymmetricFields.profilePoint w.1 w.2)) : ProblemStatement.spatialDivergence (rotationField F) w.1 w.2 = 0

The cancellation is computed from actual Cartesian derivatives.

theorem NavierStokes.DirectAngularDiagonal.rotationField_smoothAt {F : AxisymmetricFields.Profile} {w : ProblemStatement.SpaceTime} (hF : ContDiffAt ℝ (↑⊤) F (AxisymmetricFields.profilePoint w.1 w.2)) : ContDiffAt ℝ (↑⊤) (rotationField F) w

theorem NavierStokes.DirectAngularDiagonal.rate_smoothAt {U : Set Slow} (hU : IsOpen U) {b : Coefficient} (hb : ContDiffOn ℝ (↑⊤) b (positiveDomain U)) {w : ProblemStatement.SpaceTime} (hw : w ∈ physicalDomain U) (hr : 0 < radius w) : ContDiffAt ℝ (↑⊤) (rate b) (AxisymmetricFields.profilePoint w.1 w.2)

structure NavierStokes.DirectAngularDiagonal.AngularData (U : Set Slow) : Type

A moving positive inner support radius is a primitive support datum. It may shrink as the physical terminal point is approached.

• scalar : Coefficient

  Scalar of AngularData, of type Coefficient.

• smooth : ContDiffOn ℝ (↑⊤) self.scalar (positiveDomain U)
• inner : Slow → ℝ

  Inner of AngularData, of type Slow → ℝ.

• inner_continuous : ContinuousOn self.inner U
• inner_pos (s : Slow) : s ∈ U → 0 < self.inner s
• vanishes (p : CylPoint) : slowOfCyl p ∈ U → 0 ≤ p.2.1 → p.2.1 < self.inner (slowOfCyl p) → self.scalar p = 0

theorem NavierStokes.DirectAngularDiagonal.AngularData.field_zero_germ {U : Set Slow} (D : AngularData U) (hU : IsOpen U) {w : ProblemStatement.SpaceTime} (hw : w ∈ physicalDomain U) (hr : radius w < D.inner (slowPoint w)) : angularField D.scalar =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.DirectAngularDiagonal.AngularData.field_smoothAt {U : Set Slow} (D : AngularData U) (hU : IsOpen U) {w : ProblemStatement.SpaceTime} (hw : w ∈ physicalDomain U) : ContDiffAt ℝ (↑⊤) (angularField D.scalar) w

theorem NavierStokes.DirectAngularDiagonal.AngularData.field_smooth {U : Set Slow} (D : AngularData U) (hU : IsOpen U) : ContDiffOn ℝ (↑⊤) (angularField D.scalar) (physicalDomain U)

theorem NavierStokes.DirectAngularDiagonal.AngularData.field_divergence {U : Set Slow} (D : AngularData U) (hU : IsOpen U) {w : ProblemStatement.SpaceTime} (hw : w ∈ physicalDomain U) : ProblemStatement.spatialDivergence (angularField D.scalar) w.1 w.2 = 0

noncomputable def NavierStokes.DirectAngularDiagonal.AngularData.multiply {U : Set Slow} (D : AngularData U) (f : Coefficient) (hf : ContDiffOn ℝ (↑⊤) f (positiveDomain U)) : AngularData U

Multiply, bundling scalar, smooth, inner, inner_continuous and the required compatibility proofs.

Equations

• D.multiply f hf = { scalar := fun (p : NavierStokes.DirectAngularDiagonal.CylPoint) => f p * D.scalar p, smooth := ⋯, inner := D.inner, inner_continuous := ⋯, inner_pos := ⋯, vanishes := ⋯ }

theorem NavierStokes.DirectAngularDiagonal.angularField_axis (b : Coefficient) (t : ℝ) (x : ProblemStatement.Space) (h0 : x.ofLp 0 = 0) (h1 : x.ofLp 1 = 0) : angularField b (t, x) = 0

theorem NavierStokes.DirectAngularDiagonal.angularField_mul (f b : Coefficient) : (angularField fun (p : CylPoint) => f p * b p) = fun (w : ProblemStatement.SpaceTime) => f (cylPoint w) • angularField b w

noncomputable def NavierStokes.DirectAngularDiagonal.cutCoefficient (a : ℝ) (q b : Coefficient) : Coefficient

Cut coefficient, defined pointwise by SmoothCutoffs.scaledCutoff a (q p) * b p.

Equations

• NavierStokes.DirectAngularDiagonal.cutCoefficient a q b p = NavierStokes.SmoothCutoffs.scaledCutoff a (q p) * b p

theorem NavierStokes.DirectAngularDiagonal.cut_angularField (a : ℝ) (q b : Coefficient) : angularField (cutCoefficient a q b) = fun (w : ProblemStatement.SpaceTime) => SmoothCutoffs.scaledCutoff a (q (cylPoint w)) • angularField b w

noncomputable def NavierStokes.DirectAngularDiagonal.AngularData.cut {U : Set Slow} (D : AngularData U) (a : ℝ) (q : Coefficient) (hq : ContDiffOn ℝ (↑⊤) q (positiveDomain U)) : AngularData U

Cut, given by D.multiply (fun p => SmoothCutoffs.scaledCutoff a (q p)) ((SmoothCutoffs.scaledCutoff_contDiff a).comp_contDiffOn hq).

Equations

• D.cut a q hq = D.multiply (fun (p : NavierStokes.DirectAngularDiagonal.CylPoint) => NavierStokes.SmoothCutoffs.scaledCutoff a (q p)) ⋯

theorem NavierStokes.DirectAngularDiagonal.divergence_cut_angular {U : Set Slow} (hU : IsOpen U) (D : AngularData U) (a : ℝ) (q : Coefficient) (hq : ContDiffOn ℝ (↑⊤) q (positiveDomain U)) {w : ProblemStatement.SpaceTime} (hw : w ∈ physicalDomain U) : ProblemStatement.spatialDivergence (fun (y : ProblemStatement.SpaceTime) => SmoothCutoffs.scaledCutoff a (q (cylPoint y)) • angularField D.scalar y) w.1 w.2 = 0

Locally finite direct angular sums

noncomputable def NavierStokes.DirectAngularDiagonal.angularSum (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (b : ℕ → Coefficient) : ProblemStatement.VelocityField

Angular sum, given by SolenoidalDiagonal.potentialSum a q (fun j => angularField (b j)).

Equations

• NavierStokes.DirectAngularDiagonal.angularSum a q b = NavierStokes.SolenoidalDiagonal.potentialSum a q fun (j : ℕ) => NavierStokes.DirectAngularDiagonal.angularField (b j)

noncomputable def NavierStokes.DirectAngularDiagonal.angularPartial (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (b : ℕ → Coefficient) (N : ℕ) : ProblemStatement.VelocityField

Angular partial, given by SolenoidalDiagonal.partialPotential a q (fun j => angularField (b j)) N.

Equations

• NavierStokes.DirectAngularDiagonal.angularPartial a q b N = NavierStokes.SolenoidalDiagonal.partialPotential a q (fun (j : ℕ) => NavierStokes.DirectAngularDiagonal.angularField (b j)) N

theorem NavierStokes.DirectAngularDiagonal.divergence_congr {v w : ProblemStatement.VelocityField} {x : ProblemStatement.SpaceTime} (h : v =ᶠ[nhds x] w) : ProblemStatement.spatialDivergence v x.1 x.2 = ProblemStatement.spatialDivergence w x.1 x.2

theorem NavierStokes.DirectAngularDiagonal.divergence_finset_sum {I : Type} (J : Finset I) (v : I → ProblemStatement.VelocityField) (x : ProblemStatement.SpaceTime) (hv : ∀ j ∈ J, DifferentiableAt ℝ (fun (y : ProblemStatement.Space) => v j (x.1, y)) x.2) : ProblemStatement.spatialDivergence (fun (y : ProblemStatement.SpaceTime) => ∑ j ∈ J, v j y) x.1 x.2 = ∑ j ∈ J, ProblemStatement.spatialDivergence (v j) x.1 x.2

theorem NavierStokes.DirectAngularDiagonal.angularSum_eventuallyEq_partial {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {x : ProblemStatement.SpaceTime} (hq : ContinuousAt q x) (hx : 0 < q x) (b : ℕ → Coefficient) : ∃ (N : ℕ), angularSum a q b =ᶠ[nhds x] angularPartial a q b N

theorem NavierStokes.DirectAngularDiagonal.angularSum_smooth {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} (hq : ContDiffOn ℝ (↑⊤) q (physicalDomain U)) (hpos : ∀ x ∈ physicalDomain U, 0 < q x) : ContDiffOn ℝ (↑⊤) (angularSum a q fun (j : ℕ) => (D j).scalar) (physicalDomain U)

theorem NavierStokes.DirectAngularDiagonal.angularSum_allJets {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} (hq : ContDiffOn ℝ (↑⊤) q (physicalDomain U)) (hpos : ∀ x ∈ physicalDomain U, 0 < q x) {x : ProblemStatement.SpaceTime} (hx : x ∈ physicalDomain U) : ∃ (N : ℕ), ∀ (k : ℕ), ∀ᶠ (y : ProblemStatement.SpaceTime) in nhds x, iteratedFDeriv ℝ k (angularSum a q fun (j : ℕ) => (D j).scalar) y = ∑ j ∈ Finset.range N, iteratedFDeriv ℝ k (SolenoidalDiagonal.cutStage a q (fun (j : ℕ) => angularField (D j).scalar) j) y

theorem NavierStokes.DirectAngularDiagonal.angularSum_locallyFinite {U : Set Slow} (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} (hq : ContinuousOn q (physicalDomain U)) (hpos : ∀ x ∈ physicalDomain U, 0 < q x) : LocallyFinite fun (j : ℕ) => Function.support fun (x : ↑(physicalDomain U)) => SolenoidalDiagonal.cutStage a q (fun (j : ℕ) => angularField (D j).scalar) j ↑x

theorem NavierStokes.DirectAngularDiagonal.angularSum_divergence {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) (q : Coefficient) (hq : ContDiffOn ℝ (↑⊤) q (positiveDomain U)) (hqp : ContDiffOn ℝ (↑⊤) (fun (x : ProblemStatement.SpaceTime) => q (cylPoint x)) (physicalDomain U)) (hpos : ∀ x ∈ physicalDomain U, 0 < q (cylPoint x)) {x : ProblemStatement.SpaceTime} (hx : x ∈ physicalDomain U) : ProblemStatement.spatialDivergence (angularSum a (fun (x : ProblemStatement.SpaceTime) => q (cylPoint x)) fun (j : ℕ) => (D j).scalar) x.1 x.2 = 0

theorem NavierStokes.DirectAngularDiagonal.angularSum_axis (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (b : ℕ → Coefficient) (t : ℝ) (x : ProblemStatement.Space) (h0 : x.ofLp 0 = 0) (h1 : x.ofLp 1 = 0) : angularSum a q b (t, x) = 0

theorem NavierStokes.DirectAngularDiagonal.angularSum_axis_zero_germ {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {x : ProblemStatement.SpaceTime} (hq : ContinuousAt q x) (hpos : 0 < q x) (hx : x ∈ physicalDomain U) (haxis : radius x = 0) : (angularSum a q fun (j : ℕ) => (D j).scalar) =ᶠ[nhds x] fun (x : ProblemStatement.SpaceTime) => 0

Curl potentials plus direct angular velocity

noncomputable def NavierStokes.DirectAngularDiagonal.mixedVelocity (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (A : ℕ → ProblemStatement.VelocityField) (b : ℕ → Coefficient) : ProblemStatement.VelocityField

Mixed velocity, defined pointwise by SolenoidalDiagonal.velocitySum a q A x + angularSum a q b x.

Equations

• NavierStokes.DirectAngularDiagonal.mixedVelocity a q A b x = NavierStokes.SolenoidalDiagonal.velocitySum a q A x + NavierStokes.DirectAngularDiagonal.angularSum a q b x

theorem NavierStokes.DirectAngularDiagonal.mixedVelocity_smooth {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} (hq : ContDiffOn ℝ (↑⊤) q (physicalDomain U)) (hpos : ∀ x ∈ physicalDomain U, 0 < q x) {A : ℕ → ProblemStatement.VelocityField} (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) (physicalDomain U)) : ContDiffOn ℝ (↑⊤) (mixedVelocity a q A fun (j : ℕ) => (D j).scalar) (physicalDomain U)

theorem NavierStokes.DirectAngularDiagonal.mixedVelocity_divergence {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) (q : Coefficient) (hq : ContDiffOn ℝ (↑⊤) q (positiveDomain U)) (hqp : ContDiffOn ℝ (↑⊤) (fun (x : ProblemStatement.SpaceTime) => q (cylPoint x)) (physicalDomain U)) (hpos : ∀ x ∈ physicalDomain U, 0 < q (cylPoint x)) {A : ℕ → ProblemStatement.VelocityField} (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) (physicalDomain U)) {x : ProblemStatement.SpaceTime} (hx : x ∈ physicalDomain U) : ProblemStatement.spatialDivergence (mixedVelocity a (fun (x : ProblemStatement.SpaceTime) => q (cylPoint x)) A fun (j : ℕ) => (D j).scalar) x.1 x.2 = 0

theorem NavierStokes.DirectAngularDiagonal.mixedVelocity_axis (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (A : ℕ → ProblemStatement.VelocityField) (b : ℕ → Coefficient) (t : ℝ) (x : ProblemStatement.Space) (h0 : x.ofLp 0 = 0) (h1 : x.ofLp 1 = 0) : mixedVelocity a q A b (t, x) = SolenoidalDiagonal.velocitySum a q A (t, x)

The actual similarity cutoff

noncomputable def NavierStokes.DirectAngularDiagonal.preterminalSlow : Set Slow

Preterminal slow, given by {s | s.1 < 1}.

Equations

• NavierStokes.DirectAngularDiagonal.preterminalSlow = {s : NavierStokes.DirectAngularDiagonal.Slow | s.1 < 1}

theorem NavierStokes.DirectAngularDiagonal.preterminalSlow_open : IsOpen preterminalSlow

noncomputable def NavierStokes.DirectAngularDiagonal.qCoefficient (h : ℝ) : Coefficient

Q coefficient, given by SimilarityProfile.q h.

Equations

• NavierStokes.DirectAngularDiagonal.qCoefficient h = NavierStokes.SimilarityProfile.q h

theorem NavierStokes.DirectAngularDiagonal.qCoefficient_physical (h : ℝ) (w : ProblemStatement.SpaceTime) : qCoefficient h (cylPoint w) = PhysicalWaveSum.physicalQ h w

theorem NavierStokes.DirectAngularDiagonal.physicalDomain_preterminal : physicalDomain preterminalSlow = PhysicalWaveSum.preterminal

theorem NavierStokes.DirectAngularDiagonal.qCoefficient_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (qCoefficient h) (positiveDomain preterminalSlow)

theorem NavierStokes.DirectAngularDiagonal.physicalQ_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (PhysicalWaveSum.physicalQ h) (physicalDomain preterminalSlow)

theorem NavierStokes.DirectAngularDiagonal.actual_diagonal_divergence {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → AngularData preterminalSlow) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {w : ProblemStatement.SpaceTime} (hw : w.1 < 1) : ProblemStatement.spatialDivergence (angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar) w.1 w.2 = 0

theorem NavierStokes.DirectAngularDiagonal.actual_diagonal_smooth {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → AngularData preterminalSlow) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) : ContDiffOn ℝ (↑⊤) (angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar) PhysicalWaveSum.preterminal

theorem NavierStokes.DirectAngularDiagonal.actual_mixed_divergence {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → AngularData preterminalSlow) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {A : ℕ → ProblemStatement.VelocityField} (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) PhysicalWaveSum.preterminal) {w : ProblemStatement.SpaceTime} (hw : w.1 < 1) : ProblemStatement.spatialDivergence (mixedVelocity a (PhysicalWaveSum.physicalQ h) A fun (j : ℕ) => (D j).scalar) w.1 w.2 = 0

The existing Cartesian spatial cutoff is axisymmetric

noncomputable def NavierStokes.DirectAngularDiagonal.spatialProfile (p : CylPoint) : ℝ

Spatial profile, given by SpatialLocalization.cutoffProfile (p.2.1 ^ 2, p.2.2).

Equations

• NavierStokes.DirectAngularDiagonal.spatialProfile p = NavierStokes.SpatialLocalization.cutoffProfile (p.2.1 ^ 2, p.2.2)

theorem NavierStokes.DirectAngularDiagonal.spatialProfile_smooth : ContDiff ℝ (↑⊤) spatialProfile

theorem NavierStokes.DirectAngularDiagonal.spatialProfile_physical (w : ProblemStatement.SpaceTime) : spatialProfile (cylPoint w) = SpatialLocalization.spatialCutoff w.2

theorem NavierStokes.DirectAngularDiagonal.spatialCut_angular {U : Set Slow} (hU : IsOpen U) (D : AngularData U) {w : ProblemStatement.SpaceTime} (hw : w ∈ physicalDomain U) : ProblemStatement.spatialDivergence (SpatialLocalization.cutPotential (angularField D.scalar)) w.1 w.2 = 0

theorem NavierStokes.DirectAngularDiagonal.angularSum_multiply (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (f : Coefficient) (b : ℕ → Coefficient) : (angularSum a q fun (j : ℕ) (p : CylPoint) => f p * b j p) = fun (w : ProblemStatement.SpaceTime) => f (cylPoint w) • angularSum a q b w

theorem NavierStokes.DirectAngularDiagonal.spatialCut_angularSum (a : ℕ → ℝ) (q : ProblemStatement.SpaceTime → ℝ) (b : ℕ → Coefficient) : SpatialLocalization.cutPotential (angularSum a q b) = angularSum a q fun (j : ℕ) (p : CylPoint) => spatialProfile p * b j p

theorem NavierStokes.DirectAngularDiagonal.spatialCut_angularSum_divergence {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) (q : Coefficient) (hq : ContDiffOn ℝ (↑⊤) q (positiveDomain U)) (hqp : ContDiffOn ℝ (↑⊤) (fun (x : ProblemStatement.SpaceTime) => q (cylPoint x)) (physicalDomain U)) (hpos : ∀ x ∈ physicalDomain U, 0 < q (cylPoint x)) {x : ProblemStatement.SpaceTime} (hx : x ∈ physicalDomain U) : ProblemStatement.spatialDivergence (SpatialLocalization.cutPotential (angularSum a (fun (x : ProblemStatement.SpaceTime) => q (cylPoint x)) fun (j : ℕ) => (D j).scalar)) x.1 x.2 = 0

theorem NavierStokes.DirectAngularDiagonal.actual_spatialCut_diagonal_divergence {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → AngularData preterminalSlow) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) (t : ℝ) (ht : t < 1) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (SpatialLocalization.cutPotential (angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar)) t x = 0

Actual full-fiber means restricted to a physical graph

@[reducible, inline]

abbrev NavierStokes.DirectAngularDiagonal.Lift : Type

Lift: an abbreviation for PressureStream.Lift Slow.

Equations

• NavierStokes.DirectAngularDiagonal.Lift = NavierStokes.PressureStream.Lift NavierStokes.DirectAngularDiagonal.Slow

noncomputable def NavierStokes.DirectAngularDiagonal.graphSlow (G : PhysicalResidualBridge.ScaledGraph) (s : Slow) : Slow

The time/axial variables in the actual mean-field convention (T,Z).

Equations

• NavierStokes.DirectAngularDiagonal.graphSlow G s = (G.velocityScale * G.radialScale * G.epsilon * (1 - s.1), G.radialScale * G.epsilon * s.2)

noncomputable def NavierStokes.DirectAngularDiagonal.graphPoint (G : PhysicalResidualBridge.ScaledGraph) (p : CylPoint) : Lift

Graph point as an element of Lift.

Equations

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

noncomputable def NavierStokes.DirectAngularDiagonal.graphCoefficient (G : PhysicalResidualBridge.ScaledGraph) (f : Lift → ℝ) : Coefficient

The physical velocity normalization is included here.

Equations

• NavierStokes.DirectAngularDiagonal.graphCoefficient G f p = G.velocityScale * f (NavierStokes.DirectAngularDiagonal.graphPoint G p)

theorem NavierStokes.DirectAngularDiagonal.graphPoint_actual (G : PhysicalResidualBridge.ScaledGraph) (p : CylPoint) (theta : ℝ) : graphPoint G p = PhysicalResidualTZ.swapSlow (G.map (p.1, AxisymmetricResidual.pack p.2.1 theta p.2.2)).1

theorem NavierStokes.DirectAngularDiagonal.graphCoefficient_actual (G : PhysicalResidualBridge.ScaledGraph) (f : Lift → ℝ) (p : CylPoint) (theta : ℝ) : graphCoefficient G f p = G.velocityScale * f (PhysicalResidualTZ.swapSlow (G.map (p.1, AxisymmetricResidual.pack p.2.1 theta p.2.2)).1)

theorem NavierStokes.DirectAngularDiagonal.graphSlow_smooth (G : PhysicalResidualBridge.ScaledGraph) : ContDiff ℝ (↑⊤) (graphSlow G)

theorem NavierStokes.DirectAngularDiagonal.graphPoint_smoothAt (G : PhysicalResidualBridge.ScaledGraph) (hG : 0 < G.radialScale) {p : CylPoint} (hp : 0 < p.2.1) : ContDiffAt ℝ (↑⊤) (graphPoint G) p

noncomputable def NavierStokes.DirectAngularDiagonal.graphAngularData (G : PhysicalResidualBridge.ScaledGraph) (hG : 0 < G.radialScale) {U : Set Slow} (hU : IsOpen U) {a b : ℝ} (ha : 0 < a) (ell : Slow → ℝ) (hell : ContinuousOn ell U) (hpos : ∀ s ∈ U, 0 < ell s) (f : Lift → ℝ) (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : VariableGaugeMean.SupportedGauge a b ell U f) : AngularData (graphSlow G ⁻¹' U)

Smoothness and the positive moving support of the actual mean field produce the angular data. No divergence or physical output is assumed.

Equations

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

noncomputable def NavierStokes.DirectAngularDiagonal.commonAngularData {Q : ℝ} (hQ : 0 < Q) (h : ℝ) (cover : ℕ) {U : Set Slow} (hU : IsOpen U) {a b : ℝ} (ha : 0 < a) (ell : Slow → ℝ) (hell : ContinuousOn ell U) (hpos : ∀ s ∈ U, 0 < ell s) (f : Lift → ℝ) (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : VariableGaugeMean.SupportedGauge a b ell U f) : AngularData (graphSlow (PhysicalResidualBridge.commonGraph Q h cover) ⁻¹' U)

Common angular data, given by graphAngularData _ (Real.rpow_pos_of_pos hQ _) hU ha ell hell hpos f hf hs.

Equations

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

theorem NavierStokes.DirectAngularDiagonal.commonCoefficient_actual (Q h : ℝ) (cover : ℕ) (f : Lift → ℝ) (p : CylPoint) (theta : ℝ) : graphCoefficient (PhysicalResidualBridge.commonGraph Q h cover) f p = Q ^ (-CoordinateAlgebra.A h) * f (PhysicalResidualTZ.swapSlow ((PhysicalResidualBridge.commonGraph Q h cover).map (p.1, AxisymmetricResidual.pack p.2.1 theta p.2.2)).1)

The common-graph coefficient carries exactly the manuscript's Q^(-A) velocity factor, with no independent angular choice.

noncomputable def NavierStokes.DirectAngularDiagonal.temporalAngularData (G : PhysicalResidualBridge.ScaledGraph) (hG : 0 < G.radialScale) (g : VariableGaugeMean.GaugeData Slow) (h : ℝ) (index : ℕ → ℕ) (axial : Slow × PressureStream.Plane) (c : CorrectionState.Context Lift) (u : CorrectionState.State Lift) (n : ℕ) {U : Set Slow} (hU : IsOpen U) {a b : ℝ} (ha : 0 < a) (ell : Slow → ℝ) (hell : ContinuousOn ell U) (hpos : ∀ s ∈ U, 0 < ell s) (hf : ContDiffOn ℝ (↑⊤) (u.thetaResidual c n) (PhysicalMeanDomain.slowDomain U)) (hp : PhysicalMeanDomain.PeriodicOn U (u.thetaResidual c n)) (hs : VariableGaugeMean.SupportedGauge a b ell U (u.thetaResidual c n)) : AngularData (graphSlow G ⁻¹' U)

The direct angular part of the literal temporal update, with its regularity and support inherited from the actual input residual.

Equations

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

noncomputable def NavierStokes.DirectAngularDiagonal.rankAngularData (G : PhysicalResidualBridge.ScaledGraph) (hG : 0 < G.radialScale) (g : VariableGaugeMean.GaugeData Slow) (r : CorrectionState.RankData Slow) (axial : Slow × PressureStream.Plane) (c : CorrectionState.Context Lift) (u : CorrectionState.State Lift) (n : ℕ) {U : Set Slow} (hU : IsOpen U) (H : LocalRankDefect.RankGeometry g r U c u) : AngularData (graphSlow G ⁻¹' U)

The direct angular part of the literal rank update. Its smoothness comes from the actual five-row rank family and current debt.

Equations

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

Agreement with the actual offplane continuation fields

noncomputable def NavierStokes.DirectAngularDiagonal.nativeGraphData (h : ℝ) (n : ℕ) : PhysicalResidualBridge.ScaledGraph

Native graph data, bundling radialScale, velocityScale, epsilon, exponent and the required compatibility proofs.

Equations

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

theorem NavierStokes.DirectAngularDiagonal.native_graphPoint (h : ℝ) (n : ℕ) (w : ProblemStatement.SpaceTime) : graphPoint (nativeGraphData h n) (cylPoint w) = OffplaneCorrectionExtensions.physicalLift h n w

theorem NavierStokes.DirectAngularDiagonal.native_angularField (h : ℝ) (n : ℕ) (f : Lift → ℝ) : angularField (graphCoefficient (nativeGraphData h n) f) = OffplaneCorrectionExtensions.angularField h n f

This is the direct continuation field, with no curl applied.

noncomputable def NavierStokes.DirectAngularDiagonal.continuationAngularData {coord a b : ℝ} {W : OffplaneCorrectionExtensions.Window coord a b} {f : Lift → ℝ} (e : OffplaneCorrectionExtensions.SupportedContinuation W f) (h : ℝ) (n : ℕ) : AngularData (graphSlow (nativeGraphData h n) ⁻¹' W.carrier)

Continuation angular data, constructed using graphAngularData.

Equations

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

theorem NavierStokes.DirectAngularDiagonal.continuation_angular_divergence {coord a b : ℝ} {W : OffplaneCorrectionExtensions.Window coord a b} {f : Lift → ℝ} (e : OffplaneCorrectionExtensions.SupportedContinuation W f) (h : ℝ) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ OffplaneCorrectionExtensions.physicalDomain W.carrier) : ProblemStatement.spatialDivergence (OffplaneCorrectionExtensions.angularField h n e.value) w.1 w.2 = 0

Mixed finite prefixes and preservation of every axis jet

theorem NavierStokes.DirectAngularDiagonal.mixedVelocity_allJets {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} (hq : ContDiffOn ℝ (↑⊤) q (physicalDomain U)) (hpos : ∀ x ∈ physicalDomain U, 0 < q x) {A : ℕ → ProblemStatement.VelocityField} (hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) (physicalDomain U)) {x : ProblemStatement.SpaceTime} (hx : x ∈ physicalDomain U) : ∃ (N : ℕ) (M : ℕ), ∀ (k : ℕ), iteratedFDeriv ℝ k (mixedVelocity a q A fun (j : ℕ) => (D j).scalar) =ᶠ[nhds x] iteratedFDeriv ℝ k fun (y : ProblemStatement.SpaceTime) => ∑ j ∈ Finset.range N, SpatialCurl.spatialCurl (SolenoidalDiagonal.cutStage a q A j) y + angularPartial a q (fun (j : ℕ) => (D j).scalar) M y

theorem NavierStokes.DirectAngularDiagonal.angularSum_axis_jets {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {x : ProblemStatement.SpaceTime} (hq : ContinuousAt q x) (hpos : 0 < q x) (hx : x ∈ physicalDomain U) (haxis : radius x = 0) (k : ℕ) : iteratedFDeriv ℝ k (angularSum a q fun (j : ℕ) => (D j).scalar) x = 0

theorem NavierStokes.DirectAngularDiagonal.potentialSum_zero_germ {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {x : ProblemStatement.SpaceTime} (hq : ContinuousAt q x) (hpos : 0 < q x) (A : ℕ → ProblemStatement.VelocityField) (hA : ∀ (j : ℕ), A j =ᶠ[nhds x] fun (x : ProblemStatement.SpaceTime) => 0) : SolenoidalDiagonal.potentialSum a q A =ᶠ[nhds x] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.DirectAngularDiagonal.mixedVelocity_axis_zero_germ {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {x : ProblemStatement.SpaceTime} (hq : ContinuousAt q x) (hpos : 0 < q x) (hx : x ∈ physicalDomain U) (haxis : radius x = 0) (A : ℕ → ProblemStatement.VelocityField) (hA : ∀ (j : ℕ), A j =ᶠ[nhds x] fun (x : ProblemStatement.SpaceTime) => 0) : (mixedVelocity a q A fun (j : ℕ) => (D j).scalar) =ᶠ[nhds x] fun (x : ProblemStatement.SpaceTime) => 0

If the actual potentials vanish near the axis, adding the direct angular diagonal preserves the entire axis germ, hence every axis jet.

theorem NavierStokes.DirectAngularDiagonal.mixedVelocity_axis_jets {U : Set Slow} (hU : IsOpen U) (D : ℕ → AngularData U) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {x : ProblemStatement.SpaceTime} (hq : ContinuousAt q x) (hpos : 0 < q x) (hx : x ∈ physicalDomain U) (haxis : radius x = 0) (A : ℕ → ProblemStatement.VelocityField) (hA : ∀ (j : ℕ), A j =ᶠ[nhds x] fun (x : ProblemStatement.SpaceTime) => 0) (k : ℕ) : iteratedFDeriv ℝ k (mixedVelocity a q A fun (j : ℕ) => (D j).scalar) x = 0