OAI/NumberTheory/DirichletL/Detector/FiniteProductBounds.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeFiniteProductBounds.localMultiplier line 15
  2. def OAI.SevenEighths.ProbeFiniteProductBounds.selectedMultiplier line 23
  3. def OAI.SevenEighths.ProbeFiniteProductBounds.slotMultiplier line 26
  4. theorem OAI.SevenEighths.ProbeFiniteProductBounds.correction_lower_bound line 30
  5. theorem OAI.SevenEighths.ProbeFiniteProductBounds.correction_ne_zero line 40
  6. theorem OAI.SevenEighths.ProbeFiniteProductBounds.correction_inverse_bound line 47
  7. lemma OAI.SevenEighths.ProbeFiniteProductBounds.marked_differentiableAt_w line 55
  8. lemma OAI.SevenEighths.ProbeFiniteProductBounds.marked_differentiableAt_z line 68
  9. theorem OAI.SevenEighths.ProbeFiniteProductBounds.local_analytic_w line 82
  10. theorem OAI.SevenEighths.ProbeFiniteProductBounds.local_analytic_z line 107
  11. lemma OAI.SevenEighths.ProbeFiniteProductBounds.marked_bound line 132
  12. lemma OAI.SevenEighths.ProbeFiniteProductBounds.replacement_bound line 169
  13. def OAI.SevenEighths.ProbeFiniteProductBounds.localBound line 200
  14. lemma OAI.SevenEighths.ProbeFiniteProductBounds.localBound_nonneg line 203
  15. theorem OAI.SevenEighths.ProbeFiniteProductBounds.local_norm_bound line 207
  16. def OAI.SevenEighths.ProbeFiniteProductBounds.selectedBound line 246
  17. def OAI.SevenEighths.ProbeFiniteProductBounds.slotBound line 249
  18. lemma OAI.SevenEighths.ProbeFiniteProductBounds.selectedBound_nonneg line 253
  19. lemma OAI.SevenEighths.ProbeFiniteProductBounds.slotBound_nonneg line 256
  20. theorem OAI.SevenEighths.ProbeFiniteProductBounds.selected_analytic_w line 262
  21. theorem OAI.SevenEighths.ProbeFiniteProductBounds.selected_analytic_z line 268
  22. theorem OAI.SevenEighths.ProbeFiniteProductBounds.slot_analytic_w line 274
  23. theorem OAI.SevenEighths.ProbeFiniteProductBounds.slot_analytic_z line 285
  24. theorem OAI.SevenEighths.ProbeFiniteProductBounds.selected_norm_bound line 296
  25. theorem OAI.SevenEighths.ProbeFiniteProductBounds.slot_norm_bound line 304
  26. lemma OAI.SevenEighths.ProbeFiniteProductBounds.global_norm_bound line 319
  27. theorem OAI.SevenEighths.ProbeFiniteProductBounds.combined_slot_analytic_w line 327
  28. theorem OAI.SevenEighths.ProbeFiniteProductBounds.combined_slot_analytic_z line 335
  29. theorem OAI.SevenEighths.ProbeFiniteProductBounds.combined_slot_bound line 343
  30. theorem OAI.SevenEighths.ProbeFiniteProductBounds.selected_initial_identity line 353
  31. theorem OAI.SevenEighths.ProbeFiniteProductBounds.source_w_boundary line 368
  32. theorem OAI.SevenEighths.ProbeFiniteProductBounds.source_z_boundary line 390
  33. theorem OAI.SevenEighths.ProbeFiniteProductBounds.source_multiplier_differentiable_w line 411
  34. theorem OAI.SevenEighths.ProbeFiniteProductBounds.source_multiplier_differentiable_z line 432
  35. theorem OAI.SevenEighths.ProbeFiniteProductBounds.source_w_shift line 455
  36. theorem OAI.SevenEighths.ProbeFiniteProductBounds.source_residue_z_shift line 474
  37. theorem OAI.SevenEighths.ProbeFiniteProductBounds.local_eq_regionSlot line 493
  38. def OAI.SevenEighths.ProbeFiniteProductBounds.windowMultiplier line 500
  39. theorem OAI.SevenEighths.ProbeFiniteProductBounds.window_at_residue line 504
  40. theorem OAI.SevenEighths.ProbeFiniteProductBounds.slot_norm_bound_sharp line 525
  41. theorem OAI.SevenEighths.ProbeFiniteProductBounds.combined_slot_bound_sharp line 542
  42. theorem OAI.SevenEighths.ProbeFiniteProductBounds.slotMultiplier_empty line 555
  43. theorem OAI.SevenEighths.ProbeFiniteProductBounds.selected_as_slots line 559
  44. theorem OAI.SevenEighths.ProbeFiniteProductBounds.fixed_source_boundaries line 563
  45. lemma OAI.SevenEighths.ProbeFiniteProductBounds.boundary_mul_const line 588
  46. theorem OAI.SevenEighths.ProbeFiniteProductBounds.fixed_source_ordered_boundaries line 594
  47. theorem OAI.SevenEighths.ProbeFiniteProductBounds.uniform_closed_box_bound line 619