OAI/NumberTheory/Ostmann/Quadratic/QuadraticOddWeightPoisson.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite odd smoothing sum equals its original first Poisson transform

  1. theorem OAI.Ostmann.quadratic_integer_weight_finite line 12
  2. theorem OAI.Ostmann.quadratic_odd_kernel_poisson line 57