OAI/NumberTheory/PrimePackets/RootInvariance.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_periods_bot_or_top line 123
  2. theorem OAI.PrimeDegreePackets.root_invariant_of_nonzero_intrinsic_period line 155
  3. lemma OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_exists_period_diagonal line 177
  4. theorem OAI.PrimeDegreePackets.intrinsicRootLeaf_periods_ergodic_alternative line 208
  5. lemma OAI.PrimeDegreePackets.realMeasures_eq_iff_leafTests line 251
  6. def OAI.PrimeDegreePackets.projectiveLeafPeriod line 279
  7. lemma OAI.PrimeDegreePackets.projectiveLeafPeriod_iff_tests line 282
  8. lemma OAI.PrimeDegreePackets.continuous_projectiveLeaf_discrepancy line 297
  9. lemma OAI.PrimeDegreePackets.measurable_projectiveLeaf_discrepancy line 303
  10. lemma OAI.PrimeDegreePackets.isClosed_projectiveLeafPeriods line 309
  11. lemma OAI.PrimeDegreePackets.projectiveLeafPeriod_zero_time line 322
  12. lemma OAI.PrimeDegreePackets.projectiveLeafPeriod_smul line 337
  13. lemma OAI.PrimeDegreePackets.projectiveLeafPeriod_scaling line 348
  14. lemma OAI.PrimeDegreePackets.projectiveLeafPeriod_normalized_scaling line 363
  15. def OAI.PrimeDegreePackets.boundedProjectiveLeafPeriod line 380
  16. lemma OAI.PrimeDegreePackets.boundedProjectiveLeafPeriod_mono line 383
  17. lemma OAI.PrimeDegreePackets.boundedProjectiveLeafPeriod_normalized_scaling line 388
  18. lemma OAI.PrimeDegreePackets.measurableSet_exists_projectiveLeafPeriod_mem line 413
  19. lemma OAI.PrimeDegreePackets.measurableSet_boundedProjectiveLeafPeriod line 442
  20. lemma OAI.PrimeDegreePackets.not_forall_boundedProjectiveLeafPeriod line 459
  21. lemma OAI.PrimeDegreePackets.ae_boundedProjectiveLeafPeriod_scaling line 493
  22. lemma OAI.PrimeDegreePackets.ae_projectiveLeafPeriod_avoids_interval line 530
  23. lemma OAI.PrimeDegreePackets.exists_nat_mem_Icc_inv_succ line 561
  24. theorem OAI.PrimeDegreePackets.ae_projectiveLeafPeriod_multiplier_zero line 572