OAI/Combinatorics/ContingencyTables/Rooted/RootedConcentration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedConcentration.observable_constant_nonnegative line 20
2. lemma OAI.ContingencyTables.RootedConcentration.bounded_variance_factor line 25
3. theorem OAI.ContingencyTables.RootedConcentration.bounded_MSE line 33

   Source documentation

   Every actual phase observable has the source's mean-square bound 20 p² Kobs/N under a 10 p²-warm start of its original labelled chain.

   theorem bounded_MSE (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ) (hp : 0< Fintype.card (Labels A))
       (w : ((Labels A×Bool)×(Labels A×Bool)) → ((Labels A×Bool)×(Labels A×Bool)) → ℝ)
       (hw : GoodMultipliers pairs (weight A R j) w) (o : PhaseObservables (pairs : List ((Labels A×Bool)×(Labels A×Bool))))
       (nu : ChainIndex (pairs : List ((Labels A×Bool)×(Labels A×Bool))) → ℝ)
       (hwarm : ∀ S,nu S≤(10*(Fintype.card (Labels A):ℝ)^2)*
         chainWeight pairs w (weight A R j) S.val/chainTotal pairs w (weight A R j))
       (N : ℕ) (hN : 0< N) :
       let C := metropolisChain pairs PairedLabels.fresh (pairs_ne_nil A hp) PairedLabels.cover w
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PairedLabels.fresh, OAI.ContingencyTables.PairedLabels.cover

4. theorem OAI.ContingencyTables.RootedConcentration.phase_failure line 81

   Source documentation

   The source's finite union bound for all actual phase observables. The warm-start hypothesis is the restart endpoint condition, rather than an independent phase-concentration assumption.

   theorem phase_failure (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ) (hp : 0< Fintype.card (Labels A))
       (w : ((Labels A×Bool)×(Labels A×Bool)) → ((Labels A×Bool)×(Labels A×Bool)) → ℝ)
       (hw : GoodMultipliers pairs (weight A R j) w)
       (nu : ChainIndex (pairs : List ((Labels A×Bool)×(Labels A×Bool))) → ℝ)
       (hnu : ∀ S,0≤ nu S)
       (hwarm : ∀ S,nu S≤(10*(Fintype.card (Labels A):ℝ)^2)*
         chainWeight pairs w (weight A R j) S.val/chainTotal pairs w (weight A R j))
       (N : ℕ) (hN : 0< N) (eta : ℝ) (heta : 0< eta) :
       let C := metropolisChain pairs PairedLabels.fresh (pairs_ne_nil A hp) PairedLabels.cover w
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PairedLabels.fresh, OAI.ContingencyTables.PairedLabels.cover