OAI/Analysis/CircleDomains/Rigidity/TraceBalloonRealCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed physical balloon system in the real product coordinates used by the rectangle Sobolev witnesses.

  1. theorem OAI.CircleDomainRigidity.exists_trace_balloon_real_system line 14