Instantiating step_finite_contradiction at the cutoff-multiplied zoom fields #
This file assembles every piece built in FiniteZoomCutoffField.lean,
FiniteZoomCutoffData.lean, FiniteZoomCutoffBounds.lean and
FiniteZoomCutoffSecondDeriv.lean into the exact hypothesis block of
CIV.step_finite_contradiction_of_dr_dz, with Vseq := cutoffZoomV, Wseq := cutoffZoomW.
The selection data Rsel, c₀ and the lower bound hlower belong to a different step of the
proof (the meridional-smallness dichotomy that produces the selected
sequence) and are taken here as hypotheses, exactly as step_finite_contradiction_of_dr_dz
already takes them; likewise Ω_n → 0 is the endpoint vanishing of the comparison
argument and is taken as a hypothesis rather than re-derived.
The second-derivative equalities, specialised to zoomV/zoomW #
theorem
CIV.fderiv2_zoomV_slice_apply_rr
{h zc lam : ℝ}
{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 : zoomPoint lam h zc (y, -1) ∈ unitCylinder)
:
theorem
CIV.fderiv2_zoomV_slice_apply_rz
{h zc lam : ℝ}
{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 : zoomPoint lam h zc (y, -1) ∈ unitCylinder)
:
theorem
CIV.fderiv2_zoomV_slice_apply_zz
{h zc lam : ℝ}
{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 : zoomPoint lam h zc (y, -1) ∈ unitCylinder)
:
theorem
CIV.fderiv2_zoomW_slice_apply_rr
{h zc lam : ℝ}
{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 : zoomPoint lam h zc (y, -1) ∈ unitCylinder)
:
theorem
CIV.fderiv2_zoomW_slice_apply_rz
{h zc lam : ℝ}
{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 : zoomPoint lam h zc (y, -1) ∈ unitCylinder)
:
theorem
CIV.fderiv2_zoomW_slice_apply_zz
{h zc lam : ℝ}
{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 : zoomPoint lam h zc (y, -1) ∈ unitCylinder)
:
The cutoff-multiplied field's second derivative reads off the raw slice's #
theorem
CIV.eventually_fderiv2_cutoffZoomV_eq
{h : ℝ}
(hh1 : h < 1 / 2)
{zc : ℕ → ℝ}
{ζ : ℝ}
(hzc : ∀ (n : ℕ), |zc n| ≤ ζ)
(hζ : ζ < 1)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{lam : ℕ → ℝ}
(hlam0 : ∀ (n : ℕ), 0 < lam n)
(hlamTendsto : Filter.Tendsto lam Filter.atTop (nhds 0))
(y : ℝ × ℝ)
:
theorem
CIV.eventually_fderiv2_cutoffZoomW_eq
{h : ℝ}
(hh1 : h < 1 / 2)
{zc : ℕ → ℝ}
{ζ : ℝ}
(hzc : ∀ (n : ℕ), |zc n| ≤ ζ)
(hζ : ζ < 1)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{lam : ℕ → ℝ}
(hlam0 : ∀ (n : ℕ), 0 < lam n)
(hlamTendsto : Filter.Tendsto lam Filter.atTop (nhds 0))
(y : ℝ × ℝ)
:
The uniform second-derivative operator-norm bound, eventually in n #
theorem
CIV.eventually_norm_fderiv2_cutoffZoomV_le
{C h : ℝ}
(hC : 0 ≤ C)
(hh0 : 0 ≤ h)
(hh1 : h < 1 / 2)
{zc : ℕ → ℝ}
{ζ : ℝ}
(hzc : ∀ (n : ℕ), |zc n| ≤ ζ)
(hζ : ζ < 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)
{lam : ℕ → ℝ}
(hlam0 : ∀ (n : ℕ), 0 < lam n)
(hlam1 : ∀ (n : ℕ), lam n < 1)
(hlamTendsto : Filter.Tendsto lam Filter.atTop (nhds 0))
(y : ℝ × ℝ)
:
The fourth (axial-radial) entry, for the cutoff-multiplied radial field, agrees with the
radial-axial one: Vseq n is globally ContDiff ℝ (⊤ : ℕ∞)
(CIV.contDiff_cutoffZoomV), so second_derivative_symmetric applies to it directly, even
though the raw slice underneath is only locally smooth.
theorem
CIV.eventually_norm_fderiv2_cutoffZoomW_le
{C h : ℝ}
(hC : 0 ≤ C)
(hh0 : 0 ≤ h)
(hh1 : h < 1 / 2)
{zc : ℕ → ℝ}
{ζ : ℝ}
(hzc : ∀ (n : ℕ), |zc n| ≤ ζ)
(hζ : ζ < 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)
{lam : ℕ → ℝ}
(hlam0 : ∀ (n : ℕ), 0 < lam n)
(hlam1 : ∀ (n : ℕ), lam n < 1)
(hlamTendsto : Filter.Tendsto lam Filter.atTop (nhds 0))
(y : ℝ × ℝ)
:
The vertical counterpart of eventually_norm_fderiv2_cutoffZoomV_le.