OAI/Probability/Ballisticity/Walk/ProfileGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TailGrowth.normalizedRestriction line 12
2. lemma OAI.TailGrowth.normalizedRestriction_probability line 15
3. lemma OAI.TailGrowth.normalizedRestriction_supported line 23
4. lemma OAI.TailGrowth.comp_total_le_one line 28
5. lemma OAI.TailGrowth.real_le_one_of_total_le_one line 36
6. def OAI.TailGrowth.outwardMass line 40
7. lemma OAI.TailGrowth.ordered_stream_mass_lower line 44
8. theorem OAI.TailGrowth.profile_tail_growth line 82