OAI/Dynamics/StandardMap/GraphDistortion.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.StandardMapEntropy.finite_six_tenths_sumline 11 - lemma
OAI.StandardMapEntropy.log_dirichlet_row_boundline 25 - lemma
OAI.StandardMapEntropy.log_terminal_derivative_boundline 55 - lemma
OAI.StandardMapEntropy.log_ratio_of_derivative_boundline 81 - lemma
OAI.StandardMapEntropy.contracting_graph_terminal_ratioline 107