OAI/Analysis/FiniteFactor/OrbitSampling/LimitMeasure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.sourceSamplingPairHaar line 11
2. def OAI.FiniteFactor.sourceSamplingTriangleSet line 14
3. def OAI.FiniteFactor.sourceSamplingLimitMap line 17
4. def OAI.FiniteFactor.sourceSamplingLambda line 21
5. theorem OAI.FiniteFactor.sourceSamplingTriangleSet_measurable line 25
6. theorem OAI.FiniteFactor.sourceSamplingLimitMap_measurable line 35
7. instance OAI.FiniteFactor.sourceSamplingLambda_finite line 45
8. theorem OAI.FiniteFactor.sourceSamplingPairHaar_cube line 49
9. theorem OAI.FiniteFactor.sourceSamplingLambda_ordered line 66

   Source documentation

   The actual limiting measure is carried by ordered pairs.

   theorem sourceSamplingLambda_ordered (I : Finset SourceCoordinate) :
       ∀ᵐ p ∂sourceSamplingLambda I, ∀ i, p.1 i ≤ p.2 i := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingLambda

10. theorem OAI.FiniteFactor.sourceSamplingLimitRectangleMass_formula line 82

    Source documentation

    The finite rectangle formula for the source limit, written using actual Lebesgue triangular and diagonal masses.

    theorem sourceSamplingLimitRectangleMass_formula (I : Finset SourceCoordinate) (T : SourceSamplingRationalTest) :
        sourceSamplingLimitRectangleMass I T = ∏ i ∈ I ∪ T.1,
          if i ∈ I then ((unitIntervalMeasure.prod unitIntervalMeasure)
            {p : ℝ × ℝ | p.1 ∈ sourceSamplingRationalX T i ∧
              p.2 ∈ sourceSamplingRationalY T i ∧ p.1 < p.2}).toReal
          else (unitIntervalMeasure (sourceSamplingRationalX T i ∩ sourceSamplingRationalY T i)).toReal := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingRationalTest, OAI.FiniteFactor.sourceSamplingLimitRectangleMass, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceSamplingRationalX, OAI.FiniteFactor.sourceSamplingRationalY