SupportDirectionCap.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Separating one unsupported direction by a small cap

The cap preserves all the supports in a finite list of directions and strictly lowers support in a direction outside their positive rays.

theorem OAI.PolycyclicRecognition.exists_support_direction_cap line 28

Source documentation

A compact convex truncation of the unit ball leaves the prescribed support values unchanged but strictly lowers support in any additional direction not on their positive rays.

theorem exists_support_direction_cap (v : I → W) (b : W) (hb : b ≠ 0)
    (hnot : ∀ i (r : ℝ), 0 < r → b ≠ r • v i) :
    ∃ E : Set W, IsCompact E ∧ E.Nonempty ∧ Convex ℝ E ∧
      E ⊆ Metric.closedBall 0 1 ∧
      (∀ i, ∃ x ∈ E, inner ℝ (v i) x = ‖v i‖) ∧
      ∃ c : ℝ, c < ‖b‖ ∧ ∀ x ∈ E, inner ℝ b x ≤ c := by
…