OAI/Probability/SKRatio/Variational/ScalarInterpolation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Scalar.G_nonneg line 11
2. lemma OAI.SKRatio.Scalar.l_temperature_monotone line 16
3. lemma OAI.SKRatio.Scalar.memLp_F_other line 20
4. lemma OAI.SKRatio.Scalar.F_sub_F line 28
5. lemma OAI.SKRatio.Scalar.sd_F_difference line 34
6. lemma OAI.SKRatio.Scalar.abs_sub_le_interval line 70
7. lemma OAI.SKRatio.Scalar.temp_a_ratio_bounds line 74
8. lemma OAI.SKRatio.Scalar.temp_G_bounds line 88
9. def OAI.SKRatio.Scalar.crossBound line 94
10. theorem OAI.SKRatio.Scalar.sd_F_interval line 100
11. def OAI.SKRatio.Scalar.slackBound₀ line 133
12. def OAI.SKRatio.Scalar.slackBound₁ line 136
13. theorem OAI.SKRatio.Scalar.U₁_interval line 139
14. lemma OAI.SKRatio.Scalar.coherent_a_slack_mono line 149
15. theorem OAI.SKRatio.Scalar.U₀_interval line 156