OAI/NumberTheory/Jacobsthal/Analysis/WeightFutureIntegrals.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.lowerDeficit line 17
  2. def OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.upperDeficit line 18
  3. def OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.gap line 19
  4. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.deficit_sum line 21
  5. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.gap_eq_rho line 25
  6. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.lowerDeficit_continuous line 28
  7. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.upperDeficit_continuousOn line 31
  8. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.gap_continuousOn line 34
  9. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.gap_pos line 40
  10. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.lowerDeficit_mass_deriv line 43
  11. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.upperDeficit_mass_deriv line 52
  12. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.gap_mass_deriv line 61
  13. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.lowerDeficit_tendsto_zero line 70
  14. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.upperDeficit_tendsto_zero line 74
  15. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.gap_tendsto_zero line 78
  16. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.deficits_pos line 80
  17. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.deficit_offsets_pos line 96
  18. theorem OAI.Erdos970.NumberTheoryLean.NormalizedDeficits.deficits_uniform_comparison line 159
  19. theorem OAI.Erdos970.NumberTheoryLean.DeficitFutureIntegrals.future_integral_of_mass line 198
  20. theorem OAI.Erdos970.NumberTheoryLean.DeficitFutureIntegrals.deficit_mass_bounds line 235
  21. theorem OAI.Erdos970.NumberTheoryLean.DeficitFutureIntegrals.lowerDeficit_mass_tendsto_zero line 251
  22. theorem OAI.Erdos970.NumberTheoryLean.DeficitFutureIntegrals.upperDeficit_mass_tendsto_zero line 265
  23. theorem OAI.Erdos970.NumberTheoryLean.DeficitFutureIntegrals.upperDeficit_mass_deriv_of_one_lt line 279
  24. theorem OAI.Erdos970.NumberTheoryLean.DeficitFutureIntegrals.lowerDeficit_nonneg line 292
  25. theorem OAI.Erdos970.NumberTheoryLean.DeficitFutureIntegrals.lower_future_integral line 297
  26. theorem OAI.Erdos970.NumberTheoryLean.DeficitFutureIntegrals.upper_future_integral line 304
  27. def OAI.Erdos970.NumberTheoryLean.DerivativeWeights.evenInitial line 323
  28. def OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven line 326
  29. def OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiOdd line 329
  30. def OAI.Erdos970.NumberTheoryLean.DerivativeWeights.W line 332
  31. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiOdd_initial line 334
  32. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_initial line 337
  33. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_eq_deficits line 340
  34. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiOdd_eq_deficits line 349
  35. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_explicit line 359
  36. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.hasDerivAt_of_mass line 370
  37. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.lowerDeficit_hasDerivAt line 381
  38. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.upperDeficit_hasDerivAt line 389
  39. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.evenInitial_hasDerivAt line 397
  40. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_hasDerivAt line 407
  41. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiOdd_hasDerivAt line 429
  42. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_pos line 444
  43. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiOdd_pos line 454
  44. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_continuousAt line 462
  45. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiOdd_continuous line 465
  46. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.f_hasDerivAt line 482
  47. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.F_hasDerivAt line 490
  48. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.startingExtension_hasDerivAt line 505
  49. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.f_right_derivative_two line 514
  50. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_eq_deriv line 523
  51. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiOdd_eq_deriv line 528
  52. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_eq_right_deriv_two line 533
  53. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiEven_strictAntiOn line 538
  54. theorem OAI.Erdos970.NumberTheoryLean.DerivativeWeights.phiOdd_antitone line 549
  55. theorem OAI.Erdos970.NumberTheoryLean.WeightFutureIntegrals.phiEven_tendsto_zero line 581
  56. theorem OAI.Erdos970.NumberTheoryLean.WeightFutureIntegrals.phiOdd_tendsto_zero line 595
  57. theorem OAI.Erdos970.NumberTheoryLean.WeightFutureIntegrals.W_pos line 609
  58. theorem OAI.Erdos970.NumberTheoryLean.WeightFutureIntegrals.future_integral_of_shifted_deriv line 613
  59. theorem OAI.Erdos970.NumberTheoryLean.WeightFutureIntegrals.phiEven_future_integral line 643
  60. theorem OAI.Erdos970.NumberTheoryLean.WeightFutureIntegrals.phiOdd_future_integral line 654