Support.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DiagonalZonotope.centered line 15
Source documentation
The translate of the diagonal zonotope centered at the origin.
```
def centered : Set (ι → ℝ) := {x | (fun j => x j + 1) ∈ zonotope}
```
Mentions: OAI.DiagonalZonotope.zonotope
theorem OAI.DiagonalZonotope.mem_centered_iff line 18
Source documentation
Coordinate and coordinate-difference inequalities describe the centered body exactly.
```
theorem mem_centered_iff (x : ι → ℝ) :
    x ∈ centered ↔ (∀ i, |x i| ≤ 1) ∧ ∀ i j, |x i - x j| ≤ 1 := by
…
```
Mentions: OAI.DiagonalZonotope.centered
lemma OAI.DiagonalZonotope.interval_mul_bound line 53
lemma OAI.DiagonalZonotope.interval_mul_max line 61
theorem OAI.DiagonalZonotope.centered_support_le line 68
Source documentation
Every point satisfies the exact support bound, expressed as a coordinate pairing.
```
theorem centered_support_le (u x : ι → ℝ) (hx : x ∈ centered) :
    (∑ i, u i * x i) ≤ ((∑ i, |u i|) + |∑ i, u i|) / 2 := by
…
```
Mentions: OAI.DiagonalZonotope.centered
theorem OAI.DiagonalZonotope.centered_support_attained line 85
Source documentation
A sign-selected point attains the support bound in every direction.
```
theorem centered_support_attained (u : ι → ℝ) :
    ∃ x ∈ centered, (∑ i, u i * x i) =
      ((∑ i, |u i|) + |∑ i, u i|) / 2 := by
…
```
Mentions: OAI.DiagonalZonotope.centered