OAI/Analysis/FiniteFactor/CrossedProduct/FutureBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceNextCutoff_ge_square line 13

   Source documentation

   The exact recursive cutoff is at least m_j squared, giving vanishing future boundary loss rather than merely geometric cutoff growth.

   theorem sourceNextCutoff_ge_square (m : ℕ) (hm : 100 ≤ m) :
       (m : ℝ)^2 ≤ (sourceNextCutoff m : ℝ) := by
   …

   Mentions: OAI.FiniteFactor.sourceNextCutoff

2. theorem OAI.FiniteFactor.sourceCutoff_ratio_tendsto line 21
3. theorem OAI.FiniteFactor.sourceFutureBudget_tendsto line 37