OAI/Analysis/FiniteFactor/OrbitSampling/Measures.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FiniteFactor.sourceSamplingHaar line 10
2. def OAI.FiniteFactor.sourceSamplingWeightedMeasure line 13
3. instance OAI.FiniteFactor.sourceSamplingWeightedMeasure_finite line 17
4. def OAI.FiniteFactor.sourceSamplingSummand line 28
5. instance OAI.FiniteFactor.sourceSamplingSummand_finite line 33
6. theorem OAI.FiniteFactor.sourceSamplingSummand_first_marginal line 38
7. def OAI.FiniteFactor.sourceSamplingUntrimmed line 49

   Source documentation

   Finite positive untrimmed measures averaged over the constructed powers. No weak limit or uniform marginal bound is asserted by this definition.

   def sourceSamplingUntrimmed (I : Finset SourceCoordinate) (s : ℕ) (θ : SourceCoordinate → ℝ) :
       Measure ((SourceCoordinate → ℝ) × (SourceCoordinate → ℝ)) :=
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate

8. theorem OAI.FiniteFactor.sourceSamplingHaar_cube line 54
9. theorem OAI.FiniteFactor.sourceSamplingWeightedMeasure_orders line 64

   Source documentation

   The weighted source law already orders every coordinate in its prefix.

   theorem sourceSamplingWeightedMeasure_orders (I : Finset SourceCoordinate) (s : ℕ)
       (θ : SourceCoordinate → ℝ) (n : ℤ) :
       ∀ᵐ x ∂sourceSamplingWeightedMeasure I s θ n,
         ∀ i ∈ sourceSamplingPrefix s, x i < coordinateRotate θ n x i := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingWeightedMeasure, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.coordinateRotate