OAI/NumberTheory/Ostmann/Construction/DiagonalGapBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The diagonal exponent and the parameter order in (7.1), (9.6)–(9.8)

  1. def OAI.Ostmann.spectatorBaseGap line 11
  2. def OAI.Ostmann.spectatorStepGap line 13
  3. theorem OAI.Ostmann.spectator_diagonal_exponent line 16
  4. theorem OAI.Ostmann.spectator_diagonal_exponent_bound line 23
  5. theorem OAI.Ostmann.bad_diagonal_reserve line 37
  6. theorem OAI.Ostmann.two_diagonal_terms_le line 63

    Source documentation

    One unit of exponential reserve absorbs both nonnegative contributions.

    theorem two_diagonal_terms_le (bad good B t : ℝ) (ht : Real.log 2 ≤ t)
    (hbad : bad ≤ Real.exp (-(2 * B + 4) * t))
    (hgood : good ≤ Real.exp (-(2 * B + 4) * t)) :
    bad + good ≤ Real.exp (-(2 * B + 3) * t) := by
…