OAI/NumberTheory/Jacobsthal/Estimates/InverseWeightGrowth.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.WeightTailBounds.ratio_upper_from_rho line 16
  2. theorem OAI.Erdos970.NumberTheoryLean.WeightTailBounds.weights_ratio_bound line 37
  3. theorem OAI.Erdos970.NumberTheoryLean.WeightTailBounds.even_logDeriv_eq line 50
  4. theorem OAI.Erdos970.NumberTheoryLean.WeightTailBounds.odd_logDeriv_eq line 55
  5. theorem OAI.Erdos970.NumberTheoryLean.WeightTailBounds.weights_logDeriv_upper line 60
  6. theorem OAI.Erdos970.NumberTheoryLean.WeightTailBounds.slope_lower_from_rho line 87
  7. theorem OAI.Erdos970.NumberTheoryLean.WeightTailBounds.weights_logDeriv_ge_hazard line 109
  8. theorem OAI.Erdos970.NumberTheoryLean.WeightTailBounds.weights_logDeriv_growth line 123
  9. theorem OAI.Erdos970.NumberTheoryLean.WeightGlobalBounds.weights_global_ratio_bound line 147
  10. theorem OAI.Erdos970.NumberTheoryLean.WeightGlobalBounds.weights_global_logDeriv_bound line 190
  11. theorem OAI.Erdos970.NumberTheoryLean.WeightGlobalBounds.interval_abs_bound line 231
  12. theorem OAI.Erdos970.NumberTheoryLean.WeightGlobalBounds.phiOdd_max_three line 245
  13. theorem OAI.Erdos970.NumberTheoryLean.WeightGlobalBounds.weights_log_lipschitz line 250
  14. theorem OAI.Erdos970.NumberTheoryLean.WeightGlobalBounds.even_starting_derivative line 317
  15. theorem OAI.Erdos970.NumberTheoryLean.WeightGlobalBounds.phiOdd_deriv_initial line 322
  16. theorem OAI.Erdos970.NumberTheoryLean.WeightGlobalBounds.weights_global_logDeriv_bound_all line 334
  17. def OAI.Erdos970.NumberTheoryLean.InverseWeightGrowth.reference line 354
  18. theorem OAI.Erdos970.NumberTheoryLean.InverseWeightGrowth.reference_valid line 356
  19. theorem OAI.Erdos970.NumberTheoryLean.InverseWeightGrowth.reference_bounds line 359
  20. theorem OAI.Erdos970.NumberTheoryLean.InverseWeightGrowth.inverse_weight_quartic line 362
  21. theorem OAI.Erdos970.NumberTheoryLean.InverseWeightGrowth.inverse_phi_quartic line 410
  22. theorem OAI.Erdos970.NumberTheoryLean.InverseWeightGrowth.inverse_weight_below_cutoff line 416