OAI/Probability/LogConcave/LowerBounds/FrameTransport.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.LowerBound.frameTransport line 18
2. lemma OAI.LogConcaveSampling.LowerBound.measurable_frameTransport line 21
3. lemma OAI.LogConcaveSampling.LowerBound.frameCompletion_apply line 30
4. lemma OAI.LogConcaveSampling.LowerBound.frameCompletion_eq_transport line 35
5. lemma OAI.LogConcaveSampling.LowerBound.frameTransport_swap line 42
6. lemma OAI.LogConcaveSampling.LowerBound.frameCompletion_symm_eq_transport line 50
7. lemma OAI.LogConcaveSampling.LowerBound.frameTransport_preimage_mem line 58
8. lemma OAI.LogConcaveSampling.LowerBound.extendFrame_relative_mem line 68
9. def OAI.LogConcaveSampling.LowerBound.CompatibleFrames line 74
10. lemma OAI.LogConcaveSampling.LowerBound.compatibleFrames_reconstruct line 77
11. lemma OAI.LogConcaveSampling.LowerBound.compatibleFrames_inverseUpdate line 87
12. lemma OAI.LogConcaveSampling.LowerBound.compatibleFrames_forwardUpdate line 92
13. lemma OAI.LogConcaveSampling.LowerBound.subspaceStabilizer_anti line 97
14. lemma OAI.LogConcaveSampling.LowerBound.compatibleFrames_mono line 102
15. lemma OAI.LogConcaveSampling.LowerBound.compatibleFrames_trans line 106