Convex Analysis (Rockafellar, 1970) -- Chapter 02 -- Section 07 -- Part 2

noncomputable sectionopen scoped Topologysection Chap02section Section07

The Unknown identifier `Ξ±`Ξ±-sublevel of the liminf is the intersection of closed Unknown identifier `ΞΌ`ΞΌ-sublevel sets above Unknown identifier `Ξ±`Ξ±.

lemma sublevel_liminf_eq_iInter_closure_sublevel {n : Nat} (f : (Fin n β†’ Real) β†’ EReal) (Ξ± : Real) : {x | Filter.liminf (fun y : Fin n β†’ Real => f y) (𝓝 x) ≀ (Ξ± : EReal)} = β‹‚ (ΞΌ : {ΞΌ : Real // ΞΌ > Ξ±}), closure {x | f x ≀ ((ΞΌ : Real) : EReal)} := by ext x constructor Β· intro hx exact liminf_le_mem_iInter_closure_sublevel (f := f) (Ξ± := Ξ±) (x := x) hx Β· intro hx exact liminf_le_of_mem_iInter_closure_sublevel (f := f) (Ξ± := Ξ±) (x := x) hx

Text 7.0.11: For each failed to synthesize Membership ?m.1 Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Unknown identifier `Ξ±`Ξ± ∈ ℝ, {x | convexFunctionClosure sorry x ≀ sorry} = β‹‚ ΞΌ, β‹‚ (h : ΞΌ > sorry), closure {x | sorry ≀ ΞΌ} : Prop{x | (convexFunctionClosure Unknown identifier `f`f) x ≀ Unknown identifier `Ξ±`Ξ±} = β‹‚ (ΞΌ > Unknown identifier `Ξ±`Ξ±), closure {x | Unknown identifier `f`f x ≀ ΞΌ}.

theorem sublevel_convexFunctionClosure_eq_iInter_closure_sublevel {n : Nat} (f : (Fin n β†’ Real) β†’ EReal) (Ξ± : Real) (hbot : βˆ€ x, f x β‰  (βŠ₯ : EReal)) : {x | convexFunctionClosure f x ≀ (Ξ± : EReal)} = β‹‚ (ΞΌ : {ΞΌ : Real // ΞΌ > Ξ±}), closure {x | f x ≀ ((ΞΌ : Real) : EReal)} := by have hliminf := (epigraph_convexFunctionClosure_eq_closure_epigraph (f := f) hbot).2 ext x constructor Β· intro hx have hx' : Filter.liminf (fun y : Fin n β†’ Real => f y) (𝓝 x) ≀ (Ξ± : EReal) := by simpa [hliminf x] using hx exact liminf_le_mem_iInter_closure_sublevel (f := f) (Ξ± := Ξ±) (x := x) hx' Β· intro hx have hx' : Filter.liminf (fun y : Fin n β†’ Real => f y) (𝓝 x) ≀ (Ξ± : EReal) := liminf_le_of_mem_iInter_closure_sublevel (f := f) (Ξ± := Ξ±) (x := x) hx simpa [hliminf x] using hx'

The closure of a function is pointwise below the function itself.

lemma convexFunctionClosure_le_self {n : Nat} (f : (Fin n β†’ Real) β†’ EReal) : convexFunctionClosure f ≀ f := by classical by_cases hbot : βˆ€ x, f x β‰  (βŠ₯ : EReal) Β· have hspec := Classical.choose_spec (exists_lowerSemicontinuousHull (n := n) f) have hle : lowerSemicontinuousHull f ≀ f := by simpa [lowerSemicontinuousHull] using hspec.2.1 simpa [convexFunctionClosure, hbot] using hle Β· push_neg at hbot have hcl : convexFunctionClosure f = (fun _ => (βŠ₯ : EReal)) := convexFunctionClosure_eq_bot_of_exists_bot (f := f) hbot intro x simp [hcl]

The closure operator is monotone with respect to the pointwise order.

lemma convexFunctionClosure_mono {n : Nat} {f1 f2 : (Fin n β†’ Real) β†’ EReal} (h12 : f1 ≀ f2) : convexFunctionClosure f1 ≀ convexFunctionClosure f2 := by classical by_cases hbot1 : βˆ€ x, f1 x β‰  (βŠ₯ : EReal) Β· have hbot2 : βˆ€ x, f2 x β‰  (βŠ₯ : EReal) := by intro x hx have hle : f1 x ≀ (βŠ₯ : EReal) := by simpa [hx] using h12 x have hbot1x : f1 x = (βŠ₯ : EReal) := (le_bot_iff).1 hle exact hbot1 x hbot1x have hspec1 := Classical.choose_spec (exists_lowerSemicontinuousHull (n := n) f1) have hspec2 := Classical.choose_spec (exists_lowerSemicontinuousHull (n := n) f2) have hls1 : LowerSemicontinuous (lowerSemicontinuousHull f1) := by simpa [lowerSemicontinuousHull] using hspec1.1 have hle1 : lowerSemicontinuousHull f1 ≀ f1 := by simpa [lowerSemicontinuousHull] using hspec1.2.1 have hle1' : lowerSemicontinuousHull f1 ≀ f2 := by intro x exact le_trans (hle1 x) (h12 x) have hle12 : lowerSemicontinuousHull f1 ≀ lowerSemicontinuousHull f2 := by have hmax2 : βˆ€ h : (Fin n β†’ Real) β†’ EReal, LowerSemicontinuous h β†’ h ≀ f2 β†’ h ≀ lowerSemicontinuousHull f2 := by intro h hlsc hle simpa [lowerSemicontinuousHull] using hspec2.2.2 h hlsc hle exact hmax2 _ hls1 hle1' simpa [convexFunctionClosure, hbot1, hbot2] using hle12 Β· push_neg at hbot1 have hcl1 : convexFunctionClosure f1 = (fun _ => (βŠ₯ : EReal)) := convexFunctionClosure_eq_bot_of_exists_bot (f := f1) hbot1 intro x simp [hcl1]

The infimum of a function equals the infimum of its closure.

lemma iInf_convexFunctionClosure_eq {n : Nat} (f : (Fin n β†’ Real) β†’ EReal) : iInf (fun x => f x) = iInf (fun x => convexFunctionClosure f x) := by classical by_cases hbot : βˆ€ x, f x β‰  (βŠ₯ : EReal) Β· have hspec := Classical.choose_spec (exists_lowerSemicontinuousHull (n := n) f) have hmax : βˆ€ h : (Fin n β†’ Real) β†’ EReal, LowerSemicontinuous h β†’ h ≀ f β†’ h ≀ lowerSemicontinuousHull f := by intro h hlsc hle simpa [lowerSemicontinuousHull] using hspec.2.2 h hlsc hle have hconst_lsc : LowerSemicontinuous (fun _ : (Fin n β†’ Real) => iInf (fun x => f x)) := by simpa using (lowerSemicontinuous_const : LowerSemicontinuous (fun _ : (Fin n β†’ Real) => iInf (fun x => f x))) have hconst_le : (fun _ : (Fin n β†’ Real) => iInf (fun x => f x)) ≀ f := by intro x exact iInf_le (fun x => f x) x have hconst_le_hull : (fun _ : (Fin n β†’ Real) => iInf (fun x => f x)) ≀ lowerSemicontinuousHull f := hmax _ hconst_lsc hconst_le have hle_closure : iInf (fun x => convexFunctionClosure f x) ≀ iInf (fun x => f x) := iInf_mono (convexFunctionClosure_le_self (f := f)) have hle_inf : iInf (fun x => f x) ≀ iInf (fun x => convexFunctionClosure f x) := by refine le_iInf ?_ intro x have hx : iInf (fun x => f x) ≀ lowerSemicontinuousHull f x := hconst_le_hull x simpa [convexFunctionClosure, hbot] using hx exact le_antisymm hle_inf hle_closure Β· push_neg at hbot rcases hbot with ⟨x, hx⟩ have hcl : convexFunctionClosure f = (fun _ => (βŠ₯ : EReal)) := convexFunctionClosure_eq_bot_of_exists_bot (f := f) ⟨x, hx⟩ have hInf_le : iInf (fun x => f x) ≀ (βŠ₯ : EReal) := by simpa [hx] using (iInf_le (fun x => f x) x) have hInf_eq : iInf (fun x => f x) = (βŠ₯ : EReal) := le_antisymm hInf_le bot_le calc iInf (fun x => f x) = (βŠ₯ : EReal) := hInf_eq _ = iInf (fun x => convexFunctionClosure f x) := by simp [hcl]

Text 7.0.12: For any extended-real-valued function , one has Unknown identifier `cl`sorry ≀ sorry : Propcl f ≀ Unknown identifier `f`f. Moreover, if Unknown identifier `f₁`sorry ≀ sorry : Propf₁ ≀ Unknown identifier `fβ‚‚`fβ‚‚, then Unknown identifier `cl`sorry ≀ sorry : Propcl f₁ ≀ Unknown identifier `cl`cl fβ‚‚. In addition, . Here Unknown identifier `cl`cl f is convexFunctionClosure sorry : (Fin ?m.1 β†’ ℝ) β†’ ERealconvexFunctionClosure Unknown identifier `f`f.

theorem convexFunctionClosure_properties {n : Nat} : (βˆ€ f : (Fin n β†’ Real) β†’ EReal, convexFunctionClosure f ≀ f) ∧ (βˆ€ f1 f2 : (Fin n β†’ Real) β†’ EReal, f1 ≀ f2 β†’ convexFunctionClosure f1 ≀ convexFunctionClosure f2) ∧ (βˆ€ f : (Fin n β†’ Real) β†’ EReal, iInf (fun x => f x) = iInf (fun x => convexFunctionClosure f x)) := by refine ⟨?_, ?_, ?_⟩ Β· intro f exact convexFunctionClosure_le_self (f := f) Β· intro f1 f2 h12 exact convexFunctionClosure_mono (f1 := f1) (f2 := f2) h12 Β· intro f exact iInf_convexFunctionClosure_eq (f := f)

Points with positive coordinate appear frequently near the origin.

lemma frequently_pos_coord_nhds_zero : βˆƒαΆ  y in 𝓝 (0 : Fin 1 β†’ Real), 0 < y 0 := by have hclosure : (0 : Fin 1 β†’ Real) ∈ closure {y : Fin 1 β†’ Real | 0 < y 0} := by refine (mem_closure_iff_seq_limit).2 ?_ refine ⟨(fun n : β„• => fun _ : Fin 1 => (1 : Real) / ((n : Real) + 1)), ?_, ?_⟩ Β· intro n have hpos' : (0 : Real) < (n : Real) + 1 := by have hnonneg : (0 : Real) ≀ (n : Real) := by exact_mod_cast (Nat.zero_le n) linarith have hpos : 0 < (1 : Real) / ((n : Real) + 1) := (one_div_pos).2 hpos' simpa using hpos Β· refine (tendsto_pi_nhds).2 ?_ intro i fin_cases i simpa using (tendsto_one_div_add_atTop_nhds_zero_nat (π•œ := Real)) exact (mem_closure_iff_frequently).1 hclosure

At a point with positive coordinate, the liminf of the step function is 0 : β„•0.

lemma liminf_example_origin_pos {x : Fin 1 β†’ Real} (hx : 0 < x 0) : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 x) = (0 : EReal) := by have hopen : IsOpen {y : Fin 1 β†’ Real | 0 < y 0} := by simpa using (isOpen_lt (continuous_const) (continuous_apply 0)) have hmem : {y : Fin 1 β†’ Real | 0 < y 0} ∈ 𝓝 x := by exact hopen.mem_nhds hx have hEq : βˆ€αΆ  y in 𝓝 x, (if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) = (0 : EReal) := by refine Filter.mem_of_superset hmem ?_ intro y hy simp [hy] have hlim : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 x) = Filter.liminf (fun _ : Fin 1 β†’ Real => (0 : EReal)) (𝓝 x) := Filter.liminf_congr hEq simp [hlim]

At a point with negative coordinate, the liminf of the step function is ⊀ : ?m.1⊀.

lemma liminf_example_origin_neg {x : Fin 1 β†’ Real} (hx : x 0 < 0) : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 x) = (⊀ : EReal) := by have hopen : IsOpen {y : Fin 1 β†’ Real | y 0 < 0} := by simpa using (isOpen_lt (continuous_apply 0) (continuous_const)) have hmem : {y : Fin 1 β†’ Real | y 0 < 0} ∈ 𝓝 x := by exact hopen.mem_nhds hx have hEq : βˆ€αΆ  y in 𝓝 x, (if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) = (⊀ : EReal) := by refine Filter.mem_of_superset hmem ?_ intro y hy have hnot : Β¬ 0 < y 0 := by exact not_lt_of_gt hy change (if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) = (⊀ : EReal) simp [hnot] have hlim : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 x) = Filter.liminf (fun _ : Fin 1 β†’ Real => (⊀ : EReal)) (𝓝 x) := Filter.liminf_congr hEq simp [hlim]

