Preservation of the axis value under annular corrections

Actual physical wave sums vanish on a neighborhood of each preterminal axis point. Local finiteness, first in labels and then in diagonal stages, therefore preserves the zeroth potential's curl. No uniform radius in the stage number and no estimate on the final velocity are assumed.

theorem NavierStokes.AxisPreservation.wave_sum_zero_near_axis {H : ℕ} {f : PhysicalWaveSum.WaveFamily H} {a b h r0 Z : ℝ} {gap : ℕ} (hf : PhysicalWaveSum.RegularFamily f a b h r0 Z gap) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : f.sum a h r0 =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.AxisPreservation.vector_sum_zero_near_axis {H : ℕ} {f : Fin 3 → PhysicalWaveSum.WaveFamily H} {a b h r0 Z : ℝ} {gap : ℕ} (hf : ∀ (i : Fin 3), PhysicalWaveSum.RegularFamily (f i) a b h r0 Z gap) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : PhysicalWaveSum.vectorSum f a h r0 =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.AxisPreservation.wave_curl_zero_on_axis {H : ℕ} {f : Fin 3 → PhysicalWaveSum.WaveFamily H} {a b h r0 Z : ℝ} {gap : ℕ} (hf : ∀ (i : Fin 3), PhysicalWaveSum.RegularFamily (f i) a b h r0 Z gap) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) {w : ProblemStatement.SpaceTime} (hw : w ∈ PhysicalWaveSum.preterminal) (haxis : PhysicalGraphBounds.radialProjection w = 0) : SpatialCurl.spatialCurl (PhysicalWaveSum.vectorSum f a h r0) w = 0

theorem NavierStokes.AxisPreservation.potentialSum_eq_first_near {scales : ℕ → ℝ} (hscales : Filter.Tendsto scales Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A : ℕ → ProblemStatement.VelocityField} {w : ProblemStatement.SpaceTime} (hq : ContinuousAt q w) (hpos : 0 < q w) (hzero : ∀ (j : ℕ), j ≠ 0 → A j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) : SolenoidalDiagonal.potentialSum scales q A =ᶠ[nhds w] SolenoidalDiagonal.cutStage scales q A 0

Only finitely many zero germs are intersected at each positive-scale point. There is no common support radius assumed for every stage.

theorem NavierStokes.AxisPreservation.velocitySum_eq_first {scales : ℕ → ℝ} (hscales : Filter.Tendsto scales Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A : ℕ → ProblemStatement.VelocityField} {w : ProblemStatement.SpaceTime} (hq : ContinuousAt q w) (hpos : 0 < q w) (hzero : ∀ (j : ℕ), j ≠ 0 → A j =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0) (hsmall : |scales 0 * q w| < 1 / 2) : SolenoidalDiagonal.velocitySum scales q A w = SpatialCurl.spatialCurl (A 0) w

theorem NavierStokes.AxisPreservation.origin_eventually_eq_first {scales : ℕ → ℝ} (hscales : Filter.Tendsto scales Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A : ℕ → ProblemStatement.VelocityField} (hq : ∀ t < 1, ContinuousAt q (t, 0)) (hpos : ∀ t < 1, 0 < q (t, 0)) (hzero : ∀ t < 1, ∀ (j : ℕ), j ≠ 0 → A j =ᶠ[nhds (t, 0)] fun (x : ℝ × ProblemStatement.Space) => 0) (hlimit : Filter.Tendsto (fun (t : ℝ) => q (t, 0)) (nhdsWithin 1 (Set.Iio 1)) (nhds 0)) : (fun (t : ℝ) => SolenoidalDiagonal.velocitySum scales q A (t, 0)) =ᶠ[nhdsWithin 1 (Set.Iio 1)] fun (t : ℝ) => SpatialCurl.spatialCurl (A 0) (t, 0)

theorem NavierStokes.AxisPreservation.origin_blowup {scales : ℕ → ℝ} (hscales : Filter.Tendsto scales Filter.atTop Filter.atTop) {q : ProblemStatement.SpaceTime → ℝ} {A : ℕ → ProblemStatement.VelocityField} (hq : ∀ t < 1, ContinuousAt q (t, 0)) (hpos : ∀ t < 1, 0 < q (t, 0)) (hzero : ∀ t < 1, ∀ (j : ℕ), j ≠ 0 → A j =ᶠ[nhds (t, 0)] fun (x : ℝ × ProblemStatement.Space) => 0) (hlimit : Filter.Tendsto (fun (t : ℝ) => q (t, 0)) (nhdsWithin 1 (Set.Iio 1)) (nhds 0)) (hbase : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl (A 0) (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖SolenoidalDiagonal.velocitySum scales q A (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

theorem NavierStokes.AxisPreservation.physicalQ_origin {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {t : ℝ} (ht : t < 1) : PhysicalWaveSum.physicalQ h (t, 0) = 1 - t

theorem NavierStokes.AxisPreservation.physicalQ_origin_tendsto {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : Filter.Tendsto (fun (t : ℝ) => PhysicalWaveSum.physicalQ h (t, 0)) (nhdsWithin 1 (Set.Iio 1)) (nhds 0)

noncomputable def NavierStokes.AxisPreservation.waveSeries (base : ProblemStatement.VelocityField) (H : ℕ → ℕ) (f : (j : ℕ) → Fin 3 → PhysicalWaveSum.WaveFamily (H j)) (a h r0 : ℝ) : ℕ → ProblemStatement.VelocityField

The zeroth potential is kept separate from the annular wave increments. Each increment may have its own finite harmonic band.

Equations

• NavierStokes.AxisPreservation.waveSeries base H f a h r0 0 = base
• NavierStokes.AxisPreservation.waveSeries base H f a h r0 j.succ = NavierStokes.PhysicalWaveSum.vectorSum (f j) a h r0

theorem NavierStokes.AxisPreservation.physical_wave_diagonal_origin_blowup {base : ProblemStatement.VelocityField} {H : ℕ → ℕ} {f : (j : ℕ) → Fin 3 → PhysicalWaveSum.WaveFamily (H j)} {a b h r0 : ℝ} {Z : ℕ → ℝ} {gap : ℕ → ℕ} (hf : ∀ (j : ℕ) (i : Fin 3), PhysicalWaveSum.RegularFamily (f j i) a b h r0 (Z j) (gap j)) (ha : 0 < a) (hh : 0 < h) (hh1 : h < 1 / 2) {scales : ℕ → ℝ} (hscales : Filter.Tendsto scales Filter.atTop Filter.atTop) (hbase : Filter.Tendsto (fun (t : ℝ) => ‖SpatialCurl.spatialCurl base (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop) : Filter.Tendsto (fun (t : ℝ) => ‖SolenoidalDiagonal.velocitySum scales (PhysicalWaveSum.physicalQ h) (waveSeries base H f a h r0) (t, 0)‖) (nhdsWithin 1 (Set.Iio 1)) Filter.atTop