OAI/Analysis/FiniteFactor/OrbitSampling/Moments.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSamplingWidth_le_half line 10
2. theorem OAI.FiniteFactor.sourceSampling_tested_second_moment line 23

   Source documentation

   Exact stage parameters discharge all cutoff/width assumptions in the source's tested second-diagonal one-coordinate moment bound.

   theorem sourceSampling_tested_second_moment (s : ℕ) (E G : Set ℝ)
       (hE : MeasurableSet E) (hG : MeasurableSet G) :
       (∀ᵐ x ∂unitIntervalMeasure,
         0 ≤ samplingTestedSecondDensity (sourceSamplingWidth s) (sourceSamplingCutoff s) E G x ∧
         samplingTestedSecondDensity (sourceSamplingWidth s) (sourceSamplingCutoff s) E G x ≤ 2) ∧
       (∫ x, samplingTestedSecondDensity (sourceSamplingWidth s) (sourceSamplingCutoff s) E G x^2
         ∂unitIntervalMeasure) ≤ 1+4*(sourceBlockSize s : ℝ)^(-6/5 : ℝ) := by
   …

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