OAI/Analysis/CircleDomains/Selection/MeanCircuitExclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A strict lower bound for the constructed mean excludes the same map--disk pair after passing to its measurable physical coordinate.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.circleFormIntegral_eq_of_physical_values line 14
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateData.exists_mapDisk_exclusion_of_mean line 45