Hanner polytopes

DefinitionCentered unit segment#✓fully proved

The centered unit segment is the closed unit ball \(\{x \in \mathbb{R}^1 : \|x\| \le 1\}\), that is, the segment \([-1, 1]\). It is the one-dimensional leaf in the recursive definition of Hanner polytopes.

def hannerUnitSegment : Set (EuclideanSpace ℝ (Fin 1)) :=
  Metric.closedBall 0 1

Used by 13

Used byHanner polytopes are convex · Hanner polytopes live in positive dimension · Hanner cross-polytope · The Hanner cross-polytopes are Hanner polytopes · Hanner cube · The Hanner cube is the coordinate cube · The Hanner cubes are Hanner polytopes · Hanner polytopes are compact · Hanner polytopes · Membership in the Hanner unit segment · Hanner polytopes are centrally symmetric · Hanner polytopes contain the origin · Hanner polytopes contain the origin in their interior

Definition\(\ell_\infty\) sum of bodies#✓fully proved

For sets \(K \subseteq \mathbb{R}^m\) and \(L \subseteq \mathbb{R}^n\), the \(\ell_\infty\) sum of \(K\) and \(L\) is the set of points of \(\mathbb{R}^{m+n}\) whose first \(m\) coordinates form a point of \(K\) and whose last \(n\) coordinates form a point of \(L\); that is, the product \(K \times L\) under the identification \(\mathbb{R}^{m+n} = \mathbb{R}^m \times \mathbb{R}^n\).

noncomputable def hannerInfinitySum {m n : ℕ}
    (K : Set (EuclideanSpace ℝ (Fin m)))
    (L : Set (EuclideanSpace ℝ (Fin n))) :
    Set (EuclideanSpace ℝ (Fin (m + n))) :=
  EuclideanSpace.finAddEquivProd.symm.toLinearEquiv '' (K ×ˢ L)

Used by 11

Used byHanner polytopes are convex · Hanner polytopes live in positive dimension · Hanner cube · The Hanner cube is the coordinate cube · The Hanner cubes are Hanner polytopes · Hanner polytopes are compact · Hanner polytopes · Membership in the \(\ell_\infty\) Hanner sum · Hanner polytopes are centrally symmetric · Hanner polytopes contain the origin · Hanner polytopes contain the origin in their interior

Definition\(\ell_1\) sum of bodies#✓fully proved

For sets \(K \subseteq \mathbb{R}^m\) and \(L \subseteq \mathbb{R}^n\), the \(\ell_1\) sum of \(K\) and \(L\) is the convex hull in \(\mathbb{R}^{m+n}\) of \((K \times \{0\}) \cup (\{0\} \times L)\), where \(\mathbb{R}^{m+n}\) is identified with \(\mathbb{R}^m \times \mathbb{R}^n\) by splitting off the first \(m\) coordinates.

noncomputable def hannerOneSum {m n : ℕ}
    (K : Set (EuclideanSpace ℝ (Fin m)))
    (L : Set (EuclideanSpace ℝ (Fin n))) :
    Set (EuclideanSpace ℝ (Fin (m + n))) :=
  EuclideanSpace.finAddEquivProd.symm.toLinearEquiv ''
    convexHull ℝ ((K ×ˢ ({0} : Set (EuclideanSpace ℝ (Fin n)))) ∪
      (({0} : Set (EuclideanSpace ℝ (Fin m))) ×ˢ L))

Used by 9

Used byHanner polytopes are convex · Hanner polytopes live in positive dimension · Hanner cross-polytope · The Hanner cross-polytopes are Hanner polytopes · Hanner polytopes are compact · Hanner polytopes · Hanner polytopes are centrally symmetric · Hanner polytopes contain the origin · Hanner polytopes contain the origin in their interior

InductiveHanner polytopes#✓fully proved

For \(K \subseteq \mathbb{R}^m\) and \(L \subseteq \mathbb{R}^n\), identify \(\mathbb{R}^{m+n}\) with \(\mathbb{R}^m \times \mathbb{R}^n\) by splitting off the first \(m\) coordinates; the \(\ell_\infty\) sum of \(K\) and \(L\) is \(K \times L\), and their \(\ell_1\) sum is the convex hull of \((K \times \{0\}) \cup (\{0\} \times L)\), both viewed as subsets of \(\mathbb{R}^{m+n}\). The Hanner polytopes are the smallest family of subsets of the Euclidean spaces \(\mathbb{R}^n\) such that: the unit segment \([-1, 1] \subseteq \mathbb{R}^1\) is a Hanner polytope; if \(K \subseteq \mathbb{R}^n\) is a Hanner polytope and \(e \colon \mathbb{R}^n \to \mathbb{R}^n\) is an invertible linear map, then \(e(K)\) is a Hanner polytope; and if \(K \subseteq \mathbb{R}^m\) and \(L \subseteq \mathbb{R}^n\) are Hanner polytopes with \(m, n > 0\), then their \(\ell_\infty\) sum and their \(\ell_1\) sum are Hanner polytopes.

MetaMathlibExt.IsHannerPolytope · 16 lines

