OAI/NumberTheory/Jacobsthal/Estimates/ReferenceWeightedQuadrature.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.ReferenceBenchmarkDecay.benchmark line 15
  2. theorem OAI.Erdos970.NumberTheoryLean.ReferenceBenchmarkDecay.benchmark_even_below_two line 19
  3. theorem OAI.Erdos970.NumberTheoryLean.ReferenceBenchmarkDecay.benchmark_deviation_le_gap line 22
  4. theorem OAI.Erdos970.NumberTheoryLean.ReferenceBenchmarkDecay.gap_le_rho line 36
  5. theorem OAI.Erdos970.NumberTheoryLean.ReferenceBenchmarkDecay.gap_le_constant line 40
  6. theorem OAI.Erdos970.NumberTheoryLean.ReferenceBenchmarkDecay.boundary_rho_decay line 46
  7. theorem OAI.Erdos970.NumberTheoryLean.ReferenceBenchmarkDecay.boundary_benchmark_decay line 63
  8. def OAI.Erdos970.NumberTheoryLean.ReferenceDifferentiation.parentBenchmark line 105
  9. def OAI.Erdos970.NumberTheoryLean.ReferenceDifferentiation.ParentDomain line 109
  10. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDifferentiation.parent_even_eq_starting line 113
  11. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDifferentiation.parent_even_eq_ordinary line 120
  12. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDifferentiation.parent_mass_derivative line 127
  13. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDifferentiation.reference_derivative line 166
  14. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDifferentiation.omitted_lower_deviation line 185
  15. def OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.childAdmitted line 203
  16. def OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.admitted line 207
  17. def OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.endSide line 211
  18. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.gap_append line 215
  19. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.endSide_append line 221
  20. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.admitted_append line 226
  21. def OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.FirstOmitted line 233
  22. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.firstOmitted_not_admitted line 237
  23. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.exists_first_omitted_prefix line 244
  24. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.firstOmitted_boundary_gap line 259
  25. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.gap_lower_by_length line 278
  26. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.firstOmitted_boundary_length line 289
  27. def OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.referencePrefixes line 296
  28. def OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.firstOmissions line 300
  29. def OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.referencePolynomial line 304
  30. def OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.boundaryPrimes line 307
  31. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.boundary_prime_exponent_upper line 309
  32. theorem OAI.Erdos970.NumberTheoryLean.ReferenceAdmission.actual_first_omission_length line 317
  33. def OAI.Erdos970.ErdosContinuousBoundary.upperCutoff line 333
  34. theorem OAI.Erdos970.ErdosContinuousBoundary.upperCutoff_bounds line 337
  35. theorem OAI.Erdos970.ErdosContinuousBoundary.upperCutoff_continuous line 342
  36. theorem OAI.Erdos970.ErdosContinuousBoundary.upperCutoff_odd_small line 346
  37. theorem OAI.Erdos970.ErdosContinuousBoundary.upperCutoff_low line 350
  38. theorem OAI.Erdos970.ErdosContinuousBoundary.strong_gate_below_two line 355
  39. theorem OAI.Erdos970.ErdosContinuousBoundary.le_clipped_upper line 361
  40. theorem OAI.Erdos970.ErdosContinuousBoundary.mem_upperCutoff line 365
  41. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCancellation.parent_domain_mono line 396
  42. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCancellation.positive_gap_of_parent_domain line 399
  43. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCancellation.parent_domain_interval line 404
  44. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCancellation.prospective_integrand_continuousAt line 409
  45. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCancellation.prospective_interval_integrable line 423
  46. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCancellation.continuous_reference_cancellation line 431
  47. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCancellation.upper_admission_above_two line 450
  48. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCancellation.actual_omitted_deviation_above_two line 455
  49. theorem OAI.Erdos970.ErdosContinuousBoundary.upperCutoff_b_lipschitz line 468
  50. theorem OAI.Erdos970.ErdosContinuousBoundary.upperCutoff_r_lipschitz line 474
  51. theorem OAI.Erdos970.ErdosContinuousBoundary.upperCutoff_b_difference line 491
  52. theorem OAI.Erdos970.ErdosContinuousBoundary.upperCutoff_r_difference line 495
  53. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDeviationMonotonicity.lower_deficit_antitone line 510
  54. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDeviationMonotonicity.upper_deficit_pos_positive line 529
  55. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDeviationMonotonicity.upper_deficit_antitone line 537
  56. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDeviationMonotonicity.even_abs_deviation line 550
  57. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDeviationMonotonicity.odd_abs_deviation line 554
  58. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDeviationMonotonicity.prospective_absolute_monotone line 557
  59. theorem OAI.Erdos970.NumberTheoryLean.ReferenceDeviationMonotonicity.prospective_signed_monotone line 579
  60. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.starting_parent_nonpos line 619
  61. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.even_parent_le_one line 626
  62. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.even_parent_abs line 635
  63. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.weight_deviation_identity line 640
  64. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.valid_parent_domain line 668
  65. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.source_deviation_sum line 671
  66. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.ordinary_deviation_le_parent line 680
  67. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.benchmark_absolute_antitone line 695
  68. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightDomination.residual_deviations_bound line 704
  69. theorem OAI.Erdos970.NumberTheoryLean.ReferenceParentMonotonicity.even_parent_deficit_antitone line 728
  70. theorem OAI.Erdos970.NumberTheoryLean.ReferenceParentMonotonicity.parent_absolute_antitone line 751
  71. theorem OAI.Erdos970.NumberTheoryLean.ReferenceParentMonotonicity.interval_deviations_bound line 760
  72. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightedQuadrature.source_weighted_quadrature line 786