OAI/Analysis/FiniteFactor/OrbitSampling/TorusSupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingPairRepresentative line 12
2. theorem OAI.FiniteFactor.sourceSamplingPairRepresentative_measurable line 15
3. def OAI.FiniteFactor.sourceTorusRotate line 19
4. theorem OAI.FiniteFactor.sourceTorusRotate_continuous line 22
5. theorem OAI.FiniteFactor.sourceTorusQuotient_rotate line 25
6. theorem OAI.FiniteFactor.sourceSamplingTrimmed_representatives line 33

   Source documentation

   The chosen real representatives recover the actual orbit measures; closed-cube endpoints are not silently identified with distinct real points.

   theorem sourceSamplingTrimmed_representatives (I : Finset SourceCoordinate) (s : ℕ)
       (θ : SourceCoordinate → ℝ) : ∀ᵐ p ∂sourceSamplingTrimmed I s θ,
         sourceSamplingPairRepresentative (sourceSamplingTorusMap p) = p := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingTrimmed, OAI.FiniteFactor.sourceSamplingPairRepresentative, OAI.FiniteFactor.sourceSamplingTorusMap

7. def OAI.FiniteFactor.sourceSamplingTorusOrderedOrbits line 56
8. theorem OAI.FiniteFactor.sourceSamplingTorusOrderedOrbits_measurable line 60
9. theorem OAI.FiniteFactor.sourceSamplingTrimmed_torus_orbits line 82

   Source documentation

   Actual compact-torus support: representatives are ordered, and each pair lies on one of the constructed finitely many strictly positive rotation graphs.

   theorem sourceSamplingTrimmed_torus_orbits (I : Finset SourceCoordinate) (s : ℕ)
       (θ : SourceCoordinate → ℝ) :
       ∀ᵐ p ∂(sourceSamplingTrimmedTorus I s θ : Measure SourceSamplingTorus),
         (∀ i, sourceTorusRepresentative p.1 i ≤ sourceTorusRepresentative p.2 i) ∧
         ∃ n ∈ sourceSamplingPowers s, 0 < n ∧ p.2 = sourceTorusRotate θ n p.1 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingTrimmedTorus, OAI.FiniteFactor.SourceSamplingTorus, OAI.FiniteFactor.sourceTorusRepresentative, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.sourceTorusRotate