|
1 | | -/- Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. |
2 | | -Released under Apache 2.0 license as described in the file LICENSE. |
3 | | -Authors: Ilia Vlasov, František Silváši |
4 | | --/ |
| 1 | +import ArkLib.Data.CodingTheory.JohnsonBound.Basic |
| 2 | +import ArkLib.Data.CodingTheory.JohnsonBound.Choose2 |
| 3 | +import ArkLib.Data.CodingTheory.JohnsonBound.Expectations |
5 | 4 | import ArkLib.Data.CodingTheory.JohnsonBound.Lemmas |
6 | | - |
7 | | -namespace JohnsonBound |
8 | | - |
9 | | -/-! |
10 | | -This module is based on the Johnson Bound section from [listdecoding]. |
11 | | -In what follows we reference theorems from [listdecoding] by default. |
12 | | -
|
13 | | -## References |
14 | | -
|
15 | | -* [Venkatesan Guruswami, *Algorithmic Results in List Decoding*][listdecoding] |
16 | | --/ |
17 | | - |
18 | | -variable {n : ℕ} |
19 | | - {F : Type} [Fintype F] [DecidableEq F] |
20 | | - {B : Finset (Fin n → F)} {v : Fin n → F} |
21 | | - |
22 | | -/-- |
23 | | -The denominator of the bound from theorem 3.1. |
24 | | --/ |
25 | | -def JohnsonDenominator (B : Finset (Fin n → F)) (v : Fin n → F) : ℚ := |
26 | | - let e := e B v |
27 | | - let d := d B |
28 | | - let q : ℚ := Fintype.card F |
29 | | - let frac := q / (q - 1) |
30 | | - (1- frac * e/n) ^ 2 - (1 - frac * d/n) |
31 | | - |
32 | | -lemma johnson_denominator_def : |
33 | | - JohnsonDenominator B v = ((1 - ((Fintype.card F) / (Fintype.card F - 1)) * (e B v / n)) ^ 2 |
34 | | - - (1 - ((Fintype.card F) / (Fintype.card F - 1)) * (d B/n))) := by |
35 | | - simp [JohnsonDenominator] |
36 | | - field_simp |
37 | | - |
38 | | -/-- |
39 | | -The bound from theorem 3.1 makes sense only if the denominator is positive. |
40 | | -This condition ensures that holds. |
41 | | --/ |
42 | | -def JohnsonConditionStrong (B : Finset (Fin n → F)) (v : Fin n → F) : Prop := |
43 | | - let e := e B v |
44 | | - let d := d B |
45 | | - let q : ℚ := Fintype.card F |
46 | | - let frac := q / (q - 1) |
47 | | - (1 - frac * d/n) < (1- frac * e/n) ^ 2 |
48 | | - |
49 | | -/-- |
50 | | -The function used for q-ary Johnson Bound. |
51 | | --/ |
52 | | -noncomputable def J (q δ : ℚ) : ℝ := |
53 | | - let frac := q / (q - 1) |
54 | | - (1 / frac) * (1 - Real.sqrt (1 - frac * δ)) |
55 | | - |
56 | | -lemma sqrt_le_J {q x : ℚ} : |
57 | | - 1 - ((1-x) : ℝ).sqrt ≤ J q x := by sorry |
58 | | - |
59 | | -/-- |
60 | | -The q-ary Johnson bound. |
61 | | --/ |
62 | | -def JohnsonConditionWeak (B : Finset (Fin n → F)) (e : ℕ) : Prop := |
63 | | - let d := sInf { d | ∃ u ∈ B, ∃ v ∈ B, u ≠ v ∧ hammingDist u v = d } |
64 | | - let q : ℚ := Fintype.card F |
65 | | - (e : ℚ) / n < J q (d / n) |
66 | | - |
67 | | -lemma johnson_condition_weak_implies_strong {B : Finset (Fin n → F)} {v : Fin n → F} {e : ℕ} |
68 | | - (h : JohnsonConditionWeak B e) |
69 | | - : |
70 | | - JohnsonConditionStrong (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)) v := by |
71 | | - sorry |
72 | | - |
73 | | -private lemma johnson_condition_strong_implies_n_pos |
74 | | - (h_johnson : JohnsonConditionStrong B v) |
75 | | - : |
76 | | - 0 < n := by |
77 | | - cases n <;> try simp [JohnsonConditionStrong] at * |
78 | | - |
79 | | -private lemma johnson_condition_strong_implies_2_le_F_card |
80 | | - (h_johnson : JohnsonConditionStrong B v) |
81 | | - : |
82 | | - 2 ≤ Fintype.card F := by |
83 | | - revert h_johnson |
84 | | - dsimp [JohnsonConditionStrong] |
85 | | - rcases Fintype.card F with _ | _ | _ <;> aesop |
86 | | - |
87 | | -private lemma johnson_condition_strong_implies_2_le_B_card |
88 | | - (h_johnson : JohnsonConditionStrong B v) |
89 | | - : |
90 | | - 2 ≤ B.card := by |
91 | | - dsimp [JohnsonConditionStrong] at h_johnson |
92 | | - rcases eq : B.card with _ | card | _ <;> [simp_all [e, d]; skip; omega] |
93 | | - obtain ⟨a, ha⟩ := Finset.card_eq_one.1 eq |
94 | | - replace h_johnson : 1 < |1 - (Fintype.card F) / ((Fintype.card F) - 1) * Δ₀(v, a) / (n : ℚ)| := by |
95 | | - simp_all [e, d, choose_2] |
96 | | - generalize eq₁ : Fintype.card F = q |
97 | | - rcases q with _ | _ | q <;> [simp_all; simp_all; skip] |
98 | | - have h : (Fintype.card F : ℚ) / (Fintype.card F - 1) = 1 + 1 / (Fintype.card F - 1) := by |
99 | | - have : (Fintype.card F : ℚ) - 1 ≠ 0 := by simp [sub_eq_zero]; omega |
100 | | - field_simp |
101 | | - have h' := JohnsonBound.abs_one_sub_div_le_one (v := v) (a := a) (by omega) |
102 | | - exact absurd (lt_of_lt_of_le (h ▸ h_johnson) h') (lt_irrefl _) |
103 | | - |
104 | | -/-- |
105 | | -`JohnsonConditionStrong` is equvalent to `JohnsonDenominator` being positive. |
106 | | --/ |
107 | | -lemma johnson_condition_strong_iff_johnson_denom_pos {B : Finset (Fin n → F)} {v : Fin n → F} : |
108 | | - JohnsonConditionStrong B v ↔ 0 < JohnsonDenominator B v := by |
109 | | - simp [JohnsonDenominator, JohnsonConditionStrong] |
110 | | - |
111 | | -/-- |
112 | | -Theorem 3.1. |
113 | | ---/ |
114 | | -theorem johnson_bound [Field F] |
115 | | - (h_condition : JohnsonConditionStrong B v) |
116 | | - : |
117 | | - let d := d B |
118 | | - let q : ℚ := Fintype.card F |
119 | | - let frac := q / (q - 1) |
120 | | - B.card ≤ (frac * d/n) / JohnsonDenominator B v |
121 | | - := by |
122 | | - suffices B.card * JohnsonDenominator B v ≤ |
123 | | - Fintype.card F / (Fintype.card F - 1) * d B / n by |
124 | | - rw [johnson_condition_strong_iff_johnson_denom_pos] at h_condition |
125 | | - rw [←mul_le_mul_right h_condition] |
126 | | - convert this using 1 |
127 | | - field_simp; rw [mul_div_mul_right]; linarith |
128 | | - rw [johnson_denominator_def] |
129 | | - exact JohnsonBound.johnson_bound_lemma |
130 | | - (johnson_condition_strong_implies_n_pos h_condition) |
131 | | - (johnson_condition_strong_implies_2_le_B_card h_condition) |
132 | | - (johnson_condition_strong_implies_2_le_F_card h_condition) |
133 | | - |
134 | | -/-- |
135 | | -Alphabet-free Johnson bound from [codingtheory]. |
136 | | -## References |
137 | | -
|
138 | | -* [Venkatesan Guruswami, Atri Rudra, Madhu Sudan, *Essential Coding Theory*][codingtheory] |
139 | | --/ |
140 | | -theorem johnson_bound_alphabet_free [Field F] [DecidableEq F] |
141 | | - {B : Finset (Fin n → F)} |
142 | | - {v : Fin n → F} |
143 | | - {e : ℕ} |
144 | | - : |
145 | | - let d := sInf { d | ∃ u ∈ B, ∃ v ∈ B, u ≠ v ∧ hammingDist u v = d } |
146 | | - let q : ℚ := Fintype.card F |
147 | | - let frac := q / (q - 1) |
148 | | - e ≤ n - ((n * (n - d)) : ℝ).sqrt |
149 | | - → |
150 | | - (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)).card ≤ q * d * n := by |
151 | | - sorry |
152 | | - |
153 | | -end JohnsonBound |
0 commit comments