OAI/Analysis/FiniteFactor/CrossedProduct/PhaseDecay.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.sourcePhaseFailureMajorant line 12

   Source documentation

   An explicit majorant for the positive-power union bound.

   def sourcePhaseFailureMajorant (s : ℕ) : ℝ :=
   …

2. theorem OAI.FiniteFactor.phaseFailureMajorant_le line 16
3. theorem OAI.FiniteFactor.sourceBlockSize_tendsto line 40
4. theorem OAI.FiniteFactor.sourcePhaseFailureMajorant_eventually line 48
5. theorem OAI.FiniteFactor.sourceBlockSize_inverseSquare_summable line 58

   Source documentation

   The reciprocal-square majorant is summable from m_s >= 2^(s+1).

   theorem sourceBlockSize_inverseSquare_summable :
       Summable (fun s => (sourceBlockSize s : ℝ)^(-2 : ℝ)) := by
   …

   Mentions: OAI.FiniteFactor.sourceBlockSize

6. theorem OAI.FiniteFactor.sourcePhaseFailureMajorant_summable line 74