OAI/NumberTheory/DirichletL/Inversion/InitialDyadicAssembly.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.InverseInitialDyadicAssembly.Windows line 18
  2. def OAI.SevenEighths.InverseInitialDyadicAssembly.exponent line 20
  3. def OAI.SevenEighths.InverseInitialDyadicAssembly.cutoff line 22
  4. def OAI.SevenEighths.InverseInitialDyadicAssembly.weight line 24
  5. theorem OAI.SevenEighths.InverseInitialDyadicAssembly.exponent_scale line 27
  6. theorem OAI.SevenEighths.InverseInitialDyadicAssembly.weight_partition line 31
  7. theorem OAI.SevenEighths.InverseInitialDyadicAssembly.weight_eq_cutoff line 41
  8. def OAI.SevenEighths.InverseInitialDyadicAssembly.sourceNorms line 50
  9. theorem OAI.SevenEighths.InverseInitialDyadicAssembly.source_weight_cutoff line 54
  10. theorem OAI.SevenEighths.InverseInitialDyadicAssembly.sourceNorms_one_le line 62
  11. theorem OAI.SevenEighths.InverseInitialDyadicAssembly.physicalBlock_partition line 79
  12. theorem OAI.SevenEighths.InverseInitialDyadicAssembly.physicalBlock_window_partition line 102