OAI/Analysis/CircleDomains/Rigidity/MatchedInnerCircleFlux.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The inner-circle flux bound uses the actual closed correspondence, not a boundary extension of the conformal map.

  1. theorem OAI.CircleDomainRigidity.quadrantPoint_dist line 14
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.indexed_quadrantFlux_bound line 22
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.indexed_quadrantFlux_limiting_bound line 39