OAI/Combinatorics/ContingencyTables/Transport/WarmKernelIteration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.WarmKernelIteration.power_distance line 17

   Source documentation

   At every replacement step the reference distribution remains warm. No warmness assumption is imposed on the implemented distribution.

   theorem power_distance (C : FiniteChain X) (K : FiniteKernel X X)
       (nu : X → ℝ) (hnu : ∀ x,0≤nu x) (hmass : ∑ x,nu x≤1)
       (U e : ℝ) (hwarm : ∀ x,nu x≤U*C.π x)
       (hstep : ∀ rho : X → ℝ,(∀ x,0≤rho x) → (∑ x,rho x≤1) →
         (∀ x,rho x≤U*C.π x) → distance (K.push rho) (C.kernel.push rho)≤e)
       (n : ℕ) :
       distance ((K.power n).push nu) ((C.kernel.power n).push nu)≤n*e := by
   …

2. theorem OAI.ContingencyTables.WarmKernelIteration.mixing_distance line 45

   Source documentation

   A uniform relative row estimate gives the corresponding total variation estimate for every normalized incoming distribution.

   theorem mixing_distance (C : FiniteChain X) (nu : X → ℝ)
       (hnu : ∀ x,0≤nu x) (hmass : ∑ x,nu x=1) (n : ℕ) (e : ℝ)
       (hmix : ∀ x y,|((C.kernel.power n).P x y)/C.π y-1|≤e) :
       distance ((C.kernel.power n).push nu) C.π≤e/2 := by
   …