OAI/Analysis/RieszRectifiability/Kernel/FiniteStepMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Moments of finite-step functions

Finite sums of cell indicators reduce first and second moments to weighted cell masses. For disjoint cells, convergence of the coefficients and masses gives convergence of the second moments and vanishing squared approximation error.

  1. def OAI.RieszRectifiability.finiteStep line 22
  2. theorem OAI.RieszRectifiability.finiteStep_eq_cell line 27
  3. theorem OAI.RieszRectifiability.partitionMean_eq_finiteStep line 39
  4. theorem OAI.RieszRectifiability.finiteStep_sq line 43
  5. theorem OAI.RieszRectifiability.finiteStep_sub line 55
  6. theorem OAI.RieszRectifiability.integral_finiteStep line 66
  7. theorem OAI.RieszRectifiability.integral_finiteStep_sq line 76
  8. theorem OAI.RieszRectifiability.integral_finiteStep_sub_sq line 83
  9. theorem OAI.RieszRectifiability.finiteStep_second_moment_tendsto line 93
  10. theorem OAI.RieszRectifiability.finiteStep_squared_error_tendsto_zero line 104