OAI/Analysis/KadisonKastler/CountableRandomWalkLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

A symmetric fully supported law for the boundary random walk

The boundary construction starts with a probability law that assigns positive mass to every element of the countable group. A geometric enumeration gives such a law, and averaging with its inverse image makes it symmetric.

  1. def OAI.KadisonKastler.randomWalkEnumeration line 24
  2. theorem OAI.KadisonKastler.randomWalkEnumeration_surjective line 29
  3. def OAI.KadisonKastler.randomWalkGeometricParameter line 34
  4. def OAI.KadisonKastler.enumeratedRandomWalkLaw line 36
  5. instance OAI.KadisonKastler.enumeratedRandomWalkLaw_probability line 40
  6. theorem OAI.KadisonKastler.enumeratedRandomWalkLaw_singleton_pos line 44
  7. def OAI.KadisonKastler.symmetricRandomWalkLaw line 60
  8. instance OAI.KadisonKastler.symmetricRandomWalkLaw_probability line 65
  9. theorem OAI.KadisonKastler.symmetricRandomWalkLaw_inv line 72
  10. theorem OAI.KadisonKastler.symmetricRandomWalkLaw_singleton_pos line 81
  11. theorem OAI.KadisonKastler.symmetricRandomWalkLaw_null_iff line 88
  12. theorem OAI.KadisonKastler.absolutelyContinuous_symmetricRandomWalkLaw line 101
  13. theorem OAI.KadisonKastler.symmetricRandomWalkLaw_quasi line 106
  14. def OAI.KadisonKastler.randomWalkConvolution line 111

    Source documentation

    The root law after the first increment.

    def randomWalkConvolution (G : Type*) [Group G] [Countable G]
    [MeasurableSpace G] [MeasurableSingletonClass G] : Measure G :=
…
  15. instance OAI.KadisonKastler.randomWalkConvolution_probability line 116
  16. theorem OAI.KadisonKastler.randomWalkConvolution_singleton_pos line 120
  17. theorem OAI.KadisonKastler.randomWalkLaw_absolutelyContinuous_convolution line 133
  18. theorem OAI.KadisonKastler.randomWalkConvolution_absolutelyContinuous_law line 145