existence theorem

Stream: new members

[tsuki hao]

open EReal Function Topology Filter Set TopologicalSpace


variable {𝕜 E F α β ι : Type _}


variable [TopologicalSpace 𝕜] [LinearOrderedRing 𝕜] [DenselyOrdered 𝕜]

variable [AddCommMonoid E] [TopologicalSpace E] [SequentialSpace E] [FirstCountableTopology E]
variable [TopologicalSpace EReal] [SequentialSpace EReal] [DenselyOrdered EReal] [OrderTopology EReal]
variable [SequentialSpace <| E × EReal]


variable [OrderedAddCommMonoid α] [LinearOrderedAddCommMonoid β]


variable (𝕜) [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 EReal] (s : Closeds E) (f : E → EReal) {g : EReal → α}

variable (b) [SMul b E] [SMul b α] [SMul b EReal] (s : Set E) (f : E → EReal) {g : EReal → α}
/-properfun-/
noncomputable section

def exist_fun_lt_top  : Prop :=
  ∃ x ∈ s, f x < ⊤

def forall_fun_gt_top : Prop :=
  ∀ x ∈ s, f x > ⊥

def properfun : Prop :=
  exist_fun_lt_top s f ∧ forall_fun_gt_top s f

def isSup (s : Set ℝ ) (x : ℝ) : Prop :=
  upperBounds s x ∧ ∀ y, upperBounds s y → x ≤ y

/-closedfun-/
def dom : Set E :=
  {x | f x < ⊤} ∩ s

def level_set (r : EReal) : Set E :=
  { x ∈ s | f x ≤ r }

def epigraph : Set <| E × EReal :=
  {p : E × EReal | p.1 ∈ s ∧ f p.1 ≤ p.2}
-- {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}

def closedfun : Prop :=
  IsClosed <| epigraph s f

def strong_quasi : Prop :=
  Convex 𝕜 s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
    → f (a • x + b • y) < max (f x) (f y)

variable (s : Set E) (hs : s.Nonempty ∧ Convex 𝕜 s ∧ IsCompact s)  --s非空 紧 凸
variable (f : E → EReal) (hf : properfun s f ∧ closedfun s f ∧ strong_quasi 𝕜 s f) -- f适当 闭 需要加上强拟凸
#check properfun
#check closedfun
#check strong_quasi

theorem uniqueness : ∃! x', ∀ x ∈ s \ {x'}, f x' < f x := by
  constructor
  · simp
    sorry
  · simp
    sorry

Does anyone know what should I code next?

[tsuki hao]

picture.png
Does anyone know how I can introduce the ?w in the proposition

[Richard Copley]

You can say show x = 42 (where x = ?w is the thing you have there that I am not going to try to type). This will unify x = 42 with x = ?w, which will make ?w be 42.

[Notification Bot]

tsuki hao has marked this topic as resolved.

[Notification Bot]

tsuki hao has marked this topic as unresolved.

[Zhang Ruichong]

tsuki hao did not explain what they were doing. They were trying to prove a theorem in convex analysis:
A proper, closed, strong quasi-convex function f on some compact convex set s admits a unique minimum point on s.

They didn't resolve the imports either, here are the imports:

import Mathlib.Tactic
import Mathlib.Topology.Basic
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Analysis.Convex.Basic
import Mathlib.Analysis.Convex.Function
import Mathlib.Analysis.Convex.Integral
import Mathlib.Analysis.Convex.Quasiconvex

This theorem is not easy to prove, here are some supplementary materials (only in Chinese):
image.png

image.png

image.png

[tsuki hao]

In fact, what I want to prove is that for a non-empty, compact and convex subset, if f is an appropriate, closed and strongly quasi-convex function, then there is and only one and only a minimum value point. In the above code Existence and uniqueness were written together, but I have now separated them and proved them separately, this part of the code is shown below, maybe someone can help me prove existence? As far as I know this requires the use of Weierstrass theorem.

[tsuki hao]

import Mathlib.Analysis.Convex.Basic
import Mathlib.Data.Real.EReal
import Mathlib.Tactic
import Mathlib.Order.Bounds.Basic
import Mathlib.Analysis.NormedSpace.PiLp
import Mathlib.LinearAlgebra.FiniteDimensional
import Mathlib.LinearAlgebra.UnitaryGroup
import Mathlib.Analysis.InnerProductSpace.Projection
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Data.Real.Basic
import Mathlib.Topology.SubsetProperties
import Mathlib.Topology.Sets.Closeds
import Mathlib.Topology.Bases
import Mathlib.Topology.Basic
import Mathlib.Order.Bounds.Basic

open EReal Function Topology Filter Set TopologicalSpace


variable {𝕜 E F α β ι : Type _}


variable [TopologicalSpace 𝕜] [LinearOrderedRing 𝕜] [DenselyOrdered 𝕜]

variable [AddCommMonoid E] [TopologicalSpace E] [SequentialSpace E] [FirstCountableTopology E]
variable [TopologicalSpace EReal] [SequentialSpace EReal] [DenselyOrdered EReal] [OrderTopology EReal]
variable [SequentialSpace <| E × EReal] -- 不加这个会在使用sequence的时候报错


variable [OrderedAddCommMonoid α] [LinearOrderedAddCommMonoid β]


variable (𝕜) [SMul 𝕜 E] [SMul 𝕜 α] [SMul 𝕜 EReal] (s : Closeds E) (f : E → EReal) {g : EReal → α}

variable (b) [SMul b E] [SMul b α] [SMul b EReal] (s : Set E) (f : E → EReal) {g : EReal → α}
/-properfun-/
noncomputable section

