OAI/Combinatorics/ContingencyTables/Counting/CompanionConcentration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.CompanionConcentration.observable_constant_nonnegative line 16
2. lemma OAI.ContingencyTables.CompanionConcentration.bounded_variance_factor line 21
3. lemma OAI.ContingencyTables.CompanionConcentration.pairs_ne_nil line 27
4. lemma OAI.ContingencyTables.CompanionConcentration.actual_degree line 32
5. lemma OAI.ContingencyTables.CompanionConcentration.square_width_one_le line 38
6. theorem OAI.ContingencyTables.CompanionConcentration.bounded_MSE line 44

   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) (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 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 j) S.val/chainTotal pairs w (weight A j))
       (N : ℕ) (hN : 0< N) :
       let C := metropolisChain pairs PairedLabels.fresh (pairs_ne_nil A hp) PairedLabels.cover w
   …

   Mentions: OAI.ContingencyTables.PairedLabels.fresh, OAI.ContingencyTables.CompanionConcentration.pairs_ne_nil, OAI.ContingencyTables.PairedLabels.cover

7. theorem OAI.ContingencyTables.CompanionConcentration.phase_failure line 92

   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) (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 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 j) S.val/chainTotal pairs w (weight A 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.PairedLabels.fresh, OAI.ContingencyTables.CompanionConcentration.pairs_ne_nil, OAI.ContingencyTables.PairedLabels.cover