MarkedFusionSmallSets.lean`

8 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.

def OAI.CircleDomainRigidity.MarkedHit.PassesHitTests line 25
theorem OAI.CircleDomainRigidity.MarkedHit.PassesHitTests.mono line 30
def OAI.CircleDomainRigidity.MarkedHit.HitTestSmall line 39
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, Y)) (C : ℝ) (A : Set Z) : Prop :=
…
```
Mentions: OAI.CircleDomainRigidity.PathTime
theorem OAI.CircleDomainRigidity.MarkedHit.HitTestSmall.mono line 45
theorem OAI.CircleDomainRigidity.MarkedHit.hitTestSmall_empty line 52
theorem OAI.CircleDomainRigidity.MarkedHit.hitTestSmall_iUnion line 56
theorem OAI.CircleDomainRigidity.MarkedHit.HitTestSmall.union line 69
theorem OAI.CircleDomainRigidity.MarkedHit.not_hitTestSmall_univ line 84
Source documentation
The extraction hypothesis makes the whole candidate space nonsmall.
```
theorem not_hitTestSmall_univ {law : Z → ProbabilityMeasure C(PathTime, Y)} {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.MarkedHit.PassesHitTests, OAI.CircleDomainRigidity.MarkedHit.HitTestSmall