inductive IsHannerPolytope : {n : ℕ} → Set (EuclideanSpace ℝ (Fin n)) → Prop
  | unitSegment : IsHannerPolytope hannerUnitSegment
  | linearImage {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))}
      (hK : IsHannerPolytope K)
      (e : EuclideanSpace ℝ (Fin n) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin n)) :
      IsHannerPolytope (e '' K)
  | infinitySum {m n : ℕ} {K : Set (EuclideanSpace ℝ (Fin m))}
      {L : Set (EuclideanSpace ℝ (Fin n))}
      (hm : 0 < m) (hn : 0 < n)
      (hK : IsHannerPolytope K) (hL : IsHannerPolytope L) :
      IsHannerPolytope (hannerInfinitySum K L)
  | oneSum {m n : ℕ} {K : Set (EuclideanSpace ℝ (Fin m))}
      {L : Set (EuclideanSpace ℝ (Fin n))}
      (hm : 0 < m) (hn : 0 < n)
      (hK : IsHannerPolytope K) (hL : IsHannerPolytope L) :
      IsHannerPolytope (hannerOneSum K L)

Uses 3 · Used by 9

Statement uses\(\ell_\infty\) sum of bodies · \(\ell_1\) sum of bodies · Centered unit segment

Used byHanner polytopes are convex · Hanner polytopes live in positive dimension · The Hanner cross-polytopes are Hanner polytopes · The Hanner cubes are Hanner polytopes · Hanner polytopes are compact · Hanner polytopes are centrally symmetric · Negation preserves membership in a Hanner polytope · Hanner polytopes contain the origin · Hanner polytopes contain the origin in their interior

DefinitionHanner cube#✓fully proved

For \(n \in \mathbb{N}\), the Hanner cube \(C_n \subseteq \mathbb{R}^{n+1}\) is defined by recursion on \(n\): \(C_0\) is the centered unit segment \([-1, 1] \subseteq \mathbb{R}^1\), and \(C_{n+1} \subseteq \mathbb{R}^{n+2}\) is the \(\ell_\infty\) sum of \(C_n\) and the centered unit segment.

noncomputable def hannerCube : (n : ℕ) → Set (EuclideanSpace ℝ (Fin (n + 1)))
  | 0 => hannerUnitSegment
  | n + 1 => hannerInfinitySum (hannerCube n) hannerUnitSegment

Uses 2 · Used by 2

Statement uses\(\ell_\infty\) sum of bodies · Centered unit segment

Used byThe Hanner cube is the coordinate cube · The Hanner cubes are Hanner polytopes

DefinitionHanner cross-polytope#✓fully proved

For \(n \in \mathbb{N}\), the Hanner cross-polytope \(P_n \subseteq \mathbb{R}^{n+1}\) is defined by recursion on \(n\): \(P_0\) is the centered unit segment \([-1, 1] \subseteq \mathbb{R}^1\), and \(P_{n+1} \subseteq \mathbb{R}^{n+2}\) is the \(\ell_1\) sum of \(P_n\) and the centered unit segment.

noncomputable def hannerCrossPolytope : (n : ℕ) → Set (EuclideanSpace ℝ (Fin (n + 1)))
  | 0 => hannerUnitSegment
  | n + 1 => hannerOneSum (hannerCrossPolytope n) hannerUnitSegment

Uses 2 · Used by 1

Statement uses\(\ell_1\) sum of bodies · Centered unit segment

Used byThe Hanner cross-polytopes are Hanner polytopes

TheoremThe Hanner cubes are Hanner polytopes#✓fully proved

For every \(n \in \mathbb{N}\), the Hanner cube \(C_n \subseteq \mathbb{R}^{n+1}\) is a Hanner polytope.

theorem hannerCube_isHannerPolytope (n : ℕ) : IsHannerPolytope (hannerCube n)

Uses 4

Statement usesHanner polytopes · Hanner cube

Proof uses\(\ell_\infty\) sum of bodies · Centered unit segment

TheoremThe Hanner cross-polytopes are Hanner polytopes#✓fully proved

For every \(n \in \mathbb{N}\), the Hanner cross-polytope \(P_n \subseteq \mathbb{R}^{n+1}\) is a Hanner polytope.

theorem hannerCrossPolytope_isHannerPolytope (n : ℕ) :
    IsHannerPolytope (hannerCrossPolytope n)

Uses 4

Statement usesHanner polytopes · Hanner cross-polytope

Proof uses\(\ell_1\) sum of bodies · Centered unit segment

TheoremMembership in the Hanner unit segment#✓fully proved

A point \(x \in \mathbb{R}^1\) lies in the Hanner unit segment if and only if every coordinate \(x_i\) of \(x\) satisfies \(|x_i| \le 1\).

theorem mem_hannerUnitSegment_iff (x : EuclideanSpace ℝ (Fin 1)) :
    x ∈ hannerUnitSegment ↔ ∀ i, |x i| ≤ 1

Uses 1 · Used by 1

Statement usesCentered unit segment

Used byThe Hanner cube is the coordinate cube

TheoremMembership in the \(\ell_\infty\) Hanner sum#✓fully proved

