LeanPool.Monsky.SimplexBasic

Imported Lean Pool material for LeanPool.Monsky.SimplexBasic.

def LeanPool.Monsky.v (x y : ℝ) : EuclideanSpace ℝ (Fin 2)

The plane vector with the two given real coordinates.

Equations

• LeanPool.Monsky.v x y = !₂[x, y]

@[simp]

theorem LeanPool.Monsky.v₀_val {x y : ℝ} : (v x y).ofLp 0 = x

@[simp]

theorem LeanPool.Monsky.v₁_val {x y : ℝ} : (v x y).ofLp 1 = y

def LeanPool.Monsky.closedSimplex (n : ℕ) : Set (Fin n → ℝ)

The closed standard n-simplex of nonnegative weights summing to one.

Equations

• LeanPool.Monsky.closedSimplex n = {α : Fin n → ℝ | (∀ (i : Fin n), 0 ≤ α i) ∧ ∑ i : Fin n, α i = 1}

def LeanPool.Monsky.openSimplex (n : ℕ) : Set (Fin n → ℝ)

The open standard n-simplex of positive weights summing to one.

Equations

• LeanPool.Monsky.openSimplex n = {α : Fin n → ℝ | (∀ (i : Fin n), 0 < α i) ∧ ∑ i : Fin n, α i = 1}

def LeanPool.Monsky.closedHull {n : ℕ} (f : Fin n → EuclideanSpace ℝ (Fin 2)) : Set (EuclideanSpace ℝ (Fin 2))

The closed convex hull of a finite point family, via the closed simplex.

Equations

• LeanPool.Monsky.closedHull f = (fun (α : Fin n → ℝ) => ∑ i : Fin n, α i • f i) '' LeanPool.Monsky.closedSimplex n

def LeanPool.Monsky.openHull {n : ℕ} (f : Fin n → EuclideanSpace ℝ (Fin 2)) : Set (EuclideanSpace ℝ (Fin 2))

The open convex hull of a finite point family, via the open simplex.

Equations

• LeanPool.Monsky.openHull f = (fun (α : Fin n → ℝ) => ∑ i : Fin n, α i • f i) '' LeanPool.Monsky.openSimplex n

def LeanPool.Monsky.simplexVertex {n : ℕ} (i : Fin n) : Fin n → ℝ

The i-th vertex of the standard simplex, as a weight function.

Equations

• LeanPool.Monsky.simplexVertex i j = if i = j then 1 else 0

theorem LeanPool.Monsky.simplexVertex_in_simplex {n : ℕ} {i : Fin n} : simplexVertex i ∈ closedSimplex n

theorem LeanPool.Monsky.closedSimplex_zero_empty : closedSimplex 0 = ∅

theorem LeanPool.Monsky.openSimplex_zero_empty : openSimplex 0 = ∅

@[simp]

theorem LeanPool.Monsky.simplexVertex_image {n : ℕ} {i : Fin n} (f : Fin n → EuclideanSpace ℝ (Fin 2)) : ∑ k : Fin n, simplexVertex i k • f k = f i

@[simp]

theorem LeanPool.Monsky.corner_in_closedHull {n : ℕ} {i : Fin n} {P : Fin n → EuclideanSpace ℝ (Fin 2)} : P i ∈ closedHull P

theorem LeanPool.Monsky.closedHull_constant {n : ℕ} {P : EuclideanSpace ℝ (Fin 2)} (hn : n ≠ 0) : (closedHull fun (x : Fin n) => P) = {P}

theorem LeanPool.Monsky.closedHull_constant_rev {n : ℕ} {P : EuclideanSpace ℝ (Fin 2)} {f : Fin n → EuclideanSpace ℝ (Fin 2)} (hc : closedHull f = {P}) (i : Fin n) : f i = P

theorem LeanPool.Monsky.open_pol_nonempty {n : ℕ} (hn : 0 < n) (P : Fin n → EuclideanSpace ℝ (Fin 2)) : (openHull P).Nonempty

theorem LeanPool.Monsky.open_sub_closedSimplex {n : ℕ} : openSimplex n ⊆ closedSimplex n

theorem LeanPool.Monsky.open_sub_closed {n : ℕ} (P : Fin n → EuclideanSpace ℝ (Fin 2)) : openHull P ⊆ closedHull P

theorem LeanPool.Monsky.closed_pol_nonempty {n : ℕ} (hn : 0 < n) (P : Fin n → EuclideanSpace ℝ (Fin 2)) : (closedHull P).Nonempty

theorem LeanPool.Monsky.openHull_constant {n : ℕ} {P : EuclideanSpace ℝ (Fin 2)} (hn : n ≠ 0) : (openHull fun (x : Fin n) => P) = {P}

theorem LeanPool.Monsky.closedHull_zero_dim (f : Fin 0 → EuclideanSpace ℝ (Fin 2)) : closedHull f = ∅

theorem LeanPool.Monsky.openHull_zero_dim (f : Fin 0 → EuclideanSpace ℝ (Fin 2)) : openHull f = ∅

noncomputable def LeanPool.Monsky.linearCombination {n : ℕ} (α : Fin n → ℝ) (f : Fin n → EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2)

The point obtained as a weighted combination of a point family.

Equations

