OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/BilinearPart.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SourcePrimeFactor.bilinearPart line 22
2. lemma OAI.SourcePrimeFactor.continuous_weightedFunction line 26
3. theorem OAI.SourcePrimeFactor.cofactor_polynomial_integral line 31
4. theorem OAI.SourcePrimeFactor.bilinearPart_integral line 43
5. theorem OAI.SourcePrimeFactor.norm_bilinearPart_integral_le line 57