Direct angular diagonal from local raw data

The raw angular means need be smooth only where the actual physical similarity parameter is below qbig. All cutoffs use the same sequence. Its first support lies strictly inside that raw domain. Above the raw domain every cutoff vanishes on one common neighborhood, so the original sum itself is smooth and divergence-free on the whole preterminal region. No global smooth replacement of the raw scalar is chosen.

noncomputable def NavierStokes.LocalAngularDiagonal.slowQ (h : ℝ) (s : DirectAngularDiagonal.Slow) : ℝ

The actual similarity parameter depends only on physical time and the axial coordinate, and not on radius or angle.

Equations

• NavierStokes.LocalAngularDiagonal.slowQ h s = NavierStokes.SimilarityCoordinates.coordinateQ (2 * h) (1 - s.1, s.2)

noncomputable def NavierStokes.LocalAngularDiagonal.localSlowDomain (h qbig : ℝ) : Set DirectAngularDiagonal.Slow

Local slow domain, given by {s | s.1 < 1 ∧ slowQ h s < qbig}.

Equations

• NavierStokes.LocalAngularDiagonal.localSlowDomain h qbig = {s : NavierStokes.DirectAngularDiagonal.Slow | s.1 < 1 ∧ NavierStokes.LocalAngularDiagonal.slowQ h s < qbig}

theorem NavierStokes.LocalAngularDiagonal.slowQ_physical (h : ℝ) (w : ProblemStatement.SpaceTime) : slowQ h (DirectAngularDiagonal.slowPoint w) = PhysicalWaveSum.physicalQ h w

theorem NavierStokes.LocalAngularDiagonal.slowQ_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {s : DirectAngularDiagonal.Slow} (hs : s.1 < 1) : ContDiffAt ℝ (↑⊤) (slowQ h) s

theorem NavierStokes.LocalAngularDiagonal.localSlowDomain_open {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (qbig : ℝ) : IsOpen (localSlowDomain h qbig)

theorem NavierStokes.LocalAngularDiagonal.physicalDomain_eq_localDomain (h qbig : ℝ) : DirectAngularDiagonal.physicalDomain (localSlowDomain h qbig) = MixedAxisPreservation.localDomain h qbig

theorem NavierStokes.LocalAngularDiagonal.physicalDomain_eq_physicalSublevel (h qbig : ℝ) : DirectAngularDiagonal.physicalDomain (localSlowDomain h qbig) = CutStageEstimates.physicalSublevel h qbig

theorem NavierStokes.LocalAngularDiagonal.localSlowDomain_subset (h qbig : ℝ) : localSlowDomain h qbig ⊆ DirectAngularDiagonal.preterminalSlow

noncomputable def NavierStokes.LocalAngularDiagonal.rawSeries {h qbig : ℝ} (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) : ℕ → ProblemStatement.VelocityField

The literal uncut direct angular fields used in the diagonal.

Equations

• NavierStokes.LocalAngularDiagonal.rawSeries D j = NavierStokes.DirectAngularDiagonal.angularField (D j).scalar

theorem NavierStokes.LocalAngularDiagonal.rawSeries_eq {h qbig : ℝ} (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) (j : ℕ) : rawSeries D j = DirectAngularDiagonal.angularField (D j).scalar

theorem NavierStokes.LocalAngularDiagonal.rawSeries_smooth {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) (j : ℕ) : ContDiffOn ℝ (↑⊤) (rawSeries D j) (CutStageEstimates.physicalSublevel h qbig)

noncomputable def NavierStokes.LocalAngularDiagonal.angularSupport {h qbig : ℝ} (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) : ℕ → MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain h qbig)

Axis preservation uses exactly the same local scalars and support, without imposing global raw smoothness.

Equations

• NavierStokes.LocalAngularDiagonal.angularSupport D j = NavierStokes.MixedAxisPreservation.AngularSupport.ofAngularData (D j) ⋯

theorem NavierStokes.LocalAngularDiagonal.angularSupport_field {h qbig : ℝ} (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) (j : ℕ) : (angularSupport D j).field = rawSeries D j

theorem NavierStokes.LocalAngularDiagonal.angularSum_eq_potentialSum {h qbig : ℝ} (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) (a : ℕ → ℝ) : (DirectAngularDiagonal.angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar) = SolenoidalDiagonal.potentialSum a (PhysicalWaveSum.physicalQ h) (rawSeries D)