At the origin, the liminf of the step function is 0 : β„•0.

lemma liminf_example_origin_zero : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 (0 : Fin 1 β†’ Real)) = (0 : EReal) := by have hle : (0 : EReal) ≀ Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 (0 : Fin 1 β†’ Real)) := by refine (Filter.le_liminf_of_le (f := 𝓝 (0 : Fin 1 β†’ Real)) (a := (0 : EReal)) (u := fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (h := ?_)) refine Filter.Eventually.of_forall ?_ intro y by_cases hy : 0 < y 0 <;> simp [hy] have hfreq_pos : βˆƒαΆ  y in 𝓝 (0 : Fin 1 β†’ Real), 0 < y 0 := frequently_pos_coord_nhds_zero have hfreq : βˆƒαΆ  y in 𝓝 (0 : Fin 1 β†’ Real), (if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) ≀ (0 : EReal) := by exact hfreq_pos.mono (fun y hy => by simp [hy]) have hge : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 (0 : Fin 1 β†’ Real)) ≀ (0 : EReal) := Filter.liminf_le_of_frequently_le (f := 𝓝 (0 : Fin 1 β†’ Real)) (u := fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (b := (0 : EReal)) hfreq exact le_antisymm hge hle

Text 7.0.13: If is defined by for Unknown identifier `x`sorry > 0 : Propx > 0 and for Unknown identifier `x`sorry ≀ 0 : Propx ≀ 0, then Unknown identifier `cl`cl f agrees with Unknown identifier `f`f except at the origin, where rather than .

theorem convexFunctionClosure_example_origin : convexFunctionClosure (fun x : Fin 1 β†’ Real => if 0 < x 0 then (0 : EReal) else (⊀ : EReal)) = fun x => if x 0 < 0 then (⊀ : EReal) else (0 : EReal) := by classical let f : (Fin 1 β†’ Real) β†’ EReal := fun x => if 0 < x 0 then (0 : EReal) else (⊀ : EReal) have hbot : βˆ€ x, f x β‰  (βŠ₯ : EReal) := by intro x by_cases hx : 0 < x 0 <;> simp [f, hx] have hliminf := (epigraph_convexFunctionClosure_eq_closure_epigraph (f := f) hbot).2 funext x by_cases hxneg : x 0 < 0 Β· have hlim : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 x) = (⊀ : EReal) := liminf_example_origin_neg (x := x) hxneg simp [f, hxneg, hliminf x, hlim] Β· by_cases hxpos : 0 < x 0 Β· have hlim : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 x) = (0 : EReal) := liminf_example_origin_pos (x := x) hxpos simp [f, hxneg, hliminf x, hlim] Β· have hxge : 0 ≀ x 0 := le_of_not_gt hxneg have hxle : x 0 ≀ 0 := le_of_not_gt hxpos have hxzero : x 0 = 0 := le_antisymm hxle hxge have hx : x = 0 := by ext i fin_cases i simp [hxzero] have hlim : Filter.liminf (fun y : Fin 1 β†’ Real => if 0 < y 0 then (0 : EReal) else (⊀ : EReal)) (𝓝 x) = (0 : EReal) := by simpa [hx] using liminf_example_origin_zero simp [f, hxneg, hliminf x, hlim]

