OAI/Probability/SKValue/Coercivity/Coercivity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValue.Certificate.Q line 9
2. def OAI.SKValue.Certificate.T line 11
3. def OAI.SKValue.Certificate.F₂ line 12
4. def OAI.SKValue.Certificate.W₂ line 16
5. def OAI.SKValue.Certificate.remainder line 25
6. theorem OAI.SKValue.Certificate.rational_identity line 35
7. theorem OAI.SKValue.Certificate.pointwise_coercivity line 48
8. lemma OAI.SKValue.Certificate.growth_F line 83
9. lemma OAI.SKValue.Certificate.growth_W line 91
10. lemma OAI.SKValue.Certificate.flux_derivative line 109