OAI/NumberTheory/PrimePackets/LeafPeriods.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.realLeafPeriods line 120
  2. lemma OAI.PrimeDegreePackets.mem_realLeafPeriods line 137
  3. lemma OAI.PrimeDegreePackets.continuous_integral_translate line 140
  4. lemma OAI.PrimeDegreePackets.realLeafPeriods_eq_tests line 153
  5. theorem OAI.PrimeDegreePackets.isClosed_realLeafPeriods line 176
  6. lemma OAI.PrimeDegreePackets.realLeafPeriods_eq_top_of_dense line 181
  7. theorem OAI.PrimeDegreePackets.realLeaf_invariant_of_small_periods line 189
  8. theorem OAI.PrimeDegreePackets.realLeafPeriods_top_or_cyclic line 199
  9. abbrev OAI.PrimeDegreePackets.leafTestSpace line 211
  10. instance OAI.PrimeDegreePackets.(instance at line 214) line 214
  11. instance OAI.PrimeDegreePackets.(instance at line 218) line 218
  12. def OAI.PrimeDegreePackets.leafTest line 221
  13. lemma OAI.PrimeDegreePackets.leafTest_apply line 229
  14. lemma OAI.PrimeDegreePackets.continuous_leafTestSpace_integral line 232
  15. lemma OAI.PrimeDegreePackets.realLeafPeriods_iff_countable_tests line 246
  16. lemma OAI.PrimeDegreePackets.continuous_leafTest_discrepancy line 278
  17. lemma OAI.PrimeDegreePackets.measurable_leafTest_discrepancy line 283
  18. lemma OAI.PrimeDegreePackets.realLeafPeriods_smul line 294
  19. lemma OAI.PrimeDegreePackets.realLeafPeriods_scaling line 305
  20. lemma OAI.PrimeDegreePackets.realLeafPeriods_normalized_scaling line 318
  21. def OAI.PrimeDegreePackets.hasSmallLeafPeriod line 334
  22. lemma OAI.PrimeDegreePackets.hasSmallLeafPeriod_mono line 337
  23. lemma OAI.PrimeDegreePackets.hasSmallLeafPeriod_normalized_scaling line 342
  24. lemma OAI.PrimeDegreePackets.exists_pos_leafPeriod_normalized_scaling line 359
  25. lemma OAI.PrimeDegreePackets.exists_compact_zero_iff_dense_tests line 378
  26. theorem OAI.PrimeDegreePackets.measurableSet_exists_compact_zero line 420
  27. lemma OAI.PrimeDegreePackets.measurableSet_exists_leafPeriod_Icc line 439
  28. theorem OAI.PrimeDegreePackets.measurableSet_hasSmallLeafPeriod line 474
  29. theorem OAI.PrimeDegreePackets.measurableSet_exists_pos_leafPeriod line 491
  30. lemma OAI.PrimeDegreePackets.ae_hasSmallLeafPeriod_scaling line 512
  31. theorem OAI.PrimeDegreePackets.ae_realLeafPeriods_bot_or_top line 550