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.

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 ε) := byα:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ Lipschitz (hf.f_tilde c ε)
  refine hf.if ?_ ?_refine_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)) = 0refine_2α: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))
  ·refine_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 intro a harefine_1α: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
    rw [ha]refine_1α: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
    suffices h : ε / 2 / (ε / 2) = 1 byα:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εa:αha:a ∈ sphere c (ε / 2)h:_fvar.9558 / 2 / (_fvar.9558 / 2) = 1 := ?_mvar.9860⊢ 2 * ((1 - ε / 2 / (ε / 2)) * (fmax hf - fmin hf + 1)) = 0
      rw [h]α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εa:αha:a ∈ sphere c (ε / 2)h:_fvar.9558 / 2 / (_fvar.9558 / 2) = 1 := ?_mvar.9860⊢ 2 * ((1 - 1) * (fmax hf - fmin hf + 1)) = 0
      ringAll goals completed! 🐙
    exact CommGroupWithZero.mul_inv_cancel _ ((ne_of_lt (half_pos ε_pos)).symm)All goals completed! 🐙
  ·refine_2α: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)) refine const_mul <| mul_const <| sub lipschitz_const ?_refine_2α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ 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✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ compact_argmax ⋯ ∈ ball c (ε / 2)
  set x' := compact_argmax (hf.f_tilde_lipschitz c ε_pos).continuousα:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εx':_fvar.11939 := 
  @compact_argmax _fvar.11939 ℝ PseudoEMetricSpace.toUniformSpace.toTopologicalSpace _fvar.12042 _fvar.12039
    PseudoEMetricSpace.toUniformSpace.toTopologicalSpace Real.linearOrder
    (Lipschitz.f_tilde _fvar.12187 _fvar.12189 _fvar.13306) ⋯ ⋯⊢ x' ∈ ball c (ε / 2)
  by_contra h_contraα:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εx':_fvar.11939 := 
  @compact_argmax _fvar.11939 ℝ PseudoEMetricSpace.toUniformSpace.toTopologicalSpace _fvar.12042 _fvar.12039
    PseudoEMetricSpace.toUniformSpace.toTopologicalSpace Real.linearOrder
    (Lipschitz.f_tilde _fvar.12187 _fvar.12189 _fvar.13306) ⋯ ⋯h_contra:x' ∉ ball c (ε / 2)⊢ False
  have : fmax (hf.f_tilde_lipschitz c ε_pos) ≤ fmax hf := byα:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < ε⊢ compact_argmax ⋯ ∈ ball c (ε / 2)
    simp only [fmax, hf.f_tilde_apply_out c h_contra, x']α:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εx':_fvar.11939 := 
  @compact_argmax _fvar.11939 ℝ PseudoEMetricSpace.toUniformSpace.toTopologicalSpace _fvar.12042 _fvar.12039
    PseudoEMetricSpace.toUniformSpace.toTopologicalSpace Real.linearOrder
    (Lipschitz.f_tilde _fvar.12187 _fvar.12189 _fvar.13306) ⋯ ⋯h_contra:x' ∉ ball c (ε / 2)⊢ f (compact_argmax ⋯) ≤ f (compact_argmax ⋯)
    exact compact_argmax_apply hf.continuous x'All goals completed! 🐙
  have := hf.max_f_lt_max_f_tilde c ε_posα:Type u_1inst✝³:NormedAddCommGroup αinst✝²:CompactSpace αinst✝¹:Nonempty αf:α → ℝhf:Lipschitz fc:αinst✝:NormedSpace ℝ αε:ℝε_pos:0 < εx':_fvar.11939 := 
  @compact_argmax _fvar.11939 ℝ PseudoEMetricSpace.toUniformSpace.toTopologicalSpace _fvar.12042 _fvar.12039
    PseudoEMetricSpace.toUniformSpace.toTopologicalSpace Real.linearOrder
    (Lipschitz.f_tilde _fvar.12187 _fvar.12189 _fvar.13306) ⋯ ⋯h_contra:x' ∉ ball c (ε / 2)this✝:fmax ⋯ ≤ fmax _fvar.12187 := ?_mvar.14432this:?_mvar.14998 := Lipschitz.max_f_lt_max_f_tilde _fvar.12187 _fvar.12189 _fvar.13307⊢ 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}`