OAI/Analysis/FiniteFactor/Sampling/Fourier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.norm_interval_fourier_le line 13

   Source documentation

   Direct integral estimate for a real nonzero frequency on an interval.

   theorem norm_interval_fourier_le (a b w : ℝ) (hw : w ≠ 0) :
       ‖∫ t in a..b, Complex.exp ((w : ℂ) * Complex.I * t)‖ ≤ 2 / |w| := by
   …

2. theorem OAI.FiniteFactor.sourceAngle_fourier_le line 24

   Source documentation

   The actual normalized angle interval, before reducing phases modulo one.

   theorem sourceAngle_fourier_le (i : SourceCoordinate) (w : ℝ) (hw : w ≠ 0) :
       ‖∫ t, Complex.exp ((w : ℂ) * Complex.I * t) ∂sourceAngleMarginal i‖ ≤
         2 / (sourceAngleUnit i * |w|) := by
   …

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

3. theorem OAI.FiniteFactor.fourier_fract line 40

   Source documentation

   Integer frequencies do not see the integer part of a phase.

   theorem fourier_fract (v : ℤ) (t : ℝ) :
       Complex.exp (2 * Real.pi * Complex.I * ((v : ℂ) * (Int.fract t : ℝ))) =
         Complex.exp (2 * Real.pi * Complex.I * ((v : ℂ) * (t : ℂ))) := by
   …

4. theorem OAI.FiniteFactor.pair_fourier_fract line 53

   Source documentation

   The two actual phases have the Fourier transform of the combined frequency.

   theorem pair_fourier_fract (v v' : ℤ) (n n' t : ℝ) :
       Complex.exp (2 * Real.pi * Complex.I *
         ((v : ℂ) * (Int.fract (n*t) : ℝ) + (v' : ℂ) * (Int.fract (n'*t) : ℝ))) =
       Complex.exp (((2 * Real.pi * ((v : ℝ)*n + (v' : ℝ)*n') : ℝ) : ℂ) * Complex.I * t) := by
   …

5. theorem OAI.FiniteFactor.sourceAngle_pair_fourier_le line 62