CodeUnionBound.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite union-bound lemmas for the independent random binary codebook argument in polynomial-code.tex, Lemma lem:random-segments.

theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.exists_avoiding_of_sum_card_lt line 17
Source documentation
A finite family whose total cardinality is smaller than the ambient type cannot cover that type. No probability-space assumptions are required.
```
theorem exists_avoiding_of_sum_card_lt
    {Ω I : Type*} [Fintype Ω] [Fintype I]
    (bad : I → Finset Ω)
    (h : (∑ i, (bad i).card) < Fintype.card Ω) :
    ∃ ω : Ω, ∀ i : I, ω ∉ bad i := by
…
```

theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.exists_avoiding_of_probability_bounds line 38

Source documentation

The same existence statement in terms of real-valued probability bounds for the uniform distribution on a nonempty finite ambient type.

theorem exists_avoiding_of_probability_bounds
    {Ω I : Type*} [Fintype Ω] [Nonempty Ω] [Fintype I]
    (bad : I → Finset Ω) (p : I → ℝ)
    (hbound : ∀ i, ((bad i).card : ℝ) / Fintype.card Ω ≤ p i)
    (hsum : (∑ i, p i) < 1) :
    ∃ ω : Ω, ∀ i : I, ω ∉ bad i := by
…

theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.exists_avoiding_of_uniform_probability_bound line 55

Source documentation

A uniform bad-event estimate needs only a bound on the number of events.

theorem exists_avoiding_of_uniform_probability_bound
    {Ω I : Type*} [Fintype Ω] [Nonempty Ω] [Fintype I]
    (bad : I → Finset Ω) (ε : ℝ)
    (hbound : ∀ i, ((bad i).card : ℝ) / Fintype.card Ω ≤ ε)
    (hsum : (Fintype.card I : ℝ) * ε < 1) :
    ∃ ω : Ω, ∀ i : I, ω ∉ bad i := by
…

theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.exists_avoiding_of_event_count_bound line 67

Source documentation

The uniform criterion with a possibly loose real-valued upper bound on the number of comparisons. This permits endpoints represented by Fin (P+1) without changing the union-bound argument.

theorem exists_avoiding_of_event_count_bound
    {Ω I : Type*} [Fintype Ω] [Nonempty Ω] [Fintype I]
    (bad : I → Finset Ω) (ε N : ℝ) (hε : 0 ≤ ε)
    (hcount : (Fintype.card I : ℝ) ≤ N)
    (hbound : ∀ i, ((bad i).card : ℝ) / Fintype.card Ω ≤ ε)
    (hsum : N * ε < 1) :
    ∃ ω : Ω, ∀ i : I, ω ∉ bad i := by
…

abbrev OAI.TreeEdit.BinaryLower.CodeUnionBound.SegmentComparison line 80
Source documentation
There are at most K² P³ ordered choices of two codeword labels, a positive segment length at most P, and two starting positions. The validity conditions only remove comparisons from this ambient index type.
```
abbrev SegmentComparison (K P : ℕ) :=
…
```
theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.card_segmentComparison line 83
theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.comparison_frequency_lt_one line 90
Source documentation
The polynomial number of comparisons is dominated by the twentieth power appearing after the source's logarithmic segment cutoff.
```
theorem comparison_frequency_lt_one {m p : ℝ}
    (hm : 2 ≤ m) (hp : 1 ≤ p) :
    m ^ 2 * p ^ 3 / (m * p) ^ 20 < 1 := by
…
```

theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.exists_codebook_avoiding line 106

Source documentation

A uniform matching-event bound produces one codebook satisfying every segment comparison simultaneously.

theorem exists_codebook_avoiding
    {M K P : ℕ} (hM : 2 ≤ M) (hK : K ≤ M) (hP : 1 ≤ P)
    (bad : SegmentComparison K P → Finset ((Fin K × Fin P) → Bool))
    (hbound : ∀ i,
      ((bad i).card : ℝ) / (2 : ℝ) ^ (K * P) ≤
        1 / ((M : ℝ) * P) ^ 20) :
    ∃ c : (Fin K × Fin P) → Bool, ∀ i, c ∉ bad i := by
…

Mentions: OAI.TreeEdit.BinaryLower.CodeUnionBound.SegmentComparison

theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.exponential_bound_of_source_cutoff line 134
Source documentation
The source cutoff converts each 2^(-a/2) segment-failure estimate into an inverse sixtieth power of the input length.
```
theorem exponential_bound_of_source_cutoff {m a : ℝ}
    (hm : 0 < m) (ha : 120 * Real.logb 2 m ≤ a) :
    Real.exp (-a * Real.log 2 / 2) ≤ 1 / m ^ 60 := by
…
```
theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.endpoint_comparison_frequency_lt_one line 155
Source documentation
The slightly larger (P+1)^3 comparison index used by endpoint-based formalizations still has total bad probability strictly below one.
```
theorem endpoint_comparison_frequency_lt_one {m : ℝ} (hm : 2 ≤ m) :
    m ^ 2 * (m ^ 2 + 1) ^ 3 / m ^ 60 < 1 := by
…
```
theorem OAI.TreeEdit.BinaryLower.CodeUnionBound.source_cutoff_total_probability_lt_one line 175
Source documentation
Final numerical union-bound estimate at the exact logarithmic cutoff, with endpoint-based comparison indexing and P=M².
```
theorem source_cutoff_total_probability_lt_one {m a : ℝ}
    (hm : 2 ≤ m) (ha : 120 * Real.logb 2 m ≤ a) :
    m ^ 2 * (m ^ 2 + 1) ^ 3 * Real.exp (-a * Real.log 2 / 2) < 1 := by
…
```