OAI/NumberTheory/Ostmann/Construction/DiagonalTransformBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Construction.halfTransform_eq_of_value_perm line 14
2. def OAI.Ostmann.Construction.diagonalSmallMultiplier line 25
3. lemma OAI.Ostmann.Construction.diagonalSmallMultiplier_nonneg line 30
4. lemma OAI.Ostmann.Construction.complex_list_prod_norm_sq line 37
5. theorem OAI.Ostmann.Construction.halfTransform_norm_sq_le_smallMultiplier line 43
6. theorem OAI.Ostmann.Construction.remaining_giant_eq_of_product_eq_of_mass line 59
7. theorem OAI.Ostmann.Construction.remaining_halfTransform_eq_of_mass_product line 79