OAI/Combinatorics/PlanarL1/Probability.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarL1.FiniteRandom.event line 11
2. lemma OAI.PlanarL1.FiniteRandom.mem_event line 15
3. def OAI.PlanarL1.FiniteRandom.prob line 19
4. lemma OAI.PlanarL1.FiniteRandom.prob_nonneg line 23
5. lemma OAI.PlanarL1.FiniteRandom.prob_eq_sum line 27
6. lemma OAI.PlanarL1.FiniteRandom.prob_mono line 32
7. lemma OAI.PlanarL1.FiniteRandom.prob_equiv line 39
8. lemma OAI.PlanarL1.FiniteRandom.prob_prod line 46
9. lemma OAI.PlanarL1.FiniteRandom.prob_prod_bound line 53
10. lemma OAI.PlanarL1.FiniteRandom.prob_union_bound line 63
11. lemma OAI.PlanarL1.FiniteRandom.grid_card_span line 79

    Source documentation

    Cardinality of a grid subset is controlled by the span of its indices.

    lemma grid_card_span (s : Finset ℕ) {a b : ℕ} (h : ∀ i ∈ s, a ≤ i ∧ i ≤ b) :
        s.card ≤ b + 1 - a := by
    …

12. lemma OAI.PlanarL1.FiniteRandom.grid_count line 86

    Source documentation

    An interval of radius t meets at most 2t/step+1 equally spaced points. This argument is exact and includes both endpoints of the grid.

    lemma grid_count (m : ℕ) {step t : ℝ} (hstep : 0 < step) (ht : 0 ≤ t) (c : ℝ) :
        ((event (fun i : Fin (m + 1) => |c + step * i.val| ≤ t)).card : ℝ) * step ≤
          2 * t + step := by
    …

    Mentions: OAI.PlanarL1.FiniteRandom.event

13. lemma OAI.PlanarL1.FiniteRandom.grid_probability line 124

    Source documentation

    Uniform endpoint grid estimate in the normalization used by the paper.

    lemma grid_probability (m : ℕ) (hm : 0 < m) {q t : ℝ} (hq : 0 < q) (ht : 0 ≤ t) (c : ℝ) :
        prob (fun i : Fin (m + 1) => |c + q / m * i.val| ≤ t) ≤ (2 * t + q / m) / q := by
    …

    Mentions: OAI.PlanarL1.FiniteRandom.prob

14. lemma OAI.PlanarL1.FiniteRandom.coordinate_probability line 151

    Source documentation

    Independent uniform grid coordinates can be exposed one at a time by an actual equivalence of finite sample spaces.

    lemma coordinate_probability {I : Type*} [Fintype I] [DecidableEq I]
        (i : I) (m : ℕ) (hm : 0 < m) {q t : ℝ} (hq : 0 < q) (ht : 0 ≤ t)
        (F : (I → Fin (m + 1)) → ℝ)
        (hF : ∀ α : I → Fin (m + 1), ∃ c : ℝ,
          (∀ r : Fin (m + 1), F (Function.update α i r) = c + q / m * r.val) ∨
          (∀ r : Fin (m + 1), F (Function.update α i r) = c - q / m * r.val)) :
        prob (fun α => |F α| ≤ t) ≤ (2 * t + q / m) / q := by
    …

    Mentions: OAI.PlanarL1.FiniteRandom.prob

15. lemma OAI.PlanarL1.FiniteRandom.prob_false line 184
16. lemma OAI.PlanarL1.FiniteRandom.prob_pair_bound line 187
17. lemma OAI.PlanarL1.FiniteRandom.prob_prod_bound_left line 220
18. lemma OAI.PlanarL1.FiniteRandom.prob_update_bound line 236

    Source documentation

    Expose one independent finite coordinate, retaining every other coordinate. This is the conditional probability step used between distinct seed groups.

    lemma prob_update_bound {I Ω : Type*} [Fintype I] [DecidableEq I]
        [Fintype Ω] [Nonempty Ω] (i : I) (P : (I → Ω) → Prop) {b : ℝ}
        (h : ∀ α, prob (fun r : Ω => P (Function.update α i r)) ≤ b) :
        prob P ≤ b := by
    …

    Mentions: OAI.PlanarL1.FiniteRandom.prob

19. lemma OAI.PlanarL1.FiniteRandom.prob_singleton line 264
20. lemma OAI.PlanarL1.FiniteRandom.prob_prescribed line 275

    Source documentation

    Exact probability of any finite prescribed set of independent fair coins. Unprescribed coins are unrestricted, so their number does not affect the bound.

    lemma prob_prescribed {I : Type*} [Fintype I] (S : Finset I) (b : I → Bool) :
        prob (fun ω : I → Bool => ∀ i ∈ S, ω i=b i) = 1/(2:ℝ)^S.card := by
    …

    Mentions: OAI.PlanarL1.FiniteRandom.prob

21. lemma OAI.PlanarL1.FiniteRandom.prob_two_coins line 298
22. lemma OAI.PlanarL1.FiniteRandom.prob_at_least_prescription line 310

    Source documentation

    Any event forced by at most k independently prescribed group/cell coins has probability at least 2⁻ᵏ.

    lemma prob_at_least_prescription {I : Type*} [Fintype I]
        (S : Finset I) (b : I → Bool) (P : (I → Bool) → Prop) {k : ℕ}
        (hk : S.card ≤ k) (h : ∀ ω, (∀ i ∈ S, ω i=b i) → P ω) :
        1/(2:ℝ)^k ≤ prob P := by
    …

    Mentions: OAI.PlanarL1.FiniteRandom.prob