OAI/NumberTheory/Ostmann/Characters/InitialCharacterStatisticDouble.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.characterDoubleShell line 12
  2. def OAI.Ostmann.Characters.characterDoubleChar line 15
  3. def OAI.Ostmann.Characters.characterDoubleCenter line 19
  4. def OAI.Ostmann.Characters.characterDoublePhase line 22
  5. def OAI.Ostmann.Characters.characterDoubleMask line 25
  6. def OAI.Ostmann.Characters.characterTupleSplit line 29
  7. theorem OAI.Ostmann.Characters.characterDoubleShell_positive line 39
  8. theorem OAI.Ostmann.Characters.characterDoublePrior_mass line 46
  9. theorem OAI.Ostmann.Characters.characterDoubleTest_eq line 54
  10. theorem OAI.Ostmann.Characters.characterDoubleMean_eq_norm_sq line 66