OAI/Probability/CriticalPercolation/Clusters/HitValue.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.ClusterColumns.hitValue line 17
2. def OAI.CriticalPercolation.ClusterColumns.jointHitValue line 18
3. lemma OAI.CriticalPercolation.ClusterColumns.hitValue_nonneg line 21
4. lemma OAI.CriticalPercolation.ClusterColumns.hitValue_le_one line 22
5. lemma OAI.CriticalPercolation.ClusterColumns.hitValue_monotone line 23
6. lemma OAI.CriticalPercolation.ClusterColumns.jointHitValue_nonneg line 32
7. lemma OAI.CriticalPercolation.ClusterColumns.jointHitValue_monotone line 34
8. lemma OAI.CriticalPercolation.ClusterColumns.jointHitValue_eq_hitValue line 44
9. lemma OAI.CriticalPercolation.ClusterColumns.component_inter_nonempty_iff line 47