OAI/NumberTheory/DirichletL/Detector/GramAnnularLattice.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProbeGramAnnularLattice.AnnularSupport line 13
  2. theorem OAI.ProbeGramAnnularLattice.scaled_embedding_norm_sq line 17
  3. theorem OAI.ProbeGramAnnularLattice.physical_sample_eq_zero line 21
  4. def OAI.ProbeGramAnnularLattice.cauchyWeight line 42
  5. theorem OAI.ProbeGramAnnularLattice.cauchyWeight_summable line 44
  6. theorem OAI.ProbeGramAnnularLattice.cauchyWeight_mass_le line 48
  7. theorem OAI.ProbeGramAnnularLattice.physical_subunit_majorant line 51
  8. theorem OAI.ProbeGramAnnularLattice.physical_subunit_bound line 70
  9. theorem OAI.ProbeGramAnnularLattice.annular_lattice_bound line 90
  10. theorem OAI.ProbeGramAnnularLattice.weighted_summable line 133
  11. theorem OAI.ProbeGramAnnularLattice.annular_weighted_lattice_bound line 142