OAI/Combinatorics/ContingencyTables/Rooted/RootedSlowConcentration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedSlowConcentration.constant_nonnegative line 21
2. lemma OAI.ContingencyTables.RootedSlowConcentration.target_mean line 26
3. lemma OAI.ContingencyTables.RootedSlowConcentration.target_pi line 33
4. theorem OAI.ContingencyTables.RootedSlowConcentration.bounded_MSE line 41

   Source documentation

   Mean-square concentration of the real chain implemented by the actual padded proposal.

   theorem bounded_MSE (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ) (hp : 0<Fintype.card (Labels A))
       (w : Pair A → Pair A → ℚ) (hw : ∀ p q,0<w p q)
       (hgood : GoodMultipliers pairs (weight A R j) (fun p q => (w p q:ℝ)))
       (o : PhaseObservables (pairs : List (Pair A)))
       (nu : State A → ℝ)
       (hwarm : ∀ S,nu S≤(10*(Fintype.card (Labels A):ℝ)^2)*
         chainWeight pairs (fun p q => (w p q:ℝ)) (weight A R j) S.val/
           chainTotal pairs (fun p q => (w p q:ℝ)) (weight A R j))
       (N : ℕ) (hN : 0<N) :
       let D := targetChain A R j hp w hw
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection

5. theorem OAI.ContingencyTables.RootedSlowConcentration.phase_failure line 104

   Source documentation

   The full collection of phase observables obeys the source union bound for the actual dyadic holding chain.

   theorem phase_failure (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ) (hp : 0<Fintype.card (Labels A))
       (w : Pair A → Pair A → ℚ) (hw : ∀ p q,0<w p q)
       (hgood : GoodMultipliers pairs (weight A R j) (fun p q => (w p q:ℝ)))
       (nu : State A → ℝ) (hnu : ∀ S,0≤nu S)
       (hwarm : ∀ S,nu S≤(10*(Fintype.card (Labels A):ℝ)^2)*
         chainWeight pairs (fun p q => (w p q:ℝ)) (weight A R j) S.val/
           chainTotal pairs (fun p q => (w p q:ℝ)) (weight A R j))
       (N : ℕ) (hN : 0<N) (eta : ℝ) (heta : 0<eta) :
       let D := targetChain A R j hp w hw
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection