OAI/NumberTheory/DirichletL/Detector/LowNominalGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.lowUnselectedLength line 12
2. def OAI.SevenEighths.ProbePhysical.lowSelectedLength line 14
3. lemma OAI.SevenEighths.ProbePhysical.lowLength_sum line 16
4. lemma OAI.SevenEighths.ProbePhysical.lowLength_bounds line 21
5. lemma OAI.SevenEighths.ProbePhysical.lowUnselectedProduct_norm_lower line 30
6. lemma OAI.SevenEighths.ProbePhysical.originalPool_element_lower line 48
7. lemma OAI.SevenEighths.ProbePhysical.lowPhysicalScale_source line 55
8. lemma OAI.SevenEighths.ProbePhysical.lowPhysicalScale_nominal_bound line 63
9. lemma OAI.SevenEighths.ProbePhysical.lowSelectedScale_product line 82
10. lemma OAI.SevenEighths.ProbePhysical.lowSelectedCaps_product line 87