OAI/Analysis/CircleDomains/Selection/ScalarEndIdentification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single full-measure set satisfies all rational terminal bounds. Shrinking the actual source caps then identifies the scalar on every matched target end, even when those ends have positive total area.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.ae_rational_terminal_bounds line 22
  2. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.ScalarWeakLimit.eq_on_all_matched_ends line 60