Circulation bounds from pointwise and annulus bounds

The circulation Γ = x₁ u₂ − x₂ u₁ of a vector field u on a parabolic point z satisfies a plain bound 2RM whenever |u| ≤ M on a ball of radius R. 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⋆ < Rₚ.

theorem CIV.abs_circulation_le_two_mul_of_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {z : CKN.Foundation.Parabolic.ParabolicPoint} {R M : ℝ} (hR : CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ≤ R) (h0 : |u z 0| ≤ M) (h1 : |u z 1| ≤ M) : |circulation u z| ≤ 2 * R * M

The circulation Γ = x₁ u₂ − x₂ u₁ of a field bounded by M on a ball of radius R is itself bounded by 2RM there.

theorem CIV.exists_circulation_bound_of_annulus_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Rm Rp t₀ M : ℝ} (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ M) {Rstar : ℝ} (hRstar : Rstar ≤ Rp) : ∃ (CΓ : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rstar → ∀ t ∈ Set.Ioo t₀ 0, |circulation u (x, t)| ≤ CΓ

On a sub‑annulus Rm < |x| < R⋆ of the regular annulus of lem:aniso:annulus, the circulation of u is bounded, using only the order‑0 case of the annulus's derivative bound.

theorem CIV.forall_Rstar_exists_circulation_bound_of_annulus_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Rm Rp t₀ M : ℝ} (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ M) (Rstar : ℝ) : Rstar ∈ Set.Ioo Rm Rp → ∃ (CΓ : ℝ), ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rstar → ∀ t ∈ Set.Ioo t₀ 0, |circulation u (x, t)| ≤ CΓ

The circulation bound of the previous theorem, quantified over every radius R⋆ ∈ Ioo Rm Rp.

The conclusion is confined to the open sub-annulus Rm < |x| < R⋆. It asserts nothing at |x| ≤ Rm, hence nothing on the symmetry axis or on the inner ball, so it is weaker than the circulation clause of lem:aniso:annulus, which bounds Γ on the whole ball B(R⋆). The whole-ball statement is CIV.forall_Rstar_exists_circulation_bound_ball_of_annulus_bound; it needs the maximum principle to fill in the inner ball and does not follow from the algebraic bound used here.