Points in the closure of the unit ball are frequently in the unit ball.

lemma frequently_mem_ball_of_mem_closure {x : Fin 2 β†’ Real} (hx : x ∈ closure (Metric.ball (0 : Fin 2 β†’ Real) 1)) : βˆƒαΆ  y in 𝓝 x, y ∈ Metric.ball (0 : Fin 2 β†’ Real) 1 := by simpa using (mem_closure_iff_frequently.1 hx)

Points outside the closure of the unit ball have a neighborhood outside it.

lemma eventually_not_mem_closure_of_not_mem {x : Fin 2 β†’ Real} (hx : x βˆ‰ closure (Metric.ball (0 : Fin 2 β†’ Real) 1)) : βˆ€αΆ  y in 𝓝 x, y βˆ‰ closure (Metric.ball (0 : Fin 2 β†’ Real) 1) := by have hopen : IsOpen ((closure (Metric.ball (0 : Fin 2 β†’ Real) 1))ᢜ) := isClosed_closure.isOpen_compl have hxmem : x ∈ (closure (Metric.ball (0 : Fin 2 β†’ Real) 1))ᢜ := by simpa using hx have hmem : (closure (Metric.ball (0 : Fin 2 β†’ Real) 1))ᢜ ∈ 𝓝 x := hopen.mem_nhds hxmem refine Filter.mem_of_superset hmem ?_ intro y hy simpa using hy

