Exponential growth: one round, phases, and the tail

The round target E0 and the thresholds k_j are already in GrowthReal.lean. Here a single round misses its target with probability at most Q(k) = q(k) / (1 + q(k)) (Cantelli), the phase index is controlled by a potential on Kernel.iterate, and Lemma 19 crosses from k_J to f n.

theorem Epidemics.Revisited.threeFourth_sq {k : ℝ} (hk : 0 ≤ k) : threeFourth k ^ 2 = k * √k

theorem Epidemics.Revisited.stdFacts {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hf0 : 0 < f) (hn : growthN a b f ≤ n) : 0 < γ ∧ 0 < Real.log ↑n ∧ 0 < ↑n ∧ b / Real.log ↑n ≤ 1 / 4 ∧ (a + 1) * fShrink a f ≤ 1 / 8 ∧ 1 ≤ fShrink a f * ↑n ∧ growthA γlo b ≤ γ / 6 ∧ 0 < growthA γlo b

theorem Epidemics.Revisited.card_lt_fn {a f : ℝ} {n : ℕ} {k : ℝ} (hf0 : 0 < f) (hn : 0 < ↑n) (hk : k ≤ fShrink a f * ↑n) : k < f * ↑n

theorem Epidemics.Revisited.prob_mono {α : Type u_1} [Fintype α] (D : Dynamics.Distribution α) {p q : α → Prop} (h : ∀ (a : α), p a → q a) : D.prob p ≤ D.prob q

theorem Epidemics.Revisited.expect_new_eq {n : ℕ} (P : RumorProcess n) (S : Finset (Fin n)) : ((P.K S).expect fun (T : Finset (Fin n)) => ↑T.card - ↑S.card) = ∑ x ∈ Finset.univ \ S, P.informProb S x

theorem Epidemics.Revisited.expect_new_ge {n : ℕ} {γ a b c f : ℝ} (P : RumorProcess n) (hγ : 0 ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hlog : 0 < Real.log ↑n) (hn : 0 < ↑n) (hUG : P.UpperGrowth γ a b c f) {S : Finset (Fin n)} (hS : S.Nonempty) (hcard : ↑S.card < f * ↑n) : growthE γ a b n ↑S.card ≤ (P.K S).expect fun (T : Finset (Fin n)) => ↑T.card - ↑S.card

theorem Epidemics.Revisited.variance_new_le {n : ℕ} (P : RumorProcess n) {c : ℝ} (hc : 0 ≤ c) (hn : 0 < ↑n) (S : Finset (Fin n)) (hcov : ∀ x ∉ S, ∀ y ∉ S, x ≠ y → P.cov S x y ≤ c * ↑S.card / ↑n ^ 2) : ((P.K S).expect fun (T : Finset (Fin n)) => (↑T.card - (P.K S).expect fun (U : Finset (Fin n)) => ↑U.card) ^ 2) ≤ ((P.K S).expect fun (T : Finset (Fin n)) => ↑T.card - ↑S.card) + c * ↑S.card

theorem Epidemics.Revisited.shift_le {E μ A t : ℝ} (hE : 0 < E) (hμ : E ≤ μ) (hAt : A * t ≤ E) : E - A * t ≤ μ - A * t * μ / E

theorem Epidemics.Revisited.ratio_bound {μ E A t c k γ : ℝ} (hμ : E ≤ μ) (hE : 0 < E) (hA : 0 < A) (ht : 0 < t) (hc : 0 ≤ c) (hk : 0 < k) (hElin : E ≤ γ * k) (ht2 : t ^ 2 = k * √k) : (μ + c * k) * E ^ 2 / (A ^ 2 * t ^ 2 * μ ^ 2) ≤ (γ + c) / (A ^ 2 * √k)

theorem Epidemics.Revisited.cantelli_ratio {v lam q : ℝ} (hv : 0 ≤ v) (hlam : 0 < lam) (hq : v / lam ^ 2 ≤ q) : v / (v + lam ^ 2) ≤ q / (1 + q)

