OAI/NumberTheory/Ostmann/Characters/SparsePolydiscBlocks.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform side and lower bounds on the complex parameter polydisc

  1. def OAI.Ostmann.polydiscSparseScalar line 10
  2. def OAI.Ostmann.polydiscSparseSide line 15
  3. def OAI.Ostmann.polydiscSparseLower line 20
  4. theorem OAI.Ostmann.polydiscSparseSide_norm_le line 25
  5. theorem OAI.Ostmann.polydiscSparseLower_norm_le line 56