MaxLeafFormal.RSCTrials

Source file MaxLeafFormal/RSCTrials.lean of the Lean project (how it is built).

Statements of the paper formalised here: Lemma 8.4, Theorem 8.1.

import MaxLeafFormal.Budget

/-!
# The trials of RSC (`lem:rsc-trials`)
-/

namespace MaxLeafFormal.RSCTrials

open Finset MeasureTheory MaxLeafFormal.CDS MaxLeafFormal.Budget
open scoped ENNReal

variable {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]

/-- `C(X')`. -/
def cand (X' : Finset V) : Finset V :=
  univ.filter fun v => v ∉ X' ∧ 2 ≤ (G.neighborFinset v ∩ X').card

/-- `p_k` for `k ≥ 2`. -/
def pk (p₂ p₃ : ℝ) (k : ℕ) : ℝ := if k = 2 then p₂ else p₃

noncomputable def inclProb (p₂ p₃ : ℝ) (X' : Finset V) (v : V) : ℝ :=
  pk p₂ p₃ (G.neighborFinset v ∩ X').card

/-- `Pr[Υ = U]` for the closure of `X'` (alg:rsc-algorithm step (b), def:rsc-gf). -/
noncomputable def closureProb (p₂ p₃ : ℝ) (X' U : Finset V) : ℝ :=
  if U ⊆ cand G X' then
    (∏ v ∈ U, inclProb G p₂ p₃ X' v) * ∏ v ∈ cand G X' \ U, (1 - inclProb G p₂ p₃ X' v)
  else 0

/-- `W^cl_S(y)`, def:rsc-gf. -/
noncomputable def Wcl (p₂ p₃ : ℝ) (S : Finset V) (y : ℝ) : ℝ :=
  ∑ X' ∈ S.powerset, y ^ X'.card *
    ∑ U : Finset V, closureProb G p₂ p₃ X' U *
      (if U ⊆ S then (2:ℝ) ^ (-(termCount G (X' ∪ U) : ℝ)) else 0)

/-- Law of the random choices `(X', Υ)` of a trial with sample size `t` (steps (a)–(b)). -/
noncomputable def trialProb (p₂ p₃ : ℝ) (t : ℕ) (z : Finset V × Finset V) : ℝ :=
  (if z.1.card = t then (((Fintype.card V).choose t : ℕ) : ℝ)⁻¹ else 0)
    * closureProb G p₂ p₃ z.1 z.2

noncomputable def rscTrialMeasure (p₂ p₃ : ℝ) (t : ℕ) : Measure (Finset V × Finset V) :=
  ∑ z : Finset V × Finset V, ENNReal.ofReal (trialProb G p₂ p₃ t z) • Measure.dirac z

/-- `ξ_t` of lem:rsc-trials (b). -/
noncomputable def xi (S : Finset V) (z : Finset V × Finset V) : ℝ≥0∞ :=
  if z.1 ∪ z.2 ⊆ S then (termCount G (z.1 ∪ z.2) : ℝ≥0∞) else ⊤

/-- Step (c) for size `s`, threshold `θ`, with `A_St` replaced by its specification. -/
def rscAccept (s θ : ℕ) : Set (Finset V × Finset V) :=
  {z | (z.1 ∪ z.2).card ≤ s ∧ termCount G (z.1 ∪ z.2) ≤ θ ∧
       MLS.ExtYes (IsCDS G) (z.1 ∪ z.2) (s - (z.1 ∪ z.2).card)}

-- Representation checks

lemma inclProb_mem (p₂ p₃ : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (X' : Finset V) (v : V) :
    0 ≤ inclProb G p₂ p₃ X' v ∧ inclProb G p₂ p₃ X' v ≤ 1 := by
  obtain ⟨h2, h23, h3⟩ := hp
  unfold inclProb pk
  split_ifs
  · exact ⟨h2, by linarith⟩
  · exact ⟨by linarith, h3⟩

lemma closureProb_nonneg (p₂ p₃ : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (X' U : Finset V) :
    0 ≤ closureProb G p₂ p₃ X' U := by
  unfold closureProb
  split_ifs
  · apply mul_nonneg
    · exact Finset.prod_nonneg fun v _ => (inclProb_mem G p₂ p₃ hp X' v).1
    · exact Finset.prod_nonneg fun v _ => sub_nonneg.mpr (inclProb_mem G p₂ p₃ hp X' v).2
  · exact le_refl _

lemma closureProb_sum_eq (p₂ p₃ : ℝ) (X' : Finset V) :
    ∑ U : Finset V, closureProb G p₂ p₃ X' U = 1 := by
  classical
  unfold closureProb
  rw [← Finset.sum_filter]
  have hfilt : (univ : Finset (Finset V)).filter (fun U => U ⊆ cand G X') = (cand G X').powerset := by
    ext U; simp [Finset.mem_powerset]
  rw [hfilt]
  have h1 : ∀ v, inclProb G p₂ p₃ X' v + (1 - inclProb G p₂ p₃ X' v) = 1 := fun v => by ring
  have key := Finset.prod_add (fun v => inclProb G p₂ p₃ X' v)
    (fun v => 1 - inclProb G p₂ p₃ X' v) (cand G X')
  simp only [h1, Finset.prod_const_one] at key
  exact key.symm

theorem trialProb_nonneg (p₂ p₃ : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (t : ℕ)
    (z : Finset V × Finset V) : 0 ≤ trialProb G p₂ p₃ t z := by
  unfold trialProb
  apply mul_nonneg
  · split_ifs
    · exact inv_nonneg.mpr (Nat.cast_nonneg _)
    · exact le_refl _
  · exact closureProb_nonneg G p₂ p₃ hp z.1 z.2

lemma trialProb_sum (p₂ p₃ : ℝ) (_hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (t : ℕ)
    (ht : t ≤ Fintype.card V) :
    ∑ z : Finset V × Finset V, trialProb G p₂ p₃ t z = 1 := by
  rw [Fintype.sum_prod_type]
  have hin : ∀ a : Finset V, ∑ b : Finset V, trialProb G p₂ p₃ t (a, b)
      = if a.card = t then (((Fintype.card V).choose t : ℕ) : ℝ)⁻¹ else 0 := by
    intro a
    have hgen : ∀ c : ℝ, ∑ b : Finset V, c * closureProb G p₂ p₃ a b = c := fun c => by
      rw [← Finset.mul_sum, closureProb_sum_eq, mul_one]
    simp only [trialProb]
    exact hgen (if a.card = t then (((Fintype.card V).choose t : ℕ) : ℝ)⁻¹ else 0)
  simp only [hin]
  have hcard : (univ.filter (fun a : Finset V => a.card = t)).card = (Fintype.card V).choose t := by
    have : univ.filter (fun a : Finset V => a.card = t) = powersetCard t (univ : Finset V) := by
      ext a; simp [Finset.mem_powersetCard]
    rw [this, Finset.card_powersetCard, Finset.card_univ]
  rw [Finset.sum_ite, Finset.sum_const_zero, add_zero, Finset.sum_const, nsmul_eq_mul, hcard]
  have hpos : ((Fintype.card V).choose t : ℝ) ≠ 0 := by
    exact_mod_cast (Nat.choose_pos ht).ne'
  exact mul_inv_cancel₀ hpos

theorem sum_closureProb (p₂ p₃ : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (X' : Finset V) :
    (∀ U, 0 ≤ closureProb G p₂ p₃ X' U) ∧ ∑ U : Finset V, closureProb G p₂ p₃ X' U = 1 :=
  ⟨fun U => closureProb_nonneg G p₂ p₃ hp X' U, closureProb_sum_eq G p₂ p₃ X'⟩

theorem isProbabilityMeasure_rscTrialMeasure (p₂ p₃ : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1)
    (t : ℕ) (ht : t ≤ Fintype.card V) : IsProbabilityMeasure (rscTrialMeasure G p₂ p₃ t) := by
  constructor
  have h : (rscTrialMeasure G p₂ p₃ t) Set.univ
      = ∑ z : Finset V × Finset V, ENNReal.ofReal (trialProb G p₂ p₃ t z) := by
    unfold rscTrialMeasure
    simp [Measure.coe_finsetSum, Finset.sum_apply]
  rw [h, ← ENNReal.ofReal_sum_of_nonneg (fun z _ => trialProb_nonneg G p₂ p₃ hp t z),
    trialProb_sum G p₂ p₃ hp t ht, ENNReal.ofReal_one]

-- Supporting

theorem integral_rscTrialMeasure (p₂ p₃ : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (t : ℕ)
    (f : Finset V × Finset V → ℝ) :
    ∫ z, f z ∂(rscTrialMeasure G p₂ p₃ t) = ∑ z, trialProb G p₂ p₃ t z * f z := by
  unfold rscTrialMeasure
  rw [integral_finsetSum_measure]
  · refine Finset.sum_congr rfl fun z _ => ?_
    rw [integral_smul_measure, integral_dirac, ENNReal.toReal_ofReal (trialProb_nonneg G p₂ p₃ hp t z), smul_eq_mul]
  · intro z _
    exact Integrable.smul_measure Integrable.of_finite ENNReal.ofReal_ne_top

-- The identity in the proof of lem:rsc-trials

theorem twoPowNeg_xi_eq (S : Finset V) (z : Finset V × Finset V) :
    twoPowNeg (xi G S z) =
      if z.1 ∪ z.2 ⊆ S then (2:ℝ) ^ (-(termCount G (z.1 ∪ z.2) : ℝ)) else 0 := by
  by_cases h : z.1 ∪ z.2 ⊆ S
  · simp [xi, twoPowNeg, h, ENNReal.natCast_ne_top, ENNReal.toReal_natCast]
  · simp [xi, twoPowNeg, h]

theorem inner_eq (p₂ p₃ : ℝ) (S : Finset V) (t : ℕ) (ht : t ≤ S.card) :
    ((Fintype.card V).choose t : ℝ) * ∑ z, trialProb G p₂ p₃ t z * twoPowNeg (xi G S z)
      = ∑ X' ∈ S.powerset.filter (fun X' => X'.card = t), ∑ U : Finset V,
          closureProb G p₂ p₃ X' U *
            (if U ⊆ S then (2:ℝ) ^ (-(termCount G (X' ∪ U) : ℝ)) else 0) := by
  have hchoose : ((Fintype.card V).choose t : ℝ) ≠ 0 := by
    have : 0 < (Fintype.card V).choose t := Nat.choose_pos (ht.trans (card_le_univ S))
    exact_mod_cast this.ne'
  have key2 : ∀ X' : Finset V,
      ∑ U : Finset V, trialProb G p₂ p₃ t (X', U) * twoPowNeg (xi G S (X', U)) =
        if X' ∈ S.powerset.filter (fun X' => X'.card = t) then
          ((Fintype.card V).choose t : ℝ)⁻¹ *
            ∑ U : Finset V, closureProb G p₂ p₃ X' U *
              (if U ⊆ S then (2:ℝ) ^ (-(termCount G (X' ∪ U) : ℝ)) else 0)
        else 0 := by
    intro X'
    have hterm : ∀ U : Finset V,
        trialProb G p₂ p₃ t (X', U) * twoPowNeg (xi G S (X', U)) =
          (if X'.card = t then ((Fintype.card V).choose t : ℝ)⁻¹ else 0) *
            (if X' ⊆ S then closureProb G p₂ p₃ X' U *
              (if U ⊆ S then (2:ℝ) ^ (-(termCount G (X' ∪ U) : ℝ)) else 0) else 0) := by
      intro U
      unfold trialProb
      rw [twoPowNeg_xi_eq]
      simp only [union_subset_iff]
      by_cases hX : X' ⊆ S <;> by_cases hC : X'.card = t <;> by_cases hU : U ⊆ S <;>
        simp [hX, hC, hU, mul_assoc]
    rw [Finset.sum_congr rfl (fun U _ => hterm U), ← Finset.mul_sum]
    have hmem : X' ∈ S.powerset.filter (fun X' => X'.card = t) ↔ X' ⊆ S ∧ X'.card = t := by
      simp [mem_filter, mem_powerset]
    simp only [hmem]
    by_cases hX : X' ⊆ S <;> by_cases hC : X'.card = t <;> simp [hX, hC]
  rw [Fintype.sum_prod_type]
  simp only [key2]
  rw [Finset.sum_ite_mem, univ_inter, Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro X' _
  rw [← mul_assoc, mul_inv_cancel₀ hchoose, one_mul]

theorem Wcl_eq_sum (p₂ p₃ : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1) (S : Finset V) (y : ℝ) :
    Wcl G p₂ p₃ S y = ∑ t ∈ range (S.card + 1),
      ((Fintype.card V).choose t : ℝ) * y ^ t *
        ∫ z, twoPowNeg (xi G S z) ∂(rscTrialMeasure G p₂ p₃ t) := by
  have hstep : ∀ t ∈ range (S.card + 1),
      ((Fintype.card V).choose t : ℝ) * y ^ t *
        ∫ z, twoPowNeg (xi G S z) ∂(rscTrialMeasure G p₂ p₃ t)
      = ∑ X' ∈ S.powerset.filter (fun X' => X'.card = t), y ^ X'.card *
          ∑ U : Finset V, closureProb G p₂ p₃ X' U *
            (if U ⊆ S then (2:ℝ) ^ (-(termCount G (X' ∪ U) : ℝ)) else 0) := by
    intro t ht
    have ht' : t ≤ S.card := Nat.lt_succ_iff.mp (mem_range.mp ht)
    have hint := integral_rscTrialMeasure G p₂ p₃ hp t (fun z => twoPowNeg (xi G S z))
    rw [hint]
    have hrw : ((Fintype.card V).choose t : ℝ) * y ^ t *
        ∑ z, trialProb G p₂ p₃ t z * twoPowNeg (xi G S z) =
        y ^ t * (((Fintype.card V).choose t : ℝ) *
          ∑ z, trialProb G p₂ p₃ t z * twoPowNeg (xi G S z)) := by ring
    rw [hrw, inner_eq G p₂ p₃ S t ht', Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro X' hX'
    rw [(mem_filter.mp hX').2]
  have hmaps : ∀ X' ∈ S.powerset, (fun X' : Finset V => X'.card) X' ∈ range (S.card + 1) := by
    intro X' hX'
    exact mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp hX')))
  unfold Wcl
  rw [Finset.sum_congr rfl hstep]
  exact (Finset.sum_fiberwise_of_maps_to hmaps _).symm

-- lem:rsc-trials (b), last claim

/-- The inequality of `lem:rsc-trials`(b): for every `S ⊆ V` and
`y ≥ 0`, `W^cl_S(y) ≤ (1+y)^n · max_{0 ≤ t ≤ |S|} E[2^{-ξ_t}]`. -/
theorem rsc_trials_W (p₂ p₃ : ℝ) (hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1)
    (S : Finset V) (y : ℝ) (hy : 0 ≤ y) :
    ∃ t ≤ S.card, Wcl G p₂ p₃ S y
      ≤ (1 + y) ^ Fintype.card V * ∫ z, twoPowNeg (xi G S z) ∂(rscTrialMeasure G p₂ p₃ t) := by
  set e : ℕ → ℝ := fun t => ∫ z, twoPowNeg (xi G S z) ∂(rscTrialMeasure G p₂ p₃ t) with he
  have he0 : ∀ t, 0 ≤ e t := fun t =>
    integral_nonneg fun z => (twoPowNeg_mem_Icc _).1
  obtain ⟨t0, ht0, hmax⟩ := exists_max_image (range (S.card + 1)) e nonempty_range_add_one
  refine ⟨t0, Nat.lt_succ_iff.1 (mem_range.1 ht0), ?_⟩
  rw [Wcl_eq_sum G p₂ p₃ hp S y]
  have hSn : S.card ≤ Fintype.card V := card_le_univ S
  calc ∑ t ∈ range (S.card + 1), ((Fintype.card V).choose t : ℝ) * y ^ t * e t
      ≤ ∑ t ∈ range (S.card + 1), ((Fintype.card V).choose t : ℝ) * y ^ t * e t0 :=
        sum_le_sum fun t ht => mul_le_mul_of_nonneg_left (hmax t ht) (by positivity)
    _ ≤ ∑ t ∈ range (Fintype.card V + 1), ((Fintype.card V).choose t : ℝ) * y ^ t * e t0 :=
        sum_le_sum_of_subset_of_nonneg (range_subset_range.2 (by omega))
          (fun t _ _ => by have := he0 t0; positivity)
    _ = (1 + y) ^ Fintype.card V * e t0 := by
        rw [← sum_mul, add_comm (1:ℝ) y, add_pow]
        congr 1
        refine sum_congr rfl fun t _ => ?_
        rw [one_pow, mul_one, mul_comm]

-- lem:rsc-trials (b), (T3); and (a), soundness

theorem rsc_trials_T3 (p₂ p₃ : ℝ) (_hp : 0 ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₃ ≤ 1)
    (S : Finset V) (hS : IsCDS G S) (t θ : ℕ) :
    (rscTrialMeasure G p₂ p₃ t).real (leEvent (xi G S) θ)
      ≤ (rscTrialMeasure G p₂ p₃ t).real (rscAccept G S.card θ) := by
  have hsub : leEvent (xi G S) θ ⊆ rscAccept G S.card θ := by
    intro z hz
    obtain ⟨hxi, hle⟩ : xi G S z ≠ ⊤ ∧ (xi G S z).toReal ≤ θ := hz
    have hsubS : z.1 ∪ z.2 ⊆ S := by
      by_contra h
      apply hxi
      unfold xi
      rw [ite_eq_right h]
    have hxi' : xi G S z = (termCount G (z.1 ∪ z.2) : ℝ≥0∞) := by
      unfold xi
      rw [ite_eq_left hsubS]
    rw [hxi', ENNReal.toReal_natCast] at hle
    have hterm : termCount G (z.1 ∪ z.2) ≤ θ := by exact_mod_cast hle
    have hcard : (z.1 ∪ z.2).card ≤ S.card := card_le_card hsubS
    simp only [rscAccept, MLS.ExtYes, Set.mem_ofPred_eq]
    refine ⟨hcard, hterm, S \ (z.1 ∪ z.2), disjoint_sdiff, ?_, ?_⟩
    · rw [card_sdiff_of_subset hsubS]
    · rw [union_sdiff_of_subset hsubS]
      exact hS
  have hfin : ∀ A : Set (Finset V × Finset V), rscTrialMeasure G p₂ p₃ t A ≠ ⊤ := by
    intro A
    unfold rscTrialMeasure
    rw [Measure.finsetSum_apply]
    refine ENNReal.sum_ne_top.2 fun z _ => ?_
    rw [Measure.smul_apply, smul_eq_mul]
    exact ENNReal.mul_ne_top ENNReal.ofReal_ne_top (measure_ne_top _ _)
  exact measureReal_mono hsub (hfin _)

theorem rsc_trials_T2 (s θ : ℕ) (z : Finset V × Finset V) (hz : z ∈ rscAccept G s θ) :
    γc G ≤ s := by
  simp only [rscAccept, MLS.ExtYes, Set.mem_ofPred_eq] at hz
  obtain ⟨hcard, _, Y, hdisj, hYcard, hsol⟩ := hz
  have hmem : (z.1 ∪ z.2 ∪ Y).card ∈ {s | ∃ S, IsCDS G S ∧ S.card = s} :=
    ⟨z.1 ∪ z.2 ∪ Y, hsol, rfl⟩
  have h1 : γc G ≤ (z.1 ∪ z.2 ∪ Y).card := Nat.sInf_le hmem
  have hc : (z.1 ∪ z.2 ∪ Y).card = (z.1 ∪ z.2).card + Y.card :=
    card_union_of_disjoint hdisj
  omega

/-! ### Theorem RSC, probability part, conditional on prop:rsc-bound -/

/-- `ω = log ϱ`, `ϱ = (1 + y)/ê` with the constants of RSC. -/
noncomputable def rscOmega : ℝ := Real.logb 2 ((1 + 31/100) / (145729958 / 189014575))

theorem rscOmega_nonneg : 0 ≤ rscOmega := Real.logb_nonneg (by norm_num) (by norm_num)

theorem two_rpow_neg_rscOmega (n : ℕ) :
    (2:ℝ) ^ (-(rscOmega * n)) = ((145729958 / 189014575) / (1 + 31/100) : ℝ) ^ n := by
  unfold rscOmega
  rw [Real.rpow_neg (by norm_num), Real.rpow_mul (by norm_num),
    Real.rpow_logb (by norm_num) (by norm_num) (by norm_num), Real.rpow_natCast,
    ← inv_pow, inv_div]

-- Proof of thm:rsc given prop:rsc-bound (the hypothesis `hbound`), probability part

/-- Theorem RSC, probability part, conditional on `prop:rsc-bound`: the hypothesis `hbound` is
the statement of `prop:rsc-bound`, taken as an explicit assumption. -/
theorem rsc_success_of_bound (hG : G.Connected) (κ : ℝ) (hκ : 0 < κ)
    (Θ : ℕ → ℕ)
    (hΘ : ∀ s, 1 ≤ s → s ≤ Fintype.card V →
      rscOmega * Fintype.card V + Real.logb 2 2 + 1 ≤ Θ s)
    (m : ℕ → ℕ → ℕ → ℕ)
    (hm : ∀ s t θ, 1 ≤ s → s ≤ Fintype.card V → t ≤ s → θ ≤ Θ s →
      Mcount (Fintype.card V) rscOmega 2 κ (Θ s) θ ≤ m s t θ)
    (hbound : ∀ S : Finset V, IsCDS G S → S.card = γc G →
      (0.6060 : ℝ) * (145729958 / 189014575 : ℝ) ^ Fintype.card V
        ≤ Wcl G (7/100) (77/1000) S (31/100)) :
    (∀ o : CdsOutcome (Fintype.card V) (fun _ _ _ => Finset V × Finset V) Θ m,
        γc G ≤ cdsOutput (Fintype.card V) (fun s _ θ => rscAccept G s θ) o) ∧
    1 - Real.exp (-κ)
      ≤ (cdsMeasure (Fintype.card V) (fun _ t _ => rscTrialMeasure G (7/100) (77/1000) t)
          Θ m).real
          {o | cdsOutput (Fintype.card V) (fun s _ θ => rscAccept G s θ) o = γc G} := by
  have hp : (0:ℝ) ≤ 7/100 ∧ (7/100:ℝ) ≤ 77/1000 ∧ (77/1000:ℝ) ≤ 1 := by norm_num
  -- a minimum CDS
  have hne : {s | ∃ S, IsCDS G S ∧ S.card = s}.Nonempty := ⟨_, _, isCDS_univ G hG, rfl⟩
  obtain ⟨S0, hS0, hS0c⟩ := Nat.sInf_mem hne
  change S0.card = γc G at hS0c
  have hγn : γc G ≤ Fintype.card V := hS0c ▸ card_le_univ S0
  -- the moment condition, from prop:rsc-bound and lem:rsc-trials (b)
  obtain ⟨t, ht, hW⟩ := rsc_trials_W G (7/100) (77/1000) hp S0 (31/100) (by norm_num)
  have hb := hbound S0 hS0 hS0c
  set E := ∫ z, twoPowNeg (xi G S0 z) ∂(rscTrialMeasure G (7/100) (77/1000) t)
  have hmom : (2:ℝ) ^ (-(rscOmega * Fintype.card V)) / 2 ≤ E := by
    rw [two_rpow_neg_rscOmega, div_pow]
    have hpos : (0:ℝ) < (1 + 31/100) ^ Fintype.card V := by positivity
    have h1 : (0.6060 : ℝ) * (145729958 / 189014575 : ℝ) ^ Fintype.card V
        ≤ (1 + 31/100) ^ Fintype.card V * E := hb.trans hW
    have hc0 : (0:ℝ) ≤ (145729958 / 189014575 : ℝ) ^ Fintype.card V := by positivity
    rw [div_div, div_le_iff₀ (by positivity)]
    nlinarith
  refine cds_budgeted G hG (Ω := fun _ _ _ => Finset V × Finset V)
    (fun _ t _ => rscTrialMeasure G (7/100) (77/1000) t)
    (fun s t θ _ hs ht => isProbabilityMeasure_rscTrialMeasure G _ _ hp t (by omega))
    (fun s _ θ => rscAccept G s θ) (fun _ _ _ _ _ _ => MeasurableSet.of_discrete)
    (fun s _ θ _ _ _ z hz => rsc_trials_T2 G s θ z hz)
    rscOmega 2 κ rscOmega_nonneg (by norm_num) hκ Θ hΘ m hm
    (Ξ := fun _ => Finset V × Finset V)
    (fun t => rscTrialMeasure G (7/100) (77/1000) t)
    (fun t ht => isProbabilityMeasure_rscTrialMeasure G _ _ hp t (by omega))
    (fun _ => xi G S0) (fun _ _ => measurable_of_countable _)
    (fun t θ _ => hS0c ▸ rsc_trials_T3 G _ _ hp S0 hS0 t θ)
    ⟨t, hS0c ▸ ht, hmom⟩

/-! ### Representation checks -/

/-- `leEvent` at a natural threshold is the event `{ξ ≤ θ}`. -/
theorem leEvent_natCast_eq {Ξ : Type*} (ξ : Ξ → ℝ≥0∞) (θ : ℕ) : leEvent ξ θ = {x | ξ x ≤ θ} := by
  ext x
  simp only [leEvent, Set.mem_ofPred_eq]
  constructor
  · rintro ⟨h1, h2⟩
    rw [← ENNReal.toReal_le_toReal h1 (ENNReal.natCast_ne_top θ), ENNReal.toReal_natCast]
    exact h2
  · intro h
    have h1 : ξ x ≠ ⊤ := ne_top_of_le_ne_top (ENNReal.natCast_ne_top θ) h
    refine ⟨h1, ?_⟩
    rw [← ENNReal.toReal_natCast]
    exact ENNReal.toReal_mono (ENNReal.natCast_ne_top θ) h

/-- `firstAccepted` returns `n` when no size is accepted. -/
theorem firstAccepted_of_none (n : ℕ) (acc : ℕ → Prop) (h : ∀ s, ¬ acc s) : firstAccepted n acc = n := by
  classical
  unfold firstAccepted
  rw [dite_eq_right]
  rintro ⟨s, hs⟩
  exact h s (mem_filter.1 hs).2

/-- The closure of `X' = {a, c}` on the path `a – b – c` is `{b}`, included with probability `p₂`. -/
theorem cand_path3 : cand (SimpleGraph.pathGraph 3) ({0, 2} : Finset (Fin 3)) = {1} := by
  decide

theorem closureProb_path3 (p₂ p₃ : ℝ) :
    closureProb (SimpleGraph.pathGraph 3) p₂ p₃ ({0, 2} : Finset (Fin 3)) {1} = p₂ ∧
    closureProb (SimpleGraph.pathGraph 3) p₂ p₃ ({0, 2} : Finset (Fin 3)) ∅ = 1 - p₂ := by
  have hc : cand (SimpleGraph.pathGraph 3) ({0, 2} : Finset (Fin 3)) = {1} := by decide
  have hk : ((SimpleGraph.pathGraph 3).neighborFinset 1 ∩ ({0, 2} : Finset (Fin 3))).card = 2 := by
    decide
  simp [closureProb, hc, inclProb, pk, hk]

/-- Inhabitation: all hypotheses of `budgeted_success` hold at once for a trivial instance
(one index, a trial that always accepts, `ξ ≡ 0`, and the parameters of `MLS`). -/
theorem budgeted_success_inhabited : 1 - Real.exp (-1) ≤
    (budgetMeasure (ι := Unit) (Ω := fun _ _ => Unit) (fun _ _ => Measure.dirac ())
      (MLS.cap 0 0 1) (fun _ θ => MLS.trials 0 0 1 1 θ)).real
      {o | BAccepts (fun _ _ => Set.univ) o} := by
  refine budgeted_success (ι := Unit) (Ω := fun _ _ => Unit) (fun _ _ => Measure.dirac ())
    (fun _ _ => Set.univ) (fun _ _ => MeasurableSet.univ) (Ξ := fun _ => Unit)
    (fun _ => Measure.dirac ()) (fun _ _ => 0) (fun _ => measurable_const)
    (fun _ _ => ?_) 0 0 1 1 le_rfl le_rfl one_pos (MLS.cap 0 0 1)
    (params_admissible Unit 0 0 1 1 le_rfl le_rfl one_pos).1 _
    (fun i θ hθ => ((params_admissible Unit 0 0 1 1 le_rfl le_rfl one_pos).2.2 i θ hθ).1) ⟨(), ?_⟩
  · exact measureReal_mono (Set.subset_univ _)
  · simp [twoPowNeg]

end MaxLeafFormal.RSCTrials