OAI/Analysis/LipschitzHilbert/Trees/SourceEitherGrid.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The balanced and dominant source constructions give one marked predictor. Dominant-path hypotheses are only needed when the drop is small.

  1. theorem OAI.LipschitzHilbert.eventually_source_grid_parameters line 15