diff --git a/ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean b/ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean index 2b04cb5b0..e66f5d51b 100644 --- a/ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean +++ b/ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean @@ -86,11 +86,154 @@ def JohnsonConditionWeak (B : Finset (Fin n → F)) (e : ℕ) : Prop := let q : ℚ := Fintype.card F (e : ℚ) / n < J q (d / n) -lemma johnson_condition_weak_implies_strong {B : Finset (Fin n → F)} {v : Fin n → F} {e : ℕ} - (h : JohnsonConditionWeak B e) +lemma johnson_condition_weak_implies_strong [Field F] + {B : Finset (Fin n → F)} + {v : Fin n → F} + {e : ℕ} + (h_J_cond_weak : JohnsonConditionWeak B e) + (h_B2_not_one : 1 < (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)).card) + (h_F_nontriv : 2 ≤ Fintype.card F) : JohnsonConditionStrong (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)) v := by - sorry + --We show that n > 0, the theorem is ill-posed in this case but it follows from our assumptions. + have h_n_pos : 0 < n := by + by_contra hn + push_neg at hn + have : n = 0 := by omega + subst this + have B_singleton : B.card ≤ 1 := by + have : ∀ u ∈ B, ∀ v ∈ B, u = v := by + intros u hu v hv + funext s + exact Fin.elim0 s + have : ¬∃ (u v : B), u ≠ v := by grind + have neg_of_ineq := (Fintype.one_lt_card_iff.1).mt this + simp at neg_of_ineq + exact neg_of_ineq + have B2_too_small : (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)).card ≤ 1 := by + have B_supset : B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _) ⊆ B := by grind + have eval_cards := Finset.card_le_card B_supset + linarith + omega + unfold JohnsonConditionStrong + intro e_1 d q frac + -- The real 'proof' is not really by cases, the second case is uninteresting in practice. + -- However, the theorem still holds when 1 - frac * d / ↑n < 0 and we prove both cases to avoid + -- adding unnecessary assumptions. + by_cases h_dsqrt_pos : (0 : ℝ) ≤ 1 - frac * d / ↑n + · have h_B2_nonempty : (0 : ℚ) < ((B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)).card : ℚ) + := by norm_cast; omega + have h_frac_pos : frac > 0 := by + unfold frac + have : 1 < Fintype.card F := by linarith + field_simp + unfold q + exact_mod_cast this + --The main proof is here, and in the proof of err_n, the rest is algebraic manipulations. + have j_fun_bound : (↑e / ↑n : ℝ) < (1/↑frac * (1-√(1 - ↑frac * ↑d / ↑n))) := by + unfold JohnsonConditionWeak J at h_J_cond_weak + simp_all + let d_weak := sInf {d | ∃ u ∈ B, ∃ v ∈ B, ¬u=v ∧ Δ₀(u,v)=d} + have d_subset : ↑d_weak ≤ (d : ℚ) := by + unfold d + unfold JohnsonBound.d + unfold d_weak + have min_dist := min_dist_le_d h_B2_not_one + have subset_inf_ineq : sInf {d | ∃ u ∈ B, ∃ v ∈ B, u ≠ v ∧ Δ₀(u, v) = d} ≤ + sInf {d | + ∃ u ∈ (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)), + ∃ v_1 ∈ (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)), + u ≠ v_1 ∧ Δ₀(u, v_1) = d}:= by + have subset : {d | + ∃ u ∈ (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)), + ∃ v_1 ∈ (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)), + u ≠ v_1 ∧ Δ₀(u, v_1) = d} + ⊆ {d | ∃ u ∈ B, ∃ v ∈ B, u ≠ v ∧ Δ₀(u, v) = d} := by + intro d ⟨u, hu_in, v_1, hv_in, hne, heq⟩ + exact + ⟨u, by simp at hu_in; exact hu_in.1, v_1 + , by simp at hv_in; exact hv_in.1, hne, heq⟩ + gcongr + obtain ⟨u, hu, v_1, hv_1, hne⟩ := Finset.one_lt_card.mp h_B2_not_one + use Δ₀(u, v_1) + exact ⟨u, hu, v_1, hv_1, hne, rfl⟩ + calc ↑d_weak + = ↑(sInf {d | ∃ u ∈ B, ∃ v ∈ B, ¬u = v ∧ Δ₀(u, v) = d}) := by rfl + _ ≤ ↑(sInf {d | + ∃ u ∈ (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)), + ∃ v_1 ∈ (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)), + u ≠ v_1 ∧ Δ₀(u, v_1) = d}):= by exact_mod_cast subset_inf_ineq + _ ≤ JohnsonBound.d (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)) := by exact_mod_cast min_dist + have bound: (↑frac)⁻¹ * (1 - √(1 - ↑frac * ↑d_weak / ↑n)) + ≤ (↑frac)⁻¹ * (1 - √(1 - ↑frac * ↑d / ↑n)) := by + have ineq1 : (↑d_weak / ↑n) ≤ (d / ↑n) := by + rw[←mul_le_mul_iff_of_pos_left (Nat.cast_pos.mpr h_n_pos)] + field_simp + exact d_subset + have ineq2 : frac * (d_weak / n) ≤ frac * (d / n) := by + exact_mod_cast (mul_le_mul_iff_of_pos_left h_frac_pos).mpr ineq1 + have ineq3 : 1 - frac * (d / n) ≤ 1 - frac * (d_weak / n ) := by linarith + have ineq3' : (1 : ℝ) - frac * d / n ≤ (1 : ℝ) - frac * d_weak / n := by + norm_cast; grind + have ineq4 : √(1 - ↑frac * ↑d / ↑n) ≤ √(1 - ↑frac * ↑d_weak / ↑n) := + by exact Real.sqrt_le_sqrt ineq3' + have ineq5 : (1 - √(1 - ↑frac * ↑d_weak / ↑n)) ≤ (1 - √(1 - ↑frac * ↑d / ↑n)) := by + linarith + simp_all + have h_J_cond_weak' : ↑e / ↑n < 1 / (↑frac) * (1 - √(1 - frac * (d_weak / ↑n))) := by + unfold frac + unfold q + unfold d_weak + push_cast + rw [one_div_div] + exact h_J_cond_weak + field_simp + field_simp at h_J_cond_weak' + field_simp at bound + linarith + have err_n : (↑e_1 / ↑n : ℝ) ≤ (↑e / ↑n : ℝ) := by + gcongr + have err : e_1 ≤ e := by + unfold e_1 + dsimp[JohnsonBound.e] + have : ∀ x ∈ B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _), Δ₀(v, x) ≤ e := by + unfold hammingDist + simp + (simp_rw [eq_comm] ; grind) + have sum_bound := + Finset.sum_le_card_nsmul (B ∩ ({x | Δ₀(x, v) ≤ e} : Finset _)) + (fun x => Δ₀(v, x)) e this + simp + rw[inv_mul_le_iff₀ h_B2_nonempty] + exact_mod_cast sum_bound + exact_mod_cast err + have j_fun_bound_e1 : (↑e_1 / ↑n : ℝ) < (1/↑frac * (1-√(1 - ↑frac * ↑d / ↑n))) := + by linarith [err_n, j_fun_bound] + have rearrange_jboundw_e1 : √(1 - ↑frac * ↑d / ↑n) < 1 - frac * e_1 / ↑n := by + have : frac * e_1 / ↑n < 1-√(1 - frac * d / ↑n) := by + calc ↑frac * ↑e_1 / ↑n + = ↑frac * (↑e_1 / ↑n) := by ring + _ < ↑frac * (1/↑frac * (1-√(1 - ↑frac * ↑d / ↑n))) := by + exact (mul_lt_mul_left (by exact_mod_cast h_frac_pos)).mpr j_fun_bound_e1 + _ = 1-√(1 - ↑frac * ↑d / ↑n) := by ring_nf ; field_simp + linarith + have h_esqrtpos : (0 : ℝ) ≤ 1- frac * e_1 / ↑n := by + have : (0 : ℝ) ≤ √(1 - ↑frac * ↑d / ↑n) := by aesop + linarith[this, rearrange_jboundw_e1] + suffices recast_main_goal : (1 - frac * d / ↑n : ℝ) < (1 - frac * e_1 / ↑n) ^ 2 by + exact_mod_cast recast_main_goal + suffices roots : √(1 - frac * d / ↑n) < 1- frac * e_1 / ↑n by + rw[←Real.sqrt_lt h_dsqrt_pos h_esqrtpos] + exact_mod_cast roots + exact rearrange_jboundw_e1 + · have strict_neg : 1 - ↑frac * ↑d / ↑n < (0 : ℚ) := by + have : ¬(0 : ℚ) ≤ 1 - frac * d / ↑n := by exact_mod_cast h_dsqrt_pos + rw[Rat.not_le] at this + exact this + have nonneg : (0 : ℝ) ≤(1 - ↑frac * ↑e_1 / ↑n) ^ 2 := + by exact_mod_cast sq_nonneg (1 - frac * ↑e_1 / ↑n) + calc 1 - ↑frac * ↑d / ↑n < (0 : ℚ) := strict_neg + _ ≤ (1 - ↑frac * ↑e_1 / ↑n) ^ 2 := by exact_mod_cast nonneg private lemma johnson_condition_strong_implies_n_pos (h_johnson : JohnsonConditionStrong B v)