OAI/NumberTheory/Jacobsthal/Estimates/ReferenceLocalResidual.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.ReferenceLocalResidual.nodeBenchmark line 20
2. def OAI.Erdos970.NumberTheoryLean.ReferenceLocalResidual.sourceResidual line 23
3. def OAI.Erdos970.NumberTheoryLean.ReferenceLocalResidual.sourceInsertion line 29
4. theorem OAI.Erdos970.NumberTheoryLean.ReferenceLocalResidual.admitted_child_benchmark line 34
5. theorem OAI.Erdos970.NumberTheoryLean.ReferenceLocalResidual.omitted_child_benchmark line 54
6. theorem OAI.Erdos970.NumberTheoryLean.ReferenceLocalResidual.admitted_benchmark_sum line 65
7. theorem OAI.Erdos970.NumberTheoryLean.ReferenceLocalResidual.source_insertion_identity line 77