OAI/Probability/FreeIsing/Critical/CanonicalRowEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.CriticalCanonicalRowEnergy.rate line 18
  2. theorem OAI.Problem367.CriticalCanonicalRowEnergy.rate_pos line 22
  3. theorem OAI.Problem367.CriticalCanonicalRowEnergy.branching_ratio line 34
  4. theorem OAI.Problem367.CriticalCanonicalRowEnergy.ratio_lt_one line 39
  5. theorem OAI.Problem367.CriticalCanonicalRowEnergy.exp_div_one_sub_exp_le_inv line 46
  6. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_rootResponse_critical_radial_bound line 61
  7. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_rootResponse_critical_row_energy line 73
  8. theorem OAI.Problem367.HasFreeIsingLaw.integral_gaussian_rootResponse_row_le_inv_rate line 96
  9. theorem OAI.Problem367.HasFreeIsingLaw.gaussian_rootResponse_critical_row_tail line 111
  10. theorem OAI.Problem367.HasFreeIsingLaw.lintegral_gaussian_rootResponse_row_le_inv_rate line 128
  11. theorem OAI.Problem367.HasFreeIsingLaw.brownian_rootResponse_critical_row_energy line 147