OAI/MathematicalPhysics/CriticalSK/ThresholdMixing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalSK.continuousKernel_nat_mul line 14
2. lemma OAI.CriticalSK.continuousDistance_iteration line 22
3. lemma OAI.CriticalSK.discreteDistance_iteration line 34
4. lemma OAI.CriticalSK.continuousMixingAt_set_nonempty line 47
5. lemma OAI.CriticalSK.discreteMixingAt_set_nonempty line 54
6. lemma OAI.CriticalSK.continuousMixingAt_quarter_comparison line 60
7. lemma OAI.CriticalSK.discreteMixingAt_quarter_comparison line 74
8. lemma OAI.CriticalSK.exists_threshold_amplification line 85
9. theorem OAI.CriticalSK.critical_mixing_lower_bounds_at line 94