OAI/MathematicalPhysics/CriticalSK/Mixing.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.kernel_l1_contraction line 19
  2. lemma OAI.CriticalSK.kernel_row_l1_le_two line 41
  3. lemma OAI.CriticalSK.strictly_positive_kernel_mixes line 52
  4. lemma OAI.CriticalSK.discreteKernel_pos_of_sameExcept line 106
  5. lemma OAI.CriticalSK.discreteKernel_power_pos line 117
  6. lemma OAI.CriticalSK.discrete_mixing_set_nonempty line 140
  7. lemma OAI.CriticalSK.continuousKernel_add line 149
  8. lemma OAI.CriticalSK.continuousKernel_nat line 154
  9. lemma OAI.CriticalSK.continuousKernel_one_pos line 159
  10. lemma OAI.CriticalSK.continuous_mixing_set_nonempty line 170
  11. lemma OAI.CriticalSK.continuousDistance_antitone line 187
  12. lemma OAI.CriticalSK.discreteDistance_antitone line 201
  13. lemma OAI.CriticalSK.continuousMixingTime_lower line 216
  14. lemma OAI.CriticalSK.discreteMixingTime_lower line 229
  15. lemma OAI.CriticalSK.event_probability_one_of_error_zero line 243
  16. lemma OAI.CriticalSK.continuousMixingTime_lower_limit line 258
  17. lemma OAI.CriticalSK.discreteMixingTime_lower_limit line 271
  18. theorem OAI.CriticalSK.critical_mixing_lower_bounds line 284

    Distinct definitions of this name: ComparatorChallenges/CriticalSK.lean:138 (different declaration text). Qualify references as OAI.CriticalSK.critical_mixing_lower_bounds@path.