theorem proximityGap {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {L : Finset F} {d : ℕ} (C : ReedSolomonCode F L d) (δ : { x : ℝ // 0 < x ∧ x < 1 - Bstar C.rate }) (m : ℕ) (f : Fin m → { x : F // x ∈ L } → F) (h : (PMF.uniformOfFintype F).toOuterMeasure {r : F | ↑(fractionalHammingDistSet (fun (x : { x : F // x ∈ L }) => ∑ j : Fin m, r ^ ↑j • f j x) C.code ⋯) ≤ ↑δ} > err' F d C.rate (↑δ) m) : ∃ S ⊆ L, ↑S.card ≥ (1 - ↑δ) * ↑L.card ∧ ∀ (i : Fin m), ∃ u ∈ C.code, ∀ x ∈ S, ∀ (hx : x ∈ L), f i ⟨x, hx⟩ = u ⟨x, hx⟩