The circulation profile on the meridional half-disc

CIV.axisMaximumPrinciple (lem:aniso:axis) consumes a scalar on the half-disc (r, z, t), so the circulation Γ = CIV.circulation u has to be read through the meridional embedding. circulationProfile u ((r, z), t) = Γ (u, ((r, 0, z), t)), which circulationProfile_apply evaluates as r · u_θ.

This file supplies the three structural hypotheses of the maximum principle that do not involve derivatives: continuity on the closed domain, vanishing on the axis (Γ = r u_θ has the factor r, so no smoothness at r = 0 is needed for this), and the evenness of Γ under the reflection r ↦ −r of the meridional plane, which carries the conclusion from the half-disc r ≥ 0 to the full disc.

def CIV.circulationProfile (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

The circulation, read on the meridional plane as a function of (r, z, t).

Equations

• CIV.circulationProfile u p = CIV.circulation u (CIV.meridional p.1.1 p.1.2, p.2)

theorem CIV.circulationProfile_apply (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : circulationProfile u p = p.1.1 * u (meridional p.1.1 p.1.2, p.2) 1

The circulation profile is r · u_θ: the second component of meridional is 0, so the x₂ u₁ term of Γ drops out.

theorem CIV.meridional_mem_unitCylinder_of_sq_le {a b t Rstar : ℝ} (hRpos : 0 < Rstar) (hR1 : Rstar < 1) (hab : a ^ 2 + b ^ 2 ≤ Rstar ^ 2) (ht1 : -1 < t) (ht2 : t < 0) : (meridional a b, t) ∈ unitCylinder

A meridional point of radius at most R_* < 1, at a time of (−1, 0), lies in the unit cylinder. Stated with the two coordinates explicit, so that no projection has to be unfolded where it is used.

theorem CIV.mapsTo_meridional_axisClosedDomain (Rstar tη s : ℝ) (hRpos : 0 < Rstar) (hR1 : Rstar < 1) (hs0 : s < 0) (htη1 : -1 < tη) : Set.MapsTo (fun (p : (ℝ × ℝ) × ℝ) => (meridional p.1.1 p.1.2, p.2)) (axisClosedDomain Rstar tη s) unitCylinder

The meridional embedding of the closed half-disc of radius R_* < 1 at times in [t_η, s] ⊆ (−1, 0) lands in the unit cylinder.

theorem CIV.contDiff_meridional_uncurry : ContDiff ℝ ↑⊤ fun (y : ℝ × ℝ) => meridional y.1 y.2

The meridional embedding (r, z) ↦ (r, 0, z) of ℝ × ℝ into Vec3 is the linear map y ↦ y₁ e₁ + y₂ e₃, hence smooth.

theorem CIV.continuous_meridional_uncurry : Continuous fun (y : ℝ × ℝ) => meridional y.1 y.2

The meridional embedding (r, z) ↦ (r, 0, z) of ℝ × ℝ into Vec3 is continuous.

theorem CIV.continuousOn_circulationProfile (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu1 : ContDiffOn ℝ 1 (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => u w) unitCylinder) (Rstar tη s : ℝ) (hRpos : 0 < Rstar) (hR1 : Rstar < 1) (hs0 : s < 0) (htη1 : -1 < tη) : ContinuousOn (circulationProfile u) (axisClosedDomain Rstar tη s)

The circulation profile is continuous on the closed half-disc axisClosedDomain, the first hypothesis of CIV.axisMaximumPrinciple. Only C¹ regularity of u is used.

theorem CIV.circulationProfile_axis_eq_zero (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (zc tc : ℝ) : circulationProfile u ((0, zc), tc) = 0

The circulation vanishes on the axis, the second hypothesis of CIV.axisMaximumPrinciple: Γ = r u_θ carries the factor r, so the value at r = 0 is 0 with no appeal to regularity.

theorem CIV.circulationProfile_meridional_even {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) {r z t : ℝ} (hz : (meridional r z, t) ∈ unitCylinder) : circulationProfile u ((-r, z), t) = circulationProfile u ((r, z), t)

The circulation profile is even under the reflection r ↦ −r of the meridional plane: both r and u_θ change sign (apply_meridional_reflect_one), so Γ = r u_θ does not.