OAI/Probability/SKRatio/Variational/ScalarEnvelope.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKRatio.Scalar.endpointK line 11
2. def OAI.SKRatio.Scalar.endpointD line 13
3. def OAI.SKRatio.Scalar.endpointDPrime line 15
4. lemma OAI.SKRatio.Scalar.integrable_K_integrand line 18
5. lemma OAI.SKRatio.Scalar.D_integrand_pos line 35
6. lemma OAI.SKRatio.Scalar.D_integrand_le_two line 38
7. lemma OAI.SKRatio.Scalar.integrable_D_integrand line 51
8. lemma OAI.SKRatio.Scalar.integrable_DPrime_integrand line 58
9. lemma OAI.SKRatio.Scalar.endpointK_quadratic line 71
10. lemma OAI.SKRatio.Scalar.resolvent_quadratic line 93
11. lemma OAI.SKRatio.Scalar.endpointD_quadratic line 106
12. lemma OAI.SKRatio.Scalar.endpointD_field line 144
13. lemma OAI.SKRatio.Scalar.endpointK_field line 151
14. lemma OAI.SKRatio.Scalar.envelope_of_endpoint_data line 162