ConditionedProbeSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Keeping positive probe mass after conditioning the starting sample

theorem OAI.PolycyclicRecognition.exists_start_with_half_good_probes line 17

Source documentation

If joint failures occupy less than half the mass of the starting profile event, some starting sample in that event retains at least half of the independent probes. No conditioning on a singleton is used.

theorem exists_start_with_half_good_probes
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (ν : Measure Y) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (E : Set X) (bad : Set (X × Y)) (hE : MeasurableSet E) (hbad : MeasurableSet bad)
    (hsmall : (μ.prod ν) bad < (1 / 2 : ℝ≥0∞) * μ E) :
    ∃ x ∈ E, (1 / 2 : ℝ≥0∞) ≤ ν {y | (x, y) ∉ bad} := by
…

theorem OAI.PolycyclicRecognition.exists_start_with_compact_good_probes line 55

Source documentation

Inner regularity retains a compact positive-volume probe set at that same starting sample; the original starting-event probability is not lost.

theorem exists_start_with_compact_good_probes
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] [TopologicalSpace Y]
    (μ : Measure X) (ν : Measure Y) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    [ν.InnerRegular]
    (E : Set X) (bad : Set (X × Y)) (hE : MeasurableSet E) (hbad : MeasurableSet bad)
    (hsmall : (μ.prod ν) bad < (1 / 2 : ℝ≥0∞) * μ E) :
    ∃ x ∈ E, ∃ K : Set Y, IsCompact K ∧ K ⊆ {y | (x, y) ∉ bad} ∧
      (1 / 4 : ℝ≥0∞) < ν K := by
…