OAI/Analysis/FiniteFactor/CrossedProduct/PhaseCount.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourceBlockCoordinates line 12
2. theorem OAI.FiniteFactor.sourceBlockCoordinates_card line 15
3. theorem OAI.FiniteFactor.mem_sourceBlockCoordinates line 18
4. def OAI.FiniteFactor.sourcePhaseMissSet line 23
5. theorem OAI.FiniteFactor.sourcePhaseMissSet_measurable line 26
6. def OAI.FiniteFactor.sourceFewPhases line 30
7. def OAI.FiniteFactor.sourceMissCount line 34
8. theorem OAI.FiniteFactor.sourceFewPhases_subset_misses line 36
9. theorem OAI.FiniteFactor.sourceFewPhases_probability line 55

   Source documentation

   The fixed-power failure probability in Proposition phases, for the actual angle product measure. The ceiling records the exact finite counting step.

   theorem sourceFewPhases_probability (s : ℕ) (k : ℤ)
       (hk : ((sourceBlockSize s : ℝ)*(sourceStageState s).K)/4 ≤ |(k : ℝ)|) :
       sourceAngleLaw (sourceFewPhases s k) ≤
         (2 : ℝ≥0∞)^sourceBlockSize s *
           (ENNReal.ofReal (10*sourceWidth s 1))^sourceMissCount s := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.sourceStageState, OAI.FiniteFactor.sourceAngleLaw, OAI.FiniteFactor.sourceFewPhases, OAI.FiniteFactor.sourceWidth, OAI.FiniteFactor.sourceMissCount