OAI/Analysis/RieszRectifiability/Foundations/FiniteNormalizedWeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.finiteWeightDenominator line 14
2. def OAI.RieszRectifiability.finiteNormalizedWeight line 17
3. theorem OAI.RieszRectifiability.finiteWeightDenominator_ge_one line 20
4. theorem OAI.RieszRectifiability.finiteNormalizedWeight_nonneg line 23
5. theorem OAI.RieszRectifiability.finiteNormalizedWeight_eq_zero_iff line 27
6. theorem OAI.RieszRectifiability.finiteNormalizedWeight_sum_le_one line 33
7. theorem OAI.RieszRectifiability.finiteNormalizedWeight_sum_eq_one line 40
8. theorem OAI.RieszRectifiability.finiteNormalizedWeight_le_one line 47
9. theorem OAI.RieszRectifiability.finiteWeightDenominator_abs_sub_le line 55
10. theorem OAI.RieszRectifiability.finiteNormalizedWeight_sum_abs_sub_le line 65