OAI/NumberTheory/Jacobsthal/Partitions/SourceLabelCount.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseCells.labelFiber line 14
  2. theorem OAI.Erdos970.ErdosInverseCells.mem_labelFiber line 17
  3. theorem OAI.Erdos970.ErdosInverseCells.labelFiber_subset line 20
  4. theorem OAI.Erdos970.ErdosInverseCells.label_fibers_partition line 23
  5. theorem OAI.Erdos970.ErdosInverseCells.label_fibers_disjoint line 33
  6. theorem OAI.Erdos970.ErdosInverseCells.sum_label_fibers line 39
  7. def OAI.Erdos970.ErdosInverseCells.smallLabels line 46
  8. def OAI.Erdos970.ErdosInverseCells.discardedPoints line 49
  9. theorem OAI.Erdos970.ErdosInverseCells.mem_discardedPoints line 52
  10. theorem OAI.Erdos970.ErdosInverseCells.discardedPoints_subset line 65
  11. theorem OAI.Erdos970.ErdosInverseCells.sum_small_fibers line 68
  12. theorem OAI.Erdos970.ErdosInverseCells.discardedPoints_card_bound line 72
  13. def OAI.Erdos970.ErdosGeometricValueCells.coordinate line 90
  14. def OAI.Erdos970.ErdosGeometricValueCells.valueIndex line 92
  15. theorem OAI.Erdos970.ErdosGeometricValueCells.coordinate_bounds line 95
  16. theorem OAI.Erdos970.ErdosGeometricValueCells.valueIndex_eq_floor line 112
  17. theorem OAI.Erdos970.ErdosGeometricValueCells.valueIndex_interval line 120
  18. theorem OAI.Erdos970.ErdosInverseCells.exists_dense_retained_fiber line 157
  19. theorem OAI.Erdos970.ErdosGeometricValueCells.same_index_ratio line 204
  20. def OAI.Erdos970.ErdosGeometricValueCells.valueCell line 226
  21. theorem OAI.Erdos970.ErdosGeometricValueCells.valueCells_partition line 229
  22. theorem OAI.Erdos970.ErdosGeometricValueCells.valueCells_disjoint line 240
  23. theorem OAI.Erdos970.ErdosGeometricValueCells.sum_valueCells line 246
  24. theorem OAI.Erdos970.ErdosGeometricValueCells.valueCells_card_bound line 253
  25. theorem OAI.Erdos970.ErdosGeometricValueCells.same_cell_ratio line 257
  26. def OAI.Erdos970.ErdosInverseCells.cofactorHit line 277
  27. theorem OAI.Erdos970.ErdosInverseCells.cofactorHit_eq line 280
  28. theorem OAI.Erdos970.ErdosInverseCells.cofactorHit_spec line 283
  29. abbrev OAI.Erdos970.ErdosInverseCells.InitialLabel line 290
  30. def OAI.Erdos970.ErdosInverseCells.initialLabel line 292
  31. def OAI.Erdos970.ErdosInverseCells.initialCell line 295
  32. theorem OAI.Erdos970.ErdosInverseCells.initialLabel_card line 298
  33. theorem OAI.Erdos970.ErdosInverseCells.same_initial_label line 303
  34. def OAI.Erdos970.ErdosInverseCells.cellUpper line 314
  35. theorem OAI.Erdos970.ErdosInverseCells.initial_cell_interval line 317
  36. theorem OAI.Erdos970.ErdosInverseCells.mem_initialCell line 343
  37. theorem OAI.Erdos970.ErdosInverseCells.initial_cell_congruences line 348
  38. theorem OAI.Erdos970.ErdosInverseCells.initial_cell_weight_spread line 357
  39. abbrev OAI.Erdos970.ErdosInverseRefinement.RefinementLabel line 379
  40. def OAI.Erdos970.ErdosInverseRefinement.refinementLabel line 381
  41. def OAI.Erdos970.ErdosInverseRefinement.refinementCell line 384
  42. theorem OAI.Erdos970.ErdosInverseRefinement.refinementLabel_card line 387
  43. theorem OAI.Erdos970.ErdosInverseRefinement.mem_refinementCell line 391
  44. theorem OAI.Erdos970.ErdosInverseRefinement.refinement_congruences line 395
  45. theorem OAI.Erdos970.ErdosInverseCells.source_initial_label_count line 418