OAI/Probability/LogConcave/Dynamics/NormSubSqThree.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.Coupling.norm_sub_sq_three line 15
2. theorem OAI.LogConcaveSampling.Coupling.SquaredAt.trans line 19
3. lemma OAI.LogConcaveSampling.Coupling.SquaredAt.same_tape line 68