OAI/Computability/MinUncut/Estimates/CollisionIndicator.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MinUncut.CubeRows.collision_indicator line 25
2. lemma OAI.MinUncut.CubeRows.collision_probability line 34
3. lemma OAI.MinUncut.CubeRows.cubeExpectation_abs_bound line 52
4. lemma OAI.MinUncut.CubeRows.full_cube_bound line 66
5. def OAI.MinUncut.Inner.pairField line 102
6. lemma OAI.MinUncut.Inner.pair_moment line 108
7. theorem OAI.MinUncut.Inner.pair_correlation_power line 121
8. lemma OAI.MinUncut.Box.bounded_integrable line 145
9. lemma OAI.MinUncut.Box.integral_pow_bound line 149
10. lemma OAI.MinUncut.Box.integral_expect line 159