OAI/Analysis/FiniteFactor/OrbitSampling/OrderedRestriction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceSamplingOrdered line 11
2. theorem OAI.FiniteFactor.sourceSamplingOrdered_measurable line 13
3. def OAI.FiniteFactor.sourceSamplingTrimmed line 19

   Source documentation

   The actual ordered restriction of the already constructed average.

   def sourceSamplingTrimmed (I : Finset SourceCoordinate) (s : ℕ) (θ : SourceCoordinate → ℝ) :
       Measure SourceSamplingPair := (sourceSamplingUntrimmed I s θ).restrict sourceSamplingOrdered

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceSamplingPair, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceSamplingOrdered

4. instance OAI.FiniteFactor.sourceSamplingTrimmed_finite line 22
5. theorem OAI.FiniteFactor.sourceSamplingTrimmed_ordered line 27
6. theorem OAI.FiniteFactor.sourceSamplingTrimmed_le line 31
7. theorem OAI.FiniteFactor.sourceSamplingPowers_positive line 35
8. theorem OAI.FiniteFactor.sourceSampling_order_failure_tail line 44

   Source documentation

   Outside the finite prefix, every failure of global order is an actual member of the source's countable tail-failure event.

   theorem sourceSampling_order_failure_tail (s n : ℕ) (θ x : SourceCoordinate → ℝ)
       (hprefix : ∀ i ∈ sourceSamplingPrefix s, x i < coordinateRotate θ (n : ℤ) x i)
       (hbad : (x,coordinateRotate θ (n : ℤ) x) ∉ sourceSamplingOrdered) :
       x ∈ sourceTailOrderFailure θ (s+1) n := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPrefix, OAI.FiniteFactor.coordinateRotate, OAI.FiniteFactor.sourceSamplingOrdered, OAI.FiniteFactor.sourceTailOrderFailure

9. theorem OAI.FiniteFactor.sourceSamplingSummand_discarded_le line 65

   Source documentation

   Discarded mass of each real summand obeys the preserved relative weighted-tail estimate. This includes summands of mass zero.

   theorem sourceSamplingSummand_discarded_le (I : Finset SourceCoordinate) (s : ℕ)
       (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) (n : ℤ)
       (hn : n ∈ sourceSamplingPowers s) :
       sourceSamplingSummand I s θ n sourceSamplingOrderedᶜ ≤
         sourceSamplingSummand I s θ n Set.univ *
           ENNReal.ofReal (4*(sourceBlockSize s : ℝ)^(-(sourceBlockSize s : ℝ)/20)) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.sourceSamplingSummand, OAI.FiniteFactor.sourceBlockSize

10. theorem OAI.FiniteFactor.sourceSamplingUntrimmed_discarded_le line 88

    Source documentation

    The average loses at most the same relative error as each summand.

    theorem sourceSamplingUntrimmed_discarded_le (I : Finset SourceCoordinate) (s : ℕ)
        (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ) :
        sourceSamplingUntrimmed I s θ sourceSamplingOrderedᶜ ≤
          sourceSamplingUntrimmed I s θ Set.univ *
            ENNReal.ofReal (4*(sourceBlockSize s : ℝ)^(-(sourceBlockSize s : ℝ)/20)) := by
    …

    Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceSamplingUntrimmed, OAI.FiniteFactor.sourceBlockSize