OAI/NumberTheory/Jacobsthal/Partitions/CommonSliceGeometry.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosCommonParameterInterval.commonLower line 13
  2. def OAI.Erdos970.ErdosCommonParameterInterval.commonUpper line 14
  3. theorem OAI.Erdos970.ErdosCommonParameterInterval.div_between_endpoints line 16
  4. theorem OAI.Erdos970.ErdosCommonParameterInterval.common_interval_subset line 31
  5. theorem OAI.Erdos970.ErdosCommonParameterInterval.commonLower_error line 38
  6. theorem OAI.Erdos970.ErdosCommonParameterInterval.commonUpper_error line 48
  7. theorem OAI.Erdos970.ErdosCommonParameterInterval.common_length_lower line 59
  8. theorem OAI.Erdos970.ErdosCommonParameterInterval.common_height_bound line 68
  9. theorem OAI.Erdos970.ErdosCommonParameterInterval.reciprocal_width_bound line 87
  10. theorem OAI.Erdos970.ErdosCommonParameterInterval.common_length_lower_relative line 96
  11. theorem OAI.Erdos970.ErdosCommonParameterInterval.affine_common_interval line 106
  12. def OAI.Erdos970.ErdosCommonMInterval.lower line 124
  13. def OAI.Erdos970.ErdosCommonMInterval.upper line 125
  14. def OAI.Erdos970.ErdosCommonMInterval.interval line 126
  15. def OAI.Erdos970.ErdosCommonMInterval.referenceLength line 128
  16. def OAI.Erdos970.ErdosCommonMInterval.lengthExponent line 129
  17. theorem OAI.Erdos970.ErdosCommonMInterval.closed_subset line 131
  18. theorem OAI.Erdos970.ErdosCommonMInterval.closed_affine line 137
  19. theorem OAI.Erdos970.ErdosCommonMInterval.integer_decode line 143
  20. def OAI.Erdos970.ErdosCommonMInterval.decode line 163
  21. theorem OAI.Erdos970.ErdosCommonMInterval.decode_spec line 166
  22. theorem OAI.Erdos970.ErdosCommonMInterval.reference_rpow line 181
  23. theorem OAI.Erdos970.ErdosCommonMInterval.endpoint_magnitude line 196
  24. theorem OAI.Erdos970.ErdosCommonMInterval.closed_length_lower line 205
  25. theorem OAI.Erdos970.ErdosCommonMInterval.closed_length_upper line 236
  26. theorem OAI.Erdos970.ErdosCommonMInterval.closed_height line 246
  27. theorem OAI.Erdos970.ErdosCommonMInterval.eventual_polynomial_cutoff line 276
  28. theorem OAI.Erdos970.ErdosCommonMInterval.subbin_loss line 292
  29. theorem OAI.Erdos970.ErdosCommonMInterval.height_absorption line 303
  30. def OAI.Erdos970.ErdosCommonMInterval.relativeError line 318
  31. theorem OAI.Erdos970.ErdosCommonMInterval.relativeError_tends_zero line 320
  32. theorem OAI.Erdos970.ErdosCommonMInterval.uniform_common_interval line 326
  33. theorem OAI.Erdos970.ErdosCommonMInterval.uniform_integer_common_interval line 389
  34. def OAI.Erdos970.ErdosLargeHeightBlocks.blockLeft line 421
  35. def OAI.Erdos970.ErdosLargeHeightBlocks.blockRight line 423
  36. theorem OAI.Erdos970.ErdosLargeHeightBlocks.block_reciprocal_variation line 426
  37. def OAI.Erdos970.ErdosLargeHeightBlocks.coordinateLower line 461
  38. def OAI.Erdos970.ErdosLargeHeightBlocks.coordinateUpper line 463
  39. theorem OAI.Erdos970.ErdosLargeHeightBlocks.block_coordinate_containment line 466
  40. theorem OAI.Erdos970.ErdosLargeHeightBlocks.block_coordinate_width line 478
  41. theorem OAI.Erdos970.ErdosStoppedArithmetic.common_slice_mem_parameter line 499
  42. theorem OAI.Erdos970.ErdosStoppedArithmetic.common_slice_endpoint_height line 517