OAI/Analysis/RieszRectifiability/Kernel/StepPairings.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pairings with finite step functions reduce to sums of cell integrals and cell means. Convergence of cell masses and means therefore gives convergence of these pairings.

  1. theorem OAI.RieszRectifiability.integral_mul_finiteStep line 19
  2. theorem OAI.RieszRectifiability.integral_mul_finiteStep_cellMeans line 36
  3. theorem OAI.RieszRectifiability.cellMean_step_pairing_tendsto line 54