Folding preserves distance

theorem folding_preserves_distance  [Fintype F]  {domain : SmoothCosetFftDomain n F} {f : Word F (Fin (2 ^ n))} {d k : ℕ}  {δ : ℝ≥0}  (k_div_d : 2 ^ k ∣ d)  (hd0 : 0 < d)  (h_d_n : d ≤ 2 ^ n)  (δ_gt_0 : 0 < δ) -- this one is not used but should be.  (δ_lt : δ < min (δᵣ(f, ReedSolomon.code (domain : Fin (2 ^ n) ↪ F) d))    (1 - (ReedSolomon.sqrtRate d (domain : Fin (2 ^ n) ↪ F)))) :    Pr_{ let r ←$ᵖ F}[δᵣ(foldWord domain f k r,      ReedSolomon.code (domain.subdomain k : Fin (2 ^ (n - k)) ↪ F)      (d / (2 ^ k))) ≤ δ] ≤        ((2 ^ k) - 1) * ProximityGap.errorBound δ (d / (2 ^ k))        (domain.subdomain k : Fin (2 ^ (n - k)) ↪ F) := by    have h_k_d : 2 ^ k ≤ d := by exact Nat.le_of_dvd (by omega) k_div_d    have h_k_le_n : k ≤ n := by      rw [←Nat.pow_le_pow_iff_right (a := 2) (by simp)]      omega    have bound_tighter :      (↑δ) ≤ 1 - ReedSolomon.sqrtRate (d / (2 ^ k))        (domain.subdomain k : Fin (2 ^ (n - k)) ↪ F) :=      le_of_lt <| by        aesop          (add safe [(by rw [folded_sqrtRate_eq])])          (add safe [(by grind)])          (add safe (by norm_cast at *))    have correlated_agreement :=      @correlatedAgreement_affine_curves (Fin (2 ^ (n - k))) _ _ F _ _ _        (2 ^ k - 1) (d / (2 ^ k))        (domain := domain.subdomain k) (δ := δ)        (hδ := bound_tighter)    unfold foldWord δ_ε_correlatedAgreementCurves at *    by_contra contra    simp only [not_le, foldValue_eq_sum_of_foldAuxCoeff_mul_pow_alpha, bind_pure_comp, Functor.map,      PMF.bind_apply,      PMF.uniformOfFintype_apply,      comp_apply, PMF.pure_apply, eq_iff_iff, true_iff,      mul_ite, mul_one, mul_zero, tsum_fintype] at contra correlated_agreement    let cast (x : Fin (2 ^ k - 1 + 1)) : Fin (2 ^ k) :=      Fin.cast (by rw [Nat.sub_add_cancel (by omega)]) x    let cast' (x : Fin (2 ^ k)) : Fin (2 ^ k - 1 + 1) :=      Fin.cast (by rw [Nat.sub_add_cancel (by omega)]) x    have bijective_cast : Bijective cast := by      rw [bijective_iff_has_inverse]      exists cast'      simp [LeftInverse, RightInverse, cast, cast']    specialize correlated_agreement      (Matrix.of (fun i j ↦ foldWordAuxCoeff domain f k        (cast i)        (domain.subdomain k j)))    have correlated_curve_eq_sum_of_foldWord_coeffs {a : F} :      ∑ i : Fin (2 ^ k - 1 + 1), a ^ (↑i : ℕ) •        Matrix.of (fun i j ↦          foldWordAuxCoeff domain f k (cast i) (domain.subdomain k j)) i =      (fun x ↦        ∑ j, foldWordAuxCoeff domain f k j          (domain.subdomain k x) * a ^ (↑j : ℕ)) := by      ext x      simp only [Finset.sum_apply]      change (∑ i : Fin (2 ^ k - 1 + 1),        a ^ (i : ℕ) * foldWordAuxCoeff domain f k (cast i) (domain.subdomain k x)) =          ∑ j : Fin (2 ^ k), foldWordAuxCoeff domain f k j            (domain.subdomain k x) * a ^ (j : ℕ)      exact Fintype.sum_bijective cast bijective_cast _ _ <|        fun i ↦ by simp [cast, mul_comm]    specialize correlated_agreement (by {      conv_lhs =>        rhs        ext a        rw [correlated_curve_eq_sum_of_foldWord_coeffs]      norm_cast at contra    })    simp only [jointAgreement, Fintype.card_fin, Nat.cast_pow, Nat.cast_ofNat, ge_iff_le,      SetLike.mem_coe, Matrix.of_apply] at correlated_agreement    obtain ⟨S, h_card, v, h'⟩ := correlated_agreement    rw [forall_and] at h'    rcases h' with ⟨h_rs, h'⟩    have h_rs := fun x ↦ (mem_code_iff_exists_polynomial_of_ne_zero        (ne := ⟨by rw [Nat.div_ne_zero_iff]; omega⟩)).mp (h_rs x)    let u : Fin (2 ^ k - 1 + 1) → Polynomial F :=      fun i => Classical.choose (h_rs i)    have contradiction := dist_from_code_bound_of_correlated_agreement (domain := domain) (f := f)      (s := Finset.image        (domain.subdomain k) S)      (fun x hx ↦ by        rw [CosetFftDomainClass.mem_toFinset_iff_mem]        simp only [mem_image] at hx        obtain ⟨x', _, hx'⟩ := hx        aesop      )      (u := u ∘ cast')      (fun i j hj ↦ by        clear *- hj h'        let i' := cast' i        obtain ⟨j', hj, _⟩ := by simpa using hj        specialize h' i' hj        have h_spec := congrFun (a := j') <| Classical.choose_spec (h_rs i') |>.2        aesop (add norm evalOnPoints)      )      (d := d)      h_k_d      h_d_n      (fun i ↦        And.left <| Classical.choose_spec (h_rs (cast' i)))    rw [Finset.card_image_of_injective _ (by simp)] at contradiction    have contradiction : (Δ₀(f, code (domain : Fin (2 ^ n) ↪ F) d) : ENNReal)      ≤ (↑(2 ^ n) : ℚ≥0) * δ :=      le_trans (ENat.toENNReal_le.mpr contradiction) <| by        apply le_trans          (b := (2 ^ n : ENNReal) - 2 ^ k * (1 - ↑δ) * 2 ^ (n - k))        · rw [ENat.toENNReal_sub,              show ENat.toENNReal (2 ^ n) = (2 ^ n : ENNReal) by simp,              ENNReal.sub_le_sub_iff_left (h' := by simp)                (h := swap (le_trans (b := 2 ^ n * 1)) (by simp) <| by                  rw [mul_comm,                      ←mul_assoc,                      ←pow_add,                      Nat.sub_add_cancel h_k_le_n,                      ENNReal.mul_le_mul_iff_right (by simp) (by simp)]                  simp          )]          apply le_trans (b := 2 ^ k * ↑↑(#S))          · rw [mul_assoc,                ENNReal.mul_le_mul_iff_right (by simp) (by simp)]            have h_card := ENNReal.coe_le_coe_of_le h_card            exact (swap le_trans h_card) (by norm_cast)          · norm_cast        · rw [mul_comm,              ←mul_assoc,              ←pow_add,              Nat.sub_add_cancel h_k_le_n]          conv_lhs =>            lhs            rw [←mul_one (2 ^ n)]          rw [←ENNReal.mul_sub (by simp),              ENNReal.sub_sub_cancel (by simp)                (by {                  simp only [lt_inf_iff] at δ_lt                  exact le_trans (le_of_lt δ_lt.2) (by simp)                })]          norm_cast    have contradiction : δᵣ(f, code (domain : Fin (2 ^ n) ↪ F) d) ≤ (δ : NNReal) := by      rw [relDistFromCode_le_iff_distFromCode_toENNReal_le]      exact le_trans contradiction <| by        simp only [Fintype.card_fin, Nat.cast_pow, Nat.cast_ofNat]        rw [mul_comm]        norm_cast    simp only [lt_inf_iff] at δ_lt    simpa using lt_of_lt_of_le δ_lt.1 contradiction