OAI/Analysis/RieszRectifiability/Nets/ScaledSourceMeasure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RieszRectifiability.positive_nnreal_smul_support line 14
2. theorem OAI.RieszRectifiability.positive_nnreal_smul_admissibleRadius line 28
3. theorem OAI.RieszRectifiability.globalUpperGrowth_smul_nnreal line 33
4. theorem OAI.RieszRectifiability.lowerGrowth_smul_nnreal line 45
5. theorem OAI.RieszRectifiability.compactTestConvergence_smul_nnreal line 64
6. theorem OAI.RieszRectifiability.compactTestConvergence_cancel_scalar_limit line 71