OAI/MeasureTheory/Falconer/Incidence/TruncatedBlockRatio.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Prefix ratios for the actual endpoint cells of a profile interval. Both endpoint binning losses are retained explicitly.

  1. theorem OAI.Falconer.Regularization.planar_prefixFiber_children_subset line 11
  2. theorem OAI.Falconer.Regularization.blockClass_truncated_fiber_ratio line 21
  3. theorem OAI.Falconer.Regularization.blockClass_truncated_frostman line 63