OAI/Probability/SKRatio/Variational/ScalarDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Scalar.field_pdf_ratio line 11
2. def OAI.SKRatio.Scalar.densityFactor line 23
3. lemma OAI.SKRatio.Scalar.densityFactor_pos line 25
4. lemma OAI.SKRatio.Scalar.field_pdf_le_factor line 28
5. lemma OAI.SKRatio.Scalar.densityFactor_mono_left line 42
6. lemma OAI.SKRatio.Scalar.fieldLaw_le_factor line 53
7. lemma OAI.SKRatio.Scalar.fieldLaw_le_interval_factor line 66
8. lemma OAI.SKRatio.Scalar.sd_temperature_bound line 73
9. lemma OAI.SKRatio.Scalar.sd_temperature_interval_bound line 79