OAI/Analysis/CircleDomains/Probability/FusionSmallSets.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The sigma-ideal of path-law candidates failing a prescribed countable/atomless test. A finite atomless measure dominating any countable list of such tests is constructed from the existing finite-measure representative of an s-finite measure.

  1. theorem OAI.CircleDomainRigidity.exists_finite_atomless_dominating line 18
  2. def OAI.CircleDomainRigidity.PassesHitTests line 32
  3. theorem OAI.CircleDomainRigidity.PassesHitTests.mono line 37
  4. def OAI.CircleDomainRigidity.HitTestSmall line 46

    Source documentation

    A candidate family is small when one countable set and one finite atomless test measure rule out every member. This is the manuscript's small-set ideal.

    def HitTestSmall (law : Z → ProbabilityMeasure C(PathTime, X)) (C : ℝ) (A : Set Z) : Prop :=
…

    Mentions: OAI.CircleDomainRigidity.PathTime

  5. theorem OAI.CircleDomainRigidity.HitTestSmall.mono line 51
  6. theorem OAI.CircleDomainRigidity.hitTestSmall_empty line 57
  7. theorem OAI.CircleDomainRigidity.hitTestSmall_iUnion line 61
  8. theorem OAI.CircleDomainRigidity.HitTestSmall.union line 74
  9. theorem OAI.CircleDomainRigidity.not_hitTestSmall_univ line 88

    Source documentation

    The extraction hypothesis makes the whole candidate space nonsmall.

    theorem not_hitTestSmall_univ {law : Z → ProbabilityMeasure C(PathTime, X)} {C : ℝ}
    (htest : ∀ D : Set X, D.Countable → ∀ ν : Measure X,
      IsFiniteMeasure ν → NullSingletonClass ν → ∃ z, PassesHitTests C (law z) D ν) :
    ¬HitTestSmall law C univ := by
…

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