OAI/Analysis/FiniteFactor/CrossedProduct/Phases.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourcePhaseUpper line 11
2. def OAI.FiniteFactor.sourcePhaseLower line 14
3. def OAI.FiniteFactor.sourcePhaseFailure line 17
4. theorem OAI.FiniteFactor.sourcePhaseFailure_bound line 21
5. theorem OAI.FiniteFactor.sourcePhaseFailure_finite line 55
6. theorem OAI.FiniteFactor.sourcePhaseMissSet_natAbs line 65
7. theorem OAI.FiniteFactor.sourceAngleLaw_second_phases line 77

   Source documentation

   Proposition phases, assertion 2, for all signed integer powers at every sufficiently late stage on one probability-one event.

   theorem sourceAngleLaw_second_phases : ∀ᵐ θ ∂sourceAngleLaw,
       ∀ᶠ s in atTop, ∀ k : ℤ, sourcePhaseLower s ≤ |(k : ℝ)| →
         |(k : ℝ)| ≤ sourcePhaseUpper s →
         (sourceBlockSize s : ℝ)/20 ≤
           (((sourceBlockCoordinates s).filter (fun i => θ i ∉ sourcePhaseMissSet s k)).card : ℝ) := by
   …

   Mentions: OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourcePhaseLower, OAI.FiniteFactor.sourcePhaseUpper, OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceBlockCoordinates, OAI.FiniteFactor.sourcePhaseMissSet