The factorial majorant of the interior analyticity induction

The sequence b₀ = M, b_{k+1} = M K^k (k+1)!/(k+2) bounds the weighted derivatives of order k in the proof of thm:analytic:interior. This file proves that it closes the recursion produced by one derivative step: the linear term, the convective and pressure products (whose binomial convolutions stay within a constant multiple of the majorant), and the analytic force.

noncomputable def CIV.kahaneMajorant (M K : ℝ) : ℕ → ℝ

The majorant of the induction on the derivative order in the proof of thm:analytic:interior: b₀ = M and b_{k+1} = M K^k (k+1)! / (k+2).

Equations

• CIV.kahaneMajorant M K 0 = M
• CIV.kahaneMajorant M K k.succ = M * K ^ k * ↑(k + 1).factorial / (↑k + 2)

theorem CIV.kahaneMajorant_le {M K : ℝ} (hM : 0 ≤ M) (hK : 1 ≤ K) (k : ℕ) : kahaneMajorant M K k ≤ M * K ^ k * ↑k.factorial

The majorant is below M K^k k!.

theorem CIV.kahaneMajorant_convective_term_le {M K : ℝ} (hK : 1 ≤ K) {k m : ℕ} (hm1 : 1 ≤ m) (hmk : m ≤ k) : ↑(k.choose m) * (kahaneMajorant M K m * kahaneMajorant M K (k + 1 - m)) ≤ M ^ 2 * K ^ (k - 1) * ↑k.factorial / 2

Each convective product in the recursion is below M² K^{k-1} k!/2.

theorem CIV.kahaneMajorant_pressure_term_le {M K : ℝ} (hK : 1 ≤ K) {k m : ℕ} (hm1 : 1 ≤ m) (hmk : m + 1 ≤ k) : ↑(k.choose m) * (kahaneMajorant M K (m + 1) * kahaneMajorant M K (k + 1 - m)) ≤ M ^ 2 * K ^ k * ↑k.factorial

Each pressure product in the recursion is below M² K^k k!.

theorem CIV.kahaneMajorant_step_le {C M K θ Mf af : ℝ} (hC : 1 ≤ C) (hM : 1 ≤ M) (haf : 0 < af) (hMf : 0 ≤ Mf) (hMfM : Mf * (1 + 3 / af) ≤ M) (hθ : θ = 1 / (400 * C * (1 + M))) (hK : 12800 * C ^ 2 * (1 + M) ≤ K) (hKaf : 1 / af ≤ K) (hK1 : 1 ≤ K) {k : ℕ} (hk : 1 ≤ k) : 2 * (C * (θ / (↑k + 1) * (Mf * af ^ (-↑k) * ↑k.factorial + 3 * (Mf * af ^ (-↑(k + 1)) * ↑(k + 1).factorial) + 6 * ∑ m ∈ Finset.Icc 1 k, ↑(k.choose m) * (kahaneMajorant M K m * kahaneMajorant M K (k + 1 - m)) + 18 * ∑ m ∈ Finset.Icc 1 (k - 1), ↑(k.choose m) * (kahaneMajorant M K (m + 1) * kahaneMajorant M K (k + 1 - m))) + 2 * (↑k + 1) * kahaneMajorant M K k / θ)) ≤ kahaneMajorant M K (k + 1)

The majorant closes the one-step recursion of the derivative estimates: with θ = 1 / (400 C (1 + M)) and K ≥ 12800 C² (1 + M), twice the step bound at order k is below b_{k+1}.