Let \(K \subseteq \mathbb{R}^m\) and \(L \subseteq \mathbb{R}^n\). A point \(x \in \mathbb{R}^{m+n}\) lies in the \(\ell_\infty\) Hanner sum of \(K\) and \(L\) if and only if \((x_1, \dots, x_m) \in K\) and \((x_{m+1}, \dots, x_{m+n}) \in L\).

theorem mem_hannerInfinitySum_iff {m n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin m))} {L : Set (EuclideanSpace ℝ (Fin n))}
    (x : EuclideanSpace ℝ (Fin (m + n))) :
    x ∈ hannerInfinitySum K L ↔
      (EuclideanSpace.finAddEquivProd x).1 ∈ K ∧
        (EuclideanSpace.finAddEquivProd x).2 ∈ L

Uses 1 · Used by 1

Statement uses\(\ell_\infty\) sum of bodies

Used byThe Hanner cube is the coordinate cube

TheoremThe Hanner cube is the coordinate cube#✓fully proved

For every \(n \in \mathbb{N}\), the Hanner cube \(C_n \subseteq \mathbb{R}^{n+1}\) equals the coordinate cube \(\{x \in \mathbb{R}^{n+1} : -1 \le x_i \le 1 \text{ for every } i\} = [-1, 1]^{n+1}\).

theorem hannerCube_eq_coordinateCube (n : ℕ) :
    hannerCube n = ConvexCovering.coordinateCube (n + 1)

Uses 7

Statement usesCoordinate cube · Hanner cube

Proof usesThe coordinate cube as an absolute-value box · \(\ell_\infty\) sum of bodies · Centered unit segment · Membership in the \(\ell_\infty\) Hanner sum · Membership in the Hanner unit segment

TheoremHanner polytopes live in positive dimension#✓fully proved

If \(K \subseteq \mathbb{R}^n\) is a Hanner polytope, then \(0 < n\).

theorem IsHannerPolytope.dimension_pos {n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : IsHannerPolytope K) : 0 < n

Uses 4

Statement usesHanner polytopes

Proof uses\(\ell_\infty\) sum of bodies · \(\ell_1\) sum of bodies · Centered unit segment

TheoremHanner polytopes are centrally symmetric#✓fully proved

Every Hanner polytope \(K\) is centrally symmetric about the origin: \(-K = K\).

theorem IsHannerPolytope.neg_eq_self {n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : IsHannerPolytope K) : -K = K

Uses 4 · Used by 1

Statement usesHanner polytopes

Proof uses\(\ell_\infty\) sum of bodies · \(\ell_1\) sum of bodies · Centered unit segment

Used byNegation preserves membership in a Hanner polytope

TheoremNegation preserves membership in a Hanner polytope#✓fully proved

For every Hanner polytope \(K \subseteq \mathbb{R}^n\) and every \(x \in \mathbb{R}^n\), \(-x \in K\) if and only if \(x \in K\).

theorem IsHannerPolytope.neg_mem_iff {n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : IsHannerPolytope K)
    {x : EuclideanSpace ℝ (Fin n)} : -x ∈ K ↔ x ∈ K

Uses 2

Statement usesHanner polytopes

Proof usesHanner polytopes are centrally symmetric

TheoremHanner polytopes are convex#✓fully proved

Every Hanner polytope \(K \subseteq \mathbb{R}^n\) is convex.

theorem IsHannerPolytope.convex {n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : IsHannerPolytope K) : Convex ℝ K

Uses 4 · Used by 1

Statement usesHanner polytopes

Proof uses\(\ell_\infty\) sum of bodies · \(\ell_1\) sum of bodies · Centered unit segment

Used byHanner polytopes are compact

TheoremHanner polytopes contain the origin#✓fully proved

The origin belongs to every Hanner polytope.

theorem IsHannerPolytope.zero_mem {n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : IsHannerPolytope K) : 0 ∈ K

Uses 4 · Used by 1

Statement usesHanner polytopes

Proof uses\(\ell_\infty\) sum of bodies · \(\ell_1\) sum of bodies · Centered unit segment

Used byHanner polytopes are compact

TheoremHanner polytopes are compact#✓fully proved

Every Hanner polytope is compact.

theorem IsHannerPolytope.isCompact {n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : IsHannerPolytope K) : IsCompact K

Uses 6

Statement usesHanner polytopes

Proof usesHanner polytopes are convex · Hanner polytopes contain the origin · \(\ell_\infty\) sum of bodies · \(\ell_1\) sum of bodies · Centered unit segment

TheoremHanner polytopes contain the origin in their interior#✓fully proved

For every \(n \in \mathbb{N}\) and every Hanner polytope \(K \subseteq \mathbb{R}^n\), the origin is an interior point of \(K\).

theorem IsHannerPolytope.zero_mem_interior {n : ℕ}
    {K : Set (EuclideanSpace ℝ (Fin n))} (hK : IsHannerPolytope K) : 0 ∈ interior K

Uses 4

Statement usesHanner polytopes

Proof uses\(\ell_\infty\) sum of bodies · \(\ell_1\) sum of bodies · Centered unit segment

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.