OAI/MathematicalPhysics/Heisenberg/CrossingTails.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Heisenberg.Geometry.scaled_ball_card line 11
2. theorem OAI.Heisenberg.Geometry.lattice_crossing_mass_bound line 20
3. lemma OAI.Heisenberg.SparseWitness.Crosses.mono_radius line 49
4. lemma OAI.Heisenberg.SparseWitness.event_mass_mono line 54
5. theorem OAI.Heisenberg.SparseWitness.stretched_tail_of_scales line 64
6. lemma OAI.Heisenberg.SparseWitness.exists_scale_exponent line 101
7. lemma OAI.Heisenberg.SparseWitness.sparse_of_card_le line 108
8. lemma OAI.Heisenberg.SparseWitness.countable_union_mass line 117
9. theorem OAI.Heisenberg.SparseWitness.bad_count_mass line 136
10. lemma OAI.Heisenberg.Stretched.exp_power_bound line 172
11. theorem OAI.Heisenberg.Stretched.exists_polynomial_envelope line 187
12. lemma OAI.Heisenberg.LatticeSum.radius_eq_norm line 203
13. lemma OAI.Heisenberg.LatticeSum.uniform_polynomial_sum line 214
14. theorem OAI.Heisenberg.LatticeSum.exp_tail_polynomial line 226