OAI/NumberTheory/DirichletL/Detector/GaussianCompletedSlots.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.ProbePhysical.correctedSummand_normTwistedline 14 - lemma
OAI.SevenEighths.ProbePhysical.correctedSummand_fixed_finiteline 23 - lemma
OAI.SevenEighths.ProbePhysical.gaussian_slot_integrableline 30 - lemma
OAI.SevenEighths.ProbePhysical.gaussian_selected_summandline 47 - lemma
OAI.SevenEighths.ProbePhysical.correctedSummand_gaussian_factorline 98 - lemma
OAI.SevenEighths.ProbePhysical.gaussian_selected_completed_integrableline 107 - theorem
OAI.SevenEighths.ProbePhysical.gaussian_selected_completedline 128