Convex Analysis (Rockafellar, 1970) -- Chapter 04 -- Section 20 -- Part 5

open scoped BigOperators Pointwisesection Chap04section Section20

Helper for Theorem 20.0.4: mixed two-block closure bridge from a polyhedral left block and a Unknown identifier `dom`sorry / sorry : ?m.5dom/Unknown identifier `ri`ri witness.

lemma helperForTheorem_20_0_4_mem_preimage_effectiveDomain_of_equivSymm {n : โ„•} (p : (Fin n โ†’ โ„) โ†’ EReal) {x0 : Fin n โ†’ โ„} (hx0DomP : x0 โˆˆ effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) : (EuclideanSpace.equiv (๐•œ := โ„) (ฮน := Fin n)).symm x0 โˆˆ ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) := by simpa using hx0DomP

Helper for Theorem 20.0.4: the WithLp.toLp.{u_1} (p : ENNReal) {V : Type u_1} (ofLp : V) : WithLp p VWithLp.toLp image description of an effective domain agrees with the Euclidean-space preimage description.

lemma helperForTheorem_20_0_4_image_effectiveDomain_eq_preimage_effectiveDomain {n : โ„•} (q : (Fin n โ†’ โ„) โ†’ EReal) : ((fun a : Fin n โ†’ โ„ => WithLp.toLp 2 a) '' (effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q)) = ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q) := by ext x constructor ยท rintro โŸจx', hx', rflโŸฉ simpa [WithLp.ofLp_toLp] using hx' ยท intro hx refine โŸจx.ofLp, ?_, ?_โŸฉ ยท simpa using hx ยท try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [WithLp.toLp_ofLp]

Helper for Theorem 20.0.4: a mixed Unknown identifier `dom`sorry / sorry : ?m.5dom/Unknown identifier `ri`ri witness yields a point in the left effective domain preimage and in the right relative-interior preimage.

lemma helperForTheorem_20_0_4_exists_preimageDom_and_riPreimage_point_of_dom_ri_witness {n : โ„•} (p q : (Fin n โ†’ โ„) โ†’ EReal) (hdomRiWitness : โˆƒ x0 : Fin n โ†’ โ„, x0 โˆˆ effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p โˆง (EuclideanSpace.equiv (๐•œ := โ„) (ฮน := Fin n)).symm x0 โˆˆ euclideanRelativeInterior n ((fun a : Fin n โ†’ โ„ => WithLp.toLp 2 a) '' (effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q))) : โˆƒ x0E : EuclideanSpace โ„ (Fin n), x0E โˆˆ ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) โˆง x0E โˆˆ euclideanRelativeInterior n ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q) := by rcases hdomRiWitness with โŸจx0, hx0DomP, hx0RiQImageโŸฉ let x0E : EuclideanSpace โ„ (Fin n) := (EuclideanSpace.equiv (๐•œ := โ„) (ฮน := Fin n)).symm x0 have hqImageEqPreimage : ((fun a : Fin n โ†’ โ„ => WithLp.toLp 2 a) '' (effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q)) = ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q) := helperForTheorem_20_0_4_image_effectiveDomain_eq_preimage_effectiveDomain (q := q) have hx0RiQPreimage : x0E โˆˆ euclideanRelativeInterior n ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q) := by simpa [x0E, hqImageEqPreimage] using hx0RiQImage have hx0MemPPreimage : x0E โˆˆ ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) := by simpa [x0E] using helperForTheorem_20_0_4_mem_preimage_effectiveDomain_of_equivSymm (p := p) (x0 := x0) hx0DomP exact โŸจx0E, hx0MemPPreimage, hx0RiQPreimageโŸฉ

Helper for Theorem 20.0.4: a nonempty mixed preimage intersection yields an explicit mixed Unknown identifier `dom`sorry / sorry : ?m.5dom/Unknown identifier `ri`ri witness in the original coordinates.

