-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathMinimaClosedFunction.lean
142 lines (116 loc) · 5.34 KB
/
MinimaClosedFunction.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
/-
Copyright (c) 2023 Wanyi He. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wanyi He
-/
import Mathlib.Analysis.Convex.Basic
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Topology.MetricSpace.Bounded
import Mathlib.Topology.Semicontinuous
import Mathlib.Topology.Sequences
/-!
the Weierstrass theorem
-/
open Set Bornology Topology Filter TopologicalSpace
variable {E F : Type*}
variable [AddCommMonoid E]
variable [CompleteLinearOrder F] [DenselyOrdered F]
variable {f : E → F}
variable [TopologicalSpace E] [TopologicalSpace F] [OrderTopology F]
variable [FirstCountableTopology E] [FirstCountableTopology F]
/-! ### Generalized Weierstrass theorem -/
section
/- Suppose `f` is LowerSemicontinuous -/
variable (hf : LowerSemicontinuous f)
private lemma l0 (y : F) (h : (f ⁻¹' Set.Iic y).Nonempty) :
sInf {f x | x ∈ f ⁻¹' Set.Iic y} = sInf {f x | x : E}:= by
have h₀ : {f x | x : E} = {f x | x ∈ f ⁻¹' Set.Iic y} ∪ {f x | x ∈ (f ⁻¹' Set.Iic y)ᶜ} := by
ext y'; constructor
· rintro ⟨x, xeq⟩
by_cases xsub : x ∈ f ⁻¹' Set.Iic y
· exact Or.inl ⟨x, xsub, xeq⟩
· exact Or.inr ⟨x, xsub, xeq⟩
· intro h'
rcases h' with ⟨x, _, xeq⟩ | ⟨x, _, xeq⟩
· exact Exists.intro x xeq
· exact Exists.intro x xeq
have h₁ : sInf {f x | x ∈ f ⁻¹' Set.Iic y} ≤ sInf {f x | x ∈ (f ⁻¹' Set.Iic y)ᶜ} := by
apply sInf_le_sInf_of_forall_exists_le
intro y' ynsub
rcases h with ⟨x', xsub⟩; use f x'
constructor
· exact ⟨x', xsub, rfl⟩
rcases ynsub with ⟨x, xnsub, xeq⟩
apply le_trans xsub (Eq.trans_ge xeq (le_of_lt _))
simp only [← Set.preimage_setOf_eq, ← Set.preimage_compl, Set.compl_Iic, Set.Ioi_def] at xnsub
assumption
calc
sInf {f x | x ∈ f ⁻¹' Set.Iic y} =
sInf {f x | x ∈ f ⁻¹' Set.Iic y} ⊓ sInf {f x | x ∈ (f ⁻¹' Set.Iic y)ᶜ} :=
Iff.mpr left_eq_inf h₁
_ = sInf ({f x | x ∈ f ⁻¹' Set.Iic y} ∪ {f x | x ∈ (f ⁻¹' Set.Iic y)ᶜ}) := Eq.symm sInf_union
_ = sInf {f x | x : E} := congrArg sInf (id (Eq.symm h₀))
/- If a premiage of `f` is nonempty and compact,
then its minimum point set `{x | IsMinOn f univ x}` is nonempty -/
theorem IsMinOn.of_isCompact_preimage {y : F}
(h1 : (f ⁻¹' Set.Iic y).Nonempty) (h2 : IsCompact (f ⁻¹' Set.Iic y)) :
∃ x, IsMinOn f univ x := by
have hs : Set.Nonempty {f x | x ∈ (f ⁻¹' Set.Iic y)} := by
rcases h1 with ⟨x, xsub⟩
exact Exists.intro (f x) (Exists.intro x ⟨xsub, rfl⟩)
have hs' : BddBelow {f x | x ∈ (f ⁻¹' Set.Iic y)} :=
OrderBot.bddBelow {x | ∃ x_1 ∈ f ⁻¹' Iic y, f x_1 = x}
rcases exists_seq_tendsto_sInf hs hs' with ⟨fx, _, cfx, fxs⟩
choose x xsub xeq using fxs
rcases IsCompact.tendsto_subseq h2 xsub with ⟨x', xsub', k, mono, cxk⟩
have cfxk : Tendsto (f ∘ x ∘ k) atTop (𝓝 (sInf {f x | x ∈ (f ⁻¹' Set.Iic y)})) := by
have xkeq : ∀ (n : ℕ), (f ∘ x ∘ k) n = (fx ∘ k) n := fun n => xeq <| k n
rw [tendsto_congr xkeq]
apply Tendsto.comp cfx (StrictMono.tendsto_atTop mono)
have inepi : (x', sInf {f x | x ∈ (f ⁻¹' Set.Iic y)}) ∈ {p : E × F | f p.1 ≤ p.2} :=
(IsClosed.isSeqClosed (LowerSemicontinuous.isClosed_epigraph hf))
(fun n => Eq.le (by rfl)) (Tendsto.prod_mk_nhds cxk cfxk)
use x'; intro xx _
apply le_of_eq_of_le
· apply le_antisymm inepi (sInf_le (Exists.intro x' ⟨xsub', rfl⟩))
· apply le_of_eq_of_le (l0 y h1) (sInf_le (by use xx))
variable [PseudoMetricSpace E] [ProperSpace E]
/- If a premiage of `f` is nonempty and compact,
then its minimum point set `{x | IsMinOn f univ x}` is compact -/
theorem IsCompact_isMinOn_of_isCompact_preimage {y : F}
(h1 : (f ⁻¹' Set.Iic y).Nonempty) (h2 : IsCompact (f ⁻¹' Set.Iic y)) :
IsCompact {x | IsMinOn f univ x} := by
obtain ⟨x', hx'⟩ := IsMinOn.of_isCompact_preimage hf h1 h2
have seq : {x | IsMinOn f univ x} = (f ⁻¹' Set.Iic (f x')) :=
Set.ext fun xx =>
{ mp := fun hxx => isMinOn_iff.mp hxx x' trivial,
mpr := fun hxx x xuniv => ge_trans (hx' xuniv) hxx }
simp only [seq]
apply IsCompact.of_isClosed_subset h2 (LowerSemicontinuous.isClosed_preimage hf (f x'))
apply Set.preimage_mono
simp only [Set.Iic_subset_Iic]
obtain ⟨x, hx⟩ := h1
exact ge_trans hx (hx' trivial)
end
/-! ### Existence of Solutions -/
section
variable {𝕜 : Type _}
variable [LinearOrderedRing 𝕜] [DenselyOrdered 𝕜] [Module 𝕜 E]
def strong_quasi : Prop :=
∀ ⦃x⦄, ∀ ⦃y⦄, x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
→ f ((a • x : E) + (b • y : E)) < max (f x) (f y)
variable ( hf' : @strong_quasi E F _ _ f 𝕜 _ _)
/- the Minimum of strongly quasi function is unique -/
theorem isMinOn_unique {x y : E} (hx : IsMinOn f univ x) (hy : IsMinOn f univ y) : x = y := by
by_contra neq
have : (0 : 𝕜) < (1 : 𝕜) := one_pos
obtain ⟨a, lta, alt⟩ := exists_between this
have eqone : a + (1 - a) = 1 := add_sub_cancel a 1
have lta' : 0 < 1 - a := sub_pos_of_lt alt
have h : f (a • x + (1 - a) • y) < f y := by
apply Eq.trans_gt (max_eq_right (hx trivial))
apply hf' neq lta lta' eqone
simp only [isMinOn_iff] at hy
specialize hy (a • x + (1 - a) • y) trivial
apply not_le_of_lt h hy
end