OAI/NumberTheory/Ostmann/Characters/CharacterHBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.character_H_card_le line 11
2. theorem OAI.Ostmann.character_H_sum line 20
3. theorem OAI.Ostmann.character_H_product_bounds line 34

   Source documentation

   A bounded error per selected atom costs only a constant depending on the fixed depth, not on the number of primes in the word.

   theorem character_H_product_bounds {k n : ℕ} (hn : n < k)
       (w : CharacterRole k → ℝ) (lo hi : CharacterRole k → ℕ)
       (c : ℝ) (hc : 0 ≤ c)
       (hlo : ∀ i, Real.exp (w i - c) ≤ lo i)
       (hhi : ∀ i, (hi i : ℝ) ≤ Real.exp (w i + c)) :
       let T := (2 : ℝ) ^ n * w (true, none) +
   …

   Mentions: OAI.Ostmann.CharacterRole