MaxLeafFormal.RSCHeadline

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

Statements of the paper formalised here: Theorem 8.1.

import MaxLeafFormal.RSCCompose
import MaxLeafFormal.RSCFinal

/-! The success part of thm:rsc for the certificate `RSCFinal.certZ` of prop:rsc-cert, with no data
hypotheses. A separate build target, not imported by `MaxLeafFormal.lean`. It inherits the trust of
`RSCFinal`: `native_decide` in the generated shard theorems. -/

namespace MaxLeafFormal.RSCHeadline
open MaxLeafFormal.CDS (γc)
open MaxLeafFormal.Budget (CdsOutcome cdsMeasure cdsOutput Mcount)

/-- thm:rsc, success part, with the certificate of prop:rsc-cert: no data hypotheses. -/
theorem rsc_success {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.Connected) (κ : ℝ) (hκ : 0 < κ)
    (Θ : ℕ → ℕ)
    (hΘ : ∀ s, 1 ≤ s → s ≤ Fintype.card V →
      RSCTrials.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) RSCTrials.rscOmega 2 κ (Θ s) θ ≤ m s t θ) :
    (∀ o : CdsOutcome (Fintype.card V) (fun _ _ _ => Finset V × Finset V) Θ m,
        γc G ≤ cdsOutput (Fintype.card V) (fun s _ θ => RSCTrials.rscAccept G s θ) o) ∧
    1 - Real.exp (-κ)
      ≤ (cdsMeasure (Fintype.card V)
          (fun _ t _ => RSCTrials.rscTrialMeasure G (7/100) (77/1000) t) Θ m).real
          {o | cdsOutput (Fintype.card V) (fun s _ θ => RSCTrials.rscAccept G s θ) o = γc G} :=
  RSCCompose.rsc_success_of_data RSCFinal.certZ RSCFinal.certZ_nonempty RSCFinal.certZ_nonneg
    RSCFinal.certZ_C1 RSCFinal.certZ_C2 RSCFinal.certZ_C4 RSCFinal.certZ_C5 RSCFinal.certZ_cZ
    G hG κ hκ Θ hΘ m hm

end MaxLeafFormal.RSCHeadline
Back to top