OAI/Analysis/FiniteFactor/OrbitSampling/SelfMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSamplingCutoff_le_half line 9
2. theorem OAI.FiniteFactor.sourceSampling_log_self_bound line 18
3. theorem OAI.FiniteFactor.sourceSampling_oriented_self_moment line 39

   Source documentation

   All tested source weights have the logarithmic self-pair bound in both orientations. The harmless extra 1 includes triangular coordinates.

   theorem sourceSampling_oriented_self_moment (stage : ℕ) (r b : Bool) (E G : Set ℝ)
       (hE : MeasurableSet E) (hG : MeasurableSet G) :
       (∫ s, ∫ t, samplingOrientedWeight r b (sourceSamplingWidth stage) (sourceSamplingCutoff stage) E G s t ^ 2
         ∂unitIntervalMeasure ∂unitIntervalMeasure) ≤
         1+4*(sourceBlockSize stage : ℝ)^(3/5 : ℝ)*Real.log (sourceBlockSize stage : ℝ) := by
   …

   Mentions: OAI.FiniteFactor.samplingOrientedWeight, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.unitIntervalMeasure, OAI.FiniteFactor.sourceBlockSize