OAI/Analysis/FourierLLogL/Finite/Quadratic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Law.sq_Ex_le line 12
2. lemma OAI.FourierLLogL.Law.sq_Ex_mul line 25
3. lemma OAI.FourierLLogL.Law.sq_Ex line 29
4. lemma OAI.FourierLLogL.Law.quadratic_minkowski line 33
5. lemma OAI.FourierLLogL.Law.sq_Cx_norm line 49