Real estimates for the exponential-growth targets

Round target E0(k) = E(k) - A k^{3/4}, with k^{3/4} written as Real.sqrt so that no real exponentiation is required, and the phase thresholds k_{j+1} = k_j + E0(k_j). Every constant below depends only on γlo, γhi, a, b, c, f.

noncomputable def Epidemics.Revisited.fourthRoot (x : ℝ) : ℝ

Equations

• Epidemics.Revisited.fourthRoot x = √√x

noncomputable def Epidemics.Revisited.threeFourth (x : ℝ) : ℝ

Equations

• Epidemics.Revisited.threeFourth x = √x * Epidemics.Revisited.fourthRoot x

theorem Epidemics.Revisited.fourthRoot_nonneg (x : ℝ) : 0 ≤ fourthRoot x

theorem Epidemics.Revisited.threeFourth_nonneg (x : ℝ) : 0 ≤ threeFourth x

theorem Epidemics.Revisited.fourthRoot_sq (x : ℝ) : fourthRoot x ^ 2 = √x

theorem Epidemics.Revisited.fourthRoot_four {x : ℝ} (hx : 0 ≤ x) : fourthRoot x ^ 4 = x

theorem Epidemics.Revisited.threeFourth_eq_pow3 (x : ℝ) : threeFourth x = fourthRoot x ^ 3

theorem Epidemics.Revisited.fourthRoot_one : fourthRoot 1 = 1

theorem Epidemics.Revisited.fourthRoot_ge_one {x : ℝ} (hx : 1 ≤ x) : 1 ≤ fourthRoot x

theorem Epidemics.Revisited.fourthRoot_mul {u : ℝ} (hu : 0 ≤ u) (v : ℝ) : fourthRoot (u * v) = fourthRoot u * fourthRoot v

theorem Epidemics.Revisited.fourthRoot_pow (ρ : ℝ) (hρ : 0 ≤ ρ) (i : ℕ) : fourthRoot (ρ ^ i) = fourthRoot ρ ^ i

theorem Epidemics.Revisited.threeFourth_mul {u : ℝ} (hu : 0 ≤ u) (v : ℝ) : threeFourth (u * v) = threeFourth u * threeFourth v

theorem Epidemics.Revisited.threeFourth_le_self {x : ℝ} (hx : 1 ≤ x) : threeFourth x ≤ x

theorem Epidemics.Revisited.threeFourth_split {x : ℝ} (hx : 1 ≤ x) : threeFourth x * fourthRoot x = x

theorem Epidemics.Revisited.threeFourth_div_self {x : ℝ} (hx : 1 ≤ x) : threeFourth x / x = 1 / fourthRoot x

theorem Epidemics.Revisited.three_poly_nonneg {s : ℝ} (hs : 1 ≤ s) : 0 ≤ 3 * s ^ 4 - 4 * s ^ 3 + 1

3 s^4 - 4 s^3 + 1 = (s - 1)^2 (3 s^2 + 2 s + 1) ≥ 0 for s ≥ 1.

theorem Epidemics.Revisited.threeFourth_increment {t : ℝ} (ht : 1 ≤ t) : threeFourth t - 1 ≤ 3 / 4 * (t - 1)

theorem Epidemics.Revisited.threeFourth_diff {x y : ℝ} (hx : 1 ≤ x) (hxy : x ≤ y) : threeFourth y - threeFourth x ≤ 3 / 4 * (y - x)

theorem Epidemics.Revisited.exp_neg_two_le {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1 / 2) : Real.exp (-(2 * x)) ≤ 1 - x

exp(-2x) ≤ 1 - x on [0, 1/2], from y + 1 ≤ exp y.

theorem Epidemics.Revisited.log_one_sub_ge {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1 / 2) : -2 * x ≤ Real.log (1 - x)

noncomputable def Epidemics.Revisited.fShrink (a f : ℝ) : ℝ

Equations

• Epidemics.Revisited.fShrink a f = min (f / 2) (1 / (8 * (a + 1)))

theorem Epidemics.Revisited.fShrink_pos {a f : ℝ} (hf : 0 < f) (ha : 0 ≤ a) : 0 < fShrink a f

