OAI/Analysis/CircleDomains/Probability/ScalarPairNull.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Passing prescribed real scalar trace pairs to their unit-circle levels preserves planar outer-nullity. No measurability of the trace image is needed.

  1. def OAI.CircleDomainRigidity.scalarPairModOne line 13
  2. theorem OAI.CircleDomainRigidity.volume_scalarPairModOne_image_eq_zero line 16
  3. theorem OAI.CircleDomainRigidity.scalar_trace_pair_null_mod_one line 75