RepresentativeFailure.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310.RepresentativeFailure.failure_le_card_mul line 17

Source documentation

A deterministic finite representative list turns a pointwise failure bound into an all-parameters bound. No measurability of the existential event is needed: the outer-measure union bound is sufficient.

theorem failure_le_card_mul {Ω : Type u_Ω} {T : Type u_T} [MeasurableSpace Ω]
    (μ : Measure Ω) (A : Set Ω) (K : Set T) (R : Finset T)
    (failure test : Ω → T → Prop) (q : ℝ≥0∞)
    (htransfer : ∀ ω ∈ A, ∀ t ∈ K, failure ω t → ∃ r ∈ R, test ω r)
    (hbound : ∀ r ∈ R, μ {ω | ω ∈ A ∧ test ω r} ≤ q) :
    μ {ω | ω ∈ A ∧ ∃ t ∈ K, failure ω t} ≤ R.card * q := by
…

theorem OAI.Problem310.RepresentativeFailure.local_failure_le_card_mul line 38

Source documentation

Predicate agreement for the finite representative list supplies the transfer hypothesis in the local-routing argument.

theorem local_failure_le_card_mul {Ω : Type u_Ω} {T : Type u_T} {I : Type u_I} [MeasurableSpace Ω]
    (μ : Measure Ω) (A : Set Ω) (K : Set T) (R : Finset T)
    (failure : Ω → T → Prop) (localHit : Ω → I → T → Prop) (q : ℝ≥0∞)
    (hlocal : ∀ ω ∈ A, ∀ t ∈ K, failure ω t → ∀ i, ¬ localHit ω i t)
    (hreps : ∀ t ∈ K, ∃ r ∈ R,
      ∀ ω ∈ A, ∀ i, localHit ω i r ↔ localHit ω i t)
    (hbound : ∀ r ∈ R, μ {ω | ω ∈ A ∧ ∀ i, ¬ localHit ω i r} ≤ q) :
    μ {ω | ω ∈ A ∧ ∃ t ∈ K, failure ω t} ≤ R.card * q := by
…

theorem OAI.Problem310.RepresentativeFailure.local_failure_le_mul_mass line 56

Source documentation

The multiplicative form used for an exposure atom: a per-representative joint bound q * μ A and an entropy budget card R * q ≤ p give the all-scales joint bound p * μ A.

theorem local_failure_le_mul_mass {Ω : Type u_Ω} {T : Type u_T} {I : Type u_I} [MeasurableSpace Ω]
    (μ : Measure Ω) (A : Set Ω) (K : Set T) (R : Finset T)
    (failure : Ω → T → Prop) (localHit : Ω → I → T → Prop) (p q : ℝ≥0∞)
    (hlocal : ∀ ω ∈ A, ∀ t ∈ K, failure ω t → ∀ i, ¬ localHit ω i t)
    (hreps : ∀ t ∈ K, ∃ r ∈ R,
      ∀ ω ∈ A, ∀ i, localHit ω i r ↔ localHit ω i t)
    (hbound : ∀ r ∈ R, μ {ω | ω ∈ A ∧ ∀ i, ¬ localHit ω i r} ≤ q * μ A)
    (hbudget : R.card * q ≤ p) :
    μ {ω | ω ∈ A ∧ ∃ t ∈ K, failure ω t} ≤ p * μ A := by
…

theorem OAI.Problem310.RepresentativeFailure.failure_le_bad_add_atom_bound line 75
Source documentation
Sum restricted failure estimates over exposure atoms and pay once for the exceptional event on which the first default does not exist. The mass bound is separated out so this works for finite partitions, subpartitions, and any finite-family construction with total mass at most one.
```
theorem failure_le_bad_add_atom_bound {Ω : Type u_Ω} {J : Type u_J} [MeasurableSpace Ω] [Fintype J]
    (μ : Measure Ω) (F D : Set Ω) (A : J → Set Ω) (p q : ℝ≥0∞)
    (hcover : F ⊆ D ∪ ⋃ j, A j)
    (hbad : μ D ≤ q)
    (hatom : ∀ j, μ (F ∩ A j) ≤ p * μ (A j))
    (hmass : ∑ j, μ (A j) ≤ 1) : μ F ≤ q + p := by
…
```

theorem OAI.Problem310.RepresentativeFailure.raw_failure_le_two_budgets line 101

Source documentation

The all-scales probability estimate, abstracted from the finite table construction. Good exposure atoms may have different trial types, representatives and fixed-scale failure probabilities.

theorem raw_failure_le_two_budgets {Ω : Type u_Ω} {T : Type u_T} {J : Type u_J} [MeasurableSpace Ω] [Fintype J]
    (μ : Measure Ω) (K : Set T) (D : Set Ω) (A : J → Set Ω)
    (I : J → Type u_I) (R : J → Finset T) (failure : Ω → T → Prop)
    (localHit : ∀ j, Ω → I j → T → Prop) (p q : ℝ≥0∞) (rate : J → ℝ≥0∞)
    (hcover : univ ⊆ D ∪ ⋃ j, A j) (hbad : μ D ≤ q)
    (hmass : ∑ j, μ (A j) ≤ 1)
    (hlocal : ∀ j, ∀ ω ∈ A j, ∀ t ∈ K, failure ω t → ∀ i, ¬ localHit j ω i t)
    (hreps : ∀ j, ∀ t ∈ K, ∃ r ∈ R j,
      ∀ ω ∈ A j, ∀ i, localHit j ω i r ↔ localHit j ω i t)
    (hbound : ∀ j, ∀ r ∈ R j,
      μ {ω | ω ∈ A j ∧ ∀ i, ¬ localHit j ω i r} ≤ rate j * μ (A j))
    (hbudget : ∀ j, (R j).card * rate j ≤ p) :
…