OAI/Analysis/CircleDomains/Topology/CompactLineJump.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported tests turn the finite-interval jump estimate into an estimate over the entire line.

  1. theorem OAI.CircleDomainRigidity.filled_line_integration_through_disks_univ line 12