OAI/NumberTheory/PrimePackets/ScalingCovariance.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.normalized_realScaling_total_inv line 118
  2. theorem OAI.PrimeDegreePackets.ae_total_inv_eq_of_scaling_covariance line 141
  3. theorem OAI.PrimeDegreePackets.ae_dirac_of_finite_scaling_covariance line 183
  4. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_finite_dirac line 220
  5. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_trivial_or_infinite_atomless line 257
  6. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_atom_diagonal line 276
  7. theorem OAI.PrimeDegreePackets.intrinsicRootLeaf_ergodic_alternative line 307
  8. def OAI.PrimeDegreePackets.rootCanonicalWeights line 346
  9. lemma OAI.PrimeDegreePackets.rootCanonicalWeights_sum line 349
  10. lemma OAI.PrimeDegreePackets.rootCanonicalWeights_difference line 353
  11. def OAI.PrimeDegreePackets.rootCanonicalFlow line 360
  12. lemma OAI.PrimeDegreePackets.rootCanonicalFlow_preserving line 363
  13. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_canonical line 373
  14. def OAI.PrimeDegreePackets.rootInformation line 397
  15. lemma OAI.PrimeDegreePackets.aemeasurable_rootInformation line 401
  16. lemma OAI.PrimeDegreePackets.ae_rootInformation_nonneg line 413
  17. lemma OAI.PrimeDegreePackets.normalized_realScaling_ball line 429
  18. theorem OAI.PrimeDegreePackets.ae_intrinsicRootLeaf_ball_cocycle line 441
  19. theorem OAI.PrimeDegreePackets.ae_rootInformation_cocycle line 466
  20. def OAI.PrimeDegreePackets.rootInformationMean line 511
  21. lemma OAI.PrimeDegreePackets.rootInformationMean_add line 515
  22. lemma OAI.PrimeDegreePackets.rootInformationMean_zero_time line 545
  23. lemma OAI.PrimeDegreePackets.rootInformationMean_nat line 557
  24. lemma OAI.PrimeDegreePackets.ae_rootLeaf_ball_eq_one_of_mean_zero line 570
  25. theorem OAI.PrimeDegreePackets.rootInformationMean_eq_zero_iff_dirac line 593