OAI/Analysis/CircleDomains/Sobolev/FinitePeriodStokes.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The distinguished offset disappears for every fixed finite period. No normalization of that period is needed for the Stokes upper bound.

  1. theorem OAI.CircleDomainRigidity.abs_le_of_boundary_costs line 15
  2. theorem OAI.CircleDomainRigidity.finite_offset_stokes_bound_with_period line 31
  3. theorem OAI.CircleDomainRigidity.zero_offset_stokes_bound_of_period line 66