OAI/NumberTheory/Ostmann/Characters/CharacterDiagonalBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.character_anchor_diagonal_small line 11

   Source documentation

   The bulk normalization costs log 2 + log z, while the prescribed gap contains 20 log z. The same choice of B works at every fixed depth.

   theorem character_anchor_diagonal_small
       (B B₁ C z m gap energy prefactor : ℝ) (n : ℕ)
       (hz : 1 ≤ z) (hm : 0 ≤ m)
       (hB : 2 * B₁ + C + Real.log 2 + 6 ≤ B)
       (hgap : (B + 20 * Real.log z - 1) * (2 ^ n : ℕ) * m ≤ gap)
       (henergy : energy ≤ C * (2 ^ n : ℕ) * m)
       (hprefactor : prefactor ≤ Real.exp ((2 ^ n : ℕ) * m)) :
       Real.exp (-gap) * prefactor *
         Real.exp ((Real.log 2 + Real.log z) * (2 ^ n : ℕ) * m + energy) ≤
           Real.exp (-(2 * B₁ + 4) * (2 ^ n : ℕ) * m) := by
   …

2. theorem OAI.Ostmann.character_diagonal_sum_small line 37

   Source documentation

   Two independently bounded parts of the literal diagonal fit the one-unit reserve in the amplitude recurrence.

   theorem character_diagonal_sum_small (a b B m : ℝ) (n : ℕ) (hm : 1 ≤ m)
       (ha : a ≤ Real.exp (-(2 * B + 4) * (2 ^ n : ℕ) * m))
       (hb : b ≤ Real.exp (-(2 * B + 4) * (2 ^ n : ℕ) * m)) :
       a + b ≤ Real.exp (-(2 * B + 3) * (2 ^ n : ℕ) * m) := by
   …