OAI/Dynamics/StandardMap/BridgeDecay.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.StandardMapEntropy.bridge_error_geomline 11 - lemma
OAI.StandardMapEntropy.half_pow_nat_le_inverseline 22 - lemma
OAI.StandardMapEntropy.bridge_error_inverseline 26 - lemma
OAI.StandardMapEntropy.bridge_error_sumline 29 - lemma
OAI.StandardMapEntropy.window_indicesline 41