OAI/Combinatorics/ContingencyTables/Transport/FiniteChainSlowdown.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FiniteChainSlowdown.slow line 16
2. lemma OAI.ContingencyTables.FiniteChainSlowdown.stationary line 40
3. lemma OAI.ContingencyTables.FiniteChainSlowdown.mean line 43
4. lemma OAI.ContingencyTables.FiniteChainSlowdown.variance line 46
5. theorem OAI.ContingencyTables.FiniteChainSlowdown.energy line 51

   Source documentation

   Every off-diagonal move and the Dirichlet energy are scaled by the same holding factor. No irreducibility or nonzero denominator is needed.

   theorem energy (C : FiniteChain X) (a : ℝ) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (f : X → ℝ) :
       (slow C a ha0 ha1).energy f=a*C.energy f := by
   …

   Mentions: OAI.ContingencyTables.FiniteChainSlowdown.slow

6. theorem OAI.ContingencyTables.FiniteChainSlowdown.variance_bound line 72

   Source documentation

   A holding factor at least one half increases every applicable variance/energy bound by at most two, including bounds restricted to the specific observables used by the counting algorithm.

   theorem variance_bound (C : FiniteChain X) (a : ℝ) (ha0 : 0 ≤ a) (ha1 : a ≤ 1)
       (ha : 1/2 ≤ a) (K : ℝ) (hK : 0 ≤ K) (f : X → ℝ)
       (h : C.variance f ≤ K*C.energy f) :
       (slow C a ha0 ha1).variance f ≤ (2*K)*(slow C a ha0 ha1).energy f := by
   …

   Mentions: OAI.ContingencyTables.FiniteChainSlowdown.slow, OAI.ContingencyTables.FiniteChainSlowdown.variance, OAI.ContingencyTables.FiniteChainSlowdown.energy