OAI/NumberTheory/Jacobsthal/Estimates/BoundaryReferenceConvergence.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryTerms.D line 19
  2. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryTerms.D_nonneg line 22
  3. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryTerms.D_sum line 25
  4. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryTerms.D_zero line 30
  5. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryTerms.D_succ line 42
  6. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryDepth.odd_gate_impossible line 71
  7. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryDepth.odd_term_zero line 77
  8. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryDepth.D_two_zero line 84
  9. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryDepth.D_vanish line 96
  10. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryDepth.prefixWeight_positive line 112
  11. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryDepth.D_positive_of_member line 126
  12. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryDepth.admitted_length_lt line 133
  13. theorem OAI.Erdos970.NumberTheoryLean.DiscreteBoundaryExpansion.referencePolynomial_finite_sum line 162
  14. def OAI.Erdos970.NumberTheoryLean.ActualDiscreteBoundaryTerms.actualD line 196
  15. theorem OAI.Erdos970.NumberTheoryLean.ActualDiscreteBoundaryTerms.actualD_zero line 199
  16. theorem OAI.Erdos970.NumberTheoryLean.ActualDiscreteBoundaryTerms.selected_exponent_bounds line 202
  17. theorem OAI.Erdos970.NumberTheoryLean.ActualDiscreteBoundaryTerms.selected_available_set line 210
  18. theorem OAI.Erdos970.NumberTheoryLean.ActualDiscreteBoundaryTerms.actualD_succ line 216
  19. theorem OAI.Erdos970.NumberTheoryLean.ActualDiscreteBoundaryTerms.boundary_exponent_bounds line 226
  20. theorem OAI.Erdos970.NumberTheoryLean.ActualDiscreteBoundaryTerms.actualD_vanish line 232
  21. theorem OAI.Erdos970.NumberTheoryLean.ActualDiscreteBoundaryTerms.actual_reference_finite_sum line 236
  22. theorem OAI.Erdos970.ErdosContinuousBoundary.available_boundary_subset line 256
  23. theorem OAI.Erdos970.ErdosContinuousBoundary.boundary_gate_membership line 264
  24. theorem OAI.Erdos970.ErdosContinuousBoundary.available_gate_sum line 278
  25. theorem OAI.Erdos970.ErdosContinuousBoundary.actualD_succ_gate_sum line 300
  26. theorem OAI.Erdos970.ErdosContinuousBoundary.prime_gate_sum_difference line 308
  27. theorem OAI.Erdos970.ErdosContinuousBoundary.actualD_uniform_approximation line 338
  28. theorem OAI.Erdos970.ErdosContinuousBoundary.finite_reference_error line 403
  29. theorem OAI.Erdos970.ErdosContinuousBoundary.uniform_boundary_reference_convergence line 426
  30. theorem OAI.Erdos970.ErdosContinuousBoundary.boundary_two_convergence line 446