ConeFacetTemplate.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A fixed polar template near a generator facet

The template radius is independent of the small chart enlargement. Only its centre moves inward with that enlargement.

theorem OAI.PolycyclicRecognition.exists_weight_contact_point line 24

Source documentation

The Euclidean contact point has strict slack in every other oriented ray. This is the equality case of the Cauchy--Schwarz inequality.

theorem exists_weight_contact_point (α : W →L[ℝ] ℝ) (hα : α ≠ 0) :
    ∃ p : W, ‖p‖ = 1 ∧ α p = ‖α‖ ∧ ∀ β : W →L[ℝ] ℝ, β ≠ 0 →
      (¬ ∃ t : ℝ, 0 < t ∧ β = t • α) → β p < ‖β‖ := by
…

theorem OAI.PolycyclicRecognition.exists_polar_template_facet_slack line 66

Source documentation

All small polar templates centred just inside the contact facet lie strictly in the prescribed smaller weight polyhedron. One positive radius works for every sufficiently small positive chart enlargement.

theorem exists_polar_template_facet_slack
    {I : Type*} [Fintype I] (α : I → W →L[ℝ] ℝ) (hne : ∀ i, α i ≠ 0)
    (i₀ : I) (C : ProperCone ℝ (W →L[ℝ] ℝ)) (hC : α i₀ ∈ C)
    {c c' : ℝ} (hc : 0 ≤ c) (hcc : c < c') :
    ∃ (p : W) (ε₀ δ₀ : ℝ), α i₀ p = ‖α i₀‖ ∧
      0 < ε₀ ∧ 0 < δ₀ ∧ ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
      ∀ ε : ℝ, 0 ≤ ε → ε ≤ ε₀ → ∀ z ∈ conePolarTemplate C,
        ∀ i, α i ((1 - c' * δ) • p + ε • z) < (1 - c * δ) * ‖α i‖ := by
…

Mentions: OAI.PolycyclicRecognition.conePolarTemplate