4. Indistinguishable function🔗

Given a Lipschitz function f on a compact (pseudo)metric space \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{d(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} [PseudoMetricSpace α]
  [CompactSpace α] [Nonempty α] {f : α → ℝ} (hf : Lipschitz f) (c : α)
  (ε : ℝ) (x : α) : ℝ
Lipschitz.f_tilde.{u_1} {α : Type u_1}
  [PseudoMetricSpace α] [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. Writing \tilde{f} = f + g on B(c, \varepsilon / 2) and \tilde{f} = f elsewhere, the Lipschitz function g is nonnegative inside the ball and nonpositive outside of it. Hence \tilde{f} = f + \max(g, 0), which is Lipschitz as a sum of Lipschitz functions (see LipschitzWith.if). This argument only uses the metric structure of \alpha: no vector space structure is required.

lemma f_tilde_lipschitz {ε : ℝ} (ε_pos : 0 < ε) : Lipschitz (hf.f_tilde c ε) := byα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < ε⊢ Lipschitz (hf.f_tilde c ε)
  have hK : 0 ≤ fmax hf - fmin hf + 1 := by
    have : 0 ≤ fmax hf - fmin hf := compact_argmax_sub_argmin_pos hf.continuousα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εthis:0 ≤ fmax hf - fmin hf⊢ 0 ≤ fmax hf - fmin hf + 1
    linarithα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1⊢ Lipschitz (hf.f_tilde c ε)
  refine hf.if ?_ ?_ ?_refine_1α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1⊢ ∀ a ∈ ball c (ε / 2), 0 ≤ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1))refine_2α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1⊢ ∀ a ∉ ball c (ε / 2), 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) ≤ 0refine_3α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1⊢ Lipschitz fun a => 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1))
  ·refine_1α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1⊢ ∀ a ∈ ball c (ε / 2), 0 ≤ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) intro a harefine_1α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1a:αha:a ∈ ball c (ε / 2)⊢ 0 ≤ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1))
    have : dist a c / (ε / 2) < 1 := (div_lt_one (half_pos ε_pos)).mpr (mem_ball.mp ha)refine_1α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1a:αha:a ∈ ball c (ε / 2)this:dist a c / (ε / 2) < 1⊢ 0 ≤ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1))
    have : 0 ≤ (1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1) := mul_nonneg (byα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1a:αha:a ∈ ball c (ε / 2)this:dist a c / (ε / 2) < 1⊢ 0 ≤ 1 - dist a c / (ε / 2) linarithAll goals completed! 🐙) hKrefine_1α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1a:αha:a ∈ ball c (ε / 2)this✝:dist a c / (ε / 2) < 1this:0 ≤ (1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)⊢ 0 ≤ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1))
    linarithAll goals completed! 🐙
  ·refine_2α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1⊢ ∀ a ∉ ball c (ε / 2), 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) ≤ 0 intro a harefine_2α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1a:αha:a ∉ ball c (ε / 2)⊢ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) ≤ 0
    have : 1 ≤ dist a c / (ε / 2) :=
      (one_le_div (half_pos ε_pos)).mpr (not_lt.mp (mt mem_ball.mpr ha))refine_2α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1a:αha:a ∉ ball c (ε / 2)this:1 ≤ dist a c / (ε / 2)⊢ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) ≤ 0
    have : (1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1) ≤ 0 :=
      mul_nonpos_of_nonpos_of_nonneg (byα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1a:αha:a ∉ ball c (ε / 2)this:1 ≤ dist a c / (ε / 2)⊢ 1 - dist a c / (ε / 2) ≤ 0 linarithAll goals completed! 🐙) hKrefine_2α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1a:αha:a ∉ ball c (ε / 2)this✝:1 ≤ dist a c / (ε / 2)this:(1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1) ≤ 0⊢ 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) ≤ 0
    linarithAll goals completed! 🐙
  ·refine_3α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1⊢ Lipschitz fun a => 2 * ((1 - dist a c / (ε / 2)) * (fmax hf - fmin hf + 1)) refine const_mul <| mul_const <| sub lipschitz_const ?_refine_3α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εhK:0 ≤ fmax hf - fmin hf + 1⊢ Lipschitz fun a => dist a c / (ε / 2)
    exact div_const (dist_left c)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) := byα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < ε⊢ compact_argmax ⋯ ∈ ball c (ε / 2)
  set x' := compact_argmax (hf.f_tilde_lipschitz c ε_pos).continuousα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εx':α := compact_argmax ⋯⊢ x' ∈ ball c (ε / 2)
  by_contra h_contraα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εx':α := compact_argmax ⋯h_contra:x' ∉ ball c (ε / 2)⊢ False
  have : fmax (hf.f_tilde_lipschitz c ε_pos) ≤ fmax hf := byα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < ε⊢ compact_argmax ⋯ ∈ ball c (ε / 2)
    simp only [fmax, hf.f_tilde_apply_out c h_contra, x']α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εx':α := compact_argmax ⋯h_contra:x' ∉ ball c (ε / 2)⊢ f (compact_argmax ⋯) ≤ f (compact_argmax ⋯)
    exact compact_argmax_apply hf.continuous x'α:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εx':α := compact_argmax ⋯h_contra:x' ∉ ball c (ε / 2)this:fmax ⋯ ≤ fmax hf⊢ False
  have := hf.max_f_lt_max_f_tilde c ε_posα:Type u_1inst✝²:PseudoMetricSpace αinst✝¹:CompactSpace αinst✝:Nonempty αf:α → ℝhf:Lipschitz fc:αε:ℝε_pos:0 < εx':α := compact_argmax ⋯h_contra:x' ∉ ball c (ε / 2)this✝:fmax ⋯ ≤ fmax hfthis:fmax hf < fmax ⋯⊢ False
  linarithAll goals completed! 🐙

4. Indistinguishable function🔗

4.1. Expression🔗

4.2. Lipschitz property🔗

4.3. Maximum of \tilde{f}🔗

4.3. Maximum of `\tilde{f}`🔗