OAI/NumberTheory/DirichletL/Hecke/DetectorDyadicGeometry.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.HeckeDetectorDyadicGeometry.uniform_power_allowanceline 11 - lemma
OAI.SevenEighths.HeckeDetectorDyadicGeometry.uniform_scale_thresholdline 22 - lemma
OAI.SevenEighths.HeckeDetectorDyadicGeometry.uniform_zero_heightline 28 - lemma
OAI.SevenEighths.HeckeDetectorDyadicGeometry.uniform_height_budgetline 36 - lemma
OAI.SevenEighths.HeckeDetectorDyadicGeometry.uniform_fourier_allowanceline 60