OAI/Analysis/RieszRectifiability/Packing/CellHaarFunctions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Haar functions for nested cells

The difference of normalized indicators, scaled by the square root of the smaller cell's mass, has mean zero. Its squared integral is the complementary mass ratio, and pairing with an L² function recovers the difference of the two cell means.

  1. def OAI.RieszRectifiability.cellHaar line 23
  2. theorem OAI.RieszRectifiability.cellHaar_memLp line 26
  3. theorem OAI.RieszRectifiability.cellHaar_integrable line 32
  4. theorem OAI.RieszRectifiability.cellHaar_zero_of_notMem line 38
  5. theorem OAI.RieszRectifiability.cellHaar_mean_zero line 43
  6. theorem OAI.RieszRectifiability.cellHaar_sq_integral line 54
  7. theorem OAI.RieszRectifiability.cellHaar_sq_integral_le_one line 74
  8. theorem OAI.RieszRectifiability.cellHaar_pairing line 80