OAI/NumberTheory/DirichletL/Detector/LowRowMellin.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.lowAdditiveCoefficient line 13
2. def OAI.SevenEighths.ProbePhysical.lowPhysicalScale line 23
3. def OAI.SevenEighths.ProbePhysical.lowRowMellinIntegrand line 25
4. lemma OAI.SevenEighths.ProbePhysical.calibration_elementNorm_pos line 31
5. lemma OAI.SevenEighths.ProbePhysical.lowPhysicalScale_pos line 36
6. lemma OAI.SevenEighths.ProbePhysical.lowAdditiveCoefficient_outer_zero line 39
7. lemma OAI.SevenEighths.ProbePhysical.lowRowMellinIntegrand_nonzero_form line 45
8. lemma OAI.SevenEighths.ProbePhysical.lowRowMellinIntegrand_integrable line 66
9. theorem OAI.SevenEighths.ProbePhysical.physicalRowWeight_low_mellin line 92
10. lemma OAI.SevenEighths.ProbePhysical.lowAdditiveCoefficient_height line 136
11. lemma OAI.SevenEighths.ProbePhysical.lowAdditiveCoefficient_height_norm line 151
12. def OAI.SevenEighths.ProbePhysical.lowArithmeticCoefficient line 159
13. lemma OAI.SevenEighths.ProbePhysical.calibration_residue_inverse_norm line 164
14. lemma OAI.SevenEighths.ProbePhysical.lowArithmeticCoefficient_norm line 172
15. lemma OAI.SevenEighths.ProbePhysical.lowArithmeticCoefficient_source_norm line 183
16. lemma OAI.SevenEighths.ProbePhysical.lowAdditiveCoefficient_eq line 187