theorem Epidemics.Revisited.qTerm_antitone {γ c A k k' : ℝ} (hγ : 0 ≤ γ) (hc : 0 ≤ c) (hA : A ≠ 0) (hk : 0 < k) (hk' : k ≤ k') : qTerm γ c A k' ≤ qTerm γ c A k

theorem Epidemics.Revisited.fail_prob_le {n : ℕ} {γlo γ a b c f : ℝ} (P : RumorProcess n) (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (hUG : P.UpperGrowth γ a b c f) {S : Finset (Fin n)} (hS : S.Nonempty) (hk1 : 1 ≤ ↑S.card) (hkf : ↑S.card ≤ fShrink a f * ↑n) : ((P.K S).prob fun (T : Finset (Fin n)) => ↑T.card - ↑S.card ≤ growthE0 γ a b (growthA γlo b) n ↑S.card) ≤ qTerm γ c (growthA γlo b) ↑S.card / (1 + qTerm γ c (growthA γlo b) ↑S.card)

One round falls short of E0(|S|) with probability at most q / (1 + q).

noncomputable def Epidemics.Revisited.below {n : ℕ} (m : ℝ) (T : Finset (Fin n)) : ℝ

Indicator of still having fewer than m informed nodes.

Equations

• Epidemics.Revisited.below m T = if ↑T.card < m then 1 else 0

theorem Epidemics.Revisited.notYet_below {n : ℕ} (P : RumorProcess n) (m : ℝ) (t : ℕ) (S : Finset (Fin n)) : P.notYet m t S = P.K.iterate t (below m) S

theorem Epidemics.Revisited.apply_below_le {n : ℕ} (P : RumorProcess n) (m : ℝ) (S : Finset (Fin n)) : P.K.apply (below m) S ≤ below m S

theorem Epidemics.Revisited.iterate_below_succ_le {n : ℕ} (P : RumorProcess n) (m : ℝ) (t : ℕ) (S : Finset (Fin n)) : P.K.iterate (t + 1) (below m) S ≤ P.K.iterate t (below m) S

theorem Epidemics.Revisited.notYet_antitone {n : ℕ} (P : RumorProcess n) (m : ℝ) {s t : ℕ} (hst : s ≤ t) (S : Finset (Fin n)) : P.notYet m t S ≤ P.notYet m s S

theorem Epidemics.Revisited.kSeq_succ_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) (j : ℕ) (hj : j < phaseCount γ a f n) : kSeq γ a b (growthA γlo b) n j ≤ kSeq γ a b (growthA γlo b) n (j + 1)

theorem Epidemics.Revisited.kSeq_le_add {γ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 d : ℕ) (hj : j + d ≤ phaseCount γ a f n) : kSeq γ a b (growthA γlo b) n j ≤ kSeq γ a b (growthA γlo b) n (j + d)

theorem Epidemics.Revisited.kSeq_le_count {γ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 ≤ kSeq γ a b (growthA γlo b) n (phaseCount γ a f n)

noncomputable def Epidemics.Revisited.phaseIdx (γlo γ a b : ℝ) (n J : ℕ) (k : ℝ) : ℕ

Largest j ≤ J with k_j ≤ k, or 0 when k < k_0.

Equations

• Epidemics.Revisited.phaseIdx γlo γ a b n J k = Nat.findGreatest (fun (j : ℕ) => Epidemics.Revisited.kSeq γ a b (Epidemics.Revisited.growthA γlo b) n j ≤ k) J

theorem Epidemics.Revisited.phaseIdx_le (γlo γ a b : ℝ) (n J : ℕ) (k : ℝ) : phaseIdx γlo γ a b n J k ≤ J

theorem Epidemics.Revisited.phaseIdx_k_le {γlo γ a b : ℝ} {n J : ℕ} {k : ℝ} (hk : 1 ≤ k) : kSeq γ a b (growthA γlo b) n (phaseIdx γlo γ a b n J k) ≤ k

theorem Epidemics.Revisited.le_phaseIdx {γlo γ a b : ℝ} {n J j : ℕ} {k : ℝ} (hj : j ≤ J) (hk : kSeq γ a b (growthA γlo b) n j ≤ k) : j ≤ phaseIdx γlo γ a b n J k

theorem Epidemics.Revisited.phaseIdx_next {γlo γ a b : ℝ} {n J : ℕ} {k : ℝ} {j : ℕ} (hj : phaseIdx γlo γ a b n J k < j) (hjJ : j ≤ J) : ¬kSeq γ a b (growthA γlo b) n j ≤ k

theorem Epidemics.Revisited.phaseIdx_of_ge {γlo γ a b : ℝ} {n J : ℕ} {k : ℝ} (hk : kSeq γ a b (growthA γlo b) n J ≤ k) : phaseIdx γlo γ a b n J k = J

noncomputable def Epidemics.Revisited.connectP (γlo γhi a b f : ℝ) : ℝ

Equations

• Epidemics.Revisited.connectP γlo γhi a b f = γlo * (Epidemics.Revisited.alphaSeq b γlo * Epidemics.Revisited.fShrink a f / (1 + γhi)) * ((1 - a * f) / 2)

theorem Epidemics.Revisited.connectP_pos {γlo γhi a b f : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (ha : 0 ≤ a) (hf0 : 0 < f) (haf : a * f < 1) : 0 < connectP γlo γhi a b f

theorem Epidemics.Revisited.connectP_le_half {γlo γhi a b f : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (haf : a * f < 1) : connectP γlo γhi a b f ≤ 1 / 2

theorem Epidemics.Revisited.Q_le_q {q : ℝ} (hq : 0 ≤ q) : q / (1 + q) ≤ q

theorem Epidemics.Revisited.contract {Q x g : ℝ} (hx : x ≠ 0) (hden : 1 - x * Q ≠ 0) : Q * (x * (1 - Q) / (1 - x * Q) * g) + (1 - Q) * g = x * (1 - Q) / (1 - x * Q) * g / x

theorem Epidemics.Revisited.pow_inv_shift {x : ℝ} (hx : x ≠ 0) (J s : ℕ) (p : ℝ) : x⁻¹ ^ (J + s) * (x ^ J * p) = x⁻¹ ^ s * p

theorem Epidemics.Revisited.exp_rate_le {a b r : ℝ} (hab : a ≤ b) (hr : 0 ≤ r) : Real.exp (-b * r) ≤ Real.exp (-a * r)

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

Equations

• Epidemics.Revisited.phaseQ γ c A k = Epidemics.Revisited.qTerm γ c A k / (1 + Epidemics.Revisited.qTerm γ c A k)

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

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

theorem Epidemics.Revisited.phaseQ_antitone {γ c A k k' : ℝ} (hγ : 0 ≤ γ) (hc : 0 ≤ c) (hA : A ≠ 0) (hk : 0 < k) (hk' : k ≤ k') : phaseQ γ c A k' ≤ phaseQ γ c A k

theorem Epidemics.Revisited.qTerm_le_qCap {γlo γhi γ b c k : ℝ} (hγlo : 0 < γlo) (hγhi : γ ≤ γhi) (hγ0 : 0 ≤ γhi) (hc : 0 ≤ c) (hk : 1 ≤ k) : qTerm γ c (growthA γlo b) k ≤ qCap γlo γhi b c

theorem Epidemics.Revisited.phaseQ_le_Qstar {γlo γhi γ b c k : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (hγhi : γ ≤ γhi) (hc : 0 ≤ c) (hk : 1 ≤ k) : phaseQ γ c (growthA γlo b) k ≤ Qstar γlo γhi b c

noncomputable def Epidemics.Revisited.phaseRatio (γlo γhi γ a b c : ℝ) (n i : ℕ) : ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Epidemics.Revisited.phaseG (γlo γhi γ a b c f : ℝ) (n j : ℕ) : ℝ

Equations

• Epidemics.Revisited.phaseG γlo γhi γ a b c f n j = ∏ i ∈ Finset.Ico j (Epidemics.Revisited.phaseCount γ a f n), Epidemics.Revisited.phaseRatio γlo γhi γ a b c n i

theorem Epidemics.Revisited.phaseQ_k_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 : ℕ) (hi : i ≤ phaseCount γ a f n) : phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n i) ≤ Qstar γlo γhi b c

theorem Epidemics.Revisited.phaseRatio_ge_one {γ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 : ℕ} (hi : i < phaseCount γ a f n) : 1 ≤ phaseRatio γlo γhi γ a b c n i

theorem Epidemics.Revisited.phaseG_top {γlo γhi γ a b c f : ℝ} {n : ℕ} : phaseG γlo γhi γ a b c f n (phaseCount γ a f n) = 1

theorem Epidemics.Revisited.phaseG_succ {γlo γhi γ a b c f : ℝ} {n j : ℕ} (hj : j < phaseCount γ a f n) : phaseG γlo γhi γ a b c f n j = phaseRatio γlo γhi γ a b c n j * phaseG γlo γhi γ a b c f n (j + 1)

theorem Epidemics.Revisited.phaseG_ge_one {γ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) {j : ℕ} (_hj : j ≤ phaseCount γ a f n) : 1 ≤ phaseG γlo γhi γ a b c f n j

theorem Epidemics.Revisited.phaseG_antitone {γ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) {j j' : ℕ} (hjj : j ≤ j') (hj' : j' ≤ phaseCount γ a f n) : phaseG γlo γhi γ a b c f n j' ≤ phaseG γlo γhi γ a b c f n j

theorem Epidemics.Revisited.phase_contract {γ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) {j : ℕ} (hj : j < phaseCount γ a f n) : phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n j) * phaseG γlo γhi γ a b c f n j + (1 - phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n j)) * phaseG γlo γhi γ a b c f n (j + 1) = phaseG γlo γhi γ a b c f n j / xDecay γlo γhi b c

theorem Epidemics.Revisited.kSeq_le_of_phase {γlo γ a b : ℝ} {n J : ℕ} {k : ℝ} (hk : 1 ≤ k) (hidx : phaseIdx γlo γ a b n J k = J) : kSeq γ a b (growthA γlo b) n J ≤ k

theorem Epidemics.Revisited.e0_mono {γlo γ a b f : ℝ} {n : ℕ} (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hf0 : 0 < f) (hn : growthN a b f ≤ n) {x y : ℝ} (hx : 1 ≤ x) (hxy : x ≤ y) (hy : y ≤ fShrink a f * ↑n) : growthE0 γ a b (growthA γlo b) n x ≤ growthE0 γ a b (growthA γlo b) n y

theorem Epidemics.Revisited.k_shortfall {γ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) {k : ℝ} (hkf : k ≤ fShrink a f * ↑n) {j : ℕ} (hj : j < phaseCount γ a f n) (hkj : kSeq γ a b (growthA γlo b) n j ≤ k) : kSeq γ a b (growthA γlo b) n (j + 1) - k ≤ growthE0 γ a b (growthA γlo b) n k

theorem Epidemics.Revisited.short_prob_le {n : ℕ} {γlo γ a b c f : ℝ} (P : RumorProcess n) (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (hn : growthN a b f ≤ n) (hUG : P.UpperGrowth γ a b c f) {S : Finset (Fin n)} (hk1 : 1 ≤ ↑S.card) (hkf : ↑S.card ≤ fShrink a f * ↑n) {j : ℕ} (hj : j < phaseCount γ a f n) (hkj : kSeq γ a b (growthA γlo b) n j ≤ ↑S.card) : ((P.K S).prob fun (T : Finset (Fin n)) => ↑T.card < kSeq γ a b (growthA γlo b) n (j + 1)) ≤ phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n j)

theorem Epidemics.Revisited.phasePot_mix {γ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) {j : ℕ} (hj : j < phaseCount γ a f n) {T : Finset (Fin n)} (hkj : kSeq γ a b (growthA γlo b) n j ≤ ↑T.card) : phaseG γlo γhi γ a b c f n (phaseIdx γlo γ a b n (phaseCount γ a f n) ↑T.card) ≤ phaseG γlo γhi γ a b c f n (j + 1) + (phaseG γlo γhi γ a b c f n j - phaseG γlo γhi γ a b c f n (j + 1)) * below (kSeq γ a b (growthA γlo b) n (j + 1)) T

theorem Epidemics.Revisited.expect_phase_le {n : ℕ} {γlo γhi γ a b c f : ℝ} (P : RumorProcess 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) (hUG : P.UpperGrowth γ a b c f) {S : Finset (Fin n)} (hk1 : 1 ≤ ↑S.card) (hj : phaseIdx γlo γ a b n (phaseCount γ a f n) ↑S.card < phaseCount γ a f n) : ((P.K S).expect fun (T : Finset (Fin n)) => phaseG γlo γhi γ a b c f n (phaseIdx γlo γ a b n (phaseCount γ a f n) ↑T.card)) ≤ phaseG γlo γhi γ a b c f n (phaseIdx γlo γ a b n (phaseCount γ a f n) ↑S.card) / xDecay γlo γhi b c

theorem Epidemics.Revisited.below_le_phaseG {γ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) {S : Finset (Fin n)} (hk : 1 ≤ ↑S.card) : below (kSeq γ a b (growthA γlo b) n (phaseCount γ a f n)) S ≤ phaseG γlo γhi γ a b c f n (phaseIdx γlo γ a b n (phaseCount γ a f n) ↑S.card)

theorem Epidemics.Revisited.iterate_below_phase_le {n : ℕ} {γlo γhi γ a b c f : ℝ} (P : RumorProcess 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) (hUG : P.UpperGrowth γ a b c f) (t : ℕ) {S : Finset (Fin n)} (hk : 1 ≤ ↑S.card) : P.K.iterate t (below (kSeq γ a b (growthA γlo b) n (phaseCount γ a f n))) S ≤ (xDecay γlo γhi b c)⁻¹ ^ t * phaseG γlo γhi γ a b c f n (phaseIdx γlo γ a b n (phaseCount γ a f n) ↑S.card)

theorem Epidemics.Revisited.phaseG_as_prod {γlo γhi γ a b c f : ℝ} {n : ℕ} : phaseG γlo γhi γ a b c f n 0 = xDecay γlo γhi b c ^ phaseCount γ a f n * ∏ i ∈ Finset.range (phaseCount γ a f n), (1 - phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n i)) / (1 - xDecay γlo γhi b c * phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n i))

