OAI/MeasureTheory/Falconer/Incidence/NormalProfileIncidence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The normal-interval factor in the multiscale product, evaluated on the actual retained endpoint configuration.

  1. theorem OAI.Falconer.planar_critical_normalized_ratio line 12
  2. theorem OAI.Falconer.blockClass_retained_normal_ratio line 31