OAI/Probability/SKRatio/Variational/ScalarMonotone.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Scalar.covariance_nonpos_of_pairwise line 14
2. def OAI.SKRatio.Scalar.likelihood line 44
3. lemma OAI.SKRatio.Scalar.continuous_likelihood line 47
4. lemma OAI.SKRatio.Scalar.likelihood_pos line 51
5. lemma OAI.SKRatio.Scalar.fieldLaw_withDensity_likelihood line 54
6. lemma OAI.SKRatio.Scalar.integral_likelihood line 66
7. lemma OAI.SKRatio.Scalar.likelihood_integrable_iff line 75
8. lemma OAI.SKRatio.Scalar.integral_mul_likelihood line 82
9. lemma OAI.SKRatio.Scalar.likelihood_mono_sq line 89
10. lemma OAI.SKRatio.Scalar.integral_temperature_antitone line 100
11. lemma OAI.SKRatio.Scalar.m_mono line 116
12. lemma OAI.SKRatio.Scalar.m_nonneg line 123
13. lemma OAI.SKRatio.Scalar.m_abs_sq line 127
14. lemma OAI.SKRatio.Scalar.m_sq_mono_sq line 133
15. lemma OAI.SKRatio.Scalar.a_temperature_antitone line 138
16. def OAI.SKRatio.Scalar.signMeanG line 145
17. def OAI.SKRatio.Scalar.gSignFactor line 147
18. lemma OAI.SKRatio.Scalar.gSignFactor_denom line 149
19. lemma OAI.SKRatio.Scalar.continuous_gSignFactor line 154
20. lemma OAI.SKRatio.Scalar.gSignFactor_abs_le line 158
21. lemma OAI.SKRatio.Scalar.memLp_gSignFactor line 164
22. lemma OAI.SKRatio.Scalar.g_sign_expansion line 168
23. lemma OAI.SKRatio.Scalar.signMeanG_expansion line 180
24. lemma OAI.SKRatio.Scalar.memLp_signMeanG line 185
25. lemma OAI.SKRatio.Scalar.G_eq_signMeanG line 197
26. lemma OAI.SKRatio.Scalar.signMeanG_antitone_sq line 213
27. lemma OAI.SKRatio.Scalar.G_temperature_antitone line 229