OAI/Dynamics/StandardMap/TerminalCap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StandardMapEntropy.capF line 11
2. def OAI.StandardMapEntropy.capFpos line 12
3. lemma OAI.StandardMapEntropy.continuous_capF line 13
4. lemma OAI.StandardMapEntropy.continuous_capFpos line 14
5. lemma OAI.StandardMapEntropy.shortfall_one_max_mem line 15
6. lemma OAI.StandardMapEntropy.capFpos_nonneg line 20
7. lemma OAI.StandardMapEntropy.capF_sample_integral line 22
8. lemma OAI.StandardMapEntropy.capF_scale_integral line 32
9. lemma OAI.StandardMapEntropy.vague_integrable_tendsto_bound line 36
10. lemma OAI.StandardMapEntropy.CriticalScaleSequence.terminal_cap_bounds line 56
11. lemma OAI.StandardMapEntropy.CriticalScaleSequence.exists_terminal_cap_limit line 66