OAI/Analysis/AffineBernstein/NormalizedCellGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.normalizedCell line 16

   Source documentation

   The literal fixed cell of bounds.tex.

   def normalizedCell (k : ℕ) : Set (Space k) := {s | ∀ i, s i ∈ Icc (1/2) 2}

   Mentions: OAI.AffineBernstein.Space

2. def OAI.AffineBernstein.normalizedCellDomain line 18

   Source documentation

   The open positive neighbourhood used for differentiating support functions.

   def normalizedCellDomain (k : ℕ) : Set (Space k) := {s | ∀ i, s i ∈ Ioo (1/4) 4}

   Mentions: OAI.AffineBernstein.Space

3. lemma OAI.AffineBernstein.isOpen_normalizedCellDomain line 20
4. lemma OAI.AffineBernstein.convex_normalizedCellDomain line 26
5. lemma OAI.AffineBernstein.isCompact_normalizedCell line 31
6. lemma OAI.AffineBernstein.normalizedCell_subset_domain line 38
7. lemma OAI.AffineBernstein.normalizedCell_margin line 43
8. lemma OAI.AffineBernstein.capTiltedForm_eq_sum line 53
9. lemma OAI.AffineBernstein.capTiltedForm_coord_bound line 58
10. lemma OAI.AffineBernstein.capTiltedForm_center line 67
11. lemma OAI.AffineBernstein.capTiltedCovector_one_le line 72