OAI/Analysis/RieszRectifiability/Foundations/SeedMultiplicityIntegration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating finite multiplicity bounds

Finite sums of indicator functions count the sets containing a point. Integrating these identities converts pointwise multiplicity bounds into estimates for sums of measures, including bounds expressed directly using finite cardinalities.

  1. theorem OAI.RieszRectifiability.finite_indicator_one_sum_eq_card line 18
  2. theorem OAI.RieszRectifiability.lintegral_finite_indicator_multiplicity line 29
  3. theorem OAI.RieszRectifiability.measure_sum_le_of_indicator_multiplicity line 38
  4. theorem OAI.RieszRectifiability.measure_sum_le_of_count_multiplicity line 56