cleanup Johnson

Author: Ferinko

ArkLib/Data/CodingTheory/JohnsonBound.lean

@@ -2,23 +2,13 @@
 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
 
 variable {n : ℕ}
-variable {F : Type} [Fintype F] [DecidableEq F]
+         {F : Type} [Fintype F] [DecidableEq F]
+         {B : Finset (Fin n → F)} {v : Fin n → F}
 
 def JohnsonDenominator (B : Finset (Fin n → F)) (v : Fin n → F) : ℚ :=
   let e := e B v 
@@ -27,9 +17,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
 
@@ -40,81 +30,42 @@ def JohnsonConditionStrong (B : Finset (Fin n → F)) (v : Fin n → F) : Prop :
   let frac := q / (q - 1)
   (1 - frac * d/n) < (1- frac * e/n) ^ 2 
 
-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 _)
 
-lemma johnson_condition_strong_iff_johnson_denom_pos {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 [Field F] {B : Finset (Fin n → F)} {v : Fin n → F}
+theorem johnson_bound_OLD [Field F]
   (h_condition : JohnsonConditionStrong B v)
   :
   let d := d B
@@ -130,10 +81,29 @@ 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')
-    
+
+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

ArkLib/Data/CodingTheory/JohnsonBound/Choose2.lean

@@ -16,58 +16,31 @@ namespace JohnsonBound
 
 private def f (x : ℚ) : ℚ := x^2 - x 
 
-private lemma x_sqr_minus_x_is_conv' {x₁ x₂ : ℚ} {α₁ α₂ : ℚ} 
+private lemma f_convex {x₁ x₂ : ℚ} {α₁ α₂ : ℚ} 
   (h_noneg_1 : 0 ≤ α₁)
   (h_noneg_2 : 0 ≤ α₂)
   (h_conv : α₁ + α₂ = 1)
   :
   f (α₁ * x₁ + α₂ * x₂) ≤ α₁ * f x₁ + α₂ * f x₂ := by
   unfold f 
-  have h_conv : α₂ = 1 - α₁ := by 
-    rw [←h_conv]
-    field_simp
-  rw [add_sq, mul_sub, mul_sub]
-  have h : α₁ * x₁ ^ 2 - α₁ * x₁ + (α₂ * x₂ ^ 2 - α₂ * x₂) 
-    = α₁ * x₁ ^ 2  + α₂ * x₂ ^ 2 - (α₁ * x₁ + α₂ * x₂) := by ring
-  rw [h]
-  field_simp
-  rw [h_conv]
-  have h : (α₁ * x₁) ^ 2 + 2 * (α₁ * x₁) * ((1 - α₁) * x₂) + ((1 - α₁) * x₂) ^ 2
-    = α₁^2 * x₁ ^ 2 + 2 * (α₁ * (1 - α₁) * x₁ * x₂) + (1 - α₁)^2 * x₂ ^ 2 := by ring
-  rw [h]
-  apply add_le_of_le_sub_left 
-  conv =>
-    lhs 
-    rw [←add_zero ((1 - α₁) ^ 2 * x₂ ^ 2)]
-    rfl
-  apply add_le_of_le_sub_left 
-  have h : α₁ * x₁ ^ 2 
-    + (1 - α₁) * x₂ ^ 2 - (α₁ ^ 2 * x₁ ^ 2 + 2 * (α₁ * (1 - α₁) * x₁ * x₂)) - (1 - α₁) ^ 2 * x₂ ^ 2 
-    = α₁ * (1 - α₁) * x₁^2 - 2 * α₁ * (1 - α₁) * x₁ * x₂ + (1 - α₁) * α₁ * x₂^2 := by ring_nf 
-  rw [h]
-  have h : α₁ * (1 - α₁) * x₁ ^ 2 - 2 * α₁ * (1 - α₁) * x₁ * x₂ + (1 - α₁) * α₁ * x₂ ^ 2 
-    = α₁ * (1 - α₁) * (x₁ - x₂ ) ^ 2 := by ring
-  rw [h, ←h_conv]
-  apply mul_nonneg 
-  apply mul_nonneg h_noneg_1 h_noneg_2 
-  exact sq_nonneg _
+  obtain ⟨rfl⟩ := show α₂ = 1 - α₁ by rw [←h_conv]; simp
+  suffices 0 ≤ α₁ * (1 - α₁) * (x₁ - x₂) ^ 2 by linarith
+  exact mul_nonneg (mul_nonneg h_noneg_1 h_noneg_2) (sq_nonneg _)
 
 def choose_2 (x : ℚ) : ℚ := x * (x-1)/2
 
 private lemma choose_2_eq_half_f :
-  choose_2  = (1/2) * f  := by 
+  choose_2 = (1/2) * f := by 
   ext x
   simp [choose_2, f]
   ring
 
-theorem choose_2_convex :
-  ConvexOn ℚ Set.univ choose_2 := by 
-  simp [ConvexOn, Convex, StarConvex] 
+@[simp]
+theorem choose_2_convex : ConvexOn ℚ Set.univ choose_2 := by 
   rw [choose_2_eq_half_f]
+  refine ⟨convex_univ, fun x₁ _ x₂ _ α₁ α₂ hα₁ hα₂ h ↦ ?p₁⟩
+  have := f_convex (x₁ := x₁) (x₂ := x₂) hα₁ hα₂ h
   field_simp
-  intro x₁ x₂ α₁ α₂ hα₁ hα₂ h_conv
-  rw [Field.div_eq_mul_inv, Field.div_eq_mul_inv]
-  rw [mul_le_mul_right (by simp)]
-  apply x_sqr_minus_x_is_conv' <;> aesop
+  linarith
 
 end JohnsonBound

ArkLib/Data/CodingTheory/JohnsonBound/Expectations.lean

@@ -17,63 +17,42 @@ import ArkLib.Data.CodingTheory.JohnsonBound.Choose2
 namespace JohnsonBound
 
 variable {n : ℕ}
-variable {F : Type*} [Fintype F] [DecidableEq F]
+variable {F : Type*} [DecidableEq F]
+         {B : Finset (Fin n → F)} {v : Fin n → F}
 
 def e (B : Finset (Fin n → F)) (v : Fin n → F) : ℚ :=
-  (1 : ℚ)/B.card * ∑ x ∈ B, Δ₀(v, x) 
+  (1 : ℚ)/B.card * ∑ x ∈ B, Δ₀(v, x)
 
 def d (B : Finset (Fin n → F)) : ℚ :=
   (1 : ℚ)/(2 * choose_2 B.card) * ∑ x ∈ (Finset.product B B) with x.1 ≠ x.2, Δ₀(x.1, x.2) 
 
-lemma lin_shift_card [Field F] {B : Finset (Fin n → F)} {v : Fin n → F}
+lemma lin_shift_card [Field F] [Fintype F]
   :
   B.card = ({ x - v | x ∈ B} : Finset _).card := by
-  apply Finset.card_bij
-    (i := fun x _ => x - v)
-    (by aesop)
-    (by simp)
-    (by simp)
+  apply Finset.card_bij (i := fun x _ => x - v) <;> aesop
 
 @[simp]
 lemma lin_shift_hamming_distance [Field F] {x₁ x₂ v : Fin n → F}
   :
-  Δ₀(x₁ - v, x₂ - v) = Δ₀(x₁, x₂) := by
-  simp [hammingDist]
-lemma lin_shift_e [Field F] {B : Finset (Fin n → F)} {v : Fin n → F}
+  Δ₀(x₁ - v, x₂ - v) = Δ₀(x₁, x₂) := by simp [hammingDist]
+
+lemma lin_shift_e [Field F] [Fintype F]
   (h_B : B.card ≠ 0)
   :
   e B v = e ({ x - v | x ∈ B} : Finset _) 0 := by
   simp [e]
   rw [←lin_shift_card]
   field_simp
-  apply Finset.sum_bij (i := fun x _ => x - v) <;> try simp [hammingDist, hammingNorm] 
-  intro a ha 
-  apply Finset.card_bij (i := fun x _ => x) <;> try tauto
-  simp at *
-  intro α₁ h contr
-  rw [←zero_add (v α₁)] at h
-  rw [←contr] at h 
-  simp at h  
-  simp 
-  intro b h contr 
-  rw [contr] at h
-  simp at h
+  apply Finset.sum_bij (i := fun x _ => x - v) <;>
+    simp [hammingDist, hammingNorm, sub_eq_zero, eq_comm]
 
-lemma lin_shift_d [Field F] {B : Finset (Fin n → F)} (v : Fin n → F)
+lemma lin_shift_d [Field F] [Fintype F]
   (h_B : 2 ≤ B.card)
   :
-  d B = d ({ x - v | x ∈ B} : Finset _) := by
+  d B = d ({x - v | x ∈ B} : Finset _) := by
   simp [d]
   rw [←lin_shift_card]
-  have h : choose_2 B.card ≠ 0 := by
-    simp [choose_2]
-    apply And.intro (by aesop)
-    intro contr 
-    have h : (B.card : ℚ) = 1 := by 
-      rw [←zero_add (1 : ℚ), ←contr] 
-      simp
-    simp at h
-    omega
+  have h : choose_2 B.card ≠ 0 := by aesop (add simp [choose_2, sub_eq_zero])
   field_simp 
   apply Finset.sum_bij (fun x _ => (x.1 - v, x.2 -v)) <;> try aesop