On the closure of the unit ball, the liminf of Unknown identifier `f`f is 0 : β„•0.

lemma liminf_unitDisk_closure_eq_zero (f : (Fin 2 β†’ Real) β†’ EReal) (h0 : βˆ€ x, x ∈ Metric.ball (0 : Fin 2 β†’ Real) 1 β†’ f x = (0 : EReal)) (hnonneg : βˆ€ x, (0 : EReal) ≀ f x) {x : Fin 2 β†’ Real} (hx : x ∈ closure (Metric.ball (0 : Fin 2 β†’ Real) 1)) : Filter.liminf (fun y : Fin 2 β†’ Real => f y) (𝓝 x) = (0 : EReal) := by have hle : (0 : EReal) ≀ Filter.liminf (fun y : Fin 2 β†’ Real => f y) (𝓝 x) := by refine (Filter.le_liminf_of_le (f := 𝓝 x) (a := (0 : EReal)) (u := fun y : Fin 2 β†’ Real => f y) (h := ?_)) exact Filter.Eventually.of_forall (fun y => hnonneg y) have hfreq_mem : βˆƒαΆ  y in 𝓝 x, y ∈ Metric.ball (0 : Fin 2 β†’ Real) 1 := frequently_mem_ball_of_mem_closure (x := x) hx have hfreq : βˆƒαΆ  y in 𝓝 x, f y ≀ (0 : EReal) := by refine hfreq_mem.mono ?_ intro y hy have hfy : f y = (0 : EReal) := h0 y hy simp [hfy] have hge : Filter.liminf (fun y : Fin 2 β†’ Real => f y) (𝓝 x) ≀ (0 : EReal) := Filter.liminf_le_of_frequently_le (f := 𝓝 x) (u := fun y : Fin 2 β†’ Real => f y) (b := (0 : EReal)) hfreq exact le_antisymm hge hle

