getting epsilon neighbourhood from general neighbourhood

Stream: new members

[Abu Al Hassan]

Hello, I would like some help with the following. I have that the function f has a local minimum at x_star for some neighbourhood in u. I think is_local_min_on defines the neighbourhood as some general concept of the neighbourhood but because E in my case is a normed_space, I believe I should be able to get an epsilon neighbourhood.

Here is the MWE, I am working in the have statement.

import tactic
import data.real.basic
import analysis.calculus.cont_diff
import topology.local_extr
import topology.basic

variables (E : Type*) [normed_add_comm_group E] [normed_space ℝ E]

theorem necess_2nd_order_optimality_condit
    {n : ℕ} {u : set E} (h_open : is_open u)
    {x_star : E} (h_x_star : x_star ∈ u)
    {f : E → ℝ}:
    is_local_min_on f u x_star → x_star ≠ x_star :=
begin
  assume h_local_min,
  rcases h_local_min with ⟨v, hv_open, hv_subset, hx_min⟩,
  have : ∃ ε : ℝ, ε > 0 ∧ (metric.ball x_star ε ⊆ u) ∧ (metric.ball x_star ε ⊆ v),
  {

    sorry,
    },
  sorry,
end

Here is the infoview of have statement.

E: Type u_1
_inst_1: normed_add_comm_group E
_inst_2: normed_space ℝ E
n: ℕ
u: set E
h_open: is_open u
x_star: E
h_x_star: x_star ∈ u
f: E → ℝ
v: set E
hv_open: v ∈ nhds x_star
hv_subset: set E
hx_min: ∃ (H : hv_subset ∈ filter.principal u), {x : E | (λ (x : E), f x_star ≤ f x) x} = v ∩ hv_subset
⊢ ∃ (ε : ℝ), ε > 0 ∧ metric.ball x_star ε ⊆ u ∧ metric.ball x_star ε ⊆ v

[Abu Al Hassan]

I have a feeling that this problem is much more complex than I think. So any hints will be appreciated.

[Eric Wieser]

Your theorem looks false to me, did you really intend to write x_star ≠ x_star?

[Abu Al Hassan]

Yh i just did that for the sake of the MWE.

[Abu Al Hassan]

Sorry, if thats not good practice I can change it. it was kind of just a placeholder. I am just interested in the have the statement

[Kevin Buzzard]

My instinct is that it's a multistep process: first prove u is in nhds x_star, then deduce that u \inter v is in nhds x_star, then find the lemma in the library that says that for neighbourhoods of a point in a metric space there's an epsilon, and apply that to u \inter v and this epsilon will work.

[Kevin Buzzard]

You should learn how to break down a complex goal into simpler steps.