OAI/Analysis/LipschitzHilbert/Phase/AngularGraphMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual boundary masses dominate the graph's closed-neighborhood mass.

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