Outside the closure of the unit ball, the liminf of Unknown identifier `f`f is ⊀ : ?m.1⊀.

lemma liminf_unitDisk_outside_eq_top (f : (Fin 2 β†’ Real) β†’ EReal) (hInf : βˆ€ x, x βˆ‰ closure (Metric.ball (0 : Fin 2 β†’ Real) 1) β†’ f x = (⊀ : EReal)) {x : Fin 2 β†’ Real} (hx : x βˆ‰ closure (Metric.ball (0 : Fin 2 β†’ Real) 1)) : Filter.liminf (fun y : Fin 2 β†’ Real => f y) (𝓝 x) = (⊀ : EReal) := by have hEq : βˆ€αΆ  y in 𝓝 x, f y = (⊀ : EReal) := by have hmem : βˆ€αΆ  y in 𝓝 x, y βˆ‰ closure (Metric.ball (0 : Fin 2 β†’ Real) 1) := eventually_not_mem_closure_of_not_mem (x := x) hx refine hmem.mono ?_ intro y hy simp [hInf y hy] have hlim : Filter.liminf (fun y : Fin 2 β†’ Real => f y) (𝓝 x) = Filter.liminf (fun _ : Fin 2 β†’ Real => (⊀ : EReal)) (𝓝 x) := Filter.liminf_congr hEq simp [hlim]

