OAI/Analysis/FiniteFactor/CrossedProduct/PhaseFirst.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.phase_threshold_of_abs line 12

   Source documentation

   Fractional-part threshold in the small phase range, with both signs.

   theorem phase_threshold_of_abs {a t : ℝ} (ha : 0 < a) (ha4 : a ≤ 1/4)
       (hlo : a ≤ |t|) (hhi : |t| ≤ 1/2) :
       1 - Int.fract t ∈ Set.Icc a (1-a) := by
   …

2. theorem OAI.FiniteFactor.SourceAngles.first_phase line 27

   Source documentation

   Phase bounds for every stage and realization. There is no eventual-stage or probabilistic assumption.

   theorem SourceAngles.first_phase {θ : SourceCoordinate → ℝ} (hθ : SourceAngles θ)
       (s : ℕ) (k : ℤ)
       (hlo : (sourceStageState s).G * (sourceStageState s).K ≤ |(k : ℝ)|)
       (hhi : |(k : ℝ)| ≤ ((sourceBlockSize s : ℝ) * (sourceStageState s).K)/4)
       (i : Fin (sourceBlockSize s)) :
       1 - Int.fract ((k : ℝ)*θ ⟨s,i⟩) ∈
         Set.Icc ((sourceStageState s).G/(sourceBlockSize s : ℝ))
           (1-(sourceStageState s).G/(sourceBlockSize s : ℝ)) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.SourceAngles, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.sourceBlockSize