OAI/NumberTheory/DirichletL/PrincipalSlotEstimate.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.PrincipalSlotEstimate.principalMarked line 12
  2. def OAI.SevenEighths.PrincipalSlotEstimate.principalReplacement line 16
  3. def OAI.SevenEighths.PrincipalSlotEstimate.principalSlot line 20
  4. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_correction_defect line 23
  5. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_correction_lower_bound line 38
  6. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_correction_ne_zero line 46
  7. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_correction_inverse_bound line 53
  8. theorem OAI.SevenEighths.PrincipalSlotEstimate.unit_phase_inverse line 61
  9. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_coord_cancellation line 65
  10. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_V line 74
  11. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_W line 77
  12. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_B_norm line 80
  13. theorem OAI.SevenEighths.PrincipalSlotEstimate.compensated_unit_error_bound line 84
  14. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_marked_error_bounds line 140
  15. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_replacement_error line 207
  16. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_slot_error line 233
  17. theorem OAI.SevenEighths.PrincipalSlotEstimate.actual_target_norm line 249
  18. theorem OAI.SevenEighths.PrincipalSlotEstimate.actual_principal_slot_error line 260
  19. theorem OAI.SevenEighths.PrincipalSlotEstimate.weighted_slot_error line 268
  20. theorem OAI.SevenEighths.PrincipalSlotEstimate.weighted_slot_relative_error line 285
  21. theorem OAI.SevenEighths.PrincipalSlotEstimate.weighted_principal_slot_error line 296
  22. theorem OAI.SevenEighths.PrincipalSlotEstimate.product_error line 310
  23. theorem OAI.SevenEighths.PrincipalSlotEstimate.product_error_linear line 333
  24. def OAI.SevenEighths.PrincipalSlotEstimate.principalScalar line 348
  25. theorem OAI.SevenEighths.PrincipalSlotEstimate.principalScalar_eq line 351
  26. theorem OAI.SevenEighths.PrincipalSlotEstimate.principalScalar_ne_zero line 359
  27. theorem OAI.SevenEighths.PrincipalSlotEstimate.fixed_product_relative_error line 366
  28. theorem OAI.SevenEighths.PrincipalSlotEstimate.fixed_product_relative_error_linear line 382
  29. theorem OAI.SevenEighths.PrincipalSlotEstimate.weighted_principal_product_error line 390
  30. def OAI.SevenEighths.PrincipalSlotEstimate.principalRawFactor line 406
  31. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_geometric_bounds line 409
  32. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_correction_eq_raw line 424
  33. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_raw_lower_bound line 435
  34. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_raw_ne_zero line 461
  35. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_slot_eq_raw line 468
  36. theorem OAI.SevenEighths.PrincipalSlotEstimate.principal_raw_slot_error line 487
  37. theorem OAI.SevenEighths.PrincipalSlotEstimate.weighted_principal_product_error_linear line 494
  38. def OAI.SevenEighths.PrincipalSlotEstimate.regionMarked line 509
  39. def OAI.SevenEighths.PrincipalSlotEstimate.regionReplacement line 513
  40. def OAI.SevenEighths.PrincipalSlotEstimate.regionSlot line 517
  41. def OAI.SevenEighths.PrincipalSlotEstimate.regionRawFactor line 520
  42. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_correction_defect line 523
  43. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_correction_lower_bound line 538
  44. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_correction_ne_zero line 547
  45. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_correction_inverse_bound line 555
  46. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_geometric_bounds line 564
  47. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_marked_error_bounds line 575
  48. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_replacement_error line 628
  49. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_slot_error line 649
  50. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_slot_at_residue line 666
  51. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_correction_eq_raw line 669
  52. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_raw_lower_bound line 681
  53. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_raw_ne_zero line 708
  54. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_slot_eq_raw line 716
  55. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_raw_slot_error line 736
  56. theorem OAI.SevenEighths.PrincipalSlotEstimate.region_slot_norm_le line 744
  57. theorem OAI.SevenEighths.PrincipalSlotEstimate.weighted_region_slot_norm line 753
  58. theorem OAI.SevenEighths.PrincipalSlotEstimate.actual_region_slot_error line 780