Text 7.0.14: If Unknown identifier `C`C is the unit disk in failed to synthesize HPow Type β„• Type Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.ℝ ^ 2 : Typeℝ^2 and for Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `C`C while for Unknown identifier `x`sorry βˆ‰ sorry : Propx βˆ‰ Unknown identifier `C`C (with arbitrary boundary values), then for all Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `cl`cl C and elsewhere.

theorem convexFunctionClosure_example_unitDisk (f : (Fin 2 β†’ Real) β†’ EReal) (h0 : βˆ€ x, x ∈ Metric.ball (0 : Fin 2 β†’ Real) 1 β†’ f x = (0 : EReal)) (hInf : βˆ€ x, x βˆ‰ closure (Metric.ball (0 : Fin 2 β†’ Real) 1) β†’ f x = (⊀ : EReal)) (hnonneg : βˆ€ x, (0 : EReal) ≀ f x) : (βˆ€ x, x ∈ closure (Metric.ball (0 : Fin 2 β†’ Real) 1) β†’ convexFunctionClosure f x = (0 : EReal)) ∧ (βˆ€ x, x βˆ‰ closure (Metric.ball (0 : Fin 2 β†’ Real) 1) β†’ convexFunctionClosure f x = (⊀ : EReal)) := by classical have hbot : βˆ€ x, f x β‰  (βŠ₯ : EReal) := by intro x hx have hle : (0 : EReal) ≀ (βŠ₯ : EReal) := by simpa [hx] using hnonneg x have hzero : (0 : EReal) = (βŠ₯ : EReal) := (le_bot_iff).1 hle exact (EReal.zero_ne_bot hzero) have hliminf := (epigraph_convexFunctionClosure_eq_closure_epigraph (f := f) hbot).2 refine ⟨?_, ?_⟩ Β· intro x hx have hlim : Filter.liminf (fun y : Fin 2 β†’ Real => f y) (𝓝 x) = (0 : EReal) := liminf_unitDisk_closure_eq_zero (f := f) h0 hnonneg (x := x) hx simp [hliminf x, hlim] Β· intro x hx have hlim : Filter.liminf (fun y : Fin 2 β†’ Real => f y) (𝓝 x) = (⊀ : EReal) := liminf_unitDisk_outside_eq_top (f := f) hInf (x := x) hx simp [hliminf x, hlim]
end Section07end Chap02