OAI/Analysis/CircleDomains/Topology/PlanarFilledJump.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Planar integration of the actual disk-filling errors. A locally integrable gradient majorant is used only on the square containing the test.

  1. theorem OAI.CircleDomainRigidity.planar_filled_horizontal_jump_of_density line 13