OAI/NumberTheory/Ostmann/QuadraticCenter/PositiveFrequencyEnvelope.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.positive_array_divisor_weight_sum line 11
2. def OAI.Ostmann.QuadraticCenter.positiveArrayEnvelope line 20
3. theorem OAI.Ostmann.QuadraticCenter.positiveArrayEnvelope_nonneg line 24
4. theorem OAI.Ostmann.QuadraticCenter.envelope_jacobi_norm line 31
5. theorem OAI.Ostmann.QuadraticCenter.positiveDivisorArray_norm_envelope line 34