OAI/Analysis/RieszRectifiability/Rigidity/HeightTemperedDistribution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Tempered distributions associated with heights

Polynomially weighted integrability makes the positive and negative height measures temperate. Their difference defines a tempered distribution whose action on a Schwartz test function is integration against the signed height.

  1. def OAI.RieszRectifiability.positiveHeightMeasure line 21
  2. theorem OAI.RieszRectifiability.positive_height_measure_temperate line 24
  3. theorem OAI.RieszRectifiability.positivePart_sub_negativePart line 43
  4. theorem OAI.RieszRectifiability.height_schwartz_integrable line 51
  5. def OAI.RieszRectifiability.heightTemperedDistribution line 74
  6. theorem OAI.RieszRectifiability.heightTemperedDistribution_apply line 84
  7. theorem OAI.RieszRectifiability.heightTemperedDistribution_independent_of_weight line 111