def ConvexDistance.unitCube (n : ℕ) : Set (EuclideanSpace ℝ (Fin n))

The $n$-dimensional unit cube $[0,1]^n$ as a subset of $\mathbb{R}^n$.

noncomputable def ConvexDistance.weightedHammingDist {n : ℕ} (α x y : EuclideanSpace ℝ (Fin n)) : ℝ

Weighted Hamming distance from $x$ to $y$ with weight vector $\alpha$: $\sum_{i : x_i \neq y_i} |\alpha_i|$.

noncomputable def ConvexDistance.weightedHammingDistSet {n : ℕ} (α x : EuclideanSpace ℝ (Fin n)) (A : Set (EuclideanSpace ℝ (Fin n))) : ℝ

Weighted Hamming distance from $x$ to a set $A$: the infimum of weightedHammingDist α x y as $y$ ranges over $A$.

noncomputable def ConvexDistance.talagrandDist {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (A : Set (EuclideanSpace ℝ (Fin n))) : ℝ

Talagrand's convex distance from $x$ to a set $A$: the supremum over unit vectors $\alpha$ of the $\alpha$-weighted Hamming distance from $x$ to $A$.

theorem ConvexDistance.weightedHammingDist_nonneg {n : ℕ} (α x y : EuclideanSpace ℝ (Fin n)) : 0 ≤ weightedHammingDist α x y

The weighted Hamming distance is non-negative, as a sum of absolute values and zeros.

theorem ConvexDistance.abs_component_le_norm {n : ℕ} (α : EuclideanSpace ℝ (Fin n)) (i : Fin n) : |α.ofLp i| ≤ ‖α‖

Each coordinate of a vector in Euclidean space is bounded in absolute value by the Euclidean norm: $|\alpha_i| \le \|\alpha\|$.

theorem ConvexDistance.weightedHammingDist_le_of_unit_norm {n : ℕ} (α x y : EuclideanSpace ℝ (Fin n)) (hα : ‖α‖ = 1) : weightedHammingDist α x y ≤ ↑n

For a unit-norm weight vector $\alpha$, the weighted Hamming distance between any two points is at most $n$.

theorem ConvexDistance.inner_le_weightedHammingDist {n : ℕ} (x y : EuclideanSpace ℝ (Fin n)) (hx : x ∈ unitCube n) (hy : y ∈ unitCube n) (α : EuclideanSpace ℝ (Fin n)) : inner ℝ (x - y) α ≤ weightedHammingDist α x y

For $x, y$ in the unit cube and any weight vector $\alpha$, the inner product $\langle x - y, \alpha\rangle$ is bounded by the weighted Hamming distance $\mathrm{whd}_\alpha(x,y)$.

theorem ConvexDistance.talagrandDist_bddAbove {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (A : Set (EuclideanSpace ℝ (Fin n))) (hAne : A.Nonempty) : BddAbove ((fun (α : EuclideanSpace ℝ (Fin n)) => weightedHammingDistSet α x A) '' {α : EuclideanSpace ℝ (Fin n) | ‖α‖ = 1})

The set whose supremum defines talagrandDist is bounded above by $n$, hence the supremum is attainable in the extended sense (used to apply csSup lemmas).

theorem ConvexDistance.talagrandDist_nonneg {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (A : Set (EuclideanSpace ℝ (Fin n))) : 0 ≤ talagrandDist x A

Talagrand's convex distance is non-negative.

theorem ConvexDistance.convex_dist_upper_bounds_euclidean_dist {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n))) (x : EuclideanSpace ℝ (Fin n)) (hA : A ⊆ unitCube n) (hx : x ∈ unitCube n) (hAne : A.Nonempty) : Metric.infDist x ((convexHull ℝ) A) ≤ talagrandDist x A

Lemma 9.5.12 / Corollary 9.5.13 (convex distance bound). If $A \subseteq [0,1]^n$ and $x \in [0,1]^n$, then the Euclidean distance from $x$ to the convex hull of $A$ is at most Talagrand's convex distance $d_T(x, A)$.