OAI/Analysis/LipschitzHilbert/Trees/SourceReverseCellMarking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal source marking rule on every nested reverse-grid cell. Eligibility is derived from the actual first terminal block.

  1. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_reverse_cell_marking line 14