theorem Epidemics.Revisited.fShrink_le_half {a f : ℝ} : fShrink a f ≤ f / 2

theorem Epidemics.Revisited.fShrink_le_f {a f : ℝ} (hf : 0 < f) : fShrink a f ≤ f

theorem Epidemics.Revisited.fShrink_a_le {a f : ℝ} (ha : 0 ≤ a) : (a + 1) * fShrink a f ≤ 1 / 8

noncomputable def Epidemics.Revisited.growthE (γ a b : ℝ) (n : ℕ) (k : ℝ) : ℝ

Equations

• Epidemics.Revisited.growthE γ a b n k = γ * k * (1 - (a + 1) * k / ↑n - b / Real.log ↑n)

noncomputable def Epidemics.Revisited.growthE0 (γ a b A : ℝ) (n : ℕ) (k : ℝ) : ℝ

Equations

• Epidemics.Revisited.growthE0 γ a b A n k = Epidemics.Revisited.growthE γ a b n k - A * Epidemics.Revisited.threeFourth k

theorem Epidemics.Revisited.growthE_le_linear {γ a b : ℝ} {n : ℕ} {k : ℝ} (hγ : 0 ≤ γ) (hk : 0 ≤ k) (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : 0 < ↑n) (hlog : 0 < Real.log ↑n) : growthE γ a b n k ≤ γ * k

theorem Epidemics.Revisited.sqrt_pow {ρ : ℝ} (hρ : 0 ≤ ρ) (i : ℕ) : √(ρ ^ i) = √ρ ^ i

theorem Epidemics.Revisited.fourthRoot_pos {x : ℝ} (hx : 0 < x) : 0 < fourthRoot x

theorem Epidemics.Revisited.fourthRoot_mono {x y : ℝ} (hxy : x ≤ y) : fourthRoot x ≤ fourthRoot y

theorem Epidemics.Revisited.geom_sum_le_div {ρ : ℝ} (hρ : 1 < ρ) (j : ℕ) : ∑ i ∈ Finset.range j, ρ ^ i ≤ ρ ^ j / (ρ - 1)

theorem Epidemics.Revisited.prod_one_sub_ge {η : ℕ → ℝ} {m : ℕ} (h0 : ∀ i ∈ Finset.range m, 0 ≤ η i) (h1 : ∀ i ∈ Finset.range m, η i ≤ 1) (hsum : ∑ i ∈ Finset.range m, η i ≤ 1) : 1 - ∑ i ∈ Finset.range m, η i ≤ ∏ i ∈ Finset.range m, (1 - η i)

theorem Epidemics.Revisited.growthE_diff {γ a b : ℝ} {n : ℕ} {x y f' : ℝ} (hγ : 0 ≤ γ) (hxy : x ≤ y) (hy : y ≤ f' * ↑n) (ha : 0 ≤ a) (hn : 0 < ↑n) (hlog : 0 < Real.log ↑n) (hblog : b / Real.log ↑n ≤ 1 / 4) (hf' : (a + 1) * f' ≤ 1 / 8) : γ * (y - x) * (1 / 2) ≤ growthE γ a b n y - growthE γ a b n x

E(y) - E(x) ≥ (γ/2) (y - x) on 1 ≤ x ≤ y ≤ f' n, once b / log n ≤ 1/4 and (a + 1) f' ≤ 1/8.

theorem Epidemics.Revisited.growthE_lower {γ a b : ℝ} {n : ℕ} {k f' : ℝ} (hγ : 0 ≤ γ) (hk : 0 ≤ k) (hkf : k ≤ f' * ↑n) (ha : 0 ≤ a) (hn : 0 < ↑n) (hblog : b / Real.log ↑n ≤ 1 / 4) (hf' : (a + 1) * f' ≤ 1 / 8) : γ * k * (5 / 8) ≤ growthE γ a b n k

