Documentation

Convex.Function.Proximal

proximal operator

def prox_prop {E : Type u_1} [NormedAddCommGroup E] (f : E → ℝ) (x : E) (xm : E) :

Equations

prox_prop f x xm = IsMinOn (fun (u : E) => f u + ‖u - x‖ ^ 2 / 2) Set.univ xm

Instances For

def prox_set {E : Type u_1} [NormedAddCommGroup E] (f : E → ℝ) (x : E) :

Equations

prox_set f x = {u : E | prox_prop f x u}

Instances For

def prox_point {E : Type u_1} [NormedAddCommGroup E] (f : E → ℝ) (x : E) (h : ∃ (y : E), prox_set f x y) :

E

Equations

prox_point f x h = Classical.choose h

Instances For

theorem strongconvex_of_convex_add_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x : E) (hfun : ConvexOn ℝ Set.univ f) :

StrongConvexOn Set.univ 1 fun (u : E) => f u + ‖u - x‖ ^ 2 / 2

theorem bounded_lowersemicontinuous_to_epi_closed {E : Type u_1} [NormedAddCommGroup E] (f : E → ℝ) (hc : LowerSemicontinuousOn f Set.univ) (underboundf : ∃ (b : ℝ), ∀ (x : E), b ≤ f x) :

IsClosed {p : E × ℝ | f p.1 ≤ p.2}

theorem prox_set_compact_of_lowersemi {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] (f : E → ℝ) (hc : LowerSemicontinuous f) (lbdf : BddBelow (f '' Set.univ)) (x : E) :

Nonempty ↑(prox_set f x) ∧ IsCompact (prox_set f x)

theorem prox_set_compact_of_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] (f : E → ℝ) (hc : ContinuousOn f Set.univ) (hconv : ConvexOn ℝ Set.univ f) (x : E) :

Nonempty ↑(prox_set f x) ∧ IsCompact (prox_set f x)

theorem prox_well_define {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] (f : E → ℝ) (hc : LowerSemicontinuous f) (lbdf : BddBelow (f '' Set.univ)) (x : E) :

∃ (y : E), prox_prop f x y

theorem prox_well_define_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] (f : E → ℝ) (hc : ContinuousOn f Set.univ) (hconv : ConvexOn ℝ Set.univ f) (x : E) :

∃ (y : E), prox_prop f x y

theorem prox_unique_of_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {y₁ : E} {y₂ : E} (f : E → ℝ) (x : E) (hfun : ConvexOn ℝ Set.univ f) (h₁ : prox_prop f x y₁) (h₂ : prox_prop f x y₂) :

y₁ = y₂

def prox_point_c {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] (f : E → ℝ) (x : E) (hc : LowerSemicontinuous f) (lbdf : BddBelow (f '' Set.univ)) :

E

Equations

prox_point_c f x hc lbdf = let_fun h := ⋯; Classical.choose h

Instances For

def prox_point_c' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [ProperSpace E] (f : E → ℝ) (x : E) (hc : ContinuousOn f Set.univ) (hconv : ConvexOn ℝ Set.univ f) :

E

Equations

prox_point_c' f x hc hconv = let_fun h := ⋯; Classical.choose h

Instances For

theorem convex_of_norm_sq {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} (x : E) (conv : Convex ℝ s) :

ConvexOn ℝ s fun (u : E) => ‖u - x‖ ^ 2 / 2

theorem Subderivat_eq_SubderivWithinAt_univ {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E} (f : E → ℝ) :

SubderivWithinAt f Set.univ u = SubderivAt f u

theorem prox_iff_subderiv {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} (f : E → ℝ) (hfun : ConvexOn ℝ Set.univ f) (u : E) :

prox_prop f x u ↔ x - u ∈ SubderivAt f u

theorem prox_iff_grad {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} (f : E → ℝ) {f' : E → E} (hfun : ConvexOn ℝ Set.univ f) (hdiff : ∀ (x : E), HasGradientAt f (f' x) x) (u : E) :

prox_prop f x u ↔ f' u = x - u

theorem prox_iff_grad_smul {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} (f : E → ℝ) {f' : E → E} (t : ℝ) (hfun : ConvexOn ℝ Set.univ f) (hdiff : ∀ (x : E), HasGradientAt f (f' x) x) (tnonneg : 0 ≤ t) (u : E) :

prox_prop (t • f) x u ↔ t • f' u = x - u

theorem prox_iff_subderiv_smul {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {x : E} (f : E → ℝ) {t : ℝ} (hfun : ConvexOn ℝ Set.univ f) (ht : 0 < t) (u : E) :

prox_prop (t • f) x u ↔ (1 / t) • (x - u) ∈ SubderivAt f u

theorem proximal_shift {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} (a : E) {t : ℝ} (tnz : t ≠ 0) (f : E → ℝ) (z : E) :

prox_prop (fun (x : E) => f (t • x + a)) x z ↔ prox_prop (t ^ 2 • f) (t • x + a) (t • z + a)

theorem proximal_scale {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} {t : ℝ} (tpos : 0 < t) (f : E → ℝ) (z : E) :

prox_prop (fun (x : E) => t • f (t⁻¹ • x)) x z ↔ prox_prop (t⁻¹ • f) (t⁻¹ • x) (t⁻¹ • z)

theorem proximal_add_linear {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} (a : E) (f : E → ℝ) (z : E) :

prox_prop (fun (x : E) => f x + ⟪a, x⟫_ℝ) x z ↔ prox_prop f (x - a) z

theorem proximal_add_sq {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} (a : E) {l : ℝ} (lpos : 0 < l) (f : E → ℝ) (z : E) :

prox_prop (fun (x : E) => f x + l / 2 * ‖x - a‖ ^ 2) x z ↔ prox_prop ((1 / (l + 1)) • f) ((1 / (l + 1)) • (x + l • a)) z