OAI/Analysis/FiniteFactor/OrbitSampling/PairMoments.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceSampling_oriented_pair_error line 13

   Source documentation

   All four actual tested coordinate cases have the same pair-error budget.

   theorem sourceSampling_oriented_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')
       (r b : Bool) (a c a' c' s : ℝ) (hsx : s ∈ Set.Ioo (0 : ℝ) 1) :
       |(∫ θ, samplingOrientedWeight r b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
           (Set.Icc a c) (Set.Icc a' c') s (Int.fract ((n : ℝ)*θ i)) *
           samplingOrientedWeight r b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
           (Set.Icc a c) (Set.Icc a' c') s (Int.fract ((n' : ℝ)*θ i)) ∂sourceAngleLaw) -
         samplingOrientedDensity r b (sourceSamplingWidth stage) (sourceSamplingCutoff stage)
           (Set.Icc a c) (Set.Icc a' c') s ^ 2| ≤
         104*(sourceBlockSize stage : ℝ)^(-74 : ℝ) := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceSamplingPowers, OAI.FiniteFactor.samplingOrientedWeight, OAI.FiniteFactor.sourceSamplingWidth, OAI.FiniteFactor.sourceSamplingCutoff, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.samplingOrientedDensity

2. theorem OAI.FiniteFactor.sourceSampling_coordinate_pair_error line 49