OAI/Analysis/CircleDomains/Topology/SubarcIntersectionCount.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Distinct intersections decrease under subarc selection. Conditioning on a compact family of mass at least one half costs at most a factor two.

  1. theorem OAI.CircleDomainRigidity.pathImageCount_mono_range line 17
  2. theorem OAI.CircleDomainRigidity.pathImageCount_le_timeCount line 27
  3. theorem OAI.CircleDomainRigidity.pathImageCount_eq_timeCount_of_injective line 43
  4. def OAI.CircleDomainRigidity.IsSubarcLawReduction line 62

    Source documentation

    The actual measurable selection and domination data retained by compact terminal subarc conditioning.

    def IsSubarcLawReduction
    (μ η : ProbabilityMeasure C(PathTime, X)) : Prop :=
…

    Mentions: OAI.CircleDomainRigidity.PathTime

  5. theorem OAI.CircleDomainRigidity.mean_subarc_intersections_le line 69
  6. theorem OAI.CircleDomainRigidity.finite_mean_subarc_intersections line 86