OAI/Probability/FreeIsing/Estimates/ThresholdArithmetic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.branching_pos line 9
2. lemma OAI.Problem367.threshold_sqrt_pos line 13
3. lemma OAI.Problem367.threshold_iff_branching_sq line 17
4. lemma OAI.Problem367.threshold_lt_iff_branching_sq_lt line 31
5. lemma OAI.Problem367.tanh_nonneg_of_beta_nonneg line 45
6. lemma OAI.Problem367.tanh_mem_Ico_of_beta_nonneg line 50
7. lemma OAI.Problem367.tanh_threshold_iff_branching_sq line 54