OAI/Analysis/CircleDomains/Sobolev/PriorSmoothedCompatibility.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of the smoothed coordinate follows from the proved raw path-cost estimate and pointwise contraction of its dust bands.

  1. theorem OAI.CircleDomainRigidity.smoothed_barrier_compatibility_with_prior_levels line 17