-
Notifications
You must be signed in to change notification settings - Fork 257
/
Extension.lean
190 lines (170 loc) · 9.93 KB
/
Extension.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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov, Frédéric Dupuis
-/
import Mathlib.Analysis.Convex.Cone.Basic
import Mathlib.Data.Real.Archimedean
import Mathlib.LinearAlgebra.LinearPMap
#align_import analysis.convex.cone.basic from "leanprover-community/mathlib"@"915591b2bb3ea303648db07284a161a7f2a9e3d4"
/-!
# Extension theorems
We prove two extension theorems:
* `riesz_extension`:
[M. Riesz extension theorem](https://en.wikipedia.org/wiki/M._Riesz_extension_theorem) says that
if `s` is a convex cone in a real vector space `E`, `p` is a submodule of `E`
such that `p + s = E`, and `f` is a linear function `p → ℝ` which is
nonnegative on `p ∩ s`, then there exists a globally defined linear function
`g : E → ℝ` that agrees with `f` on `p`, and is nonnegative on `s`.
* `exists_extension_of_le_sublinear`:
Hahn-Banach theorem: if `N : E → ℝ` is a sublinear map, `f` is a linear map
defined on a subspace of `E`, and `f x ≤ N x` for all `x` in the domain of `f`,
then `f` can be extended to the whole space to a linear map `g` such that `g x ≤ N x`
for all `x`
-/
open Set LinearMap
variable {𝕜 E F G : Type*}
/-!
### M. Riesz extension theorem
Given a convex cone `s` in a vector space `E`, a submodule `p`, and a linear `f : p → ℝ`, assume
that `f` is nonnegative on `p ∩ s` and `p + s = E`. Then there exists a globally defined linear
function `g : E → ℝ` that agrees with `f` on `p`, and is nonnegative on `s`.
We prove this theorem using Zorn's lemma. `RieszExtension.step` is the main part of the proof.
It says that if the domain `p` of `f` is not the whole space, then `f` can be extended to a larger
subspace `p ⊔ span ℝ {y}` without breaking the non-negativity condition.
In `RieszExtension.exists_top` we use Zorn's lemma to prove that we can extend `f`
to a linear map `g` on `⊤ : Submodule E`. Mathematically this is the same as a linear map on `E`
but in Lean `⊤ : Submodule E` is isomorphic but is not equal to `E`. In `riesz_extension`
we use this isomorphism to prove the theorem.
-/
variable [AddCommGroup E] [Module ℝ E]
namespace RieszExtension
open Submodule
variable (s : ConvexCone ℝ E) (f : E →ₗ.[ℝ] ℝ)
/-- Induction step in M. Riesz extension theorem. Given a convex cone `s` in a vector space `E`,
a partially defined linear map `f : f.domain → ℝ`, assume that `f` is nonnegative on `f.domain ∩ p`
and `p + s = E`. If `f` is not defined on the whole `E`, then we can extend it to a larger
submodule without breaking the non-negativity condition. -/
theorem step (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
(dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) (hdom : f.domain ≠ ⊤) :
∃ g, f < g ∧ ∀ x : g.domain, (x : E) ∈ s → 0 ≤ g x := by
obtain ⟨y, -, hy⟩ : ∃ y ∈ ⊤, y ∉ f.domain := SetLike.exists_of_lt (lt_top_iff_ne_top.2 hdom)
obtain ⟨c, le_c, c_le⟩ :
∃ c, (∀ x : f.domain, -(x : E) - y ∈ s → f x ≤ c) ∧
∀ x : f.domain, (x : E) + y ∈ s → c ≤ f x := by
set Sp := f '' { x : f.domain | (x : E) + y ∈ s }
set Sn := f '' { x : f.domain | -(x : E) - y ∈ s }
suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
simpa only [Set.Nonempty, upperBounds, lowerBounds, forall_mem_image] using this
refine' exists_between_of_forall_le (Nonempty.image f _) (Nonempty.image f (dense y)) _
· rcases dense (-y) with ⟨x, hx⟩
rw [← neg_neg x, NegMemClass.coe_neg, ← sub_eq_add_neg] at hx
exact ⟨_, hx⟩
rintro a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩
have := s.add_mem hxp hxn
rw [add_assoc, add_sub_cancel, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this
replace := nonneg _ this
rwa [f.map_sub, sub_nonneg] at this
-- Porting note: removed an unused `have`
refine' ⟨f.supSpanSingleton y (-c) hy, _, _⟩
· refine' lt_iff_le_not_le.2 ⟨f.left_le_sup _ _, fun H => _⟩
replace H := LinearPMap.domain_mono.monotone H
rw [LinearPMap.domain_supSpanSingleton, sup_le_iff, span_le, singleton_subset_iff] at H
exact hy H.2
· rintro ⟨z, hz⟩ hzs
rcases mem_sup.1 hz with ⟨x, hx, y', hy', rfl⟩
rcases mem_span_singleton.1 hy' with ⟨r, rfl⟩
simp only [Subtype.coe_mk] at hzs
erw [LinearPMap.supSpanSingleton_apply_mk _ _ _ _ _ hx, smul_neg, ← sub_eq_add_neg, sub_nonneg]
rcases lt_trichotomy r 0 with (hr | hr | hr)
· have : -(r⁻¹ • x) - y ∈ s := by
rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul,
mul_inv_cancel hr.ne, one_smul, sub_eq_add_neg, neg_smul, neg_neg]
-- Porting note: added type annotation and `by exact`
replace : f (r⁻¹ • ⟨x, hx⟩) ≤ c := le_c (r⁻¹ • ⟨x, hx⟩) (by exact this)
rwa [← mul_le_mul_left (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul,
smul_eq_mul, ← mul_assoc, mul_inv_cancel hr.ne, one_mul] at this
· subst r
simp only [zero_smul, add_zero] at hzs ⊢
apply nonneg
exact hzs
· have : r⁻¹ • x + y ∈ s := by
rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel hr.ne', one_smul]
-- Porting note: added type annotation and `by exact`
replace : c ≤ f (r⁻¹ • ⟨x, hx⟩) := c_le (r⁻¹ • ⟨x, hx⟩) (by exact this)
rwa [← mul_le_mul_left hr, f.map_smul, smul_eq_mul, ← mul_assoc, mul_inv_cancel hr.ne',
one_mul] at this
#align riesz_extension.step RieszExtension.step
theorem exists_top (p : E →ₗ.[ℝ] ℝ) (hp_nonneg : ∀ x : p.domain, (x : E) ∈ s → 0 ≤ p x)
(hp_dense : ∀ y, ∃ x : p.domain, (x : E) + y ∈ s) :
∃ q ≥ p, q.domain = ⊤ ∧ ∀ x : q.domain, (x : E) ∈ s → 0 ≤ q x := by
set S := { p : E →ₗ.[ℝ] ℝ | ∀ x : p.domain, (x : E) ∈ s → 0 ≤ p x }
have hSc : ∀ c, c ⊆ S → IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub := by
intro c hcs c_chain y hy
clear hp_nonneg hp_dense p
have cne : c.Nonempty := ⟨y, hy⟩
have hcd : DirectedOn (· ≤ ·) c := c_chain.directedOn
refine' ⟨LinearPMap.sSup c hcd, _, fun _ ↦ LinearPMap.le_sSup hcd⟩
rintro ⟨x, hx⟩ hxs
have hdir : DirectedOn (· ≤ ·) (LinearPMap.domain '' c) :=
directedOn_image.2 (hcd.mono LinearPMap.domain_mono.monotone)
rcases (mem_sSup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩
have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc
convert ← hcs hfc ⟨x, hfx⟩ hxs using 1
exact this.2 rfl
obtain ⟨q, hqs, hpq, hq⟩ := zorn_nonempty_partialOrder₀ S hSc p hp_nonneg
refine ⟨q, hpq, ?_, hqs⟩
contrapose! hq
have hqd : ∀ y, ∃ x : q.domain, (x : E) + y ∈ s := fun y ↦
let ⟨x, hx⟩ := hp_dense y
⟨Submodule.inclusion hpq.left x, hx⟩
rcases step s q hqs hqd hq with ⟨r, hqr, hr⟩
exact ⟨r, hr, hqr.le, hqr.ne'⟩
#align riesz_extension.exists_top RieszExtension.exists_top
end RieszExtension
/-- M. **Riesz extension theorem**: given a convex cone `s` in a vector space `E`, a submodule `p`,
and a linear `f : p → ℝ`, assume that `f` is nonnegative on `p ∩ s` and `p + s = E`. Then
there exists a globally defined linear function `g : E → ℝ` that agrees with `f` on `p`,
and is nonnegative on `s`. -/
theorem riesz_extension (s : ConvexCone ℝ E) (f : E →ₗ.[ℝ] ℝ)
(nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
(dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) :
∃ g : E →ₗ[ℝ] ℝ, (∀ x : f.domain, g x = f x) ∧ ∀ x ∈ s, 0 ≤ g x := by
rcases RieszExtension.exists_top s f nonneg dense
with ⟨⟨g_dom, g⟩, ⟨-, hfg⟩, rfl : g_dom = ⊤, hgs⟩
refine' ⟨g.comp (LinearMap.id.codRestrict ⊤ fun _ ↦ trivial), _, _⟩
· exact fun x => (hfg rfl).symm
· exact fun x hx => hgs ⟨x, _⟩ hx
#align riesz_extension riesz_extension
/-- **Hahn-Banach theorem**: if `N : E → ℝ` is a sublinear map, `f` is a linear map
defined on a subspace of `E`, and `f x ≤ N x` for all `x` in the domain of `f`,
then `f` can be extended to the whole space to a linear map `g` such that `g x ≤ N x`
for all `x`. -/
theorem exists_extension_of_le_sublinear (f : E →ₗ.[ℝ] ℝ) (N : E → ℝ)
(N_hom : ∀ c : ℝ, 0 < c → ∀ x, N (c • x) = c * N x) (N_add : ∀ x y, N (x + y) ≤ N x + N y)
(hf : ∀ x : f.domain, f x ≤ N x) :
∃ g : E →ₗ[ℝ] ℝ, (∀ x : f.domain, g x = f x) ∧ ∀ x, g x ≤ N x := by
let s : ConvexCone ℝ (E × ℝ) :=
{ carrier := { p : E × ℝ | N p.1 ≤ p.2 }
smul_mem' := fun c hc p hp =>
calc
N (c • p.1) = c * N p.1 := N_hom c hc p.1
_ ≤ c * p.2 := mul_le_mul_of_nonneg_left hp hc.le
add_mem' := fun x hx y hy => (N_add _ _).trans (add_le_add hx hy) }
set f' := (-f).coprod (LinearMap.id.toPMap ⊤)
have hf'_nonneg : ∀ x : f'.domain, x.1 ∈ s → 0 ≤ f' x := fun x (hx : N x.1.1 ≤ x.1.2) ↦ by
simpa [f'] using le_trans (hf ⟨x.1.1, x.2.1⟩) hx
have hf'_dense : ∀ y : E × ℝ, ∃ x : f'.domain, ↑x + y ∈ s := by
rintro ⟨x, y⟩
refine' ⟨⟨(0, N x - y), ⟨f.domain.zero_mem, trivial⟩⟩, _⟩
simp only [s, ConvexCone.mem_mk, mem_setOf_eq, Prod.fst_add, Prod.snd_add, zero_add,
sub_add_cancel, le_rfl]
obtain ⟨g, g_eq, g_nonneg⟩ := riesz_extension s f' hf'_nonneg hf'_dense
replace g_eq : ∀ (x : f.domain) (y : ℝ), g (x, y) = y - f x := fun x y ↦
(g_eq ⟨(x, y), ⟨x.2, trivial⟩⟩).trans (sub_eq_neg_add _ _).symm
refine ⟨-g.comp (inl ℝ E ℝ), fun x ↦ ?_, fun x ↦ ?_⟩
· simp [g_eq x 0]
· calc -g (x, 0) = g (0, N x) - g (x, N x) := by simp [← map_sub, ← map_neg]
_ = N x - g (x, N x) := by simpa using g_eq 0 (N x)
_ ≤ N x := by simpa using g_nonneg ⟨x, N x⟩ (le_refl (N x))
#align exists_extension_of_le_sublinear exists_extension_of_le_sublinear