Convex Analysis (Rockafellar, 1970) -- Chapter 03 -- Section 14 -- Part 11
section Chap03section Section14open scoped Pointwiseopen scoped Topologyvariable {E : Type*} [AddCommGroup E] [Module ℝ E]noncomputable local instance : TopologicalSpace (Module.Dual ℝ E) :=
WeakBilin.instTopologicalSpace
(B := (LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ)).flip)
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).
lemma section14_dualAnnihilator_span_primal_eq_span_lineality_Cpolar_of_hpolar
{C : Set E} {Cpolar : Set (Module.Dual ℝ E)}
(hpolar : Cpolar = polar (E := E) C) (hCpolar0 : (0 : Module.Dual ℝ E) ∈ Cpolar) :
(Submodule.span ℝ C).dualAnnihilator =
Submodule.span ℝ ((-Set.recessionCone Cpolar) ∩ Set.recessionCone Cpolar) := by
classical
have hlin :
(-Set.recessionCone Cpolar) ∩ Set.recessionCone Cpolar =
{ψ : Module.Dual ℝ E | ∀ x ∈ C, ψ x = 0} :=
section14_lineality_Cpolar_eq_forall_primal_eq_zero_of_hpolar (E := E) (C := C) (Cpolar := Cpolar)
hpolar hCpolar0
refine le_antisymm ?_ ?_
· intro ψ hψ
have hker : C ⊆ LinearMap.ker ψ := by
change ψ ∈ ((Submodule.span ℝ C).dualAnnihilator : Set (Module.Dual ℝ E)) at hψ
simpa using hψ
have hψ0 : ∀ x ∈ C, ψ x = 0 := by
intro x hxC
have : x ∈ LinearMap.ker ψ := hker hxC
simpa [LinearMap.mem_ker] using this
have hmem : ψ ∈ (-Set.recessionCone Cpolar) ∩ Set.recessionCone Cpolar := by
have : ψ ∈ {ψ : Module.Dual ℝ E | ∀ x ∈ C, ψ x = 0} := by
simpa [Set.mem_setOf_eq] using hψ0
simpa [hlin] using this
exact Submodule.subset_span hmem
· refine Submodule.span_le.2 ?_
intro ψ hψ
have hψ0 : ∀ x ∈ C, ψ x = 0 := by
have : ψ ∈ {ψ : Module.Dual ℝ E | ∀ x ∈ C, ψ x = 0} := by simpa [hlin] using hψ
simpa [Set.mem_setOf_eq] using this
have hker : C ⊆ LinearMap.ker ψ := by
intro x hxC
have hx0 : ψ x = 0 := hψ0 x hxC
simp [LinearMap.mem_ker, hx0]
change ψ ∈ ((Submodule.span ℝ C).dualAnnihilator : Set (Module.Dual ℝ E))
simpa using hker
Theorem 14.6: Let C and 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 are polar to
each other. The lineality space of C and the subspace generated by are orthogonally
complementary. Dually, the same statements hold with C and interchanged.
theorem recessionCone_polar_eq_closure_coneHull_and_lineality_orthogonal_of_polarPair
[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 : E) ∈ C)
(_hCpolar_closed : IsClosed Cpolar) (_hCpolar_conv : Convex ℝ Cpolar)
(hCpolar0 : (0 : Module.Dual ℝ E) ∈ Cpolar)
(hpolar : Cpolar = polar (E := E) C) (hbipolar : {x : E | ∀ φ ∈ Cpolar, φ x ≤ 1} = C) :
polarCone (E := E) (Set.recessionCone C) =
closure ((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) : Set _) ∧
(PointedCone.dual (R := ℝ)
((-LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))).flip
(closure ((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) : Set _)) :
Set E) =
Set.recessionCone C ∧
(Submodule.span ℝ ((-Set.recessionCone C) ∩ Set.recessionCone C)).dualAnnihilator =
Submodule.span ℝ Cpolar ∧
(Submodule.span ℝ Cpolar).dualCoannihilator =
Submodule.span ℝ ((-Set.recessionCone C) ∩ Set.recessionCone C) ∧
(PointedCone.dual (R := ℝ)
((-LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))).flip
(Set.recessionCone Cpolar) :
Set E) =
closure ((ConvexCone.hull ℝ C : ConvexCone ℝ E) : Set _) ∧
polarCone (E := E) (closure ((ConvexCone.hull ℝ C : ConvexCone ℝ E) : Set _)) =
Set.recessionCone Cpolar ∧
(Submodule.span ℝ C).dualAnnihilator =
Submodule.span ℝ ((-Set.recessionCone Cpolar) ∩ Set.recessionCone Cpolar) ∧
(Submodule.span ℝ ((-Set.recessionCone Cpolar) ∩ Set.recessionCone Cpolar)).dualCoannihilator
=
Submodule.span ℝ C := by
classical
have hrec :
Set.recessionCone C = {y : E | ∀ φ ∈ Cpolar, φ y ≤ 0} :=
section14_recessionCone_eq_forall_polar_le_zero_of_bipolar (E := E) (C := C) (Cpolar := Cpolar)
hbipolar hC0
have hCpolar_ne : Cpolar.Nonempty := ⟨0, hCpolar0⟩
have hKne :
(closure
((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) :
Set (Module.Dual ℝ E))).Nonempty :=
section14_closure_coneHull_nonempty_of_nonempty (E := E) (T := Cpolar) hCpolar_ne
have h4 :
(Submodule.span ℝ Cpolar).dualCoannihilator =
Submodule.span ℝ ((-Set.recessionCone C) ∩ Set.recessionCone C) := by
simpa using
(section14_dualCoannihilator_span_polar_eq_span_negRec_inter_rec_of_bipolar (E := E)
(C := C) (Cpolar := Cpolar) hbipolar hC0)
have h7 :
(Submodule.span ℝ C).dualAnnihilator =
Submodule.span ℝ ((-Set.recessionCone Cpolar) ∩ Set.recessionCone Cpolar) := by
simpa using
(section14_dualAnnihilator_span_primal_eq_span_lineality_Cpolar_of_hpolar (E := E)
(C := C) (Cpolar := Cpolar) hpolar hCpolar0)
refine And.intro ?_ (And.intro ?_ (And.intro ?_ (And.intro ?_ (And.intro ?_ (And.intro ?_ (And.intro ?_ ?_))))))
·
have hclosed : IsClosed (polarCone (E := E) (Set.recessionCone C)) :=
section14_isClosed_polarCone (E := E) (K := Set.recessionCone C)
have hclosure_le :
closure ((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) : Set _) ⊆
polarCone (E := E) (Set.recessionCone C) := by
have hgen : Cpolar ⊆ polarCone (E := E) (Set.recessionCone C) := by
intro φ hφ
refine (mem_polarCone_iff (E := E) (K := Set.recessionCone C) (φ := φ)).2 ?_
intro y hy
have hy' : ∀ ψ ∈ Cpolar, ψ y ≤ 0 := by
have : y ∈ {y : E | ∀ ψ ∈ Cpolar, ψ y ≤ 0} := by simpa [hrec] using hy
simpa [Set.mem_setOf_eq] using this
exact hy' φ hφ
exact
section14_closure_coneHull_subset_polarCone_of_subset (E := E) (K := Set.recessionCone C)
(T := Cpolar) hgen hclosed
have hle :
polarCone (E := E) (Set.recessionCone C) ⊆
closure ((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) : Set _) := by
intro φ hφ
by_contra hφcl
obtain ⟨x, hx_nonpos, hx_pos⟩ :=
section14_exists_eval_pos_of_not_mem_closure_coneHull (E := E) (T := Cpolar) (hKne := hKne)
(φ := φ) hφcl
have hxCpolar : ∀ ψ : Module.Dual ℝ E, ψ ∈ Cpolar → ψ x ≤ 0 := by
intro ψ hψ
apply hx_nonpos ψ
exact subset_closure (ConvexCone.subset_hull (R := ℝ) (s := Cpolar) hψ)
have hxrec : x ∈ Set.recessionCone C := by
have : x ∈ {y : E | ∀ ψ ∈ Cpolar, ψ y ≤ 0} := by
simpa [Set.mem_setOf_eq] using hxCpolar
simpa [hrec] using this
have hxle : φ x ≤ 0 :=
(mem_polarCone_iff (E := E) (K := Set.recessionCone C) (φ := φ)).1 hφ x hxrec
exact (not_lt_of_ge hxle) hx_pos
exact Set.Subset.antisymm hle hclosure_le
·
ext x
constructor
· intro hx
have hx' :
∀ ψ : Module.Dual ℝ E,
ψ ∈
closure
((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) :
Set (Module.Dual ℝ E)) →
ψ x ≤ 0 :=
(section14_mem_dual_flip_eval_iff_forall_le_zero (E := E)
(S :=
closure
((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) :
Set (Module.Dual ℝ E)))
(x := x)).1 hx
have hxCpolar : ∀ φ : Module.Dual ℝ E, φ ∈ Cpolar → φ x ≤ 0 := by
intro φ hφ
exact hx' φ (subset_closure (ConvexCone.subset_hull (R := ℝ) (s := Cpolar) hφ))
have : x ∈ {y : E | ∀ φ ∈ Cpolar, φ y ≤ 0} := by
simpa [Set.mem_setOf_eq] using hxCpolar
simpa [hrec] using this
· intro hx
have hxCpolar : ∀ φ : Module.Dual ℝ E, φ ∈ Cpolar → φ x ≤ 0 := by
have : x ∈ {y : E | ∀ φ ∈ Cpolar, φ y ≤ 0} := by simpa [hrec] using hx
simpa [Set.mem_setOf_eq] using this
have hclosed : IsClosed (polarCone (E := E) ({x} : Set E)) :=
section14_isClosed_polarCone (E := E) (K := ({x} : Set E))
have hgen : Cpolar ⊆ polarCone (E := E) ({x} : Set E) := by
intro φ hφ
refine (mem_polarCone_iff (E := E) (K := ({x} : Set E)) (φ := φ)).2 ?_
intro y hy
rcases hy with rfl
exact hxCpolar φ hφ
have hclosure :
closure
((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) :
Set (Module.Dual ℝ E)) ⊆
polarCone (E := E) ({x} : Set E) :=
section14_closure_coneHull_subset_polarCone_of_subset (E := E) (K := ({x} : Set E))
(T := Cpolar) hgen hclosed
refine
(section14_mem_dual_flip_eval_iff_forall_le_zero (E := E)
(S :=
closure
((ConvexCone.hull ℝ Cpolar : ConvexCone ℝ (Module.Dual ℝ E)) :
Set (Module.Dual ℝ E)))
(x := x)).2 ?_
intro ψ hψ
have hψpol : ψ ∈ polarCone (E := E) ({x} : Set E) := hclosure hψ
exact
(mem_polarCone_iff (E := E) (K := ({x} : Set E)) (φ := ψ)).1 hψpol x (by simp)
·
have h4' := congrArg Submodule.dualAnnihilator h4
have hW :
((Submodule.span ℝ Cpolar).dualCoannihilator).dualAnnihilator =
Submodule.span ℝ Cpolar := by
simpa using (Subspace.dualCoannihilator_dualAnnihilator_eq (W := (Submodule.span ℝ Cpolar)))
have :
Submodule.span ℝ Cpolar =
(Submodule.span ℝ ((-Set.recessionCone C) ∩ Set.recessionCone C)).dualAnnihilator := by
simpa [hW] using h4'
simpa using this.symm
·
-- This direction (coannihilator equality) follows from the bipolar characterization of the recession cone.
exact h4
·
have hrecCpolar : Set.recessionCone Cpolar = polarCone (E := E) C := by
ext ψ
simp [section14_recessionCone_Cpolar_eq_forall_primal_le_zero_of_hpolar (E := E) (C := C)
(Cpolar := Cpolar) hpolar hCpolar0, mem_polarCone_iff]
have hKne : (((ConvexCone.hull ℝ C : ConvexCone ℝ E) : Set E)).Nonempty :=
⟨0, ConvexCone.subset_hull (R := ℝ) (s := C) hC0⟩
have hdual :
(PointedCone.dual (R := ℝ)
((-LinearMap.applyₗ (R := ℝ) (M := E) (M₂ := ℝ))).flip
(polarCone (E := E) C) :
Set E) =
closure ((ConvexCone.hull ℝ C : ConvexCone ℝ E) : Set E) := by
simpa [section14_polarCone_hull_eq (E := E) (S := C)] using
(polarCone_polar_eq_closure (E := E) (K := ConvexCone.hull ℝ C) hKne)
simpa [hrecCpolar] using hdual
·
have hrecCpolar : Set.recessionCone Cpolar = polarCone (E := E) C := by
ext ψ
simp [section14_recessionCone_Cpolar_eq_forall_primal_le_zero_of_hpolar (E := E) (C := C)
(Cpolar := Cpolar) hpolar hCpolar0, mem_polarCone_iff]
calc
polarCone (E := E) (closure ((ConvexCone.hull ℝ C : ConvexCone ℝ E) : Set E)) =
polarCone (E := E) ((ConvexCone.hull ℝ C : ConvexCone ℝ E) : Set E) := by
simpa using (polarCone_closure_eq (E := E) (K := ConvexCone.hull ℝ C))
_ = polarCone (E := E) C := by
simpa using (section14_polarCone_hull_eq (E := E) (S := C))
_ = Set.recessionCone Cpolar := by
simp [hrecCpolar]
·
exact h7
·
have h7' := congrArg Submodule.dualCoannihilator h7
have hW :
((Submodule.span ℝ C).dualAnnihilator).dualCoannihilator = Submodule.span ℝ C := by
simp
have :
Submodule.span ℝ C =
(Submodule.span ℝ ((-Set.recessionCone Cpolar) ∩ Set.recessionCone Cpolar)).dualCoannihilator := by
simpa [hW] using h7'
simpa using this.symmend Section14end Chap03