OAI/NumberTheory/DirichletL/Detector/CentralExponent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeCentralExponent.sourceExponent line 11
2. def OAI.SevenEighths.ProbeCentralExponent.relativeExponent line 15
3. lemma OAI.SevenEighths.ProbeCentralExponent.original_exponent_identity line 18
4. lemma OAI.SevenEighths.ProbeCentralExponent.frequency_slope_bounds line 23
5. lemma OAI.SevenEighths.ProbeCentralExponent.relative_extend line 28
6. lemma OAI.SevenEighths.ProbeCentralExponent.balanced_source_margin line 36
7. lemma OAI.SevenEighths.ProbeCentralExponent.high_source_margin line 53
8. lemma OAI.SevenEighths.ProbeCentralExponent.floor_source_margin line 66
9. lemma OAI.SevenEighths.ProbeCentralExponent.intermediate_source_margin line 75
10. def OAI.SevenEighths.ProbeCentralExponent.realLoss line 83
11. lemma OAI.SevenEighths.ProbeCentralExponent.realLoss_bound line 86
12. lemma OAI.SevenEighths.ProbeCentralExponent.physical_scale_identity line 94