OAI/Analysis/FiniteFactor/OrbitSampling/CylinderSystem.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteFactor.sourceSamplingCylinder line 14

    Source documentation

    Finite cylinders in the full real product: coordinates outside the finite support are unrestricted. On the conull cube these are the original rational tests. The ambient real product is not asserted to be compact.

    def sourceSamplingCylinder (T : SourceSamplingRationalTest) : Set SourceSamplingPair :=
…

    Mentions: OAI.FiniteFactor.SourceSamplingRationalTest, OAI.FiniteFactor.SourceSamplingPair

  2. theorem OAI.FiniteFactor.sourceSamplingCylinder_measurable line 17
  3. theorem OAI.FiniteFactor.sourceSamplingCylinder_on_cube line 24
  4. def OAI.FiniteFactor.sourceSamplingTestMeet line 37
  5. theorem OAI.FiniteFactor.sourceSamplingCylinder_inter line 48
  6. theorem OAI.FiniteFactor.sourceSamplingCylinder_piSystem line 68