OAI/NumberTheory/DirichletL/PrimeRows/MarkedNormalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeHighRowFamily.localNormalization line 11
2. def OAI.SevenEighths.ProbeHighRowFamily.markedLocalCorrection line 16
3. theorem OAI.SevenEighths.ProbeHighRowFamily.localCorrection_eq_normalization line 19
4. lemma OAI.SevenEighths.ProbeHighRowFamily.lift_outside_hasProd line 25
5. theorem OAI.SevenEighths.ProbeHighRowFamily.localNormalization_hasProd line 34
6. theorem OAI.SevenEighths.ProbeHighRowFamily.markedRowSeries_normalized line 48
7. theorem OAI.SevenEighths.ProbeHighRowFamily.markedRowSeries_original_L_factorization line 93