Smooth solenoidal diagonal sums #
The sum in this file is an actual tsum of cut potentials. At each point
where the continuous scale q is positive, an entire tail is identically zero
on a common neighborhood. Thus the sum equals a finite prefix locally.
Smoothness requires smooth q and smooth potentials; mere continuity of q
is sufficient for local finiteness only. The resulting spatial curl is smooth
and divergence-free. No residual estimate or singular endpoint regularity is
assumed or proved here.
noncomputable def
NavierStokes.SolenoidalDiagonal.cutStage
{X : Type u_1}
{V : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(a : ℕ → ℝ)
(q : X → ℝ)
(A : ℕ → X → V)
(j : ℕ)
(x : X)
:
V
Cut the potential before applying any velocity derivative.
Equations
- NavierStokes.SolenoidalDiagonal.cutStage a q A j x = NavierStokes.SmoothCutoffs.scaledCutoff (a j) (q x) • A j x
Instances For
noncomputable def
NavierStokes.SolenoidalDiagonal.potentialSum
{X : Type u_1}
{V : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(a : ℕ → ℝ)
(q : X → ℝ)
(A : ℕ → X → V)
(x : X)
:
V
The actual infinite sum; local finiteness below proves it is well behaved on the positive-scale domain.
Equations
- NavierStokes.SolenoidalDiagonal.potentialSum a q A x = ∑' (j : ℕ), NavierStokes.SolenoidalDiagonal.cutStage a q A j x
Instances For
noncomputable def
NavierStokes.SolenoidalDiagonal.partialPotential
{X : Type u_1}
{V : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
(a : ℕ → ℝ)
(q : X → ℝ)
(A : ℕ → X → V)
(N : ℕ)
(x : X)
:
V
Partial potential, given by ∑ j ∈ Finset.range N, cutStage a q A j x.
Equations
- NavierStokes.SolenoidalDiagonal.partialPotential a q A N x = ∑ j ∈ Finset.range N, NavierStokes.SolenoidalDiagonal.cutStage a q A j x
Instances For
theorem
NavierStokes.SolenoidalDiagonal.eventually_zero_tail
{X : Type u_1}
{V : Type u_2}
[TopologicalSpace X]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : X → ℝ}
{x : X}
(hq : ContinuousAt q x)
(hqx : 0 < q x)
(A : ℕ → X → V)
:
A common neighborhood, not merely a pointwise support bound, kills all sufficiently late stages. No regularity of the potentials is needed.
theorem
NavierStokes.SolenoidalDiagonal.potentialSum_eventuallyEq_partial
{X : Type u_1}
{V : Type u_2}
[TopologicalSpace X]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : X → ℝ}
{x : X}
(hq : ContinuousAt q x)
(hqx : 0 < q x)
(A : ℕ → X → V)
:
∃ (N : ℕ), potentialSum a q A =ᶠ[nhds x] partialPotential a q A N
Local equality to a finite prefix establishes the meaning of the tsum.
The prefix length works for all derivative orders.
theorem
NavierStokes.SolenoidalDiagonal.summable_cutStage
{X : Type u_1}
{V : Type u_2}
[TopologicalSpace X]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : X → ℝ}
{x : X}
(hq : ContinuousAt q x)
(hqx : 0 < q x)
(A : ℕ → X → V)
:
theorem
NavierStokes.SolenoidalDiagonal.locallyFinite_cutStage_support
{X : Type u_1}
{V : Type u_2}
[TopologicalSpace X]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : X → ℝ}
(hq : Continuous q)
(hqpos : ∀ (x : X), 0 < q x)
(A : ℕ → X → V)
:
LocallyFinite fun (j : ℕ) => Function.support (cutStage a q A j)
The family of supports is locally finite on every domain on which q
is continuous and positive.
theorem
NavierStokes.SolenoidalDiagonal.locallyFinite_cutStage_support_on
{X : Type u_1}
{V : Type u_2}
[TopologicalSpace X]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : X → ℝ}
{U : Set X}
(hq : ContinuousOn q U)
(hqpos : ∀ x ∈ U, 0 < q x)
(A : ℕ → X → V)
:
LocallyFinite fun (j : ℕ) => Function.support fun (x : ↑U) => cutStage a q A j ↑x
theorem
NavierStokes.SolenoidalDiagonal.cutStage_contDiffAt
{E : Type u_1}
{V : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
{q : E → ℝ}
{A : ℕ → E → V}
{x : E}
(hq : ContDiffAt ℝ (↑⊤) q x)
(hA : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (A j) x)
(j : ℕ)
:
ContDiffAt ℝ (↑⊤) (cutStage a q A j) x
theorem
NavierStokes.SolenoidalDiagonal.potentialSum_contDiffAt
{E : Type u_1}
{V : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : E → ℝ}
{A : ℕ → E → V}
{x : E}
(hqx : 0 < q x)
(hq : ContDiffAt ℝ (↑⊤) q x)
(hA : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (A j) x)
:
ContDiffAt ℝ (↑⊤) (potentialSum a q A) x
Smoothness is proved for the constructed sum, not postulated.
theorem
NavierStokes.SolenoidalDiagonal.potentialSum_contDiffOn
{E : Type u_1}
{V : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : E → ℝ}
{A : ℕ → E → V}
{U : Set E}
(hU : IsOpen U)
(hqpos : ∀ x ∈ U, 0 < q x)
(hq : ContDiffOn ℝ (↑⊤) q U)
(hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U)
:
ContDiffOn ℝ (↑⊤) (potentialSum a q A) U
theorem
NavierStokes.SolenoidalDiagonal.iteratedFDeriv_eventuallyEq
{E : Type u_1}
{V : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{f g : E → V}
{x : E}
(h : f =ᶠ[nhds x] g)
(k : ℕ)
:
Equality on a neighborhood preserves every iterated actual Fréchet derivative, including the totalized derivative at nonsmooth points.
theorem
NavierStokes.SolenoidalDiagonal.potentialSum_allJets_eventuallyEq_partial
{E : Type u_1}
{V : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : E → ℝ}
{A : ℕ → E → V}
{x : E}
(hq : ContinuousAt q x)
(hqx : 0 < q x)
:
∃ (N : ℕ), ∀ (k : ℕ), iteratedFDeriv ℝ k (potentialSum a q A) =ᶠ[nhds x] iteratedFDeriv ℝ k (partialPotential a q A N)
theorem
NavierStokes.SolenoidalDiagonal.iteratedFDeriv_partialPotential
{E : Type u_1}
{V : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
{q : E → ℝ}
{A : ℕ → E → V}
{x : E}
(hq : ContDiffAt ℝ (↑⊤) q x)
(hA : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (A j) x)
(N k : ℕ)
:
iteratedFDeriv ℝ k (partialPotential a q A N) x = ∑ j ∈ Finset.range N, iteratedFDeriv ℝ k (cutStage a q A j) x
theorem
NavierStokes.SolenoidalDiagonal.potentialSum_allJets_eventuallyEq_sum
{E : Type u_1}
{V : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : E → ℝ}
{A : ℕ → E → V}
{U : Set E}
(hU : IsOpen U)
(hqpos : ∀ x ∈ U, 0 < q x)
(hq : ContDiffOn ℝ (↑⊤) q U)
(hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U)
{x : E}
(hx : x ∈ U)
:
∃ (N : ℕ),
∀ (k : ℕ),
∀ᶠ (y : E) in nhds x, iteratedFDeriv ℝ k (potentialSum a q A) y = ∑ j ∈ Finset.range N, iteratedFDeriv ℝ k (cutStage a q A j) y
Every derivative is locally the finite sum of the corresponding stage derivatives. The prefix length is independent of the derivative order.
noncomputable def
NavierStokes.SolenoidalDiagonal.velocitySum
(a : ℕ → ℝ)
(q : ProblemStatement.SpaceTime → ℝ)
(A : ℕ → ProblemStatement.VelocityField)
:
The constructed velocity is the actual spatial curl of the summed
potential, with time held fixed by SpatialCurl.spatialCurl.
Equations
Instances For
theorem
NavierStokes.SolenoidalDiagonal.velocitySum_contDiffAt
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : ProblemStatement.SpaceTime → ℝ}
{A : ℕ → ProblemStatement.VelocityField}
{z : ProblemStatement.SpaceTime}
(hqz : 0 < q z)
(hq : ContDiffAt ℝ (↑⊤) q z)
(hA : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (A j) z)
:
ContDiffAt ℝ (↑⊤) (velocitySum a q A) z
theorem
NavierStokes.SolenoidalDiagonal.velocitySum_contDiffOn
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : ProblemStatement.SpaceTime → ℝ}
{A : ℕ → ProblemStatement.VelocityField}
{U : Set ProblemStatement.SpaceTime}
(hU : IsOpen U)
(hqpos : ∀ z ∈ U, 0 < q z)
(hq : ContDiffOn ℝ (↑⊤) q U)
(hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U)
:
ContDiffOn ℝ (↑⊤) (velocitySum a q A) U
theorem
NavierStokes.SolenoidalDiagonal.divergence_velocitySum
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : ProblemStatement.SpaceTime → ℝ}
{A : ℕ → ProblemStatement.VelocityField}
{z : ProblemStatement.SpaceTime}
(hqz : 0 < q z)
(hq : ContDiffAt ℝ (↑⊤) q z)
(hA : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (A j) z)
:
Incompressibility follows from actual second-derivative symmetry, already
proved in SpatialCurl, applied to the constructed smooth potential.
theorem
NavierStokes.SolenoidalDiagonal.divergence_velocitySum_on
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : ProblemStatement.SpaceTime → ℝ}
{A : ℕ → ProblemStatement.VelocityField}
{U : Set ProblemStatement.SpaceTime}
(hU : IsOpen U)
(hqpos : ∀ z ∈ U, 0 < q z)
(hq : ContDiffOn ℝ (↑⊤) q U)
(hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U)
(z : ProblemStatement.SpaceTime)
:
z ∈ U → ProblemStatement.spatialDivergence (velocitySum a q A) z.1 z.2 = 0
theorem
NavierStokes.SolenoidalDiagonal.spatialCurl_eq_of_eventuallyEq
{A B : ProblemStatement.VelocityField}
{z : ProblemStatement.SpaceTime}
(h : A =ᶠ[nhds z] B)
:
theorem
NavierStokes.SolenoidalDiagonal.spatialCurl_eventuallyEq
{A B : ProblemStatement.VelocityField}
{z : ProblemStatement.SpaceTime}
(h : A =ᶠ[nhds z] B)
:
theorem
NavierStokes.SolenoidalDiagonal.spatialCurl_partialPotential
{a : ℕ → ℝ}
{q : ProblemStatement.SpaceTime → ℝ}
{A : ℕ → ProblemStatement.VelocityField}
{z : ProblemStatement.SpaceTime}
(hq : ContDiffAt ℝ (↑⊤) q z)
(hA : ∀ (j : ℕ), ContDiffAt ℝ (↑⊤) (A j) z)
(N : ℕ)
:
SpatialCurl.spatialCurl (partialPotential a q A N) z = ∑ j ∈ Finset.range N, SpatialCurl.spatialCurl (cutStage a q A j) z
theorem
NavierStokes.SolenoidalDiagonal.velocitySum_eventuallyEq_sum
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : ProblemStatement.SpaceTime → ℝ}
{A : ℕ → ProblemStatement.VelocityField}
{U : Set ProblemStatement.SpaceTime}
(hU : IsOpen U)
(hqpos : ∀ z ∈ U, 0 < q z)
(hq : ContDiffOn ℝ (↑⊤) q U)
(hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U)
{z : ProblemStatement.SpaceTime}
(hz : z ∈ U)
:
∃ (N : ℕ),
velocitySum a q A =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) =>
∑ j ∈ Finset.range N, SpatialCurl.spatialCurl (cutStage a q A j) w
The curl of the summed potential is locally the finite sum of the curls of the cut potentials. Thus it also realizes the manuscript's stage sum.
theorem
NavierStokes.SolenoidalDiagonal.smooth_solenoidal_diagonal
{a : ℕ → ℝ}
(ha : Filter.Tendsto a Filter.atTop Filter.atTop)
{q : ProblemStatement.SpaceTime → ℝ}
{A : ℕ → ProblemStatement.VelocityField}
{U : Set ProblemStatement.SpaceTime}
(hU : IsOpen U)
(hqpos : ∀ z ∈ U, 0 < q z)
(hq : ContDiffOn ℝ (↑⊤) q U)
(hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U)
:
(LocallyFinite fun (j : ℕ) => Function.support fun (z : ↑U) => cutStage a q A j ↑z) ∧ ContDiffOn ℝ (↑⊤) (potentialSum a q A) U ∧ ContDiffOn ℝ (↑⊤) (velocitySum a q A) U ∧ ∀ z ∈ U, ProblemStatement.spatialDivergence (velocitySum a q A) z.1 z.2 = 0
A direct open-domain theorem for the constructed potential and velocity.
theorem
NavierStokes.SolenoidalDiagonal.realScales_tendsto
{a : ℕ → ℕ}
(ha : StrictMono a)
:
Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop
Integer schedules from DiagonalScale supply the required real divergence
of the cutoff scales.
theorem
NavierStokes.SolenoidalDiagonal.doublingEnvelope_tendsto
(b : ℕ → ℕ)
:
Filter.Tendsto (fun (j : ℕ) => ↑(DiagonalScale.doublingEnvelope b j)) Filter.atTop Filter.atTop
theorem
NavierStokes.SolenoidalDiagonal.exists_diagonal_scales_smooth_solenoidal
(C p : ℕ → ℕ → ℝ)
(g : ℕ → ℝ)
(hg : ∀ (j : ℕ), 1 ≤ j → 0 < g j)
(B : ℕ)
{q : ProblemStatement.SpaceTime → ℝ}
{A : ℕ → ProblemStatement.VelocityField}
{U : Set ProblemStatement.SpaceTime}
(hU : IsOpen U)
(hqpos : ∀ z ∈ U, 0 < q z)
(hq : ContDiffOn ℝ (↑⊤) q U)
(hA : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (A j) U)
:
∃ (a : ℕ → ℕ),
B ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ (∀ (j : ℕ),
1 ≤ j →
∀ m ≤ j + 2,
∀ (r : ℝ),
0 < r → r ≤ 1 / ↑(a j) → |DiagonalScale.logPowerWeight (C j m) (p j m) (g j / 2) r| ≤ (1 / 2) ^ j) ∧ ContDiffOn ℝ (↑⊤) (potentialSum (fun (j : ℕ) => ↑(a j)) q A) U ∧ ContDiffOn ℝ (↑⊤) (velocitySum (fun (j : ℕ) => ↑(a j)) q A) U ∧ ∀ z ∈ U, ProblemStatement.spatialDivergence (velocitySum (fun (j : ℕ) => ↑(a j)) q A) z.1 z.2 = 0
The numerical diagonal schedule and the smooth solenoidal construction can be chosen together. The numerical bounds are not asserted to be estimates for the potentials; that requires the manuscript's separate analytic input.