theorem Epidemics.Revisited.growthE0_diff {γ a b A : ℝ} {n : ℕ} {x y f' : ℝ} (hγ : 0 ≤ γ) (hx : 1 ≤ x) (hxy : x ≤ y) (hy : y ≤ f' * ↑n) (ha : 0 ≤ a) (hA : A ≤ γ / 6) (hn : 0 < ↑n) (hlog : 0 < Real.log ↑n) (hblog : b / Real.log ↑n ≤ 1 / 4) (hf' : (a + 1) * f' ≤ 1 / 8) : γ * (y - x) * (3 / 8) ≤ growthE0 γ a b A n y - growthE0 γ a b A n x

theorem Epidemics.Revisited.growthE0_lower {γ a b A : ℝ} {n : ℕ} {k f' : ℝ} (hγ : 0 ≤ γ) (hk : 1 ≤ k) (hkf : k ≤ f' * ↑n) (ha : 0 ≤ a) (hA : A ≤ γ / 6) (hn : 0 < ↑n) (hblog : b / Real.log ↑n ≤ 1 / 4) (hf' : (a + 1) * f' ≤ 1 / 8) : γ * k * (11 / 24) ≤ growthE0 γ a b A n k

noncomputable def Epidemics.Revisited.alpha0 (b γlo : ℝ) : ℝ

Equations

• Epidemics.Revisited.alpha0 b γlo = Real.exp (-2 * b / Real.log (1 + γlo))

noncomputable def Epidemics.Revisited.alphaSeq (b γlo : ℝ) : ℝ

Equations

• Epidemics.Revisited.alphaSeq b γlo = Epidemics.Revisited.alpha0 b γlo / 2

noncomputable def Epidemics.Revisited.fourthGap (γlo : ℝ) : ℝ

Equations

• Epidemics.Revisited.fourthGap γlo = 1 - (Epidemics.Revisited.fourthRoot (1 + γlo))⁻¹

noncomputable def Epidemics.Revisited.growthA (γlo b : ℝ) : ℝ

Equations

• Epidemics.Revisited.growthA γlo b = min (γlo / 6) (1 / 8 * Epidemics.Revisited.fourthRoot (Epidemics.Revisited.alphaSeq b γlo) * Epidemics.Revisited.fourthGap γlo)

theorem Epidemics.Revisited.alpha0_pos (b γlo : ℝ) : 0 < alpha0 b γlo

theorem Epidemics.Revisited.alpha0_le_one {b γlo : ℝ} (hb : 0 ≤ b) (hγlo : 0 < γlo) : alpha0 b γlo ≤ 1

theorem Epidemics.Revisited.alphaSeq_pos (b γlo : ℝ) : 0 < alphaSeq b γlo

theorem Epidemics.Revisited.alphaSeq_le_one {b γlo : ℝ} (hb : 0 ≤ b) (hγlo : 0 < γlo) : alphaSeq b γlo ≤ 1

theorem Epidemics.Revisited.fourthGap_pos {γlo : ℝ} (hγlo : 0 < γlo) : 0 < fourthGap γlo

theorem Epidemics.Revisited.growthA_pos {b γlo : ℝ} (hγlo : 0 < γlo) : 0 < growthA γlo b

theorem Epidemics.Revisited.growthA_le_gamma {b γlo : ℝ} : growthA γlo b ≤ γlo / 6

theorem Epidemics.Revisited.growthA_le_series {b γlo : ℝ} : growthA γlo b ≤ 1 / 8 * fourthRoot (alphaSeq b γlo) * fourthGap γlo

theorem Epidemics.Revisited.growthA_le_eighth {b γlo : ℝ} (hb : 0 ≤ b) (hγlo : 0 < γlo) : growthA γlo b ≤ 1 / 8

noncomputable def Epidemics.Revisited.logNeed (a b f : ℝ) : ℝ

Equations

• Epidemics.Revisited.logNeed a b f = max (4 * b) (max (2 * b / (1 - a * f)) 1)

noncomputable def Epidemics.Revisited.growthN (a b f : ℝ) : ℕ

Equations

• Epidemics.Revisited.growthN a b f = max 3 (max ⌈Real.exp (Epidemics.Revisited.logNeed a b f)⌉₊ (max ⌈(Epidemics.Revisited.fShrink a f)⁻¹⌉₊ (⌈2 / f⌉₊ + 1)))

