OAI/Analysis/FiniteFactor/CrossedProduct/TorusModel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.SourceTorus line 10
2. abbrev OAI.FiniteFactor.sourceTorusHaar line 11
3. instance OAI.FiniteFactor.sourceUnitCircle_probability line 14
4. def OAI.FiniteFactor.sourceTorusQuotient line 18
5. def OAI.FiniteFactor.sourceTorusRepresentative line 19
6. theorem OAI.FiniteFactor.sourceTorusQuotient_preserving line 22
7. theorem OAI.FiniteFactor.sourceTorusRepresentative_preserving line 28
8. theorem OAI.FiniteFactor.sourceTorusRepresentative_cube line 35
9. theorem OAI.FiniteFactor.sourceTorusRepresentative_quotient line 41
10. theorem OAI.FiniteFactor.sourceTorusQuotient_representative line 47
11. theorem OAI.FiniteFactor.sourceTorusQuotient_withDensity line 54

    Source documentation

    Change of variables for actual weighted laws across the real representatives and compact torus, with the inverse needed only almost everywhere.

    theorem sourceTorusQuotient_withDensity (w : (SourceCoordinate → ℝ) → ℝ≥0∞) (hw : Measurable w) :
        (sourceSamplingHaar.withDensity w).map sourceTorusQuotient =
          sourceTorusHaar.withDensity (fun z => w (sourceTorusRepresentative z)) := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceTorusQuotient, OAI.FiniteFactor.sourceTorusRepresentative