The receding-axis contradiction at the selected points

The last paragraph of Step 3 of the proof of prop:aniso:small: in the receding-axis case (A_n = r_n / λ_n → ∞) the rescaled fields V_n, W_n of eq:aniso:zoom:fields, taken about the selected points x_n = (r_n, z_n) in the variables eq:aniso:zoom:receding:variables, are bounded in C² on compact sets at τ = -1; if the rescaled azimuthal vorticity Θ_n(·, -1) tends to zero, the endpoint argument eq:aniso:zoom:receding:endpoint makes ∂_R V_n(0,0,-1) and ∂_Z W_n(0,0,-1) tend to zero, eq:aniso:zoom:receding:quotient makes the quotient term tend to zero, and the selection eq:aniso:zoom:selected is contradicted.

The endpoint argument (CIV.step_receding_contradiction) is stated for fields smooth on the whole plane. The rescaled fields at τ = -1 are smooth only on the preimage of the unit cylinder under the zoom map, a region which exhausts the plane as n → ∞; they are multiplied here by a bump function equal to 1 on a ball of radius (1 - ρ) / (4 (λ_n + μ_n)) and supported where the zoom map lands in the cylinder, μ_n = λ_n^{1-2h}.

The slice region

def CIV.recSliceSet (lam h rc zc : ℝ) : Set (ℝ × ℝ)

The points of the recentred zoomed plane mapped into the unit cylinder at τ = -1.

Equations

• CIV.recSliceSet lam h rc zc = {q : ℝ × ℝ | CIV.zoomPointRec lam h rc zc (q, -1) ∈ CIV.unitCylinder}

theorem CIV.isOpen_recSliceSet (lam h rc zc : ℝ) : IsOpen (recSliceSet lam h rc zc)

A safe radius around the selected point

theorem CIV.mem_recSliceSet_of_norm_le {h ρ lam rc zc s : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hcz : rc ^ 2 + zc ^ 2 ≤ ρ ^ 2) (hlam0 : 0 < lam) (hlam1 : lam < 1) (hs : (lam + lam ^ (1 - 2 * h)) * s ≤ (1 - ρ) / 2) {q : ℝ × ℝ} (hq : ‖q‖ ≤ s) : q ∈ recSliceSet lam h rc zc

If rc² + zc² ≤ ρ² < 1, a sup-ball of radius s with (λ + λ^{1-2h}) s ≤ (1 - ρ)/2 lies in the slice region.

The bump function and the cutoff fields

noncomputable def CIV.recCutoffRadius (h ρ lam : ℝ) : ℝ

The outer radius (1 - ρ) / (2 (λ + λ^{1-2h})) of the cutoff at scale λ.

Equations

• CIV.recCutoffRadius h ρ lam = (1 - ρ) / (2 * (lam + lam ^ (1 - 2 * h)))

theorem CIV.recCutoffRadius_pos {h ρ lam : ℝ} (hρ1 : ρ < 1) (hlam0 : 0 < lam) : 0 < recCutoffRadius h ρ lam

noncomputable def CIV.recCutoffBump (h ρ lam : ℝ) (hρ1 : ρ < 1) (hlam0 : 0 < lam) : ContDiffBump 0

The cutoff at scale λ: equal to 1 on the closed ball of radius half the outer radius.

Equations

