OAI/Probability/CriticalPercolation/Modular/InputMass.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.QueryTree.inputMass line 25
2. def OAI.CriticalPercolation.QueryTree.inputNumerator line 27
3. def OAI.CriticalPercolation.QueryTree.bitValue line 29
4. lemma OAI.CriticalPercolation.QueryTree.inputMass_eq_sum line 31
5. lemma OAI.CriticalPercolation.QueryTree.inputNumerator_eq_sum line 34
6. lemma OAI.CriticalPercolation.QueryTree.inputMass_nonneg line 43
7. lemma OAI.CriticalPercolation.QueryTree.inputNumerator_eq_zero line 49
8. lemma OAI.CriticalPercolation.QueryTree.charge_eq_input_sum line 65
9. lemma OAI.CriticalPercolation.MarkedTree.pooled_inputMass line 77
10. lemma OAI.CriticalPercolation.MarkedTree.pooled_inputNumerator line 84
11. lemma OAI.CriticalPercolation.OrderedQuery.fresh_weighted_input line 98
12. lemma OAI.CriticalPercolation.OrderedQuery.weighted_pooled_numerator line 124
13. lemma OAI.CriticalPercolation.OrderedQuery.pooled_mass_le line 139
14. lemma OAI.CriticalPercolation.OrderedQuery.weighted_pooled_mass_le line 150