The circulation profile as an input to the axis maximum principle

CIV.circulation_pde (eq:aniso:circulation:pde) is stated in the Cartesian derivative calculus timePartial/spatialPartial/spatialSecondPartial on the meridional plane. CIV.axisMaximumPrinciple instead consumes the half-disc operators dtPast, dr, dz. This file transports the equation between the two, through the meridional chain rules of CIV/Axis/MeridionalScalarChainRule.lean, and records the regularity hypothesis (hreg_circulationProfile) the maximum principle asks for.

The resulting equation hpde_circulationProfile is lem:aniso:axis's eq:aniso:axis:pde with drift (u_r, u_z), exponent k = −1, zeroth-order coefficient γ = 0 and source r f_θ, exactly as the proof of lem:aniso:annulus reads it.

The C² spatial slice of the circulation

theorem CIV.contDiffOn_circulation (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu2 : ContDiffOn ℝ 2 (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => u w) unitCylinder) : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => circulation u z) unitCylinder

The circulation of a C² field is C² on the cylinder: it is a polynomial in the coordinates and the components of u.

theorem CIV.contDiffOn_circulation_slice (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu2 : ContDiffOn ℝ 2 (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => u w) unitCylinder) {t : ℝ} (ht : t ∈ Set.Ioo (-1) 0) : ContDiffOn ℝ 2 (fun (y : CKN.Foundation.Parabolic.Vec3) => circulation u (y, t)) (CKN.Foundation.Parabolic.vec3Ball 0 1)

The spatial slice of the circulation at a fixed time is C² on the unit ball.

theorem CIV.differentiableAt_circulation_slice (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu1 : ContDiffOn ℝ 1 (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => u w) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => circulation u (y, z.2)) z.1

The spatial slice of the circulation is differentiable at every point of the cylinder.

theorem CIV.differentiableAt_circulation_time (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu1 : ContDiffOn ℝ 1 (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => u w) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : DifferentiableAt ℝ (fun (s : ℝ) => circulation u (z.1, s)) z.2

The time slice of the circulation is differentiable at every point of the cylinder.

Regularity of the circulation profile

theorem CIV.hreg_circulationProfile (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu2 : ContDiffOn ℝ 2 (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η) (p : (ℝ × ℝ) × ℝ) : p ∈ axisDomain Rstar tη s → ContDiffAt ℝ 2 (fun (y : ℝ × ℝ) => circulationProfile u (y, p.2)) p.1 ∧ DifferentiableWithinAt ℝ (fun (t : ℝ) => circulationProfile u (p.1, t)) (Set.Iic p.2) p.2

The regularity hypothesis of CIV.axisMaximumPrinciple for the circulation profile: C² in the half-disc variables and differentiable from the past in time, at every interior point of the half-disc.

Translating dtPast, dr, dz into the Cartesian derivative calculus

theorem CIV.dtPast_circulationProfile_eq (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu1 : ContDiffOn ℝ 1 (fun (w : CKN.Foundation.Parabolic.Vec3 × ℝ) => u w) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hz : (meridional p.1.1 p.1.2, p.2) ∈ unitCylinder) : dtPast (circulationProfile u) p = CKN.timePartial (circulation u) (meridional p.1.1 p.1.2, p.2)

dtPast of the circulation profile is timePartial of the circulation.

theorem CIV.dr_circulationProfile_eq (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) (hdiff : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => circulation u (y, p.2)) (meridional p.1.1 p.1.2)) : dr (circulationProfile u) p = CKN.spatialPartial (circulation u) 0 (meridional p.1.1 p.1.2, p.2)

dr of the circulation profile is ∂₁ of the circulation.

theorem CIV.dz_circulationProfile_eq (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) (hdiff : DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => circulation u (y, p.2)) (meridional p.1.1 p.1.2)) : dz (circulationProfile u) p = CKN.spatialPartial (circulation u) 2 (meridional p.1.1 p.1.2, p.2)

dz of the circulation profile is ∂₃ of the circulation.

theorem CIV.dr_dr_circulationProfile_eq (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) (hg : ContDiffOn ℝ 2 (fun (y : CKN.Foundation.Parabolic.Vec3) => circulation u (y, p.2)) (CKN.Foundation.Parabolic.vec3Ball 0 1)) (hmem : meridional p.1.1 p.1.2 ∈ CKN.Foundation.Parabolic.vec3Ball 0 1) : dr (dr (circulationProfile u)) p = CKN.spatialSecondPartial (circulation u) 0 0 (meridional p.1.1 p.1.2, p.2)

dr (dr ·) of the circulation profile is ∂₁² of the circulation.

theorem CIV.dz_dz_circulationProfile_eq (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) (hg : ContDiffOn ℝ 2 (fun (y : CKN.Foundation.Parabolic.Vec3) => circulation u (y, p.2)) (CKN.Foundation.Parabolic.vec3Ball 0 1)) (hmem : meridional p.1.1 p.1.2 ∈ CKN.Foundation.Parabolic.vec3Ball 0 1) : dz (dz (circulationProfile u)) p = CKN.spatialSecondPartial (circulation u) 2 2 (meridional p.1.1 p.1.2, p.2)

dz (dz ·) of the circulation profile is ∂₃² of the circulation.

The equation eq:aniso:axis:pde for the circulation profile

theorem CIV.hpde_circulationProfile (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (a b t : ℝ) (hz : (meridional a b, t) ∈ unitCylinder) (ha : a ≠ 0) : dtPast (circulationProfile u) ((a, b), t) + u (meridional a b, t) 0 * dr (circulationProfile u) ((a, b), t) + u (meridional a b, t) 2 * dz (circulationProfile u) ((a, b), t) = dr (dr (circulationProfile u)) ((a, b), t) + -1 / a * dr (circulationProfile u) ((a, b), t) + dz (dz (circulationProfile u)) ((a, b), t) + a * f (meridional a b, t) 1

The circulation equation eq:aniso:circulation:pde, written in the half-disc calculus CIV.axisMaximumPrinciple consumes: drift (u_r, u_z), exponent k = −1, no zeroth-order term and source r f_θ.