OAI/MeasureTheory/Falconer/Angular/IneligibleCapTerms.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of individual ineligible original cap terms

One null set is chosen before frequency. This permits arbitrary whole-cell edge decisions in the finite graph without introducing angular cutoffs.

  1. theorem OAI.Falconer.DyadicCube.ineligible_transform_ae_zero line 16
  2. theorem OAI.Falconer.angularProduct_ae_first line 36
  3. theorem OAI.Falconer.angularProduct_ae_second line 42
  4. theorem OAI.Falconer.dyadicCapIntegrand_star line 48
  5. theorem OAI.Falconer.dyadicCapIntegrand_row_ineligible line 58
  6. theorem OAI.Falconer.dyadicCapIntegrand_col_ineligible line 90