OAI/NumberTheory/DirichletL/Detector/RaySlots.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeRaySlots.pool line 14
2. theorem OAI.SevenEighths.ProbeRaySlots.mem_pool line 17
3. theorem OAI.SevenEighths.ProbeRaySlots.pool_norm_bounds line 23
4. lemma OAI.SevenEighths.ProbeRaySlots.pool_sum line 29
5. theorem OAI.SevenEighths.ProbeRaySlots.pool_mass_eq_deleted line 42
6. theorem OAI.SevenEighths.ProbeRaySlots.ray_pool_mass_eventually_positive line 57
7. theorem OAI.SevenEighths.ProbeRaySlots.ray_pool_mass_eventually_lower_bound line 68