Elementary real-number lemmas

theorem CIV.exists_two_lt_of_lt {Rm Rp : ℝ} (h : Rm < Rp) : ∃ (Rm' : ℝ) (Rp' : ℝ), Rm < Rm' ∧ Rm' < Rp' ∧ Rp' < Rp

Given Rm < Rp, there exist two reals strictly between them.

theorem CIV.exists_sq_lt_neg_and_mem_Ioo {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (-1) 0) : ∃ (varrho : ℝ), 0 < varrho ∧ varrho ^ 2 < -t₀ ∧ t₀ < t₀ + varrho ^ 2 ∧ t₀ + varrho ^ 2 < 0

Given t₀ ∈ (-1, 0), there exists varrho > 0 such that varrho² < -t₀, t₀ + varrho² is still in (-1, 0), and t₀ + varrho² > t₀.

theorem CIV.step_annulus_derivative_bounds (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Rm Rp t₀ : ℝ) (hR : 0 ≤ Rm ∧ Rm < Rp ∧ Rp ≤ 1) (ht₀ : t₀ ∈ Set.Ioo (-1) 0) (Mu : ℝ) (hbdd : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) (hserrin : (∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ Mu) → ∀ (Rm' Rp' t₀' : ℝ), Rm < Rm' → Rm' < Rp' → Rp' < Rp → t₀ < t₀' → t₀' < 0 → ∃ (K : ℝ), ∀ (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)| ≤ K) : ∃ (Rm' : ℝ) (Rp' : ℝ) (t₀' : ℝ), Rm < Rm' ∧ Rm' < Rp' ∧ Rp' < Rp ∧ t₀ < t₀' ∧ t₀' < 0 ∧ ∃ (K : ℝ), ∀ (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)| ≤ K

Reduction step for annulus derivative bounds: fix varrho and shrink the annulus radii so that Serrin's interior estimates (assumed as hypothesis hserrin) produce bounds on u, ∇u, ∇²u on a compactly contained sub-annulus over (t₀, 0), uniformly up to the blow-up time.

This is lem:aniso:annulus: the Serrin-type hypothesis hserrin states that whenever u is bounded on a slightly larger annulus and time interval, it and its first two spatial derivatives are bounded on any strictly smaller concentric sub-annulus over any strictly earlier time interval (t₀', 0) with t₀' > t₀. The conclusion produces such a sub-annulus and time interval where the derivative bounds hold.