OAI/Analysis/RieszRectifiability/Projections/FiniteProjectionAveraging.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite projection averages

Weighted displacement averages interpolate between the identity and local projections. Nonnegative weights control displacement from the original point or a common reference point, and continuous data give a continuous average.

  1. def OAI.RieszRectifiability.finiteProjectionAverage line 22
  2. theorem OAI.RieszRectifiability.finiteProjectionAverage_eq_self line 26
  3. theorem OAI.RieszRectifiability.finiteProjectionAverage_eq_weighted_sum line 34
  4. theorem OAI.RieszRectifiability.finiteProjectionAverage_dist_self_le line 42
  5. theorem OAI.RieszRectifiability.finiteProjectionAverage_dist_reference_le line 62
  6. theorem OAI.RieszRectifiability.finiteProjectionAverage_continuous line 84