OAI/Probability/SKGap/Localization/ConditionalWeight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.SKGap.conditionalGoeLaw_probability line 12
2. lemma OAI.SKGap.conditionalFieldWeight_le_one line 17
3. lemma OAI.SKGap.conditionalFieldWeight_of_real_bound line 21
4. lemma OAI.SKGap.measurable_scalarIntegrand line 28
5. lemma OAI.SKGap.scalar_density_prefactor_le_one line 35
6. lemma OAI.SKGap.scalarIntegrand_nonneg line 44
7. lemma OAI.SKGap.scalar_weighted_density_bound line 48