Consistency of global optimization algorithms

4. Indistinguishable function🔗

Given a Lipschitz function f on a compact domain \alpha, a positive real number \varepsilon, and an element of \alpha c, we construct a new Lipschitz function \tilde{f} such that f = \tilde{f} outside of the ball centered at c with radius \varepsilon/2, and such that the maximum value of \tilde{f} is inside this ball and is strictly greater than the maximum value of f.

4.1. Expression🔗

We define the function \tilde{f} as follows: \tilde{f}(x) \triangleq \begin{cases} f (x) + 2 \cdot \left(1 - \frac{\|x - c\|}{\varepsilon / 2} \right) \cdot (\max_{x \in \alpha} f(x) - \min_{x \in \alpha} f(x) + 1) & \text{if } x \in B(c, \varepsilon / 2) \\ f (x) & \text{otherwise} \end{cases}

Here is a visualization of this expression using the reverse Ackley function.

🔗def
Lipschitz.f_tilde.{u_1} {α : Type u_1} [NormedAddCommGroup α]
  [CompactSpace α] [Nonempty α] {f : α → ℝ} (hf : Lipschitz f) (c : α)
  (ε : ℝ) (x : α) : ℝ
Lipschitz.f_tilde.{u_1} {α : Type u_1}
  [NormedAddCommGroup α] [CompactSpace α]
  [Nonempty α] {f : α → ℝ}
  (hf : Lipschitz f) (c : α) (ε : ℝ)
  (x : α) : ℝ

Given a Lipschitz function f over a CompactSpace α, construct a Lipschitz function (see Lipschitz.f_tilde_lipschitz) that is indistinguishable from f outside of a ball of radius ε such that the maximum of this new function is greater than the maximum of f and is located in the ball.

noncomputable def f_tilde (ε : ℝ) (x : α) := if x ∈ ball c (ε/2) then f x + 2 * ((1 - (dist x c) / (ε/2)) * (fmax hf - fmin hf + 1)) else f x

4.2. Lipschitz property🔗

We show that \tilde{f} is Lipschitz continuous. The proof relies on the fact that \tilde{f} is a cases function of two Lipschitz functions that are equal on the frontier of the ball B(c, \varepsilon / 2).

lemma f_tilde_lipschitz {ε : ℝ} (ε_pos : 0 < ε) : Lipschitz (hf.f_tilde c ε) := α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ Lipschitz (hf.f_tilde c ε) α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ ∀ a ∈ sphere c (ε / 2), 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) = 0α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ Lipschitz fun a => 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ ∀ a ∈ sphere c (ε / 2), 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) = 0 α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εa:αha:a ∈ sphere c (ε / 2)⊢ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) = 0 α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εa:αha:a ∈ sphere c (ε / 2)⊢ 2 * ((1 - ε / 2 / (ε / 2)) * (fmax hf - fmin hf + 1)) = 0 α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εa:αha:a ∈ sphere c (ε / 2)⊢ ε / 2 / (ε / 2) = 1 All goals completed! 🐙 α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ Lipschitz fun a => 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ Lipschitz fun a => dist a c / (ε / 2) All goals completed! 🐙

4.3. Maximum of \tilde{f}🔗

One can show that \tilde{f}(c) is strictly greater than the maximum of f (see max_f_lt_f_tilde_c). Hence, by transitivity, the maximum of \tilde{f} is strictly greater than the maximum of f.

lemma max_f_lt_max_f_tilde {ε : ℝ} (ε_pos : 0 < ε) : fmax hf < fmax (hf.f_tilde_lipschitz c ε_pos) := suffices h : fmax hf < hf.f_tilde c ε c from lt_of_le_of_lt' (compact_argmax_apply (hf.f_tilde_lipschitz c ε_pos).continuous c) h hf.max_f_lt_f_tilde_c c ε_pos

Finally, we show that the maximum of \tilde{f} is attained in the ball B(c, \varepsilon / 2).

lemma max_f_tilde_in_ball {ε : ℝ} (ε_pos : 0 < ε) : compact_argmax (hf.f_tilde_lipschitz c ε_pos).continuous ∈ ball c (ε/2) := α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ compact_argmax ⋯ ∈ ball c (ε / 2) α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εx':α := compact_argmax ⋯⊢ x' ∈ ball c (ε / 2) α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εx':α := compact_argmax ⋯h_contra:x' ∉ ball c (ε / 2)⊢ False α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εx':α := compact_argmax ⋯h_contra:x' ∉ ball c (ε / 2)this:fmax ⋯ ≤ fmax hf⊢ False α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εx':α := compact_argmax ⋯h_contra:x' ∉ ball c (ε / 2)this✝:fmax ⋯ ≤ fmax hfthis:fmax hf < fmax ⋯⊢ False All goals completed! 🐙