OAI/Analysis/CircleDomains/Sobolev/FiniteOffsetStokes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite offset estimate from Green's formula. The nonzero period is kept at the distinguished hole. All other boundary costs use the oscillations of their real lifts.

  1. theorem OAI.CircleDomainRigidity.circle_boundary_mem_smooth_region line 17
  2. theorem OAI.CircleDomainRigidity.abs_le_of_distinguished_boundary line 38
  3. theorem OAI.CircleDomainRigidity.finite_offset_stokes_bound line 61
  4. theorem OAI.CircleDomainRigidity.circle_costs_le_square_norm line 97