OAI/Analysis/FiniteFactor/OrbitSampling/OrbitSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingPositiveOrbits line 10
2. theorem OAI.FiniteFactor.sourceSamplingPositiveOrbits_measurable line 13
3. theorem OAI.FiniteFactor.sourceSamplingSummand_positive_orbit line 26
4. theorem OAI.FiniteFactor.sourceSamplingTrimmed_orbits line 35

   Source documentation

   Trimming preserves the constructed finite set of strictly positive orbit powers while imposing coordinatewise order everywhere.

   theorem sourceSamplingTrimmed_orbits (I : Finset SourceCoordinate) (s : ℕ)
       (θ : SourceCoordinate → ℝ) : ∀ᵐ p ∂sourceSamplingTrimmed I s θ,
         (∀ i, p.1 i ≤ p.2 i) ∧ ∃ n ∈ sourceSamplingPowers s, 0 < n ∧ p.2 = coordinateRotate θ n p.1 := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingTrimmed, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.coordinateRotate