OAI/MeasureTheory/Falconer/Angular/DyadicCapTerms.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cap terms on the original dyadic descendants

The finite graph expansion and the analytic endpoint cross terms use the same restricted laws and model masses. These identities connect them without changing the spatial labels or taking an absolute value early.

  1. def OAI.Falconer.dyadicCapIntegrand line 16
  2. theorem OAI.Falconer.dyadicCapIntegrand_integrable line 24
  3. theorem OAI.Falconer.integral_dyadicCapIntegrand line 44