cleanup Johnson

Author: Ferinko

ArkLib/Data/CodingTheory/JohnsonBound.lean

@@ -2,17 +2,6 @@
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ilia Vlasov 
 -/
-import Mathlib.Algebra.Field.Rat
-import Mathlib.Analysis.Convex.Function
-import Mathlib.Data.Real.Sqrt
-import Mathlib.Data.Set.Pairwise.Basic
-import Mathlib.Algebra.BigOperators.Field
-import Mathlib.Analysis.Convex.Jensen
-import Mathlib.Algebra.Module.LinearMap.Defs
-
-import ArkLib.Data.CodingTheory.Basic
-import ArkLib.Data.CodingTheory.JohnsonBound.Choose2
-import ArkLib.Data.CodingTheory.JohnsonBound.Expectations
 import ArkLib.Data.CodingTheory.JohnsonBound.Lemmas
 
 namespace JohnsonBound
@@ -27,7 +16,8 @@ In what follows we reference theorems from [listdecoding] by default.
 -/
 
 variable {n : ℕ}
-variable {F : Type} [Fintype F] [DecidableEq F]
+         {F : Type} [Fintype F] [DecidableEq F]
+         {B : Finset (Fin n → F)} {v : Fin n → F}
 
 /--
 The denominator of the bound from theorem 3.1. 
@@ -39,9 +29,9 @@ def JohnsonDenominator (B : Finset (Fin n → F)) (v : Fin n → F) : ℚ :=
   let frac := q / (q - 1)
   (1- frac * e/n) ^ 2 - (1 - frac * d/n)
 
-lemma johnson_denominator_def {B : Finset (Fin n → F)} {v : Fin n → F} :
-  JohnsonDenominator B v = ((1 - ((Fintype.card F : ℚ) / (Fintype.card F - 1)) * (e B v / n)) ^ 2 
-      - (1 - ((Fintype.card F : ℚ) / (Fintype.card F - 1)) * (d B/n))) := by
+lemma johnson_denominator_def :
+  JohnsonDenominator B v = ((1 - ((Fintype.card F) / (Fintype.card F - 1)) * (e B v / n)) ^ 2 
+      - (1 - ((Fintype.card F) / (Fintype.card F - 1)) * (d B/n))) := by
   simp [JohnsonDenominator]
   field_simp
 
