Interleaved affine gaps imply tensor gaps

theorem interleaved_affine_gaps_imply_tensor_gaps    (hC_proximityGapAffineLines : e_ε_correlatedAgreementAffineLinesNat      (F := F) (A := A) (ι := ι) (C := MC) (e := e) (ε := ε))    (h_interleaved_gaps : ∀ m : ℕ, m ≥ 1 →      e_ε_correlatedAgreementAffineLinesNat (F := F)        (A := InterleavedSymbol A (Fin m)) (ι := ι) (C := MC ^⋈ (Fin m)) e ε) :    ∀ (ϑ : ℕ), (hϑ_gt_0 : ϑ > 0) → δ_ε_multilinearCorrelatedAgreement_Nat (F := F) (A := A)      (ι := ι) (C := MC) (ϑ := ϑ) (e := e) (ε := ε) := by    classical    intro ϑ    induction ϑ with    | zero =>      intro u      contradiction    | succ ϑ_sub_1 ih =>      cases ϑ_sub_1 with      | zero =>        -- `ϑ = 1`        simp only [zero_add, gt_iff_lt, zero_lt_one, ModuleCode, forall_const]        intro u        let toAffineLineEval := multilinearCombine₁_eq_affineLineEvaluation (F := F) (u := u)        intro hprob_gt        simp_rw [toAffineLineEval] at hprob_gt        let prob_eq := prob_uniform_singleton_finFun_eq (F := F)          (P := fun r => Δ₀(affineLineEvaluation (u 0) (u 1) r, MC) ≤ e)        -- Convert sampling (r ← (Fin 1 → F)) into sampling (r ← F)        simp_rw [prob_eq, Nat.cast_one, ENNReal.coe_one, one_mul] at hprob_gt        have h_correlated_agreement := hC_proximityGapAffineLines (u 0) (u 1) hprob_gt        simp only [jointProximityNat₂, Fin.isValue] at h_correlated_agreement        have h_u_eq: u = finMapTwoWords (u 0) (u 1) := by          funext rowIdx          match rowIdx with          | 0 => rfl          | 1 => rfl        rw [h_u_eq.symm] at h_correlated_agreement        exact h_correlated_agreement      | succ ϑ_sub_2 =>        intro hϑ_gt_0 u hP_multilinearCombine_close_gt        -- `ϑ ≥ 2`        -- set ϑ_sub_1 := ϑ_sub_2 + 1        let ϑ := ϑ_sub_2 + 1 + 1        have hϑ : ϑ = ϑ_sub_2 + 1 + 1 := by rfl        -- have hfinϑ : Fin ϑ = Fin (ϑ_sub_2 + 1 + 1) := by rfl        set U₀ : Fin (2 ^ (ϑ_sub_2 + 1)) → Word A ι :=          (splitHalfRowWiseInterleavedWords (ϑ := ϑ_sub_2 + 1) u).1        set U₁ : Fin (2 ^ (ϑ_sub_2 + 1)) → Word A ι :=          (splitHalfRowWiseInterleavedWords (ϑ := ϑ_sub_2 + 1) u).2        unfold jointProximityNat        simp only        -- intro hP_multilinearCombine_close_gt        have h_finsnoc_eq_r: ∀ r: Fin (ϑ_sub_2 + 1 + 1) → F,          Fin.snoc (fun (i : Fin (ϑ_sub_2 + 1)) ↦ r i.castSucc)            (r (Fin.last (ϑ_sub_2 + 1))) = r := fun r => by          funext i          have hi_le_lt := i.isLt          by_cases h : i = Fin.last (ϑ_sub_2 + 1)          · simp only [h, Fin.snoc_last]          · have h_i_ne_last: i ≠ Fin.last (ϑ_sub_2 + 1) := by omega            have h_i_ne_last_val: i.val ≠ Fin.last (ϑ_sub_2 + 1) := by omega            rw [Fin.val_last] at h_i_ne_last_val            have h_i_lt: i.val < (ϑ_sub_2 + 1) := by omega            simp only [Fin.snoc, Fin.castSucc_castLT, cast_eq, dite_eq_ite, ite_eq_left_iff, not_lt]            simp only [isEmpty_Prop, not_le, h_i_lt, IsEmpty.forall_iff]        let P : F → (Fin (ϑ_sub_2 + 1) → F) → Prop := fun r_last r_init =>          Δ₀(multilinearCombine (u:=u) (r:=Fin.snoc r_init r_last), MC) ≤ e        let hP_split_r_last := prob_split_last_uniform_sampling_of_finFun          (ϑ := ϑ_sub_2 + 1) (F := F) (P := P)        unfold P at hP_split_r_last        simp_rw [h_finsnoc_eq_r] at hP_split_r_last        rw [hP_split_r_last] at hP_multilinearCombine_close_gt        -- Now we have two randomness sampling in hP_multilinearCombine_close_gt :        -- `((ϑ_sub_2 + 1 + 1) * ε) / |𝔽|          -- < Pr_{ r_last; r_init }[  Δ₀((Fin.snoc r_init r_last)|⨂|u, ↑MC) ≤ ↑e)) ]` (0)        -- We need to achieve the upperbound for hP_multilinearCombine_close_gt probability by:        -- i.e. `Pr_{ r_last; r_init }[  Δ₀((Fin.snoc r_init r_last)|⨂|u, ↑MC) ≤ ↑e)) ]`        -- `= Pr_{ r_last; r_init }[ Δ₀((r_init)|⨂|affineCombine(U₀, U₁, r_last), ↑MC) ≤ ↑e)) ]`        -- `= PR_{ r_last }[ r_init; Δ₀((r_init)|⨂|affineCombine(U₀, U₁, r_last), ↑MC) ≤ ↑e)) ]`        -- Divide into two cases: r_last ∈ R* and r_last ∉ R*        -- `= Pr_{ r_last }[ r_last ∈ R* ∧          -- Pr_{ r_init }[ Δ₀((r_init)|⨂|affineCombine(U₀, U₁, r_last), ↑MC) ≤ ↑e)) ]` (1)        -- `+ Pr_{ r_last }[ r_last ∉ R* ∧          -- Pr_{ r_init }[ Δ₀((r_init)|⨂|affineCombine(U₀, U₁, r_last), ↑MC) ≤ ↑e)) ]` (2)        -- `(1) = Pr_{ r_last }[ r_last ∈ R* ]` (3)        -- `(2): ∀ r ∉ R*, it's trivial that the probability          -- ≤ ((ϑ_sub_2 + 1) * ε) / |𝔽|, due to definition of membership of R*` (4)         -- Combine (0), (3), (4): we have `Pr_{ r_last }[ r_last ∈ R* ] > ε/|𝔽|` (5)         -- Applying `correlatedAgreement_of_mem_R_star_tensor` to (5), we get          -- `Δ₀((r_last)|⨂|affineCombine(U₀, U₁, r_last), ↑MC) ≤ ↑e)) ] > ε/|𝔽|` (6)        -- This is premise for affineProxmityGaps of interleaved code (`h_interleaved_gaps`)          -- for `m = 2^{ϑ_sub_2 + 1}`, which directly leads to Q.E.D.        let  ϑ_pred := ϑ_sub_2 + 1        have h_ϑ_pred : ϑ_pred = ϑ_sub_2 + 1 := by rfl        have h_ϑ : ϑ = ϑ_pred + 1 := by rfl        -- Step 1: Apply multilinearCombine recursive form        -- We need the lemma `multilinearCombine u r = multilinearCombine`          -- `(affineLineEvaluation U₀ U₁ r_last) r_init` where `r = Fin.snoc r_init r_last`        have multilinearCombine_snoc_eq_multilinearCombine_affine          (r_init : Fin ϑ_pred → F) (r_last : F) : multilinearCombine u (Fin.snoc r_init r_last) =            multilinearCombine (affineLineEvaluation U₀ U₁ r_last) r_init := by          rw [multilinearCombine_recursive_form]          simp only [Fin.snoc_last, Fin.init_snoc]          rfl        -- Rewrite the probability using this identity        simp_rw [multilinearCombine_snoc_eq_multilinearCombine_affine]          at hP_multilinearCombine_close_gt        -- hP_multilinearCombine_close_gt now looks like:        -- Pr_{ r_last ← $ᵖ F; r_init ← $ᵖ (Fin ϑ_pred → F) }[ Δ₀(multilinearCombine            -- (affineLineEvaluation U₀ U₁ r_last) r_init, ↑MC) ≤ ↑e ] > ↑(↑ϑ * ↑ε) / q        -- Step 2 & 3: Define R* and apply Law of Total Probability        let R_star_set := R_star_tensor MC (m:=ϑ_pred) (e:=e) (ε:=ε) U₀ U₁        -- Step 5: Show Pr[R*] > ε / q        have h_prob_Rstar_gt_eps_div_q : Pr_{ let r ← $ᵖ F }[ r ∈ R_star_set ]          > (↑ε : ENNReal) / (Fintype.card F : ENNReal) := by          let res := prob_R_star_gt_threshold (MC := MC) (ε := ε) (ϑ := ϑ_sub_2 + 1) (u := u)            (e := e) (hP_multilinearCombine_close_gt)          exact res        -- Convert Pr_{}[] to cardinality        have h_R_star_card_gt_eps : R_star_set.card > ε := by          rw [prob_uniform_eq_card_filter_div_card] at h_prob_Rstar_gt_eps_div_q -- Needs NNReal          simp only [ENNReal.coe_natCast] at h_prob_Rstar_gt_eps_div_q          rw [gt_iff_lt] at h_prob_Rstar_gt_eps_div_q          have h_cancel_q_denom := ENNReal.div_lt_div_iff_left            (a := (ε : ENNReal))            (b := (#(filter (fun r => r ∈ R_star_set) Finset.univ)))            (c := (Fintype.card F : ENNReal)) (hc₀ := by simp only [ne_eq,            Nat.cast_eq_zero, Fintype.card_ne_zero, not_false_eq_true]) (hc := by simp only [ne_eq,              ENNReal.natCast_ne_top, not_false_eq_true])          rw [h_cancel_q_denom] at h_prob_Rstar_gt_eps_div_q          simp only [filter_univ_mem, Nat.cast_lt] at h_prob_Rstar_gt_eps_div_q          exact h_prob_Rstar_gt_eps_div_q        -- Step 6: Apply Inductive Hypothesis for r_last ∈ R*        have h_line_close_to_C_m : ∀ (r : R_star_set),          jointProximityNat (u := affineLineEvaluation U₀ U₁ r.val) (e := e) (C := MC) := by          intro r_in_Rstar          -- Use the lemma proven earlier          apply correlatedAgreement_of_mem_R_star_tensor            (ih := fun u_prev => ih (by omega) u_prev ) (u := u)        -- Step 7: Apply Affine Gap of Interleaved Code C^(m = 2^(ϑ_sub_2 + 1))        have h_C_m_gap := h_interleaved_gaps (2^(ϑ_sub_2 + 1)) (Nat.one_le_two_pow)        -- Need the hypothesis Pr[...] > ε/q for h_C_m_gap        have h_prob_line_gt_eps_div_q :          Pr_{ let r ← $ᵖ F }[            Δ₀(affineLineEvaluation (u₀ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₀))              (u₁ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₁)) (r := r),              ((MC ^⋈ (Fin (2 ^ (ϑ_sub_2 + 1)))))) ≤ e          ] > (↑ε : ENNReal) / (Fintype.card F : ENNReal) := by            -- This is implied by h_prob_Rstar_gt_eps_div_q becuz R* is a subset of the success set            apply lt_of_le_of_lt' _ h_prob_Rstar_gt_eps_div_q            have h_r_implies: ∀ (r : F), r ∈ R_star_set →              Δ₀(affineLineEvaluation                (u₀ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₀))                (u₁ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₁)) (r := r),                ((MC ^⋈ (Fin (2 ^ (ϑ_sub_2 + 1)))))) ≤ e := by              intro r hr_in_Rstar              specialize h_line_close_to_C_m ⟨r, hr_in_Rstar⟩              unfold jointProximityNat at h_line_close_to_C_m              exact h_line_close_to_C_m            let Pr_le := Pr_le_Pr_of_implies (D := $ᵖ F)              (g := fun r => Δ₀(affineLineEvaluation                (u₀ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₀))                (u₁ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₁)) (r := r),                ((MC ^⋈ (Fin (2 ^ (ϑ_sub_2 + 1)))))) ≤ e)              (f := fun r => r ∈ R_star_set) (h_imp := h_r_implies)            simp only at Pr_le            exact Pr_le        -- Apply the gap property of C^m        have h_final_gap : jointProximityNat₂          (u₀ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₀))          (u₁ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₁)) (e := e)          (C := (MC ^⋈ (Fin (2^(ϑ_sub_2 + 1))))) := by          apply h_C_m_gap (u₀ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₀))            (u₁ := ⋈|(show WordStack A (Fin (2 ^ (ϑ_sub_2 + 1))) ι from U₁))            (h_prob_line_gt_eps_div_q)        apply CA_split_rowwise_implies_CA (u := u) (e := e)        exact h_final_gap