OAI/Analysis/CircleDomains/Sobolev/ColoredGridEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The enlarged graph-grid balls have a uniform energy sum, with no doubling hypothesis on the measure.

  1. lemma OAI.CircleDomainRigidity.colored_grid_energy_sum line 13
  2. lemma OAI.CircleDomainRigidity.all_colored_grid_energy_sum line 24