theorem Epidemics.Revisited.sum_phaseQ_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), phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n i) ≤ tailQSum γlo γhi b c

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

Equations

• One or more equations did not get rendered due to their size.

theorem Epidemics.Revisited.prod_phase_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), (1 - phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n i)) / (1 - xDecay γlo γhi b c * phaseQ γ c (growthA γlo b) (kSeq γ a b (growthA γlo b) n i)) ≤ tailProd γlo γhi b c

theorem Epidemics.Revisited.phase_iterate_exp {n : ℕ} {γlo γhi γ a b c f : ℝ} (P : RumorProcess 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) (hUG : P.UpperGrowth γ a b c f) (r : ℕ) {S : Finset (Fin n)} (hk : 1 ≤ ↑S.card) : P.K.iterate (phaseCount γ a f n + r / 2) (below (kSeq γ a b (growthA γlo b) n (phaseCount γ a f n))) S ≤ tailProd γlo γhi b c * √(xDecay γlo γhi b c) * Real.exp (-(Real.log (xDecay γlo γhi b c) / 2) * ↑r)

theorem Epidemics.Revisited.inform_ge_connect {n : ℕ} {γlo γhi γ a b c f : ℝ} (P : RumorProcess n) (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (hγhi : γ ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (haf : a * f < 1) (hn : growthN a b f ≤ n) (hUG : P.UpperGrowth γ a b c f) {S : Finset (Fin n)} (hℓ : ⌈kSeq γ a b (growthA γlo b) n (phaseCount γ a f n)⌉₊ ≤ S.card) (hlt : ↑S.card < f * ↑n) {x : Fin n} (hx : x ∉ S) : connectP γlo γhi a b f ≤ P.informProb S x

theorem Epidemics.Revisited.bridge_le {n : ℕ} {γlo γhi γ a b c f : ℝ} (P : RumorProcess n) (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (hγhi : γ ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf0 : 0 < f) (hf1 : f < 1) (haf : a * f < 1) (hn : growthN a b f ≤ n) (hUG : P.UpperGrowth γ a b c f) (t : ℕ) (U : Finset (Fin n)) : P.K.iterate t (below (f * ↑n)) U ≤ below (kSeq γ a b (growthA γlo b) n (phaseCount γ a f n)) U + (↑n - ↑⌈kSeq γ a b (growthA γlo b) n (phaseCount γ a f n)⌉₊) / (↑n - f * ↑n) * (1 - connectP γlo γhi a b f) ^ t

theorem Epidemics.Revisited.connect_ratio_le {γlo γ a b f : ℝ} {n : ℕ} (_hγlo : 0 < γlo) (_hγ : γlo ≤ γ) (_ha : 0 ≤ a) (_hb : 0 ≤ b) (_hf0 : 0 < f) (hf1 : f < 1) (hn : growthN a b f ≤ n) : (↑n - ↑⌈kSeq γ a b (growthA γlo b) n (phaseCount γ a f n)⌉₊) / (↑n - f * ↑n) ≤ 1 / (1 - f)

noncomputable def Epidemics.Revisited.decayAlpha (γlo γhi a b c f : ℝ) : ℝ

Equations

• Epidemics.Revisited.decayAlpha γlo γhi a b c f = min (Real.log (Epidemics.Revisited.xDecay γlo γhi b c) / 2) (-Real.log (1 - Epidemics.Revisited.connectP γlo γhi a b f) / 2)

noncomputable def Epidemics.Revisited.tailPrefactor (γlo γhi _a b c f : ℝ) : ℝ

Equations

• Epidemics.Revisited.tailPrefactor γlo γhi _a b c f = Epidemics.Revisited.tailProd γlo γhi b c * √(Epidemics.Revisited.xDecay γlo γhi b c) + 1 / (1 - f)

theorem Epidemics.Revisited.decayAlpha_pos {γlo γhi a b c f : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (haf : a * f < 1) : 0 < decayAlpha γlo γhi a b c f

theorem Epidemics.Revisited.tailPrefactor_nonneg {γlo γhi a b c f : ℝ} (hf1 : f < 1) : 0 ≤ tailPrefactor γlo γhi a b c f

theorem Epidemics.Revisited.notYet_growth_le {n : ℕ} {γlo γhi γ a b c f : ℝ} (P : RumorProcess n) (hγlo : 0 < γlo) (hγ : γlo ≤ γ) (hγhi : γ ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (hf1 : f < 1) (haf : a * f < 1) (hn : growthN a b f ≤ n) (hUG : P.UpperGrowth γ a b c f) {S : Finset (Fin n)} (hk : 1 ≤ ↑S.card) (r : ℕ) : P.notYet (f * ↑n) (⌈Real.logb (1 + γ) ↑n⌉₊ + r) S ≤ tailPrefactor γlo γhi a b c f * Real.exp (-decayAlpha γlo γhi a b c f * ↑r)

theorem Epidemics.Revisited.growth_upper_tail_proof {γlo γhi a b c f : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (hf1 : f < 1) (haf : a * f < 1) : ∃ (A : ℝ) (α : ℝ), 0 < α ∧ ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (γ : ℝ), γlo ≤ γ → γ ≤ γhi → ∀ (P : RumorProcess n), P.UpperGrowth γ a b c f → ∀ (S : Finset (Fin n)), S.Nonempty → ∀ (r : ℕ), P.notYet (f * ↑n) (⌈Real.logb (1 + γ) ↑n⌉₊ + r) S ≤ A * Real.exp (-α * ↑r)

theorem Epidemics.Revisited.growth_upper_expect_proof {γlo γhi a b c f : ℝ} (hγlo : 0 < γlo) (hγ : γlo ≤ γhi) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hf0 : 0 < f) (hf1 : f < 1) (haf : a * f < 1) : ∃ (B : ℝ) (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (γ : ℝ), γlo ≤ γ → γ ≤ γhi → ∀ (P : RumorProcess n), P.UpperGrowth γ a b c f → ∀ (S : Finset (Fin n)), S.Nonempty → ∀ (R : ℕ), ∑ t ∈ Finset.range R, P.notYet (f * ↑n) t S ≤ Real.logb (1 + γ) ↑n + B