OAI/Analysis/CircleDomains/Rigidity/TraceBalloonDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual trace balloon density is square integrable. Positive source disks pay for one sublist; reserved pieces pay for the zero-radius sublist. The two sublists may overlap each other.

  1. theorem OAI.CircleDomainRigidity.exists_trace_balloon_density line 15