theorem Epidemics.Revisited.log_ge_need {a b f : ℝ} {n : ℕ} (hn : growthN a b f ≤ n) : logNeed a b f ≤ Real.log ↑n

theorem Epidemics.Revisited.log_pos_of_large {a b f : ℝ} {n : ℕ} (hn : growthN a b f ≤ n) : 0 < Real.log ↑n

theorem Epidemics.Revisited.n_cast_pos {a b f : ℝ} {n : ℕ} (hn : growthN a b f ≤ n) : 0 < ↑n

theorem Epidemics.Revisited.blog_quarter {a b f : ℝ} {n : ℕ} (hn : growthN a b f ≤ n) : b / Real.log ↑n ≤ 1 / 4

theorem Epidemics.Revisited.blog_connect {a b f : ℝ} {n : ℕ} (haf : a * f < 1) (hn : growthN a b f ≤ n) : b / Real.log ↑n ≤ (1 - a * f) / 2

theorem Epidemics.Revisited.shrink_n_ge_one {a b f : ℝ} {n : ℕ} (hf0 : 0 < f) (ha : 0 ≤ a) (hn : growthN a b f ≤ n) : 1 ≤ fShrink a f * ↑n

theorem Epidemics.Revisited.n_gt_two_div_f {a b f : ℝ} {n : ℕ} (hn : growthN a b f ≤ n) : 2 / f < ↑n

theorem Epidemics.Revisited.shrink_slack {a b f : ℝ} {n : ℕ} (hf0 : 0 < f) (hn : growthN a b f ≤ n) : fShrink a f * ↑n + 1 < f * ↑n

theorem Epidemics.Revisited.pow_le_of_logb {ρ x : ℝ} {j : ℕ} (hρ : 1 < ρ) (hx : 0 < x) (hj : ↑j ≤ Real.logb ρ x) : ρ ^ j ≤ x

theorem Epidemics.Revisited.lt_pow_of_logb {ρ x : ℝ} {j : ℕ} (hρ : 1 < ρ) (hx : 0 < x) (hj : Real.logb ρ x < ↑j) : x < ρ ^ j

theorem Epidemics.Revisited.logb_nonneg_of_one_le {ρ x : ℝ} (hρ : 1 < ρ) (hx : 1 ≤ x) : 0 ≤ Real.logb ρ x

noncomputable def Epidemics.Revisited.phaseCount (γ a f : ℝ) (n : ℕ) : ℕ

Equations

• Epidemics.Revisited.phaseCount γ a f n = ⌊Real.logb (1 + γ) (Epidemics.Revisited.fShrink a f * ↑n)⌋₊

theorem Epidemics.Revisited.phaseCount_pow_le {γ a f : ℝ} {n : ℕ} (hγ : 0 < γ) (hfn : 1 ≤ fShrink a f * ↑n) : (1 + γ) ^ phaseCount γ a f n ≤ fShrink a f * ↑n

theorem Epidemics.Revisited.phaseCount_succ_gt {γ a f : ℝ} {n : ℕ} (hγ : 0 < γ) (hfn : 1 ≤ fShrink a f * ↑n) : fShrink a f * ↑n < (1 + γ) ^ (phaseCount γ a f n + 1)

noncomputable def Epidemics.Revisited.gammaFactor (γ b : ℝ) (n : ℕ) : ℝ

Equations

• Epidemics.Revisited.gammaFactor γ b n = 1 + γ - γ * b / Real.log ↑n

theorem Epidemics.Revisited.gammaFactor_ge_one {γ b : ℝ} {n : ℕ} (hγ : 0 ≤ γ) (hblog : b / Real.log ↑n ≤ 1 / 4) : 1 ≤ gammaFactor γ b n

theorem Epidemics.Revisited.gammaFactor_ratio {γ b : ℝ} {n : ℕ} (hγ : 0 ≤ γ) (hblog : b / Real.log ↑n ≤ 1 / 4) : γ ≤ 4 / 3 * gammaFactor γ b n

noncomputable def Epidemics.Revisited.etaTerm (γ a b A : ℝ) (n : ℕ) (k : ℝ) : ℝ

