OAI/Analysis/FiniteFactor/CrossedProduct/TorusErgodic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.sourceRotationL2 line 13
2. theorem OAI.FiniteFactor.sourceCharacterL2_zero_inner line 17
3. theorem OAI.FiniteFactor.sourceRotationL2_zero_character line 22
4. theorem OAI.FiniteFactor.sourceRotationL2_fixed_orthogonal_zero line 29

   Source documentation

   An invariant vector orthogonal to the constant character is zero.

   theorem sourceRotationL2_fixed_orthogonal_zero (θ : SourceCoordinate → ℝ)
       (hr : SourceRationalIndependent θ) (f : Lp ℂ 2 sourceTorusHaar)
       (hf : sourceRotationL2 θ f = f) (h0 : inner ℂ (sourceCharacterL2 0) f = 0) : f = 0 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.sourceTorusHaar, OAI.FiniteFactor.sourceRotationL2, OAI.FiniteFactor.sourceCharacterL2

5. theorem OAI.FiniteFactor.sourceRotationL2_fixed_constant line 53
6. theorem OAI.FiniteFactor.sourceTorus_invariant_memLp_constant line 64
7. theorem OAI.FiniteFactor.sourceTorusRotationStep_ergodic line 83

   Source documentation

   Ergodicity of the constructed countable-torus rotation itself.

   theorem sourceTorusRotationStep_ergodic (θ : SourceCoordinate → ℝ)
       (hr : SourceRationalIndependent θ) : Ergodic (sourceTorusRotationStep θ) sourceTorusHaar := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceRationalIndependent, OAI.FiniteFactor.sourceTorusRotationStep, OAI.FiniteFactor.sourceTorusHaar