OAI/Analysis/CircleDomains/Probability/MonotoneDyadicMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Atomless time measures split exactly over a monotone image of a dyadic partition. This bounds restricted physical length by the old time measure.

  1. theorem OAI.CircleDomainRigidity.sum_monotone_dyadic_restrict line 15
  2. theorem OAI.CircleDomainRigidity.sum_monotone_dyadic_mass line 36