OAI/Analysis/CircleDomains/Sobolev/SobolevGraphEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The original Sobolev energy pushed to the scalar graph. The local capacity cost is bounded by its mass on an actual ambient graph ball.

  1. def OAI.CircleDomainRigidity.sobolevGraph line 13
  2. def OAI.CircleDomainRigidity.sobolevGraphEnergy line 16
  3. lemma OAI.CircleDomainRigidity.sobolevGraph_continuous line 21
  4. lemma OAI.CircleDomainRigidity.sobolev_graph_band_energy_le_ball line 24