Equations

• Epidemics.Revisited.etaTerm γ a b A n k = γ * (a + 1) * k / (Epidemics.Revisited.gammaFactor γ b n * ↑n) + A / (Epidemics.Revisited.gammaFactor γ b n * Epidemics.Revisited.fourthRoot k)

theorem Epidemics.Revisited.k_div_fourthRoot {k : ℝ} (hk : 1 ≤ k) : k / fourthRoot k = threeFourth k

theorem Epidemics.Revisited.growthStep_factor {γ a b A : ℝ} {n : ℕ} {k : ℝ} (hk : 1 ≤ k) (hΓ : gammaFactor γ b n ≠ 0) (hn : ↑n ≠ 0) (hlog : Real.log ↑n ≠ 0) : k + growthE0 γ a b A n k = gammaFactor γ b n * k * (1 - etaTerm γ a b A n k)

noncomputable def Epidemics.Revisited.kSeq (γ a b A : ℝ) (n : ℕ) : ℕ → ℝ

Equations

• Epidemics.Revisited.kSeq γ a b A n 0 = 1
• Epidemics.Revisited.kSeq γ a b A n j.succ = Epidemics.Revisited.kSeq γ a b A n j + Epidemics.Revisited.growthE0 γ a b A n (Epidemics.Revisited.kSeq γ a b A n j)

