Circulation bounds from an annulus bound #
The circulation Γ = x₁ u₂ − x₂ u₁ of a vector field u satisfies a plain bound
|Γ| ≤ 2RM whenever |u| ≤ M on a ball of radius R (by abs_circulation_le_two_mul_of_bound).
On a sub‑annulus of the regular annulus where only the order‑0 derivative is bounded,
the circulation is controlled by 2 R⋆ M for any R⋆ of the annulus, via
circulation_hbdry_of_annulus_bound. The third theorem assembles the main-result statement
CIV.timeZeroSingularSetNull with the elementary circulation bound to produce the
parabolic‑boundary data that lem:aniso:axis needs for the lateral boundary of its
regular‑sphere closure argument.
theorem
CIV.abs_circulation_le_of_vec3EuclideanNorm_bound
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{x : CKN.Foundation.Parabolic.Vec3}
{t R M : ℝ}
(hR : CKN.Foundation.Parabolic.vec3EuclideanNorm x = R)
(hbound : CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ M)
:
theorem
CIV.circulation_hbdry_of_annulus_bound
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Rlo Rhi t₀ M : ℝ}
(hbound :
∀ (x : CKN.Foundation.Parabolic.Vec3),
Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x →
CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi →
∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ M)
(Rstar : ℝ)
:
Rstar ∈ Set.Ioo Rlo Rhi →
∀ (x : CKN.Foundation.Parabolic.Vec3),
CKN.Foundation.Parabolic.vec3EuclideanNorm x = Rstar → ∀ t ∈ Set.Ioo t₀ 0, |circulation u (x, t)| ≤ 2 * Rstar * M
theorem
CIV.exists_circulation_hbdry_of_timeZeroSingularSetNull
(q : ℝ)
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f)
(henergy : GlobalEnergyClass u Du p)
(hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
(hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder)
(hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder)
(hMf : ForceC2Bounded f)
(R₁ R₀ : ℝ)
(hR₁ : 0 ≤ R₁)
(hR₁R₀ : R₁ < R₀)
(hR₀ : R₀ < 1)
: