OAI/Analysis/FiniteFactor/OrbitSampling/Fourier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceBlockSize_monotone line 10
2. theorem OAI.FiniteFactor.sourceFrequencyScale_monotone line 25
3. theorem OAI.FiniteFactor.sourceAngleLaw_pair_fourier_le line 37

   Source documentation

   The full infinite-product angle expectation has the same coordinate Fourier estimate; no independence between two phases is asserted.

   theorem sourceAngleLaw_pair_fourier_le (i : SourceCoordinate) (v v' : ℤ) (n n' : ℝ)
       (hw : (v : ℝ)*n+(v' : ℝ)*n' ≠ 0) :
       ‖∫ θ, Complex.exp (2 * Real.pi * Complex.I *
         ((v : ℂ) * (Int.fract (n*θ i) : ℝ) + (v' : ℂ) * (Int.fract (n'*θ i) : ℝ)))
         ∂sourceAngleLaw‖ ≤
         1/(Real.pi*sourceAngleUnit i*|(v : ℝ)*n+(v' : ℝ)*n'|) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceAngleUnit

4. theorem OAI.FiniteFactor.sourceSampling_pair_fourier_bound line 49