lemma helperForTheorem_20_0_4_extract_dom_ri_witness_of_nonempty_preimageDom_inter_riPreimage {n : โ„•} (p q : (Fin n โ†’ โ„) โ†’ EReal) (hnonemptyDomInterRi : Set.Nonempty (((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) โˆฉ euclideanRelativeInterior n ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q))) : โˆƒ x0 : Fin n โ†’ โ„, x0 โˆˆ effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p โˆง (EuclideanSpace.equiv (๐•œ := โ„) (ฮน := Fin n)).symm x0 โˆˆ euclideanRelativeInterior n ((fun a : Fin n โ†’ โ„ => WithLp.toLp 2 a) '' (effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q)) := by rcases hnonemptyDomInterRi with โŸจx0E, hx0EโŸฉ refine โŸจ(x0E : Fin n โ†’ โ„), hx0E.1, ?_โŸฉ have hqImageEqPreimage : ((fun a : Fin n โ†’ โ„ => WithLp.toLp 2 a) '' (effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q)) = ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q) := helperForTheorem_20_0_4_image_effectiveDomain_eq_preimage_effectiveDomain (q := q) have hx0EriImage : x0E โˆˆ euclideanRelativeInterior n ((fun a : Fin n โ†’ โ„ => WithLp.toLp 2 a) '' (effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q)) := by simpa [hqImageEqPreimage] using hx0E.2 have hx0Esymm : (EuclideanSpace.equiv (๐•œ := โ„) (ฮน := Fin n)).symm (x0E : Fin n โ†’ โ„) = x0E := by simp simpa [hx0Esymm] using hx0EriImage

Helper for Theorem 20.0.4: a mixed Unknown identifier `dom`sorry / sorry : ?m.5dom/Unknown identifier `ri`ri witness induces a nonempty intersection of the left effective-domain preimage and the right relative-interior preimage.

lemma helperForTheorem_20_0_4_nonempty_preimageDom_inter_riPreimage_of_dom_ri_witness {n : โ„•} (p q : (Fin n โ†’ โ„) โ†’ EReal) (hdomRiWitness : โˆƒ x0 : Fin n โ†’ โ„, x0 โˆˆ effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p โˆง (EuclideanSpace.equiv (๐•œ := โ„) (ฮน := Fin n)).symm x0 โˆˆ euclideanRelativeInterior n ((fun a : Fin n โ†’ โ„ => WithLp.toLp 2 a) '' (effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q))) : Set.Nonempty (((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) โˆฉ euclideanRelativeInterior n ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q)) := by rcases helperForTheorem_20_0_4_exists_preimageDom_and_riPreimage_point_of_dom_ri_witness (p := p) (q := q) hdomRiWitness with โŸจx0E, hx0MemPPreimage, hx0RiQPreimageโŸฉ exact โŸจx0E, โŸจhx0MemPPreimage, hx0RiQPreimageโŸฉโŸฉ

Helper for Theorem 20.0.4: mixed two-block closure bridge from a polyhedral left block and a Unknown identifier `dom`sorry / sorry : ?m.5dom/Unknown identifier `ri`ri witness.

lemma helperForTheorem_20_0_4_convex_preimage_effectiveDomain_of_proper {n : โ„•} (p : (Fin n โ†’ โ„) โ†’ EReal) (hproperP : ProperConvexFunctionOn (Set.univ : Set (Fin n โ†’ โ„)) p) : Convex โ„ (((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p)) := by have hconvDom : Convex โ„ (effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) := effectiveDomain_convex (S := (Set.univ : Set (Fin n โ†’ โ„))) (f := p) hproperP.1 simpa using hconvDom.linear_preimage ((EuclideanSpace.equiv (๐•œ := โ„) (ฮน := Fin n)).toLinearMap)

Helper for Theorem 20.0.4: from a nonempty mixed intersection, the left effective-domain preimage is nonempty.

lemma helperForTheorem_20_0_4_nonempty_preimage_effectiveDomain_left_of_nonempty_dom_inter_ri_right {n : โ„•} (p q : (Fin n โ†’ โ„) โ†’ EReal) (hnonemptyDomInterRi : Set.Nonempty (((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) โˆฉ euclideanRelativeInterior n ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) q))) : Set.Nonempty ((fun x : EuclideanSpace โ„ (Fin n) => (x : Fin n โ†’ โ„)) โปยน' effectiveDomain (Set.univ : Set (Fin n โ†’ โ„)) p) := by rcases hnonemptyDomInterRi with โŸจx0E, hx0EโŸฉ exact โŸจx0E, hx0E.1โŸฉ
end Section20end Chap04