OAI/Probability/Subsphere/Estimates/Weighted.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubsphereCurrent.Weighted.block_parameters line 16
2. lemma OAI.SubsphereCurrent.Weighted.weighted_block_test line 30
3. lemma OAI.SubsphereCurrent.Weighted.weighted_block line 71
4. lemma OAI.SubsphereCurrent.Weighted.measurable_onTest line 103
5. lemma OAI.SubsphereCurrent.Weighted.terminal_test line 106
6. lemma OAI.SubsphereCurrent.Weighted.terminal_average line 127
7. lemma OAI.SubsphereCurrent.Weighted.weighted_terminal line 168
8. theorem OAI.SubsphereCurrent.Weighted.radius_weighted_estimate line 216
9. theorem OAI.SubsphereCurrent.Weighted.radius_weighted_full_estimate line 233