@@ -81,73 +71,37 @@ lemma johnson_condition_weak_implies_strong {B : Finset (Fin n → F)} {v : Fin
   sorry
 
 private lemma johnson_condition_strong_implies_n_pos {B : Finset (Fin n → F)} {v : Fin n → F} 
+private lemma johnson_condition_strong_implies_n_pos
   (h_johnson : JohnsonConditionStrong B v)
   :
   0 < n := by
   cases n <;> try simp [JohnsonConditionStrong] at *
 
-private lemma johnson_condition_strong_implies_2_le_F_card {B : Finset (Fin n → F)} {v : Fin n → F} 
+private lemma johnson_condition_strong_implies_2_le_F_card
   (h_johnson : JohnsonConditionStrong B v)
   :
   2 ≤ Fintype.card F := by
-  generalize h : Fintype.card F = card 
-  rcases card with _ | card 
-  · simp [JohnsonConditionStrong] at h_johnson 
-    rw [h] at h_johnson 
-    simp at h_johnson
-  · rcases card with _ | card 
-    · simp [JohnsonConditionStrong] at h_johnson 
-      rw [h] at h_johnson
-      simp at h_johnson 
-    · omega
+  revert h_johnson
+  dsimp [JohnsonConditionStrong]
+  rcases Fintype.card F with _ | _ | _ <;> aesop
 
 private lemma johnson_condition_strong_implies_2_le_B_card {B : Finset (Fin n → F)} {v : Fin n → F} 
+private lemma johnson_condition_strong_implies_2_le_B_card
   (h_johnson : JohnsonConditionStrong B v)
   :
   2 ≤ B.card := by
-  generalize h : B.card = card 
-  rcases card with _ | card 
-  · simp [JohnsonConditionStrong] at *
-    simp [e, d] at *
-    subst h
-    simp at h_johnson
-  · rcases card with _ | card 
-    · simp [JohnsonConditionStrong] at *
-      simp [e, d] at *
-      rw [h] at h_johnson
-      simp [choose_2] at h_johnson
-      have h_set := Finset.card_eq_one.1 h 
-      rcases h_set with ⟨a, h_set⟩
-      rw [h_set] at h_johnson 
-      simp at h_johnson
-      generalize hq : Fintype.card F = q 
-      rcases q with _ | q
-      · simp [hq] at h_johnson 
-      · rcases q with _ | q 
-        · simp [hq] at h_johnson
-        · have h : (Fintype.card F : ℚ) /((Fintype.card F : ℚ) - 1) = 
-            (1 : ℚ) + (1:ℚ)/((Fintype.card F : ℚ) - 1) := by
-            have h : (Fintype.card F : ℚ) = ((Fintype.card F : ℚ) - 1) + 1 := by ring
-            conv =>
-              lhs 
-              congr 
-              rw [h]
-              rfl
-              rfl
-            rw [Field.div_eq_mul_inv, Field.div_eq_mul_inv]
-            rw [add_mul]
-            rw [Field.mul_inv_cancel _ (by {
-              rw [hq]
-              simp
-              aesop
-            })]
-          rw [h] at h_johnson 
-          have h' := JohnsonBound.a_lemma_im_not_proud_of (v := v) (a := a) (by omega)
-          have h : (1 :ℚ) < (1 : ℚ) := by 
-            apply lt_of_lt_of_le h_johnson 
-            assumption 
-          simp at h
-    · omega 
+  dsimp [JohnsonConditionStrong] at h_johnson
+  rcases eq : B.card with _ | card | _ <;> [simp_all [e, d]; skip; omega]
+  obtain ⟨a, ha⟩ := Finset.card_eq_one.1 eq
+  replace h_johnson : 1 < |1 - (Fintype.card F) / ((Fintype.card F) - 1) * Δ₀(v, a) / (n : ℚ)| := by
+    simp_all [e, d, choose_2]
+  generalize eq₁ : Fintype.card F = q
+  rcases q with _ | _ | q <;> [simp_all; simp_all; skip]
+  have h : (Fintype.card F : ℚ) / (Fintype.card F - 1) = 1 + 1 / (Fintype.card F - 1) := by
+    have : (Fintype.card F : ℚ) - 1 ≠ 0 := by simp [sub_eq_zero]; omega
+    field_simp
+  have h' := JohnsonBound.abs_one_sub_div_le_one (v := v) (a := a) (by omega)
+  exact absurd (lt_of_lt_of_le (h ▸ h_johnson) h') (lt_irrefl _)
 
 /-- 
 `JohnsonConditionStrong` is equvalent to `JohnsonDenominator` being positive.
@@ -160,6 +114,11 @@ lemma johnson_condition_strong_iff_johnson_denom_pos {B : Finset (Fin n → F)}
 Theorem 3.1.
 --/
 theorem johnson_bound [Field F] {B : Finset (Fin n → F)} {v : Fin n → F}
+lemma johnson_condition_strong_iff_johnson_denom_pos :
+  JohnsonConditionStrong B v ↔ 0 < JohnsonDenominator B v := by
+  simp [JohnsonDenominator, JohnsonConditionStrong]
+
+theorem johnson_bound_OLD [Field F]
   (h_condition : JohnsonConditionStrong B v)
   :
   let d := d B
@@ -175,7 +134,7 @@ theorem johnson_bound [Field F] {B : Finset (Fin n → F)} {v : Fin n → F}
   rw [mul_assoc, mul_comm ((_)⁻¹) _, Field.mul_inv_cancel _ (by linarith)]
   simp 
   rw [johnson_denominator_def]
-  apply JohnsonBound.johnson_bound_lemma 
+  exact JohnsonBound.johnson_bound_lemma 
     (johnson_condition_strong_implies_n_pos h_condition') 
     (johnson_condition_strong_implies_2_le_B_card h_condition') 
     (johnson_condition_strong_implies_2_le_F_card h_condition')
@@ -198,5 +157,24 @@ theorem johnson_bound_alphabet_free [Field F] [DecidableEq F]
   →
   (B ∩ ({ x | Δ₀(x, v) ≤ e } : Finset _)).card ≤ q * d * n := by
   sorry
+theorem johnson_bound [Field F]
+  (h_condition : JohnsonConditionStrong B v)
+  :
+  let d := d B
+  let q : ℚ := Fintype.card F
+  let frac := q / (q - 1)
+  B.card ≤ (frac * d/n) / JohnsonDenominator B v 
+  := by
+  suffices B.card * JohnsonDenominator B v ≤
+           Fintype.card F / (Fintype.card F - 1) * d B / n by
+    rw [johnson_condition_strong_iff_johnson_denom_pos] at h_condition
+    rw [←mul_le_mul_right h_condition]
+    convert this using 1
+    field_simp; rw [mul_div_mul_right]; linarith
+  rw [johnson_denominator_def]
+  exact JohnsonBound.johnson_bound_lemma 
+    (johnson_condition_strong_implies_n_pos h_condition) 
+    (johnson_condition_strong_implies_2_le_B_card h_condition) 
+    (johnson_condition_strong_implies_2_le_F_card h_condition)
 
 end JohnsonBound