OAI/Analysis/CircleDomains/Probability/AffineTimeMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The precise pullback of an arbitrary time measure to a retained affine interval. This is the measure identity used for arclength restriction.

  1. theorem OAI.CircleDomainRigidity.preimage_rescale_Icc line 15
  2. theorem OAI.CircleDomainRigidity.map_rescale_restrict_Icc line 39