OAI/Analysis/CircleDomains/Sobolev/ModelBarrierGradient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The reference differential in the selected barrier comparison is exactly the weak gradient of the actual conformal pullback barrier.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.reference_barrier_value line 16
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.reference_barrier_gradient line 28