def exist_fun_lt_top  : Prop :=
  ∃ x ∈ s, f x < ⊤

def forall_fun_gt_top : Prop :=
  ∀ x ∈ s, f x > ⊥

def properfun : Prop :=
  exist_fun_lt_top s f ∧ forall_fun_gt_top s f

def isSup (s : Set ℝ ) (x : ℝ) : Prop :=
  upperBounds s x ∧ ∀ y, upperBounds s y → x ≤ y

/-closedfun-/
/- 定义域-/
def dom : Set E :=
  {x | f x < ⊤} ∩ s

/- 下水平集 -/
def level_set (r : EReal) : Set E :=
  { x ∈ s | f x ≤ r }

/- 上方图 -/
def epigraph : Set <| E × EReal :=
  {p : E × EReal | p.1 ∈ s ∧ f p.1 ≤ p.2}
-- {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2}

/- 闭函数 -/
def closedfun : Prop :=
  IsClosed <| epigraph s f

/-强拟凸函数-/
def strong_quasi : Prop :=
  Convex 𝕜 s ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
    → f (a • x + b • y) < max (f x) (f y)

/-唯一性定理-/
variable (s : Set E) (hs : s.Nonempty ∧ Convex 𝕜 s ∧ IsCompact s)  --s非空 紧 凸
variable (f : E → EReal) (hf : properfun s f ∧ closedfun s f ∧ strong_quasi 𝕜 s f) -- f适当 闭 需要加上强拟凸
#check properfun
#check closedfun
#check strong_quasi

-- theorem uniqueness : ∃! x', ∀ x ∈ s \ {x'}, f x' < f x := by
--   constructor
--   · simp    --唯一性
--     use
--     constructor
--     rcases hs with ⟨h1, h2, h3⟩
--     rcases hf with ⟨h4, h5, h6⟩
--     · simp

--   · simp

-- theorem ExistsUnique.intro2 {p : α → Prop} (w : α)
--   (h₁ : p w) (h₂ : ∀ y, p y → y = w) : ∃! x, p x := by
--   --⟨w, h₁, h₂⟩
--   use w

-- variable [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
-- variable (pf : properfun s f) (cf : closedfun s f)
-- theorem aux1 (h : BddAbove s ∧ BddBelow s) : {x ∈ s | ∀ y ∈ s, f x ≤ f y} := by
--   sorry

theorem existence
 {s : Set E} (hs : s.Nonempty ∧ Convex 𝕜 s ∧ IsCompact s)
 {f : E → EReal} (hf : properfun s f ∧ closedfun s f ∧ strong_quasi 𝕜 s f)
 : ∃ x', ∀ x ∈ s \ {x'}, f x' < f x := by sorry

theorem uniqueness {s : Set E} (hs : s.Nonempty ∧ Convex 𝕜 s ∧ IsCompact s)
  {f : E → EReal} (hf : properfun s f ∧ closedfun s f ∧ strong_quasi 𝕜 s f)
  (h0 : x' ∈ s)
  (h_0 : y' ∈ s)
  (h1 : ∀ x ∈ s \ {x'}, f x' < f x)
  (h2 : ∀ x ∈ s \ {y'}, f y' < f x)
  : x' = y' := by
  by_cases h: x' = y'
  · exact h
  · push_neg at h
    have l1 : f x' < f y' := by
      have c1 : y' ∈ s \ {x'} := by
        constructor
        · apply h_0
        · by_contra h3
          have c2 : x' = y' := by
            exact False.elim (id (Ne.symm h) h3)
          apply h
          apply c2
      apply h1
      apply c1
    have l2 : f y' < f x' := by
      have c3 : x' ∈ s \ {y'} := by
        constructor
        · apply h0
        · by_contra h4
          have c4 : x' = y' := by
            exact h4
          apply h
          apply c4
      apply h2
      apply c3
    by_contra h'
    push_neg at h'
    have l3 : f x' < f x' := by
      apply lt_trans l1 l2
    have l4 : f x' ≠ f x' := by
      apply ne_of_lt l3
    exact l4 rfl
    ```

[Anatole Dedecker]

tsuki hao said:

picture.png
Does anyone know how I can introduce the ?w in the proposition

Let me just mention that if you have sorryAx in your goal then there's something very wrong somewhere. You should always try to fix the red squiggles before going on with your proof!

[Anatole Dedecker]

Is this intended for Mathlib contribution or as an exercise? If it's for mathlib contribution, the right way to prove the existence is to use the fact that, since the epigraph is closed, your functions is lower semicontinuous, hence it has a minimum on any compact subset. We don't have that result yet but I've been slowly working towards it, so if you need it for contributing let me know so I bump it up of my priority list. But of course it's also a good exercise to do things by hand with sequences if you don't care about generality!

[tsuki hao]

Anatole Dedecker said:

Is this intended for Mathlib contribution or as an exercise? If it's for mathlib contribution, the right way to prove the existence is to use the fact that, since the epigraph is closed, your functions is lower semicontinuous, hence it has a minimum on any compact subset. We don't have that result yet but I've been slowly working towards it, so if you need it for contributing let me know so I bump it up of my priority list. But of course it's also a good exercise to do things by hand with sequences if you don't care about generality!

Is this intended for Mathlib contribution.I want to prove it using the generalized Weierstrass theorem, that is, for an appropriate and closed function, if the domain of definition of fx<+\infty is bounded, then the minimum point is non-empty (my English is not very good and I am not sure if The statement is completely correct, if you can understand Chinese, you can refer to the ppt above.

[Yaël Dillies]

Btw do you know about docs#QuasiConvexOn ?