theorem NavierStokes.LocalAngularDiagonal.angularSum_eq_directDiagonal {h qbig : ℝ} (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) (a : ℕ → ℝ) : (DirectAngularDiagonal.angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar) = MixedAxisPreservation.directDiagonal h (angularSupport D) a

One common zero neighborhood above the cutoff support

theorem NavierStokes.LocalAngularDiagonal.cutStages_zero_germ {a : ℕ → ℝ} (ha0 : 0 < a 0) (ham : ∀ (j : ℕ), a 0 ≤ a j) {q : ProblemStatement.SpaceTime → ℝ} {w : ProblemStatement.SpaceTime} (hq : ContinuousAt q w) (hlarge : 1 / a 0 < q w) (F : ℕ → ProblemStatement.VelocityField) : ∀ᶠ (y : ProblemStatement.SpaceTime) in nhds w, ∀ (j : ℕ), SolenoidalDiagonal.cutStage a q F j y = 0

theorem NavierStokes.LocalAngularDiagonal.sum_zero_germ {a : ℕ → ℝ} (ha0 : 0 < a 0) (ham : ∀ (j : ℕ), a 0 ≤ a j) {q : ProblemStatement.SpaceTime → ℝ} {w : ProblemStatement.SpaceTime} (hq : ContinuousAt q w) (hlarge : 1 / a 0 < q w) (F : ℕ → ProblemStatement.VelocityField) : SolenoidalDiagonal.potentialSum a q F =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.LocalAngularDiagonal.angularSum_zero_germ {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) {a : ℕ → ℝ} (ha0 : 0 < a 0) (ham : ∀ (j : ℕ), a 0 ≤ a j) (hgap : 1 / a 0 < qbig) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) (hq : qbig ≤ PhysicalWaveSum.physicalQ h w) : (DirectAngularDiagonal.angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar) =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.LocalAngularDiagonal.spatialCut_zero_germ {f : ProblemStatement.VelocityField} {w : ProblemStatement.SpaceTime} (hf : f =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) : SpatialLocalization.cutPotential f =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

Smoothness on the whole preterminal region

theorem NavierStokes.LocalAngularDiagonal.angularSum_smoothAt {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) {a : ℕ → ℝ} (hat : Filter.Tendsto a Filter.atTop Filter.atTop) (ha0 : 0 < a 0) (ham : ∀ (j : ℕ), a 0 ≤ a j) (hgap : 1 / a 0 < qbig) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : ContDiffAt ℝ (↑⊤) (DirectAngularDiagonal.angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar) w

theorem NavierStokes.LocalAngularDiagonal.angularSum_smooth {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) {a : ℕ → ℝ} (hat : Filter.Tendsto a Filter.atTop Filter.atTop) (ha0 : 0 < a 0) (ham : ∀ (j : ℕ), a 0 ≤ a j) (hgap : 1 / a 0 < qbig) : ContDiffOn ℝ (↑⊤) (DirectAngularDiagonal.angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar) PhysicalWaveSum.preterminal

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

theorem NavierStokes.LocalAngularDiagonal.physicalQ_smooth {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (fun (w : ProblemStatement.SpaceTime) => DirectAngularDiagonal.qCoefficient h (DirectAngularDiagonal.cylPoint w)) (DirectAngularDiagonal.physicalDomain (localSlowDomain h qbig))

theorem NavierStokes.LocalAngularDiagonal.angularSum_divergence {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) {a : ℕ → ℝ} (hat : Filter.Tendsto a Filter.atTop Filter.atTop) (ha0 : 0 < a 0) (ham : ∀ (j : ℕ), a 0 ≤ a j) (hgap : 1 / a 0 < qbig) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : ProblemStatement.spatialDivergence (DirectAngularDiagonal.angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar) w.1 w.2 = 0

theorem NavierStokes.LocalAngularDiagonal.spatialCut_angularSum_divergence {h qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (D : ℕ → DirectAngularDiagonal.AngularData (localSlowDomain h qbig)) {a : ℕ → ℝ} (hat : Filter.Tendsto a Filter.atTop Filter.atTop) (ha0 : 0 < a 0) (ham : ∀ (j : ℕ), a 0 ≤ a j) (hgap : 1 / a 0 < qbig) (t : ℝ) (ht : t < 1) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (SpatialLocalization.cutPotential (DirectAngularDiagonal.angularSum a (PhysicalWaveSum.physicalQ h) fun (j : ℕ) => (D j).scalar)) t x = 0

Multiplication by the existing axisymmetric spatial cutoff preserves divergence of the same local-data diagonal on every preterminal point.