OAI/NumberTheory/DirichletL/Detector/PrincipalContours.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbePrincipalContours.measurable_const_cpow line 19
  2. lemma OAI.SevenEighths.ProbePrincipalContours.ideal_correction_measurable line 24
  3. lemma OAI.SevenEighths.ProbePrincipalContours.global_correction_measurable line 35
  4. lemma OAI.SevenEighths.ProbePrincipalContours.local_multiplier_measurable line 42
  5. lemma OAI.SevenEighths.ProbePrincipalContours.slot_multiplier_measurable line 54
  6. def OAI.SevenEighths.ProbePrincipalContours.zBoxAmplitude line 65
  7. lemma OAI.SevenEighths.ProbePrincipalContours.zBoxAmplitude_nonneg line 68
  8. lemma OAI.SevenEighths.ProbePrincipalContours.fixed_principal_z_box_growth line 73
  9. lemma OAI.SevenEighths.ProbePrincipalContours.LFunction_eq_pole_quotient line 104
  10. lemma OAI.SevenEighths.ProbePrincipalContours.LFunction_vertical_continuous line 109
  11. lemma OAI.SevenEighths.ProbePrincipalContours.reciprocal_vertical_continuous line 118
  12. lemma OAI.SevenEighths.ProbePrincipalContours.LFunction_norm_le_of_poleRemoved line 125
  13. lemma OAI.SevenEighths.ProbePrincipalContours.fixed_principal_w_bound line 134
  14. lemma OAI.SevenEighths.ProbePrincipalContours.fixed_principal_z_bound line 147
  15. def OAI.SevenEighths.ProbePrincipalContours.arithmeticMultiplier line 162
  16. lemma OAI.SevenEighths.ProbePrincipalContours.arithmetic_profile_eq_source line 170
  17. lemma OAI.SevenEighths.ProbePrincipalContours.arithmetic_onLines_measurable line 179
  18. def OAI.SevenEighths.ProbePrincipalContours.boxScale line 208
  19. lemma OAI.SevenEighths.ProbePrincipalContours.boxScale_pos line 212
  20. def OAI.SevenEighths.ProbePrincipalContours.arithmeticAmplitude line 216
  21. lemma OAI.SevenEighths.ProbePrincipalContours.height_le_joint_s line 222
  22. lemma OAI.SevenEighths.ProbePrincipalContours.height_le_joint_z line 224
  23. lemma OAI.SevenEighths.ProbePrincipalContours.height_le_joint_w line 226
  24. lemma OAI.SevenEighths.ProbePrincipalContours.arithmetic_onLines_bound_of_gaps line 229
  25. lemma OAI.SevenEighths.ProbePrincipalContours.arithmetic_onLines_bound line 311
  26. theorem OAI.SevenEighths.ProbePrincipalContours.continued_source_joint_integrable line 329
  27. lemma OAI.SevenEighths.ProbePrincipalContours.outer_height_ne_zero_ae line 354
  28. lemma OAI.SevenEighths.ProbePrincipalContours.continued_joint_ae_raw line 359
  29. theorem OAI.SevenEighths.ProbePrincipalContours.source_joint_integrable line 372
  30. theorem OAI.SevenEighths.ProbePrincipalContours.source_joint_fubini line 391
  31. lemma OAI.SevenEighths.ProbePrincipalContours.arithmeticAmplitude_nonneg line 418
  32. theorem OAI.SevenEighths.ProbePrincipalContours.continued_source_slices line 430
  33. theorem OAI.SevenEighths.ProbePrincipalContours.source_w_leftover_outer_integrable line 465
  34. theorem OAI.SevenEighths.ProbePrincipalContours.source_z_boundary_any line 494
  35. theorem OAI.SevenEighths.ProbePrincipalContours.source_ordered_at_height line 519
  36. theorem OAI.SevenEighths.ProbePrincipalContours.source_ordered_ae line 567
  37. def OAI.SevenEighths.ProbePrincipalContours.residueArithmetic line 590
  38. lemma OAI.SevenEighths.ProbePrincipalContours.residue_profile_eq_source line 597
  39. lemma OAI.SevenEighths.ProbePrincipalContours.residue_arithmetic_measurable line 607
  40. def OAI.SevenEighths.ProbePrincipalContours.residueAmplitude line 632
  41. lemma OAI.SevenEighths.ProbePrincipalContours.residue_arithmetic_bound line 637
  42. lemma OAI.SevenEighths.ProbePrincipalContours.residueAmplitude_nonneg line 680
  43. theorem OAI.SevenEighths.ProbePrincipalContours.continued_residue_pair_integrable line 689
  44. theorem OAI.SevenEighths.ProbePrincipalContours.residue_pair_integrable line 715
  45. theorem OAI.SevenEighths.ProbePrincipalContours.source_iterated_integrable line 734
  46. theorem OAI.SevenEighths.ProbePrincipalContours.residue_iterated_integrable line 751
  47. theorem OAI.SevenEighths.ProbePrincipalContours.source_ordered_outer line 766
  48. theorem OAI.SevenEighths.ProbePrincipalContours.source_initial_ordered line 823
  49. theorem OAI.SevenEighths.ProbePrincipalContours.source_uniform_joint_tails line 844
  50. lemma OAI.SevenEighths.ProbePrincipalContours.LFunction_measurable line 897
  51. lemma OAI.SevenEighths.ProbePrincipalContours.arithmetic_onLines_measurable_all line 915
  52. def OAI.SevenEighths.ProbePrincipalContours.joinWGap line 936
  53. def OAI.SevenEighths.ProbePrincipalContours.joinZGap line 937
  54. lemma OAI.SevenEighths.ProbePrincipalContours.joinWGap_pos line 939
  55. lemma OAI.SevenEighths.ProbePrincipalContours.joinZGap_pos line 944
  56. lemma OAI.SevenEighths.ProbePrincipalContours.slice_w_gap line 950
  57. lemma OAI.SevenEighths.ProbePrincipalContours.slice_z_gap line 956
  58. theorem OAI.SevenEighths.ProbePrincipalContours.source_uniform_high_slices line 965
  59. theorem OAI.SevenEighths.ProbePrincipalContours.residue_uniform_moments line 1003
  60. def OAI.SevenEighths.ProbePrincipalContours.residueOutside line 1075
  61. lemma OAI.SevenEighths.ProbePrincipalContours.residueOutside_measurable line 1076
  62. theorem OAI.SevenEighths.ProbePrincipalContours.residue_uniform_tails line 1080
  63. lemma OAI.SevenEighths.ProbePrincipalContours.continued_high_slice_ae_raw line 1127
  64. lemma OAI.SevenEighths.ProbePrincipalContours.source_axis_gaps line 1155
  65. theorem OAI.SevenEighths.ProbePrincipalContours.raw_source_uniform_high_slices line 1163