OAI/Geometry/PinnedDistances/VarianceRates.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Bounded.test_bound_rate line 13
2. lemma OAI.WeakPinned.Bounded.zeroAtInfty_tail line 35
3. lemma OAI.WeakPinned.Bounded.zeroAtInfty_modulus line 49
4. def OAI.WeakPinned.Bounded.sphereTest line 60
5. lemma OAI.WeakPinned.Bounded.sphereTest_bound line 68
6. lemma OAI.WeakPinned.Bounded.testDiscrep_sub_const line 87
7. lemma OAI.WeakPinned.Bounded.C0_arch_test_rate line 103
8. lemma OAI.WeakPinned.Bounded.sphere_arch_test_rate line 132
9. lemma OAI.WeakPinned.Bounded.incoming_discrep_bound line 167
10. lemma OAI.WeakPinned.Bounded.incoming_test_bound line 189
11. lemma OAI.WeakPinned.Bounded.integral_uniformLaw line 236
12. lemma OAI.WeakPinned.Bounded.integral_edgeProbability line 241
13. lemma OAI.WeakPinned.Bounded.integral_expandedProbability line 249
14. lemma OAI.WeakPinned.Bounded.expanded_test_bound line 256
15. lemma OAI.WeakPinned.Bounded.integral_target line 276
16. lemma OAI.WeakPinned.Bounded.incoming_law_test_bound line 287
17. lemma OAI.WeakPinned.Bounded.expanded_test_rate line 314
18. lemma OAI.WeakPinned.Bounded.incoming_law_test_rate line 333