OAI/Analysis/FourierLLogL/Thermal/Order.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Comparisons in form order

  1. lemma OAI.FourierLLogL.Dyadic.Thermal.K_add line 15
  2. lemma OAI.FourierLLogL.Dyadic.Thermal.ex_tilt line 20
  3. lemma OAI.FourierLLogL.Dyadic.Thermal.ex_untilt line 25
  4. lemma OAI.FourierLLogL.Dyadic.Thermal.boltz_mean line 29
  5. lemma OAI.FourierLLogL.Dyadic.Thermal.cred_add_mono line 33
  6. lemma OAI.FourierLLogL.Dyadic.Thermal.cred_mono line 45
  7. lemma OAI.FourierLLogL.Dyadic.Thermal.F_increment line 50
  8. lemma OAI.FourierLLogL.Dyadic.Thermal.mean_energy line 60
  9. lemma OAI.FourierLLogL.Dyadic.Thermal.cred_cost line 68
  10. lemma OAI.FourierLLogL.Dyadic.Thermal.form_energy_mono line 72
  11. lemma OAI.FourierLLogL.Dyadic.Thermal.q_express line 79
  12. lemma OAI.FourierLLogL.Dyadic.Thermal.q_compare line 83
  13. def OAI.FourierLLogL.Dyadic.Thermal.delta line 89
  14. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_sq line 91
  15. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_zero line 96
  16. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_even line 100
  17. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_mono line 107
  18. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_triangle line 113
  19. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_nsmul line 122
  20. lemma OAI.FourierLLogL.Dyadic.Thermal.delta_int line 130