OAI/NumberTheory/Jacobsthal/Estimates/BoundaryGateSets.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm line 16
  2. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_continuous line 20
  3. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_reciprocal line 39
  4. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_low line 49
  5. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_odd_small line 53
  6. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_depth_zero line 57
  7. def OAI.Erdos970.ErdosContinuousBoundary.boundaryIntegrand line 95
  8. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryIntegrand_continuous line 98
  9. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryIntegrand_integrable line 110
  10. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_nonnegative line 114
  11. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_abs_le_one line 122
  12. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryIntegrand_abs_le_one line 138
  13. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_r_difference line 153
  14. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_b_difference line 178
  15. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_child_lipschitz line 192
  16. def OAI.Erdos970.ErdosContinuousBoundary.boundaryGateSet line 221
  17. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryGateSet_closed line 224
  18. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryGateSet_open_inter line 229
  19. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryGateSet_open_diff line 241
  20. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryGateSet_orderConnected line 253
  21. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryGateSet_subset line 259
  22. theorem OAI.Erdos970.ErdosContinuousBoundary.boundary_reference_integral line 262
  23. theorem OAI.Erdos970.ErdosContinuousBoundary.boundaryTerm_gate_integral line 273