OAI/NumberTheory/Jacobsthal/Paths/ActualSampleWitness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosInverseCounts.NodeBadEdge line 13
2. def OAI.Erdos970.ErdosInverseCounts.WitnessingBadEdge line 17
3. theorem OAI.Erdos970.ErdosInverseCounts.modulusCount_child_mass line 20
4. theorem OAI.Erdos970.ErdosInverseCounts.nodeBadEdge_iff_tree_mass line 27
5. theorem OAI.Erdos970.ErdosInverseCounts.literal_witnessing_bad_edge line 35
6. def OAI.Erdos970.ErdosInverseSampleCost.actualWitness line 52
7. theorem OAI.Erdos970.ErdosInverseSampleCost.selected_actual_witness line 57
8. theorem OAI.Erdos970.ErdosInverseSampleCost.actualWitness_iff_counts line 73
9. theorem OAI.Erdos970.ErdosInverseSampleCost.selected_actual_witness_positive line 82