Transfer of the weighted bounds one derivative up

The weighted bound at depth τ and order k + 1 from the weighted bounds of orders ≤ k and a provisional bound Y at order k + 1, all at every depth. The one-step estimate is applied on the backward window of radius θ τ d / (k + 1), which lies one geometric step deeper. The provisional bound enters with the small coefficient ε, which is absorbed in the induction of thm:analytic:interior.

theorem CIV.sum_range_succ_eq_zero_add_Icc (g : ℕ → ℝ) (k : ℕ) : ∑ m ∈ Finset.range (k + 1), g m = g 0 + ∑ m ∈ Finset.Icc 1 k, g m

A sum over range (k + 1) splits off its first term.

theorem CIV.sum_range_succ_eq_zero_add_last_add_Icc (g : ℕ → ℝ) {k : ℕ} (hk : 1 ≤ k) : ∑ m ∈ Finset.range (k + 1), g m = g 0 + g k + ∑ m ∈ Finset.Icc 1 (k - 1), g m

For k ≥ 1 a sum over range (k + 1) splits off its first and last terms.

theorem CIV.kahane_level_transfer : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Ω : Set CKN.Foundation.Parabolic.Vec3) (I : Set ℝ) (R' d s₁ s₂ θ Y : ℝ) (k : ℕ) (A F : ℕ → ℝ), IsOpen Ω → IsOpen I → IsClassicalSolutionOn u p f (CKN.spaceTimeSet Ω I) → 0 < d → d ≤ 1 → 0 < θ → θ ≤ 1 / 4 → 1 ≤ k → 0 ≤ Y → (∀ (j : ℕ), 0 ≤ A j) → (∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ R' + d → s₁ - d ^ 2 ≤ t → t ≤ s₂ → x ∈ Ω ∧ t ∈ I) → (∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ R' + d → s₁ - d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ) (i : Fin 3), |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) γ (x, t)| ≤ F (γ 0 + γ 1 + γ 2)) → (∀ j ≤ k, ∀ (τ : ℝ), 0 < τ → τ ≤ 1 → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x < R' + (1 - τ) * d → s₁ - (1 - τ) * d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = j → (∀ (i : Fin 3), (τ * d) ^ j * |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) γ (x, t)| ≤ A j) ∧ (τ * d) ^ j * |multiPartial p γ (x, t)| ≤ A j) → (∀ (τ : ℝ), 0 < τ → τ ≤ 1 → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x < R' + (1 - τ) * d → s₁ - (1 - τ) * d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k + 1 → (∀ (i : Fin 3), (τ * d) ^ (k + 1) * |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) γ (x, t)| ≤ Y) ∧ (τ * d) ^ (k + 1) * |multiPartial p γ (x, t)| ≤ Y) → ∀ (τ : ℝ), 0 < τ → τ ≤ 1 → ∀ (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm x < R' + (1 - τ) * d → s₁ - (1 - τ) * d ^ 2 ≤ t → t ≤ s₂ → ∀ (γ : Fin 3 → ℕ), γ 0 + γ 1 + γ 2 = k + 1 → have X := C * (θ / (↑k + 1) * (F k + 3 * F (k + 1) + 6 * ∑ m ∈ Finset.Icc 1 k, ↑(k.choose m) * (A m * A (k + 1 - m)) + 18 * ∑ m ∈ Finset.Icc 1 (k - 1), ↑(k.choose m) * (A (m + 1) * A (k + 1 - m))) + 2 * (↑k + 1) * A k / θ); have ε := C * θ * (2 + 6 * A 0 + 36 * A 1) / (↑k + 1); (∀ (i : Fin 3), (τ * d) ^ (k + 1) * |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) γ (x, t)| ≤ X + ε * Y) ∧ (τ * d) ^ (k + 1) * |multiPartial p γ (x, t)| ≤ X + ε * Y

The level transfer: from the weighted bounds A j at orders j ≤ k and a provisional bound Y at order k + 1, all at every depth, the order-k + 1 weighted bound at every depth is at most X + ε Y with ε = C θ (2 + 6 A₀ + 36 A₁) / (k + 1).