FixedWeightContact.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common Euclidean contact point for every cone containing one root

theorem OAI.PolycyclicRecognition.weight_contact_unique line 16

Source documentation

All unit contact points for a nonzero functional coincide.

theorem weight_contact_unique (α : W →L[ℝ] ℝ) (hα : α ≠ 0)
    {p q : W} (hp : ‖p‖ = 1) (hq : ‖q‖ = 1)
    (hap : α p = ‖α‖) (haq : α q = ‖α‖) : p = q := by
…

theorem OAI.PolycyclicRecognition.exists_polar_template_facet_slack_at line 30

Source documentation

The contact point is fixed before choosing any cone that contains the root.

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

Mentions: OAI.PolycyclicRecognition.conePolarTemplate