• LeanPool.Monsky.linearCombination α f = ∑ i : Fin n, α i • f i

theorem LeanPool.Monsky.linear_co_closed {n : ℕ} {α : Fin n → ℝ} (f : Fin n → EuclideanSpace ℝ (Fin 2)) (h : α ∈ closedSimplex n) : linearCombination α f ∈ closedHull f

theorem LeanPool.Monsky.simplex_co_eq_1 {n : ℕ} {α : Fin n → ℝ} {i : Fin n} (h₁ : α ∈ closedSimplex n) (h₂ : α i = 1) (j : Fin n) : j ≠ i → α j = 0

theorem LeanPool.Monsky.simplex_exists_co_pos {n : ℕ} {α : Fin n → ℝ} (h : α ∈ closedSimplex n) : ∃ (i : Fin n), 0 < α i

theorem LeanPool.Monsky.simplex_co_leq_1 {n : ℕ} {α : Fin n → ℝ} (h₁ : α ∈ closedSimplex n) (i : Fin n) : α i ≤ 1

theorem LeanPool.Monsky.simplex_co_leq_1_open {n : ℕ} {α : Fin n → ℝ} (hn : 1 < n) (h₁ : α ∈ openSimplex n) (i : Fin n) : α i < 1

theorem LeanPool.Monsky.simplex_closed_sub_fin2 {α : Fin 2 → ℝ} (h : α ∈ closedSimplex 2) (i : Fin 2) : α i = 1 - α ((fun (x : Fin 2) => match x with | 0 => 1 | 1 => 0) i)

theorem LeanPool.Monsky.simplex_open_sub_fin2 {α : Fin 2 → ℝ} (h : α ∈ openSimplex 2) (i : Fin 2) : α i = 1 - α ((fun (x : Fin 2) => match x with | 0 => 1 | 1 => 0) i)

def LeanPool.Monsky.real_to_fin_2 (x : ℝ) : Fin 2 → ℝ

Encodes a real x as the pair of weights (x, 1 - x).

Equations

• LeanPool.Monsky.real_to_fin_2 x 0 = x
• LeanPool.Monsky.real_to_fin_2 x 1 = 1 - x

theorem LeanPool.Monsky.real_to_fin_2_closed {x : ℝ} (h₁ : 0 ≤ x) (h₂ : x ≤ 1) : real_to_fin_2 x ∈ closedSimplex 2

theorem LeanPool.Monsky.real_to_fin_2_open {x : ℝ} (h₁ : 0 < x) (h₂ : x < 1) : real_to_fin_2 x ∈ openSimplex 2

theorem LeanPool.Monsky.closedHull_convex {n₁ n₂ : ℕ} {P₁ : Fin n₁ → EuclideanSpace ℝ (Fin 2)} {P₂ : Fin n₂ → EuclideanSpace ℝ (Fin 2)} (h : ∀ (i : Fin n₁), P₁ i ∈ closedHull P₂) : closedHull P₁ ⊆ closedHull P₂

theorem LeanPool.Monsky.closedHull_openHull_com {n : ℕ} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {x y : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ openHull P) (hy : y ∈ closedHull P) : (1 / 2) • x + (1 / 2) • y ∈ openHull P

def LeanPool.Monsky.boundary {n : ℕ} (P : Fin n → EuclideanSpace ℝ (Fin 2)) : Set (EuclideanSpace ℝ (Fin 2))

The boundary of the convex hull of a point family: closed hull minus open hull.

Equations

• LeanPool.Monsky.boundary P = LeanPool.Monsky.closedHull P \ LeanPool.Monsky.openHull P

theorem LeanPool.Monsky.boundary_sub_closed {n : ℕ} (P : Fin n → EuclideanSpace ℝ (Fin 2)) : boundary P ⊆ closedHull P

theorem LeanPool.Monsky.boundary_not_in_open {n : ℕ} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary P) : x ∉ openHull P

theorem LeanPool.Monsky.boundary_in_closed {n : ℕ} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary P) : x ∈ closedHull P

theorem LeanPool.Monsky.boundary_int_open_empty {n : ℕ} {P : Fin n → EuclideanSpace ℝ (Fin 2)} : boundary P ∩ openHull P = ∅

theorem LeanPool.Monsky.boundary_open_disjoint {n : ℕ} {P : Fin n → EuclideanSpace ℝ (Fin 2)} : Disjoint (boundary P) (openHull P)

theorem LeanPool.Monsky.boundary_union_open_closed {n : ℕ} {P : Fin n → EuclideanSpace ℝ (Fin 2)} : boundary P ∪ openHull P = closedHull P

theorem LeanPool.Monsky.open_closedHull_minus_boundary {n : ℕ} {P : Fin n → EuclideanSpace ℝ (Fin 2)} : closedHull P \ boundary P = openHull P

theorem LeanPool.Monsky.boundary_constant {n : ℕ} {P : EuclideanSpace ℝ (Fin 2)} : (boundary fun (x : Fin n) => P) = ∅

theorem LeanPool.Monsky.openHull_constant_rev {n : ℕ} {P : EuclideanSpace ℝ (Fin 2)} {f : Fin n → EuclideanSpace ℝ (Fin 2)} (ho : openHull f = {P}) (i : Fin n) : f i = P