OAI/Analysis/FourierLLogL/Thermal/Ginibre.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Cosine covariance. On an even cyclic group the two-copy change of variables

uses two branches (one of them half-translated).

  1. lemma OAI.FourierLLogL.Dyadic.Thermal.chi_one_ne line 15
  2. lemma OAI.FourierLLogL.Dyadic.Thermal.odd_phase line 23
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.ch_parity line 31
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.c_parity line 43
  5. lemma OAI.FourierLLogL.Dyadic.Thermal.r_parity line 55
  6. def OAI.FourierLLogL.Dyadic.Thermal.dblmean line 61
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.dbl_ex line 62
  8. def OAI.FourierLLogL.Dyadic.Thermal.branch line 65
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.branch_eq line 68
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.branch_sum line 79
  11. def OAI.FourierLLogL.Dyadic.Thermal.halfWave line 91
  12. def OAI.FourierLLogL.Dyadic.Thermal.unitWave line 94
  13. lemma OAI.FourierLLogL.Dyadic.Thermal.half_mul line 96
  14. lemma OAI.FourierLLogL.Dyadic.Thermal.branch_waves line 101
  15. def OAI.FourierLLogL.Dyadic.Thermal.bil line 121
  16. def OAI.FourierLLogL.Dyadic.Thermal.pairPot line 124
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.bil_sum line 127
  18. lemma OAI.FourierLLogL.Dyadic.Thermal.dblmean_scale line 131
  19. lemma OAI.FourierLLogL.Dyadic.Thermal.bil_scale line 135
  20. lemma OAI.FourierLLogL.Dyadic.Thermal.pair_nonneg line 141
  21. lemma OAI.FourierLLogL.Dyadic.Thermal.pair_exp_nonneg line 165
  22. lemma OAI.FourierLLogL.Dyadic.Thermal.branch_pos line 178
  23. theorem OAI.FourierLLogL.Dyadic.Thermal.ginibre line 212