OAI/NumberTheory/DirichletL/Detector/LowSourceScales.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.ProbePhysical.source_scale_ratioline 10 - lemma
OAI.SevenEighths.ProbePhysical.source_scale_squareline 15 - lemma
OAI.SevenEighths.ProbePhysical.source_compensated_scale_admissibleline 20 - lemma
OAI.SevenEighths.ProbePhysical.source_compensated_gram_scaleline 38 - lemma
OAI.SevenEighths.ProbePhysical.source_compensated_gram_sqrtline 62 - lemma
OAI.SevenEighths.ProbePhysical.lowGramFactor_source_boundline 72 - lemma
OAI.SevenEighths.ProbePhysical.eventually_compensated_source_scalesline 79