theorem Epidemics.Revisited.kSeq_in_range {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (j : ℕ) (hj : j ≤ phaseCount γ a f n) : 1 ≤ kSeq γ a b (growthA γlo b) n j ∧ kSeq γ a b (growthA γlo b) n j ≤ (1 + γ) ^ j

theorem Epidemics.Revisited.fShrink_le_one {a f : ℝ} (ha : 0 ≤ a) : fShrink a f ≤ 1

theorem Epidemics.Revisited.gammaFactor_ge_scaled {γ b : ℝ} {n : ℕ} (hb : 0 ≤ b) (hlog : 0 < Real.log ↑n) : (1 + γ) * (1 - b / Real.log ↑n) ≤ gammaFactor γ b n

theorem Epidemics.Revisited.one_sub_blog_pow_ge {γlo γ a b f : ℝ} {n j : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (hj : j ≤ phaseCount γ a f n) : alpha0 b γlo ≤ (1 - b / Real.log ↑n) ^ j

theorem Epidemics.Revisited.phaseCount_pow_ge {γ a f : ℝ} {n : ℕ} (hγ : 0 < γ) (hfn : 1 ≤ fShrink a f * ↑n) : fShrink a f * ↑n / (1 + γ) ≤ (1 + γ) ^ phaseCount γ a f n

theorem Epidemics.Revisited.kSeq_le_shrink {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (j : ℕ) (hj : j ≤ phaseCount γ a f n) : kSeq γ a b (growthA γlo b) n j ≤ fShrink a f * ↑n

theorem Epidemics.Revisited.kSeq_eq_prod {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (m : ℕ) : m ≤ phaseCount γ a f n → kSeq γ a b (growthA γlo b) n m = gammaFactor γ b n ^ m * ∏ i ∈ Finset.range m, (1 - etaTerm γ a b (growthA γlo b) n (kSeq γ a b (growthA γlo b) n i))

theorem Epidemics.Revisited.etaTerm_nonneg {γ a b A : ℝ} {n : ℕ} {k : ℝ} (hγ : 0 ≤ γ) (ha : 0 ≤ a) (hA : 0 ≤ A) (hΓ : 0 < gammaFactor γ b n) (hn : 0 < ↑n) (hk0 : 0 < k) : 0 ≤ etaTerm γ a b A n k

theorem Epidemics.Revisited.etaTerm_le_half {γ a b A : ℝ} {n : ℕ} {k f' : ℝ} (hγ : 0 ≤ γ) (hk : 1 ≤ k) (hkf : k ≤ f' * ↑n) (ha : 0 ≤ a) (hA0 : 0 ≤ A) (hA : A ≤ 1 / 8) (hn : 0 < ↑n) (hblog : b / Real.log ↑n ≤ 1 / 4) (hf' : (a + 1) * f' ≤ 1 / 8) : etaTerm γ a b A n k ≤ 1 / 2

theorem Epidemics.Revisited.sum_eta_linear_le {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (m : ℕ) (hm : m ≤ phaseCount γ a f n) : ∑ i ∈ Finset.range m, γ * (a + 1) * kSeq γ a b (growthA γlo b) n i / ↑n ≤ 1 / 8

theorem Epidemics.Revisited.sum_eta_fourth_le {γlo γ a b : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (m : ℕ) (hk : ∀ i < m, alphaSeq b γlo * (1 + γ) ^ i ≤ kSeq γ a b (growthA γlo b) n i) : ∑ i ∈ Finset.range m, growthA γlo b / fourthRoot (kSeq γ a b (growthA γlo b) n i) ≤ 1 / 8

theorem Epidemics.Revisited.eta_sum_le {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (m : ℕ) (hm : m ≤ phaseCount γ a f n) (hk : ∀ i < m, alphaSeq b γlo * (1 + γ) ^ i ≤ kSeq γ a b (growthA γlo b) n i) : ∑ i ∈ Finset.range m, etaTerm γ a b (growthA γlo b) n (kSeq γ a b (growthA γlo b) n i) ≤ 1 / 4

theorem Epidemics.Revisited.kSeq_lower {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (m : ℕ) (hm : m ≤ phaseCount γ a f n) : alphaSeq b γlo * (1 + γ) ^ m ≤ kSeq γ a b (growthA γlo b) n m

theorem Epidemics.Revisited.kSeq_phase_ge {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) : alphaSeq b γlo * fShrink a f * ↑n / (1 + γ) ≤ kSeq γ a b (growthA γlo b) n (phaseCount γ a f n)

theorem Epidemics.Revisited.kSeq_div_ge {γlo γhi γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (hγhi : γ ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) : alphaSeq b γlo * fShrink a f / (1 + γhi) ≤ kSeq γ a b (growthA γlo b) n (phaseCount γ a f n) / ↑n

theorem Epidemics.Revisited.phaseCount_le_ceil {γ a b f : ℝ} {n : ℕ} (hγ : 0 < γ) (ha : 0 ≤ a) (hf0 : 0 < f) (hn : growthN a b f ≤ n) : phaseCount γ a f n ≤ ⌈Real.logb (1 + γ) ↑n⌉₊

theorem Epidemics.Revisited.nat_half_ge (r : ℕ) : ↑(r / 2) ≥ (↑r - 1) / 2 ∧ ↑(r - r / 2) ≥ ↑r / 2

noncomputable def Epidemics.Revisited.sqrtGap (γlo : ℝ) : ℝ

Equations

• Epidemics.Revisited.sqrtGap γlo = 1 - (√(1 + γlo))⁻¹

theorem Epidemics.Revisited.sqrtGap_pos {γlo : ℝ} (hγlo : 0 < γlo) : 0 < sqrtGap γlo

noncomputable def Epidemics.Revisited.qCap (γlo γhi b c : ℝ) : ℝ

Equations

• Epidemics.Revisited.qCap γlo γhi b c = (γhi + c) / Epidemics.Revisited.growthA γlo b ^ 2

theorem Epidemics.Revisited.qCap_pos {γlo γhi b c : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (hc : 0 ≤ c) : 0 < qCap γlo γhi b c

noncomputable def Epidemics.Revisited.qTerm (γ c A k : ℝ) : ℝ

Equations

• Epidemics.Revisited.qTerm γ c A k = (γ + c) / (A ^ 2 * √k)

theorem Epidemics.Revisited.qTerm_nonneg {γ c A k : ℝ} (hγ : 0 ≤ γ) (hc : 0 ≤ c) : 0 ≤ qTerm γ c A k

theorem Epidemics.Revisited.qTerm_le_scaled {γ γhi c A k : ℝ} (hγ : γ ≤ γhi) (hA : A ≠ 0) (hk : 0 < k) : qTerm γ c A k ≤ (γhi + c) / A ^ 2 * (√k)⁻¹

noncomputable def Epidemics.Revisited.tailQSum (γlo γhi b c : ℝ) : ℝ

Equations

• Epidemics.Revisited.tailQSum γlo γhi b c = Epidemics.Revisited.qCap γlo γhi b c * (√(Epidemics.Revisited.alphaSeq b γlo))⁻¹ * (Epidemics.Revisited.sqrtGap γlo)⁻¹

theorem Epidemics.Revisited.inv_sqrt_kSeq_le {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (j : ℕ) (hj : j ≤ phaseCount γ a f n) : (√(kSeq γ a b (growthA γlo b) n j))⁻¹ ≤ (√(alphaSeq b γlo))⁻¹ * (√(1 + γ))⁻¹ ^ j

theorem Epidemics.Revisited.sum_inv_sqrt_kSeq_le {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (m : ℕ) (hm : m ≤ phaseCount γ a f n) : ∑ i ∈ Finset.range m, (√(kSeq γ a b (growthA γlo b) n i))⁻¹ ≤ (√(alphaSeq b γlo))⁻¹ * (sqrtGap γlo)⁻¹

theorem Epidemics.Revisited.sum_qTerm_le {γlo γhi γ a b c f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (hγhi : γ ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (hn : growthN a b f ≤ n) : ∑ i ∈ Finset.range (phaseCount γ a f n), qTerm γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n i) ≤ tailQSum γlo γhi b c

noncomputable def Epidemics.Revisited.xDecay (γlo γhi b c : ℝ) : ℝ

Equations

• Epidemics.Revisited.xDecay γlo γhi b c = 1 + 1 / (2 * Epidemics.Revisited.qCap γlo γhi b c)

noncomputable def Epidemics.Revisited.Qstar (γlo γhi b c : ℝ) : ℝ

Equations

• Epidemics.Revisited.Qstar γlo γhi b c = Epidemics.Revisited.qCap γlo γhi b c / (1 + Epidemics.Revisited.qCap γlo γhi b c)

theorem Epidemics.Revisited.xDecay_gt_one {γlo γhi b c : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (hc : 0 ≤ c) : 1 < xDecay γlo γhi b c

theorem Epidemics.Revisited.Qstar_bounds {γlo γhi b c : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (hc : 0 ≤ c) : 0 < Qstar γlo γhi b c ∧ Qstar γlo γhi b c < 1

theorem Epidemics.Revisited.xDecay_Qstar_lt_one {γlo γhi b c : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (hc : 0 ≤ c) : xDecay γlo γhi b c * Qstar γlo γhi b c < 1

theorem Epidemics.Revisited.Qof_mono {q Qs : ℝ} (hq0 : 0 ≤ q) (hQ : q ≤ Qs) : q / (1 + q) ≤ Qs / (1 + Qs)

theorem Epidemics.Revisited.ratio_le_exp {Q x Qs : ℝ} (hx : 1 ≤ x) (hxQ : x * Qs < 1) (hQ0 : 0 ≤ Q) (hQ : Q ≤ Qs) : (1 - Q) / (1 - x * Q) ≤ Real.exp ((x - 1) / (1 - x * Qs) * Q)

theorem Epidemics.Revisited.prod_ratio_le_exp {Q : ℕ → ℝ} {J : ℕ} {x Qs : ℝ} (hx : 1 ≤ x) (hxQ : x * Qs < 1) (hQ0 : ∀ i ∈ Finset.range J, 0 ≤ Q i) (hQ : ∀ i ∈ Finset.range J, Q i ≤ Qs) : ∏ i ∈ Finset.range J, (1 - Q i) / (1 - x * Q i) ≤ Real.exp ((x - 1) / (1 - x * Qs) * ∑ i ∈ Finset.range J, Q i)

theorem Epidemics.Revisited.inv_pow_half_le {x : ℝ} (hx : 1 < x) (r : ℕ) : x⁻¹ ^ (r / 2) ≤ √x * Real.exp (-(Real.log x / 2) * ↑r)

theorem Epidemics.Revisited.one_sub_pow_half {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) (r : ℕ) : (1 - p) ^ (r - r / 2) ≤ Real.exp (-(-Real.log (1 - p) / 2) * ↑r)