theorem
lift_mem_ri_cone_iff
(n : ℕ)
(C : Set (EuclideanSpace ℝ (Fin n)))
(hC : Convex ℝ C)
(hCne : C.Nonempty)
:
have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0;
have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i);
have S := {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C};
have K := ↑(ConvexCone.hull ℝ S);
have y0 := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => 1;
have append := fun (y : EuclideanSpace ℝ (Fin 1)) (z : EuclideanSpace ℝ (Fin n)) =>
(EuclideanSpace.equiv (Fin (1 + n)) ℝ).symm
((Fin.appendIsometry 1 n) ((EuclideanSpace.equiv (Fin 1) ℝ) y, (EuclideanSpace.equiv (Fin n) ℝ) z));
have lift := fun (x : EuclideanSpace ℝ (Fin n)) => append y0 x;
∀ (x : EuclideanSpace ℝ (Fin n)), x ∈ euclideanRelativeInterior n C ↔ lift x ∈ euclideanRelativeInterior (1 + n) K
Lifting a point into the cone over C preserves relative interior membership.
theorem
choose_index_family_of_mem_iUnion_euclidean
{n : ℕ}
{ι : Type u_1}
{I : Type u_2}
{C : I → Set (EuclideanSpace ℝ (Fin n))}
{x : ι → EuclideanSpace ℝ (Fin n)}
(hx : ∀ (i : ι), x i ∈ ⋃ (j : I), C j)
:
∃ (f : ι → I), ∀ (i : ι), x i ∈ C (f i)
Choose indices witnessing membership in a union of sets (Euclidean space).
theorem
ri_sum_cones_eq_sum_ri
(n m : ℕ)
(K : Fin m.succ → Set (EuclideanSpace ℝ (Fin n)))
(hK : ∀ (i : Fin m.succ), Convex ℝ (K i))
:
euclideanRelativeInterior n (∑ i : Fin m.succ, K i) = ∑ i : Fin m.succ, euclideanRelativeInterior n (K i)
Relative interior of a finite Minkowski sum of convex sets.
theorem
eq_of_first_tail_eq
(n : ℕ)
:
have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0;
have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i);
∀ (u v : EuclideanSpace ℝ (Fin (1 + n))), first u = first v → tail u = tail v → u = v
A vector in R^{n+1} is determined by its first and tail coordinates.
The first coordinate scales linearly under scalar multiplication.
theorem
tail_smul
(n : ℕ)
:
have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i);
∀ (a : ℝ) (v : EuclideanSpace ℝ (Fin (1 + n))), tail (a • v) = a • tail v
The tail map scales linearly under scalar multiplication.
theorem
dist_lift_eq
(n : ℕ)
:
have y0 := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => 1;
have append := fun (y : EuclideanSpace ℝ (Fin 1)) (z : EuclideanSpace ℝ (Fin n)) =>
(EuclideanSpace.equiv (Fin (1 + n)) ℝ).symm
((Fin.appendIsometry 1 n) ((EuclideanSpace.equiv (Fin 1) ℝ) y, (EuclideanSpace.equiv (Fin n) ℝ) z));
have lift := fun (x : EuclideanSpace ℝ (Fin n)) => append y0 x;
∀ (x y : EuclideanSpace ℝ (Fin n)), dist (lift x) (lift y) = dist x y
The lift map preserves distances.
theorem
sum_smul_lift_eq_lift_sum
(n m : ℕ)
(w : Fin m.succ → ℝ)
(x_i : Fin m.succ → EuclideanSpace ℝ (Fin n))
(hsum : ∑ i : Fin m.succ, w i = 1)
:
have y0 := (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => 1;
have append := fun (y : EuclideanSpace ℝ (Fin 1)) (z : EuclideanSpace ℝ (Fin n)) =>
(EuclideanSpace.equiv (Fin (1 + n)) ℝ).symm
((Fin.appendIsometry 1 n) ((EuclideanSpace.equiv (Fin 1) ℝ) y, (EuclideanSpace.equiv (Fin n) ℝ) z));
have lift := fun (x : EuclideanSpace ℝ (Fin n)) => append y0 x;
∑ i : Fin m.succ, w i • lift (x_i i) = lift (∑ i : Fin m.succ, w i • x_i i)
Weighted sums of lifts with total weight 1 collapse to a single lift.
theorem
mem_sum_ri_cones_iff_weights
(n m : ℕ)
(C : Fin m.succ → Set (EuclideanSpace ℝ (Fin n)))
(hCne : ∀ (i : Fin m.succ), (C i).Nonempty)
(hCconv : ∀ (i : Fin m.succ), Convex ℝ (C i))
:
have coords := ⇑(EuclideanSpace.equiv (Fin (1 + n)) ℝ);
have first := fun (v : EuclideanSpace ℝ (Fin (1 + n))) => coords v 0;
have tail := fun (v : EuclideanSpace ℝ (Fin (1 + n))) =>
(EuclideanSpace.equiv (Fin n) ℝ).symm fun (i : Fin n) => coords v (Fin.natAdd 1 i);
have S := fun (i : Fin m.succ) => {v : EuclideanSpace ℝ (Fin (1 + n)) | first v = 1 ∧ tail v ∈ C i};
have K := fun (i : Fin m.succ) => ↑(ConvexCone.hull ℝ (S i));
∀ (v : EuclideanSpace ℝ (Fin (1 + n))),
first v = 1 →
(v ∈ ∑ i : Fin m.succ, euclideanRelativeInterior (1 + n) (K i) ↔ ∃ (w : Fin m.succ → ℝ) (x_i : Fin m.succ → EuclideanSpace ℝ (Fin n)),
(∀ (i : Fin m.succ), 0 < w i) ∧ ∑ i : Fin m.succ, w i = 1 ∧ (∀ (i : Fin m.succ), x_i i ∈ euclideanRelativeInterior n (C i)) ∧ tail v = ∑ i : Fin m.succ, w i • x_i i)
Membership in the sum of the relative interiors of the lifted cones gives positive weights.
theorem
convexHull_iUnion_exists_weights_points
(n m : ℕ)
(C : Fin m.succ → Set (EuclideanSpace ℝ (Fin n)))
(hCne : ∀ (i : Fin m.succ), (C i).Nonempty)
(hCconv : ∀ (i : Fin m.succ), Convex ℝ (C i))
(x : EuclideanSpace ℝ (Fin n))
:
A point in the convex hull of a finite union of convex sets admits one point per set.