OAI/Analysis/CircleDomains/Probability/IntervalPaymentNullImage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite payment measure that vanishes on free times forces their trace image to be null, once interval oscillation is paid. This is the last measure-theoretic step of the local tag argument.

  1. theorem OAI.CircleDomainRigidity.locallyConnected_pathTime line 16

    Distinct definitions of this name: OAI/Analysis/CircleDomains/Topology/PathImageSimpleArc.lean:22 (different declaration text). Qualify references as OAI.CircleDomainRigidity.locallyConnected_pathTime@path.

  2. theorem OAI.CircleDomainRigidity.path_time_null_image_of_interval_payment line 25