OAI/Probability/SKGap/Localization/LocalVolumeChange.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.map_affine_matrix_volume line 13
2. lemma OAI.SKGap.affine_set_lintegral_le line 22
3. lemma OAI.SKGap.gaussian_standard_density line 39
4. lemma OAI.SKGap.gaussian_tilt_cancellation line 50
5. theorem OAI.SKGap.local_volume_change_of_variables line 67
6. lemma OAI.SKGap.conditional_lintegral_identity line 100
7. lemma OAI.SKGap.whitening_logdet line 107
8. def OAI.SKGap.localAction line 120
9. def OAI.SKGap.localVolume line 124
10. lemma OAI.SKGap.localAction_continuous line 129
11. theorem OAI.SKGap.local_volume_quantitative line 137