• CIV.recCutoffBump h ρ lam hρ1 hlam0 = { rIn := CIV.recCutoffRadius h ρ lam / 2, rOut := CIV.recCutoffRadius h ρ lam, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

theorem CIV.recCutoffBump_safe {h ρ lam rc zc : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hcz : rc ^ 2 + zc ^ 2 ≤ ρ ^ 2) (hlam0 : 0 < lam) (hlam1 : lam < 1) : Metric.closedBall 0 (recCutoffBump h ρ lam hρ1 hlam0).rOut ⊆ recSliceSet lam h rc zc

theorem CIV.eventually_lt_recCutoffBump_rIn {h ρ : ℝ} (hh1 : h < 1 / 2) (hρ1 : ρ < 1) {lam : ℕ → ℝ} (hlam0 : ∀ (n : ℕ), 0 < lam n) (hlam_lim : Filter.Tendsto lam Filter.atTop (nhds 0)) (r : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, r < (recCutoffBump h ρ (lam n) hρ1 ⋯).rIn

The inner radius of the cutoff grows without bound along a zoom sequence.

noncomputable def CIV.recCutoffV (h ρ lam rc zc : ℝ) (hρ1 : ρ < 1) (hlam0 : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : ℝ × ℝ → ℝ

The cutoff-multiplied recentred radial field at τ = -1.

Equations

• CIV.recCutoffV h ρ lam rc zc hρ1 hlam0 u q = ↑(CIV.recCutoffBump h ρ lam hρ1 hlam0) q * CIV.zoomVRec lam h rc zc u (q, -1)

noncomputable def CIV.recCutoffW (h ρ lam rc zc : ℝ) (hρ1 : ρ < 1) (hlam0 : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : ℝ × ℝ → ℝ

The cutoff-multiplied recentred axial field at τ = -1.

Equations

• CIV.recCutoffW h ρ lam rc zc hρ1 hlam0 u q = ↑(CIV.recCutoffBump h ρ lam hρ1 hlam0) q * CIV.zoomWRec lam h rc zc u (q, -1)

theorem CIV.contDiff_recCutoffV {h ρ lam rc zc : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hcz : rc ^ 2 + zc ^ 2 ≤ ρ ^ 2) (hlam0 : 0 < lam) (hlam1 : lam < 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) : ContDiff ℝ (↑⊤) (recCutoffV h ρ lam rc zc hρ1 hlam0 u)

theorem CIV.contDiff_recCutoffW {h ρ lam rc zc : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hcz : rc ^ 2 + zc ^ 2 ≤ ρ ^ 2) (hlam0 : 0 < lam) (hlam1 : lam < 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) : ContDiff ℝ (↑⊤) (recCutoffW h ρ lam rc zc hρ1 hlam0 u)

theorem CIV.recCutoffV_eventuallyEq {h ρ lam rc zc : ℝ} (hρ1 : ρ < 1) (hlam0 : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {y : ℝ × ℝ} (hy : ‖y‖ < (recCutoffBump h ρ lam hρ1 hlam0).rIn) : recCutoffV h ρ lam rc zc hρ1 hlam0 u =ᶠ[nhds y] fun (q : ℝ × ℝ) => zoomVRec lam h rc zc u (q, -1)

Inside the inner ball the cutoff fields agree with the raw slices near the point.

theorem CIV.recCutoffW_eventuallyEq {h ρ lam rc zc : ℝ} (hρ1 : ρ < 1) (hlam0 : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {y : ℝ × ℝ} (hy : ‖y‖ < (recCutoffBump h ρ lam hρ1 hlam0).rIn) : recCutoffW h ρ lam rc zc hρ1 hlam0 u =ᶠ[nhds y] fun (q : ℝ × ℝ) => zoomWRec lam h rc zc u (q, -1)

theorem CIV.mem_recSliceSet_of_lt_rIn {h ρ lam rc zc : ℝ} (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hcz : rc ^ 2 + zc ^ 2 ≤ ρ ^ 2) (hlam0 : 0 < lam) (hlam1 : lam < 1) {y : ℝ × ℝ} (hy : ‖y‖ < (recCutoffBump h ρ lam hρ1 hlam0).rIn) : y ∈ recSliceSet lam h rc zc

The inner ball lies in the slice region.

Pointwise bounds of the cutoff fields inside the inner ball

theorem CIV.hasFDerivAt_zoomVRec_slice {h lam rc zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) {y : ℝ × ℝ} (hy : y ∈ recSliceSet lam h rc zc) : HasFDerivAt (fun (q : ℝ × ℝ) => zoomVRec lam h rc zc u (q, -1)) (fderiv ℝ (fun (q : ℝ × ℝ) => zoomVRec lam h rc zc u (q, -1)) y) y

theorem CIV.hasFDerivAt_zoomWRec_slice {h lam rc zc : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) {y : ℝ × ℝ} (hy : y ∈ recSliceSet lam h rc zc) : HasFDerivAt (fun (q : ℝ × ℝ) => zoomWRec lam h rc zc u (q, -1)) (fderiv ℝ (fun (q : ℝ × ℝ) => zoomWRec lam h rc zc u (q, -1)) y) y

theorem CIV.recCutoffV_bounds {C h ρ lam rc zc : ℝ} (hC : 0 ≤ C) (hh1 : h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hcz : rc ^ 2 + zc ^ 2 ≤ ρ ^ 2) (hlam0 : 0 < lam) (hlam1 : lam < 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) {y : ℝ × ℝ} (hy : ‖y‖ < (recCutoffBump h ρ lam hρ1 hlam0).rIn) : |recCutoffV h ρ lam rc zc hρ1 hlam0 u y| ≤ 4 * C ∧ ‖fderiv ℝ (recCutoffV h ρ lam rc zc hρ1 hlam0 u) y‖ ≤ 4 * C ∧ ‖fderiv ℝ (fderiv ℝ (recCutoffV h ρ lam rc zc hρ1 hlam0 u)) y‖ ≤ 4 * C

theorem CIV.recCutoffW_bounds {C h ρ lam rc zc : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hh1 : h < 1 / 2) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) (hcz : rc ^ 2 + zc ^ 2 ≤ ρ ^ 2) (hlam0 : 0 < lam) (hlam1 : lam < 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) {y : ℝ × ℝ} (hy : ‖y‖ < (recCutoffBump h ρ lam hρ1 hlam0).rIn) : |recCutoffW h ρ lam rc zc hρ1 hlam0 u y| ≤ 4 * C ∧ ‖fderiv ℝ (recCutoffW h ρ lam rc zc hρ1 hlam0 u) y‖ ≤ 4 * C ∧ ‖fderiv ℝ (fderiv ℝ (recCutoffW h ρ lam rc zc hρ1 hlam0 u)) y‖ ≤ 4 * C

The contradiction

theorem CIV.norm_le_of_mem_planeRectangle {j : ℕ} {y : ℝ × ℝ} (hy : y ∈ planeRectangle j) : ‖y‖ ≤ ↑j + 1

Every point of planeRectangle j has sup norm at most j + 1.

theorem CIV.false_of_real_receding_selection {C h ρ : ℝ} (hC : 0 ≤ C) (hh0 : 0 < h) (hh1 : h < 1 / 2) (hρ : ρ < 1) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hb : AnisotropicBounds C h u) {pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u pres f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {c₀ : ℝ} (hc₀ : 0 < c₀) {t x₁ x₃ : ℕ → ℝ} (htlim : Filter.Tendsto t Filter.atTop (nhds 0)) (hmem : ∀ (n : ℕ), meridional (x₁ n) (x₃ n) ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (htmem : ∀ (n : ℕ), t n ∈ Set.Ioo (-1) 0) (hineq : ∀ (n : ℕ), c₀ < -t n * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional (x₁ n) (x₃ n), t n)| + |radialQuotient u (meridional (x₁ n) (x₃ n), t n)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 (meridional (x₁ n) (x₃ n), t n)|)) (hA : Filter.Tendsto (fun (n : ℕ) => x₁ n / √(-t n)) Filter.atTop Filter.atTop) (hΘ0 : ∀ (q : ℝ × ℝ), Filter.Tendsto (fun (n : ℕ) => zoomTheta (√(-t n)) h (x₁ n) (x₃ n) u (q, -1)) Filter.atTop (nhds 0)) : False

The receding-axis branch of the selection of eq:aniso:zoom:selected is contradictory once the rescaled azimuthal vorticity about the selected points x_n = (x₁ n, x₃ n), at scale λ_n = √(-t_n), tends to zero at every point of {τ = -1}.