OAI/Analysis/CircleDomains/Topology/MarkedClosedHitSplit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite fusion split with closed nonsmall children. The weighted estimate holds for every simultaneous choice from the children; their diameters can be prescribed arbitrarily small.

  1. theorem OAI.CircleDomainRigidity.MarkedHit.exists_closed_nonsmall_hit_split line 18
  2. theorem OAI.CircleDomainRigidity.MarkedHit.exists_closed_nonsmall_hit_split_all line 78

    Source documentation

    Empty configuration spaces impose no test, but still admit a small closed child.

    theorem exists_closed_nonsmall_hit_split_all
    {X Y Z : Type*} [MetricSpace X] [MetricSpace Y] [CompactSpace X] [SecondCountableTopology X]
    [MeasurableSpace X] [BorelSpace X]
  [SecondCountableTopology Y] [MeasurableSpace Y] [BorelSpace Y]
    [MeasurableSpace C(PathTime, Y)] [BorelSpace C(PathTime, Y)] (ι : C(X, Y))
    [MetricSpace Z] [SecondCountableTopology Z]
    (law : Z → ProbabilityMeasure C(PathTime, Y)) (hlaw : Continuous law)
    {A : Set Z} (hAclosed : IsClosed A) {C ε η r : ℝ} (hC : 0 ≤ C)
    (hε : 0 < ε) (hη : 0 < η) (hr : 0 < r)
    (n : ℕ) (hA : ¬HitTestSmall ι law C A) :
    ∃ (k : ℕ) (w : Fin k → ℝ) (D : Fin k → Set Z),
      (∀ i, 0 ≤ w i) ∧ (∑ i, w i) = 1 ∧
…

    Mentions: OAI.CircleDomainRigidity.PathTime, OAI.CircleDomainRigidity.MarkedHit.HitTestSmall