OAI/Analysis/CircleDomains/Sobolev/FixedWidthIntegrability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Spatial integrability at every fixed staircase width

The derivative of a smooth staircase is periodic and bounded. Thus each fixed choice of shifts has integrable spatial wedges whenever the original three wedge terms are integrable. In particular, the cost identity needs no separate integrability assumption for the modified coordinates.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.periodic_deriv_shiftedStaircase line 23
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.bounded_staircase_multiplier line 32
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_staircase_pair_at_shifts line 55
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_staircase_pair_at_shifts_of_memLp line 90