OAI/Probability/SpanningForest/CanonicalDrift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem336.CanonicalDrift.outerLimit line 13
2. theorem OAI.Problem336.CanonicalDrift.measurable_outerLimit line 16
3. theorem OAI.Problem336.CanonicalDrift.outerLimit_mem_Icc line 21
4. theorem OAI.Problem336.CanonicalDrift.outerLimit_le_add line 33
5. theorem OAI.Problem336.CanonicalDrift.abs_outerLimit_sub_le line 50
6. theorem OAI.Problem336.CanonicalDrift.outerLimit_transport line 67
7. theorem OAI.Problem336.CanonicalDrift.outerLimit_eq_of_tendsto line 73