OAI/NumberTheory/Ostmann/Construction/VariableTransferIteration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.half_sq_exp line 12
2. theorem OAI.Ostmann.variable_transfer_iteration line 21

   Source documentation

   Summing the actual losses before using the geometric reserve avoids a uniform per-step loss assumption. The endpoint is finite, as in the paper.

   theorem variable_transfer_iteration (k : ℕ) (η : ℕ → ℂ) (diag d : ℕ → ℝ)
       (B₀ m : ℝ) (hm : 0 ≤ m) (hd : ∀ j < k, 0 ≤ d j)
       (hbudget : ∑ j ∈ Finset.range k, (d j + Real.log 2) ≤ m)
       (hzero : Real.exp (-B₀ * m) ≤ ‖η 0‖)
       (hdiag : ∀ j < k, diag j ≤ Real.exp (-(2 * (B₀ + 1) + 3) * (2 : ℝ) ^ j * m))
       (htransfer : ∀ j < k, Real.exp (-d j) * ‖η j‖ ^ 2 ≤ diag j + ‖η (j + 1)‖) :
       ∀ j ≤ k, Real.exp (-(B₀ + 1) * (2 : ℝ) ^ j * m) ≤ ‖η j‖ := by
   …