OAI/Analysis/CircleDomains/Topology/ClosedHitSplit.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.exists_closed_nonsmall_hit_split line 18
  2. theorem OAI.CircleDomainRigidity.exists_closed_nonsmall_hit_split_all line 77

    Source documentation

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

    theorem exists_closed_nonsmall_hit_split_all
    {X Z : Type*} [MetricSpace X] [CompactSpace X] [SecondCountableTopology X]
    [MeasurableSpace X] [BorelSpace X]
    [MeasurableSpace C(PathTime, X)] [BorelSpace C(PathTime, X)]
    [MetricSpace Z] [SecondCountableTopology Z]
    (law : Z → ProbabilityMeasure C(PathTime, X)) (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 ∧
      (∀ i, IsClosed (D i) ∧ D i ⊆ A ∧ ¬HitTestSmall law C (D i) ∧
…

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