OAI/NumberTheory/DirichletL/Detector/FiniteProductX.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbeFiniteProductX.marked_differentiableAt_x line 14
  2. theorem OAI.SevenEighths.ProbeFiniteProductX.local_analytic_x line 29
  3. theorem OAI.SevenEighths.ProbeFiniteProductX.selected_analytic_x line 54
  4. theorem OAI.SevenEighths.ProbeFiniteProductX.slot_analytic_x line 60
  5. theorem OAI.SevenEighths.ProbeFiniteProductX.window_analytic_x line 71
  6. theorem OAI.SevenEighths.ProbeFiniteProductX.combined_selected_analytic_x line 78
  7. theorem OAI.SevenEighths.ProbeFiniteProductX.combined_slot_analytic_x line 86
  8. def OAI.SevenEighths.ProbeFiniteProductX.continuedSourceMultiplier line 95
  9. theorem OAI.SevenEighths.ProbeFiniteProductX.continued_source_analytic_x line 104
  10. theorem OAI.SevenEighths.ProbeFiniteProductX.continued_source_eq_raw line 123
  11. theorem OAI.SevenEighths.ProbeFiniteProductX.continued_source_ae_raw line 133
  12. theorem OAI.SevenEighths.ProbeFiniteProductX.source_analytic_x_off_one line 147
  13. theorem OAI.SevenEighths.ProbeFiniteProductX.continued_source_differentiable_strip line 170
  14. theorem OAI.SevenEighths.ProbeFiniteProductX.continued_source_principal_one line 182