OAI/Analysis/FourierLLogL/Finite/Complex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Complex moments

  1. def OAI.FourierLLogL.Law.Cx line 12
  2. lemma OAI.FourierLLogL.Law.Cx_ofReal line 14
  3. lemma OAI.FourierLLogL.Law.re_Cx line 17
  4. lemma OAI.FourierLLogL.Law.Cx_mul line 21
  5. lemma OAI.FourierLLogL.Law.Cx_lmul line 24
  6. lemma OAI.FourierLLogL.Law.Cx_conj line 27
  7. lemma OAI.FourierLLogL.Law.Cx_norm line 30
  8. lemma OAI.FourierLLogL.Law.norm_Cx_unit line 36
  9. lemma OAI.FourierLLogL.Law.Cx_swap line 39
  10. lemma OAI.FourierLLogL.Law.Ex_swap line 46
  11. lemma OAI.FourierLLogL.Law.Cx_prod line 53
  12. lemma OAI.FourierLLogL.Law.sq_norm_Cx line 58
  13. lemma OAI.FourierLLogL.Law.Ex_exp line 67