OAI/MathematicalPhysics/Heisenberg/SparseCrossings.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Heisenberg.SparseWitness.first_crossing line 15
2. theorem OAI.Heisenberg.SparseWitness.crossing_witness line 40
3. lemma OAI.Heisenberg.SparseWitness.geometric_scale_gap line 99
4. def OAI.Heisenberg.SparseWitness.candidates line 110
5. lemma OAI.Heisenberg.SparseWitness.mem_candidates_root line 114
6. lemma OAI.Heisenberg.SparseWitness.admissible_mem_candidates line 123
7. lemma OAI.Heisenberg.SparseWitness.card_candidates_le line 134
8. def OAI.Heisenberg.SparseWitness.assignmentBound line 156
9. lemma OAI.Heisenberg.SparseWitness.assignmentBound_formula line 160
10. lemma OAI.Heisenberg.SparseWitness.assignmentBound_le line 172
11. theorem OAI.Heisenberg.SparseWitness.geometric_candidates_count line 183
12. lemma OAI.Heisenberg.SparseWitness.Sparse.mono_constant line 195
13. def OAI.Heisenberg.SparseWitness.Crosses line 200
14. lemma OAI.Heisenberg.SparseWitness.finite_union_mass line 204
15. theorem OAI.Heisenberg.SparseWitness.crossing_mass_bound line 220