OAI/NumberTheory/PrimePackets/ErgodicDecomposition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PrimeDegreePackets.condExpKernel_invariant line 56
  2. theorem OAI.PrimeDegreePackets.invariant_kernel_decomposition line 90
  3. theorem OAI.PrimeDegreePackets.condExpKernel_ae_constant line 104
  4. theorem OAI.PrimeDegreePackets.action_ergodic_decomposition line 127
  5. theorem OAI.PrimeDegreePackets.preserving_of_dense_action line 186
  6. theorem OAI.PrimeDegreePackets.continuous_action_ergodic_decomposition line 215
  7. lemma OAI.PrimeDegreePackets.standardBorel_of_measurableEquiv line 254
  8. theorem OAI.PrimeDegreePackets.standardBorel_of_sigmaCompact line 264
  9. instance OAI.PrimeDegreePackets.xStandardBorel line 287
  10. instance OAI.PrimeDegreePackets.diagonalLogAction line 291
  11. instance OAI.PrimeDegreePackets.diagonalLogAction_continuous line 301
  12. theorem OAI.PrimeDegreePackets.diagonal_positive_ergodic_decomposition line 311
  13. theorem OAI.PrimeDegreePackets.packet_probability_subsequence_bounded_discr line 355
  14. theorem OAI.PrimeDegreePackets.packet_limit_positive_ergodic_components_bounded_discr line 386
  15. theorem OAI.PrimeDegreePackets.ae_constant_of_transitive_right_action line 423
  16. theorem OAI.PrimeDegreePackets.invariant_probability_unique_transitive line 449