OAI/NumberTheory/Jacobsthal/Estimates/InvariantFiniteness.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.Erdos970Dependency.InvariantDensities.oddFactor line 16
  2. def OAI.Erdos970.Erdos970Dependency.InvariantDensities.evenDensity line 17
  3. def OAI.Erdos970.Erdos970Dependency.InvariantDensities.oddDensity line 18
  4. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.oddFactor_bounds line 20
  5. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.oddFactor_pos line 28
  6. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.oddFactor_measurable line 34
  7. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.evenDensity_measurable line 38
  8. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.oddDensity_measurable line 41
  9. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.evenDensity_nonneg line 44
  10. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.oddDensity_nonneg line 50
  11. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.oddFactor_hasDerivAt line 56
  12. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.integral_oddFactor line 63
  13. def OAI.Erdos970.Erdos970Dependency.InvariantDensities.beta line 81
  14. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.beta_eq line 83
  15. theorem OAI.Erdos970.Erdos970Dependency.InvariantDensities.beta_pos line 95
  16. theorem OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.integrableOn_Ici_of_exp_tail line 111
  17. theorem OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.weights_exp_majorant line 126
  18. theorem OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.phiEven_integrableOn line 145
  19. theorem OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.phiOdd_integrableOn line 152
  20. theorem OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.evenDensity_integrable line 157
  21. theorem OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.oddDensity_integrable line 160
  22. def OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.evenMeasure line 171
  23. def OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.oddMeasure line 172
  24. instance OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.evenMeasure_isFiniteMeasure line 174
  25. instance OAI.Erdos970.Erdos970Dependency.InvariantFiniteness.oddMeasure_isFiniteMeasure line 181