OAI/Probability/RadialTransition/DeletedInteractions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RadialTransition.pairGrand_grid_perturbation line 16
2. def OAI.RadialTransition.deletedPair line 62
3. lemma OAI.RadialTransition.measurable_deletedPair line 66
4. lemma OAI.RadialTransition.deletedPair_symm line 75
5. lemma OAI.RadialTransition.continuous_deletedPair_cell line 79
6. def OAI.RadialTransition.deletionMajorant line 96
7. lemma OAI.RadialTransition.deletionMajorant_nonneg line 99
8. theorem OAI.RadialTransition.deletedPair_grid_bound line 103