OAI/Dynamics/StandardMap/ObservationTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.transferStep_difference_bound line 11
2. lemma OAI.StandardMapEntropy.transferProduct_difference_bound line 20
3. lemma OAI.StandardMapEntropy.log_lipschitz_above_one line 55
4. lemma OAI.StandardMapEntropy.transfer_log_difference_bound line 67