OAI/Analysis/FiniteFactor/OrbitSampling/FirstCorrelation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSampling_first_height_bound line 10
2. theorem OAI.FiniteFactor.sourceSampling_first_pair_error line 38

   Source documentation

   Explicit first-oriented pair correlation error for every prefix coordinate, every rectangle endpoint and both source coordinate types.

   theorem sourceSampling_first_pair_error (stage : ℕ) (hs : 200000 ≤ sourceBlockSize stage)
       (i : SourceCoordinate) (hi : i.1 ≤ stage) (n n' : ℤ)
       (hn : n ∈ sourceSamplingPowers stage) (hn' : n' ∈ sourceSamplingPowers stage) (hne : n ≠ n')
       (b : Bool) (E : Set ℝ) (a c s : ℝ) (hsx : s ∈ Set.Ico (0 : ℝ) 1) :
       |(∫ θ, samplingTestedFirstWeight b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
           E (Set.Icc a c) s (Int.fract ((n : ℝ)*θ i)) *
           samplingTestedFirstWeight b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
           E (Set.Icc a c) s (Int.fract ((n' : ℝ)*θ i)) ∂sourceAngleLaw) -
         samplingTestedFirstDensity b (sourceSamplingWidth stage) (sourceSamplingCutoff stage) E (Set.Icc a c) s ^ 2| ≤
         26*(sourceBlockSize stage : ℝ)^(-74 : ℝ) := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.samplingTestedFirstWeight, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.samplingTestedFirstDensity