OAI/Probability/FreeIsing/Estimates/SupercriticalProfile.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.SupercriticalProfile.dual line 9
  2. def OAI.Problem367.SupercriticalProfile.rate line 11
  3. def OAI.Problem367.SupercriticalProfile.mixture line 13
  4. def OAI.Problem367.SupercriticalProfile.profile line 16
  5. lemma OAI.Problem367.SupercriticalProfile.dual_pos line 19
  6. lemma OAI.Problem367.SupercriticalProfile.dual_lt line 24
  7. lemma OAI.Problem367.SupercriticalProfile.rate_sub_theta line 30
  8. lemma OAI.Problem367.SupercriticalProfile.rate_sub_dual line 36
  9. lemma OAI.Problem367.SupercriticalProfile.rate_sub_dual_pos line 42
  10. lemma OAI.Problem367.SupercriticalProfile.mixture_nonneg line 49
  11. lemma OAI.Problem367.SupercriticalProfile.mixture_lt_one line 58
  12. lemma OAI.Problem367.SupercriticalProfile.profile_zero_pos line 65
  13. lemma OAI.Problem367.SupercriticalProfile.profile_le_power line 70
  14. lemma OAI.Problem367.SupercriticalProfile.profile_nonneg line 77
  15. lemma OAI.Problem367.SupercriticalProfile.profile_root line 91
  16. lemma OAI.Problem367.SupercriticalProfile.theta_quadratic line 99
  17. lemma OAI.Problem367.SupercriticalProfile.dual_quadratic line 104
  18. lemma OAI.Problem367.SupercriticalProfile.power_recurrence line 110
  19. lemma OAI.Problem367.SupercriticalProfile.profile_recurrence line 120
  20. lemma OAI.Problem367.SupercriticalProfile.rate_gap line 128
  21. lemma OAI.Problem367.SupercriticalProfile.rate_gt_tree_rate line 136