OAI/Analysis/CircleDomains/Selection/FillRegionPotential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Filling the terminal collar with the constant value one preserves the true-path cost inequality. At dust points away from its boundary, the band is either unchanged or collapses to the constant value.

  1. def OAI.CircleDomainRigidity.fillRegionOne line 22
  2. theorem OAI.CircleDomainRigidity.fillRegionOne_mem_Icc line 26
  3. theorem OAI.CircleDomainRigidity.one_sided_cost_to_constant_frontier line 36
  4. theorem OAI.CircleDomainRigidity.fillRegionOne_path_inequality line 63