OAI/NumberTheory/Ostmann/Construction/TransferIteration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.half_exponential_square line 13
2. theorem OAI.Ostmann.transfer_half_lower line 26
3. theorem OAI.Ostmann.transfer_iteration_lower line 48

   Source documentation

   The reserve comes from the initial bound. The loss c + log 2 is counted by the exact geometric multiplicity 2^j-1.

   theorem transfer_iteration_lower (η : ℕ → ℂ) (D : ℕ → ℝ)
       (Bstar m c : ℝ) (hm : 0 ≤ m) (hbudget : c + Real.log 2 ≤ m)
       (hzero : Real.exp (-Bstar * m) ≤ ‖η 0‖)
       (hD : ∀ j, D j ≤ Real.exp (-(2 * (Bstar + 3) + 3) * (2 : ℝ) ^ j * m))
       (htransfer : ∀ j, Real.exp (-c) * ‖η j‖ ^ 2 ≤ D j + ‖η (j + 1)‖) :
       ∀ j, Real.exp (-((2 : ℝ) ^ j * Bstar * m +
         ((2 : ℝ) ^ j - 1) * (c + Real.log 2))) ≤ ‖η j‖ := by
   …