OAI/Analysis/RieszRectifiability/Nets/CellVariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.cellMean line 14
2. theorem OAI.RieszRectifiability.integral_sq_sub_const line 17
3. theorem OAI.RieszRectifiability.pairwise_square_integrable_right line 25
4. theorem OAI.RieszRectifiability.inner_pairwise_square_formula line 30
5. theorem OAI.RieszRectifiability.iterated_pairwise_square_integrable line 40
6. theorem OAI.RieszRectifiability.iterated_pairwise_square_formula line 47
7. theorem OAI.RieszRectifiability.cell_variance_eq_half_pairwise line 63