Instances For
theorem
section14_dualAnnihilator_span_primal_eq_span_lineality_Cpolar_of_hpolar
{E : Type u_1}
[AddCommGroup E]
[Module ℝ E]
{C : Set E}
{Cpolar : Set (Module.Dual ℝ E)}
(hpolar : Cpolar = polar C)
(hCpolar0 : 0 ∈ Cpolar)
:
(Submodule.span ℝ C).dualAnnihilator = Submodule.span ℝ (-Cpolar.recessionCone ∩ Cpolar.recessionCone)
If Cpolar = polar C and 0 ∈ Cpolar, then the span of C is the orthogonal complement of
the lineality subspace of Cpolar (expressed via dual annihilators).
theorem
recessionCone_polar_eq_closure_coneHull_and_lineality_orthogonal_of_polarPair
{E : Type u_1}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[IsTopologicalAddGroup E]
[ContinuousSMul ℝ E]
[T2Space E]
[FiniteDimensional ℝ E]
[LocallyConvexSpace ℝ E]
{C : Set E}
{Cpolar : Set (Module.Dual ℝ E)}
(_hCclosed : IsClosed C)
(_hCconv : Convex ℝ C)
(hC0 : 0 ∈ C)
(_hCpolar_closed : IsClosed Cpolar)
(_hCpolar_conv : Convex ℝ Cpolar)
(hCpolar0 : 0 ∈ Cpolar)
(hpolar : Cpolar = polar C)
(hbipolar : {x : E | ∀ φ ∈ Cpolar, φ x ≤ 1} = C)
:
polarCone C.recessionCone = closure ↑(ConvexCone.hull ℝ Cpolar) ∧ ↑(PointedCone.dual (-LinearMap.applyₗ).flip (closure ↑(ConvexCone.hull ℝ Cpolar))) = C.recessionCone ∧ (Submodule.span ℝ (-C.recessionCone ∩ C.recessionCone)).dualAnnihilator = Submodule.span ℝ Cpolar ∧ (Submodule.span ℝ Cpolar).dualCoannihilator = Submodule.span ℝ (-C.recessionCone ∩ C.recessionCone) ∧ ↑(PointedCone.dual (-LinearMap.applyₗ).flip Cpolar.recessionCone) = closure ↑(ConvexCone.hull ℝ C) ∧ polarCone (closure ↑(ConvexCone.hull ℝ C)) = Cpolar.recessionCone ∧ (Submodule.span ℝ C).dualAnnihilator = Submodule.span ℝ (-Cpolar.recessionCone ∩ Cpolar.recessionCone) ∧ (Submodule.span ℝ (-Cpolar.recessionCone ∩ Cpolar.recessionCone)).dualCoannihilator = Submodule.span ℝ C
Theorem 14.6: Let C and C^∘ be a polar pair of closed convex sets containing the origin.
Then the recession cone of C and the closure of the convex cone generated by C^∘ are polar to
each other. The lineality space of C and the subspace generated by C^∘ are orthogonally
complementary. Dually, the same statements hold with C and C^∘ interchanged.