OAI/Analysis/RieszRectifiability/Nets/NativeCellMeanBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cell means from native vector norm bounds

Cell means respect addition, subtraction, and constants, and inherit almost-everywhere uniform bounds. For a vector field controlled in L² by a scalar input, its components along vectors of norm at most one have bounded means on sets of finite positive mass. The estimate combines the squared norm bound with the scalar input's local energy budget.

  1. theorem OAI.RieszRectifiability.cellMean_add line 24
  2. theorem OAI.RieszRectifiability.cellMean_sub line 29
  3. theorem OAI.RieszRectifiability.cellMean_const line 34
  4. theorem OAI.RieszRectifiability.cellMean_abs_le_ae_bound line 39
  5. theorem OAI.RieszRectifiability.cellMean_near_constant line 47
  6. theorem OAI.RieszRectifiability.native_vector_cellMean_bound line 53