Euclidean.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Coordinate and Euclidean versions of the explicit centered zonotope.

def OAI.DiagonalZonotope.euclidean line 16
Source documentation
The actual scalar image of the cube-plus-diagonal body in Euclidean space.
```
def euclidean (c : ℝ) : Set (EuclideanSpace ℝ ι) :=
…
```
def OAI.DiagonalZonotope.support line 20
Source documentation
The directional support value, before multiplication by the scale.
```
def support (u : ι → ℝ) : ℝ := ((∑ i, |u i|) + |∑ i, u i|) / 2
```
lemma OAI.DiagonalZonotope.support_zero line 22
lemma OAI.DiagonalZonotope.support_smul line 24
lemma OAI.DiagonalZonotope.inner_eq_coordinates line 27
lemma OAI.DiagonalZonotope.mem_euclidean_iff line 32

theorem OAI.DiagonalZonotope.euclidean_eq_halfspaces line 41

Source documentation

All directional inequalities characterize this concrete Euclidean body.

theorem euclidean_eq_halfspaces [DecidableEq ι] (c : ℝ) (hc : 0 < c) :
    (euclidean c : Set (EuclideanSpace ℝ ι)) =
      {x | ∀ u : EuclideanSpace ℝ ι, ⟪u, x⟫ ≤ c * support (WithLp.ofLp u)} := by
…

Mentions: OAI.DiagonalZonotope.euclidean, OAI.DiagonalZonotope.support

theorem OAI.DiagonalZonotope.euclidean_support_attained line 53
Source documentation
Every directional support inequality is attained by an explicit point.
```
theorem euclidean_support_attained (c : ℝ) (u : EuclideanSpace ℝ ι) :
    ∃ x ∈ euclidean c, ⟪u, x⟫ = c * support (WithLp.ofLp u) := by
…
```
Mentions: OAI.DiagonalZonotope.euclidean, OAI.DiagonalZonotope.support
lemma OAI.DiagonalZonotope.isCompact_euclidean line 59
lemma OAI.DiagonalZonotope.convex_euclidean line 62
lemma OAI.DiagonalZonotope.euclidean_interior_nonempty line 66