LocalFailure.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Local failure of the actual resampling experiment

theorem OAI.LeanBlast.SecondKahnKalai.target_subset_iff_required_subset line 20
theorem OAI.LeanBlast.SecondKahnKalai.fragment_subset_inter_of_target_subset line 34
theorem OAI.LeanBlast.SecondKahnKalai.inverse_power_card_cancel line 44

theorem OAI.LeanBlast.SecondKahnKalai.resampling_large_fragment_term_le line 61

Source documentation

At a large denominator, the actual large-fragment weight is bounded by an intersection-tail indicator and the required-coordinate indicator.

theorem resampling_large_fragment_term_le (ν : FiniteLaw B) (A : B → Finset X)
    {ρ : ℝ} (hρ : 0 < ρ) (m : ℕ) (W : Finset X) (c b : B) :
    (if Real.exp (-10 * (m : ℝ)) ≤ resamplingZ ν A ρ (resamplingY A W c) ∧
          m / 2 < (A b \ W).card then resamplingWeight ν A ρ W (c, b) else 0) ≤
      if m < 2 * (A c ∩ A b).card ∧ A b \ A c ⊆ W then
        Real.exp (10 * (m : ℝ)) * ν.weight c * ν.weight b * (ρ⁻¹) ^ (A b).card
      else 0 := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.resamplingZ, OAI.LeanBlast.SecondKahnKalai.resamplingY, OAI.LeanBlast.SecondKahnKalai.resamplingWeight

theorem OAI.LeanBlast.SecondKahnKalai.local_bernoulliExpectation_sum line 114
theorem OAI.LeanBlast.SecondKahnKalai.resampling_large_fragment_pair_bound line 121
theorem OAI.LeanBlast.SecondKahnKalai.resampling_large_fragment_bound line 163
theorem OAI.LeanBlast.SecondKahnKalai.resampling_small_density_bound line 229
Source documentation
The density identity bounds the probability of a small denominator by the cutoff itself.
```
theorem resampling_small_density_bound (ν : FiniteLaw B) (A : B → Finset X)
    {ρ τ : ℝ} (hν : ν.IsPositive) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hτ : 0 ≤ τ) :
    bernoulliExpectation ρ (fun W => (resamplingLaw ν A ρ W hν hρ).prob
      (fun cb => resamplingZ ν A ρ (resamplingY A W cb.1) < τ)) ≤ τ := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation, OAI.LeanBlast.SecondKahnKalai.resamplingLaw, OAI.LeanBlast.SecondKahnKalai.resamplingZ, OAI.LeanBlast.SecondKahnKalai.resamplingY
theorem OAI.LeanBlast.SecondKahnKalai.local_failure_bound line 246
theorem OAI.LeanBlast.SecondKahnKalai.local_failure_probability_bound line 283
theorem OAI.LeanBlast.SecondKahnKalai.localFailure_iff_real line 308
theorem OAI.LeanBlast.SecondKahnKalai.local_failure_source_form line 323