OAI/Probability/PosteriorReplicas/Geometry/DensityBinEnvelope.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PosteriorReplicas.expectedDensity line 12
2. lemma OAI.PosteriorReplicas.measurable_expectedDensity line 16
3. def OAI.PosteriorReplicas.binEnvelope line 21
4. lemma OAI.PosteriorReplicas.measurable_binEnvelope line 24
5. lemma OAI.PosteriorReplicas.ae_expectedDensity_le_inverse line 29
6. lemma OAI.PosteriorReplicas.ae_constrainedRows_mem line 59
7. lemma OAI.PosteriorReplicas.ae_equalReference_bin_bound line 70
8. lemma OAI.PosteriorReplicas.binTerm_volume line 84
9. lemma OAI.PosteriorReplicas.normalized_binEnvelope_integral_le line 96