OAI/Analysis/Littlewood/ProductProbability.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AsymptoticallyMinimalLittlewood.Nibble.coinWeight line 15
2. def OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation line 18
3. def OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit line 21
4. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_prod line 24
5. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.coinWeight_sum line 32
6. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.coinWeight_nonneg line 37
7. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_const line 43
8. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_add line 46
9. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_sub line 50
10. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_mul_const line 54
11. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_const_mul line 58
12. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_sum line 62
13. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_mono line 67
14. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_nonneg line 71
15. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.exists_le_expectation line 75
16. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit_eq line 94
17. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit_nonneg line 106
18. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit_le_one line 110
19. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit_union line 114
20. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_noHit line 119
21. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.one_sub_pow_le line 135
22. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit_covariance_le line 141
23. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit_sum_variance line 159

    Source documentation

    The second-moment estimate used for every residual degree. Each test set has size at most L and each independent edge-bit occurs in at most K tests.

    lemma noHit_sum_variance {I : Type uI} [DecidableEq I] {p : ℝ}
        (hp : 0 ≤ p) (hp1 : p ≤ 1) (S : Finset I) (A : I → Finset E)
        {K L : ℝ} (hK0 : 0 ≤ K) (hL : ∀ i ∈ S, ((A i).card : ℝ) ≤ L)
        (hK : ∀ e, ((S.filter fun i ↦ e ∈ A i).card : ℝ) ≤ K) :
        let Y : (E → Bool) → ℝ := fun s ↦ ∑ i ∈ S, noHit (A i) s
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit

24. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.pow_bonferroni line 216
25. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.markov_indicator line 228
26. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.chebyshev_indicator line 237
27. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.exists_of_three_bad_bounds line 250
28. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.noHit_mean_error line 262
29. def OAI.AsymptoticallyMinimalLittlewood.Nibble.selectedIndicator line 292

    Source documentation

    A Bernoulli indicator, for counting selected edges.

    def selectedIndicator (e : E) (s : E → Bool) : ℝ := if s e then 1 else 0
    …

30. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.selectedIndicator_eq line 295
31. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.selectedIndicator_nonneg line 300
32. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_selected line 304
33. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation_selected_mul line 310
34. lemma OAI.AsymptoticallyMinimalLittlewood.Nibble.exists_controlled_outcome line 325

    Source documentation

    Simultaneous second-moment control of many local tests, one global test, and a nonnegative collision count. No randomness remains in the conclusion.

    lemma exists_controlled_outcome {I : Type uI} [DecidableEq I] {p : ℝ}
        (hp : 0 ≤ p) (hp1 : p ≤ 1) (U : Finset I)
        (Y : I → (E → Bool) → ℝ) (Z W : (E → Bool) → ℝ)
        {V Vz M t b u c : ℝ} (ht : 0 < t) (hb : 0 < b) (hu : 0 < u) (hc : 0 < c)
        (hY : ∀ i ∈ U, expectation p (fun s ↦ (Y i s - expectation p (Y i))^2) ≤ V)
        (hZ : expectation p (fun s ↦ (Z s - expectation p Z)^2) ≤ Vz)
        (hW0 : ∀ s, 0 ≤ W s) (hW : expectation p W ≤ M)
        (hV : 4 * U.card * V ≤ t^2*b) (hVz : 4*Vz ≤ u^2) (hM : 4*M ≤ c) :
        ∃ s, (((U.filter fun i ↦ t < |Y i s - expectation p (Y i)|).card : ℝ) ≤ b) ∧
          |Z s - expectation p Z| ≤ u ∧ W s ≤ c := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Nibble.expectation