OAI/Geometry/RCD/Sobolev/FiniteDirectedCut.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A directed cut captures one quarter of the off-diagonal weight

The finite counting step in Rajala--Sturm, Lemma 3.1. Averaging over all Boolean cuts is implemented by the two coordinate-flip bijections.

  1. def OAI.RegularPointCoordinates.flipColor line 16
  2. def OAI.RegularPointCoordinates.directedCutWeight line 28
  3. theorem OAI.RegularPointCoordinates.four_color_sum line 31
  4. theorem OAI.RegularPointCoordinates.sum_directedCutWeight line 49
  5. theorem OAI.RegularPointCoordinates.exists_directedCutWeight_ge_quarter line 70