OAI/Probability/FreeIsing/Gaussian/Attenuation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem367.GaussianAttenuation.tanh_strictMono line 13
2. lemma OAI.Problem367.GaussianAttenuation.tanh_abs line 19
3. lemma OAI.Problem367.GaussianAttenuation.attenuation_sq_le_one line 28
4. lemma OAI.Problem367.GaussianAttenuation.integrable_attenuation_sq line 34
5. theorem OAI.Problem367.GaussianAttenuation.integral_attenuation_sq_le line 44
6. theorem OAI.Problem367.GaussianAttenuation.integral_attenuation_sq_le_of_hasLaw line 68
7. theorem OAI.Problem367.GaussianAttenuation.exists_uniform_attenuation_gap line 79
8. theorem OAI.Problem367.GaussianAttenuation.integral_shifted_attenuation_sq_mul_le line 95
9. theorem OAI.Problem367.GaussianAttenuation.integral_shifted_attenuation_sq_mul_le_of_indepFun line 135