OAI/Analysis/RieszRectifiability/Kernel/WeightedCentering.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RieszRectifiability.cutoffMean line 14
2. theorem OAI.RieszRectifiability.cutoffMean_integral_zero line 17
3. theorem OAI.RieszRectifiability.cutoffMean_sq_bound line 31
4. theorem OAI.RieszRectifiability.centered_second_moment_le line 64
5. theorem OAI.RieszRectifiability.cutoff_centered_second_moment_bound line 80
6. theorem OAI.RieszRectifiability.cutoff_mass_lower_of_one_on line 95