OAI/NumberTheory/Ostmann/Arithmetic/IdealHistoryNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The norm of the idealized arithmetic history expansion

Both sets of residue variables retain their original independent Haar laws. The smooth amplitude may depend on every coordinate.

  1. def OAI.Ostmann.idealHistoryNorm line 17
  2. theorem OAI.Ostmann.idealHistoryNorm_le line 29
  3. theorem OAI.Ostmann.ideal_history_norm_rate line 46