BanLat/Operators/Positive.lean
All source files · Download exact source
SHA-256: ff39c2e000bdd315c914a68708d2fd3854a74accbe0ed5ec3901c331347dfe7d
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Normed6import Mathlib.Algebra.Order.Module.Basic7import Mathlib.Topology.Algebra.Module.Equiv89/-!10# Positive operators1112A linear map between vector lattices is **positive** if it sends non-negative elements to13non-negative elements. For linear maps, positivity is equivalent to monotonicity, and a14positive operator satisfies `|f x| ≤ f |x|`.1516The **extension lemma** shows that an additive map on the positive cone extends uniquely17to a positive linear operator when the codomain is Archimedean. Finally, every positive18operator from a Banach lattice to a normed vector lattice is automatically continuous.19-/2021/-! ## Definition and basic properties -/2223variable {X Y : Type*} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y]24 [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y]2526/-- A linear map is *positive* if it sends non-negative elements to non-negative elements. -/27def Positive (f : X →ₗ[ℝ] Y) : Prop :=28 ∀ x : X, 0 ≤ x → 0 ≤ f x2930namespace Positive3132/-- For a linear map between vector lattices, monotonicity and positivity are equivalent. -/33theorem monotone_iff {f : X →ₗ[ℝ] Y} : Monotone f ↔ Positive f := by34 constructor35 · intro hm x hx36 simpa [map_zero] using hm hx37 · intro hp a b hab38 have h : 0 ≤ f (b - a) := hp (b - a) (sub_nonneg.mpr hab)39 rwa [map_sub, sub_nonneg] at h4041/-- A positive operator satisfies `|f x| ≤ f |x|`. -/42theorem abs_le_map_abs {f : X →ₗ[ℝ] Y} (hf : Positive f) (x : X) : |f x| ≤ f |x| := by43 rw [abs]44 apply sup_le45 · exact (monotone_iff.mpr hf) (by rw [abs]; exact le_sup_left)46 · have h : f (-x) ≤ f |x| := (monotone_iff.mpr hf) (by rw [abs]; exact le_sup_right)47 rwa [map_neg] at h4849/-! ## Order on linear operators5051The space `X →ₗ[ℝ] Y` of linear operators between vector lattices is partially52ordered by `T ≤ S ↔ Positive (S - T)`, equivalently `T x ≤ S x` for every53`0 ≤ x`. Under this order, `0 ≤ T` is the same as `Positive T`. -/5455instance : LE (X →ₗ[ℝ] Y) where56 le T S := Positive (S - T)5758theorem le_def {T S : X →ₗ[ℝ] Y} : T ≤ S ↔ Positive (S - T) := Iff.rfl5960theorem le_iff {T S : X →ₗ[ℝ] Y} : T ≤ S ↔ ∀ x, 0 ≤ x → T x ≤ S x := by61 refine ⟨fun h x hx => ?_, fun h x hx => ?_⟩62 · have hxs := h x hx; rwa [LinearMap.sub_apply, sub_nonneg] at hxs63 · rw [LinearMap.sub_apply, sub_nonneg]; exact h x hx6465@[simp] theorem zero_le_iff {T : X →ₗ[ℝ] Y} : 0 ≤ T ↔ Positive T := by66 change Positive (T - 0) ↔ _; rw [sub_zero]6768instance : PartialOrder (X →ₗ[ℝ] Y) where69 le_refl T := by70 change Positive (T - T); rw [sub_self]; intro _ _; exact le_refl 071 le_trans T S R hTS hSR := by72 intro x hx73 have heq : (R - T) x = (R - S) x + (S - T) x := by74 simp [LinearMap.sub_apply]75 rw [heq]76 exact add_nonneg (hSR x hx) (hTS x hx)77 le_antisymm T S hTS hST := by78 ext x79 have hp : T x⁺ = S x⁺ :=80 le_antisymm ((le_iff.mp hTS) _ (posPart_nonneg x))81 ((le_iff.mp hST) _ (posPart_nonneg x))82 have hn : T x⁻ = S x⁻ :=83 le_antisymm ((le_iff.mp hTS) _ (negPart_nonneg x))84 ((le_iff.mp hST) _ (negPart_nonneg x))85 rw [show x = x⁺ - x⁻ from (posPart_sub_negPart x).symm,86 map_sub, map_sub, hp, hn]8788/-! ## Extension from the positive cone -/8990section ExtensionLemma9192variable {X Y : Type*} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y]93 [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y]94 [IsVLArchimedean Y] {τ : X → Y}9596omit [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]97 [VectorLattice X] [VectorLattice Y] [IsVLArchimedean Y] in98private lemma tau_zero99 (hτ_add : ∀ x y, 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y) :100 τ 0 = 0 := by101 have h := hτ_add 0 0 le_rfl le_rfl102 rw [add_zero] at h103 exact (add_left_cancel (show τ 0 + 0 = τ 0 + τ 0 from by104 rw [add_zero]; exact h)).symm105106omit [Lattice Y] [IsOrderedAddMonoid Y] [VectorLattice X]107 [VectorLattice Y] [IsVLArchimedean Y] in108private lemma tau_nsmul109 (hτ_add : ∀ x y, 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y)110 (n : ℕ) {x : X} (hx : 0 ≤ x) :111 τ (n • x) = n • τ x := by112 induction n with113 | zero => simp [tau_zero hτ_add]114 | succ n ih =>115 rw [succ_nsmul, hτ_add _ _ (nsmul_nonneg hx n) hx, ih, succ_nsmul]116117omit [VectorLattice X] [VectorLattice Y] [IsVLArchimedean Y] in118private lemma tau_mono119 (hτ_nn : ∀ x, 0 ≤ x → 0 ≤ τ x)120 (hτ_add : ∀ x y, 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y)121 {a b : X} (ha : 0 ≤ a) (_hb : 0 ≤ b) (hab : a ≤ b) :122 τ a ≤ τ b := by123 have hd : 0 ≤ b - a := sub_nonneg.mpr hab124 have : τ b = τ a + τ (b - a) := by125 rw [← hτ_add a (b - a) ha hd]; congr 1; abel126 rw [this]127 exact le_add_of_nonneg_right (hτ_nn _ hd)128129private lemma tau_real_smul130 (hτ_nn : ∀ x, 0 ≤ x → 0 ≤ τ x)131 (hτ_add : ∀ x y, 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y)132 {r : ℝ} (hr : 0 ≤ r) {x : X} (hx : 0 ≤ x) :133 τ (r • x) = r • τ x := by134 set d := τ (r • x) - r • τ x with hd_def135 suffices hd : d = 0 from sub_eq_zero.mp hd136 rw [← abs_eq_zero_iff_zero]137 apply IsVLArchimedean.eq_zero_of_nonneg_of_forall_nsmul_le138 (y := τ x) (abs_nonneg d)139 intro m140 set k := Nat.floor ((m : ℝ) * r)141 have hmr : 0 ≤ (m : ℝ) * r := mul_nonneg (Nat.cast_nonneg m) hr142 have hk_le : (k : ℝ) ≤ (m : ℝ) * r := Nat.floor_le hmr143 have hmr_lt : (m : ℝ) * r < (k : ℝ) + 1 := Nat.lt_floor_add_one _144 have hmrx : m • (r • x) = ((m : ℝ) * r) • x := by145 rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul]146 -- m • τ(r•x) and m • (r • τ x) both lie in [k • τ x, (k+1) • τ x]147 have hlo : k • τ x ≤ m • τ (r • x) := by148 rw [← tau_nsmul hτ_add m (smul_nonneg hr hx),149 ← tau_nsmul hτ_add k hx]150 exact tau_mono hτ_nn hτ_add (nsmul_nonneg hx k)151 (nsmul_nonneg (smul_nonneg hr hx) m) <| by152 rw [hmrx, ← Nat.cast_smul_eq_nsmul ℝ k x]153 exact smul_le_smul_of_nonneg_right hk_le hx154 have hhi : m • τ (r • x) ≤ (k + 1) • τ x := by155 rw [← tau_nsmul hτ_add m (smul_nonneg hr hx),156 ← tau_nsmul hτ_add (k + 1) hx]157 exact tau_mono hτ_nn hτ_add158 (nsmul_nonneg (smul_nonneg hr hx) m)159 (nsmul_nonneg hx (k + 1)) <| by160 rw [hmrx, ← Nat.cast_smul_eq_nsmul ℝ (k + 1) x]161 exact smul_le_smul_of_nonneg_right (by push_cast; exact hmr_lt.le) hx162 have hlo' : k • τ x ≤ m • (r • τ x) := by163 rw [← Nat.cast_smul_eq_nsmul ℝ, ← Nat.cast_smul_eq_nsmul ℝ, smul_smul]164 exact smul_le_smul_of_nonneg_right hk_le (hτ_nn _ hx)165 have hhi' : m • (r • τ x) ≤ (k + 1) • τ x := by166 rw [← Nat.cast_smul_eq_nsmul ℝ m (r • τ x),167 ← Nat.cast_smul_eq_nsmul ℝ (k + 1) (τ x), smul_smul]168 exact smul_le_smul_of_nonneg_right (by push_cast; exact hmr_lt.le)169 (hτ_nn _ hx)170 -- Both values lie in an interval of width τ x, so |m•d| ≤ τ x171 have h1 : m • τ (r • x) - m • (r • τ x) ≤ τ x :=172 calc m • τ (r • x) - m • (r • τ x)173 ≤ (k + 1) • τ x - k • τ x := sub_le_sub hhi hlo'174 _ = τ x := by rw [add_nsmul, one_nsmul, add_sub_cancel_left]175 have h2 : m • (r • τ x) - m • τ (r • x) ≤ τ x :=176 calc m • (r • τ x) - m • τ (r • x)177 ≤ (k + 1) • τ x - k • τ x := sub_le_sub hhi' hlo178 _ = τ x := by rw [add_nsmul, one_nsmul, add_sub_cancel_left]179 -- Convert to m • |d| ≤ τ x180 have habs : |m • τ (r • x) - m • (r • τ x)| ≤ τ x :=181 sup_le h1 (show -(m • τ (r • x) - m • (r • τ x)) ≤ τ x by rwa [neg_sub])182 have hmd : m • τ (r • x) - m • (r • τ x) = m • d := by183 rw [← smul_sub]184 rw [hmd] at habs185 rw [← Nat.cast_smul_eq_nsmul ℝ m d] at habs186 rw [abs_smul' d (↑m : ℝ), abs_of_nonneg (Nat.cast_nonneg m)] at habs187 rwa [Nat.cast_smul_eq_nsmul ℝ m |d|] at habs188189private lemma posPart_smul_nonneg {r : ℝ} (hr : 0 ≤ r) (x : X) :190 (r • x)⁺ = r • x⁺ := by191 change (r • x) ⊔ 0 = r • (x ⊔ 0)192 rw [← smul_zero r, ← nonneg_smul_sup x 0 r hr, smul_zero]193194private lemma negPart_smul_nonneg {r : ℝ} (hr : 0 ≤ r) (x : X) :195 (r • x)⁻ = r • x⁻ := by196 change (-(r • x)) ⊔ 0 = r • ((-x) ⊔ 0)197 rw [← smul_neg, ← smul_zero r, ← nonneg_smul_sup (-x) 0 r hr, smul_zero]198199omit [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y]200 [IsVLArchimedean Y] in201private lemma extFun_add202 (_hτ_nn : ∀ x, 0 ≤ x → 0 ≤ τ x)203 (hτ_add : ∀ x y, 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y)204 (x y : X) :205 τ (x + y)⁺ - τ (x + y)⁻ = (τ x⁺ - τ x⁻) + (τ y⁺ - τ y⁻) := by206 have hid : (x + y)⁺ + x⁻ + y⁻ = (x + y)⁻ + x⁺ + y⁺ := by207 have l1 : (x + y)⁺ = x + y + (x + y)⁻ :=208 eq_add_of_sub_eq (posPart_sub_negPart _)209 have l2 : x⁺ = x + x⁻ := eq_add_of_sub_eq (posPart_sub_negPart x)210 have l3 : y⁺ = y + y⁻ := eq_add_of_sub_eq (posPart_sub_negPart y)211 rw [l1, l2, l3]; abel212 have hlhs : τ ((x + y)⁺ + x⁻ + y⁻) =213 τ (x + y)⁺ + τ x⁻ + τ y⁻ := by214 rw [hτ_add _ _ (add_nonneg (posPart_nonneg _) (negPart_nonneg _))215 (negPart_nonneg _),216 hτ_add _ _ (posPart_nonneg _) (negPart_nonneg _)]217 have hrhs : τ ((x + y)⁻ + x⁺ + y⁺) =218 τ (x + y)⁻ + τ x⁺ + τ y⁺ := by219 rw [hτ_add _ _ (add_nonneg (negPart_nonneg _) (posPart_nonneg _))220 (posPart_nonneg _),221 hτ_add _ _ (negPart_nonneg _) (posPart_nonneg _)]222 have key := hlhs.symm.trans ((congrArg τ hid).trans hrhs)223 calc τ (x + y)⁺ - τ (x + y)⁻224 = τ (x + y)⁺ + τ x⁻ + τ y⁻ - τ x⁻ - τ y⁻ - τ (x + y)⁻ := by225 abel226 _ = τ (x + y)⁻ + τ x⁺ + τ y⁺ - τ x⁻ - τ y⁻ - τ (x + y)⁻ := by227 rw [key]228 _ = τ x⁺ - τ x⁻ + (τ y⁺ - τ y⁻) := by abel229230private lemma extFun_smul231 (hτ_nn : ∀ x, 0 ≤ x → 0 ≤ τ x)232 (hτ_add : ∀ x y, 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y)233 (r : ℝ) (x : X) :234 τ (r • x)⁺ - τ (r • x)⁻ = r • (τ x⁺ - τ x⁻) := by235 by_cases hr : 0 ≤ r236 · rw [posPart_smul_nonneg hr, negPart_smul_nonneg hr,237 tau_real_smul hτ_nn hτ_add hr (posPart_nonneg _),238 tau_real_smul hτ_nn hτ_add hr (negPart_nonneg _), smul_sub]239 · push Not at hr240 have hnr : 0 ≤ -r := le_of_lt (neg_pos.mpr hr)241 have hrx : r • x = -((-r) • x) := by rw [neg_smul, neg_neg]242 have hp : (r • x)⁺ = (-r) • x⁻ := by243 rw [hrx, posPart_neg, negPart_smul_nonneg hnr]244 have hn : (r • x)⁻ = (-r) • x⁺ := by245 rw [hrx, negPart_neg, posPart_smul_nonneg hnr]246 rw [hp, hn,247 tau_real_smul hτ_nn hτ_add hnr (negPart_nonneg _),248 tau_real_smul hτ_nn hτ_add hnr (posPart_nonneg _)]249 rw [← smul_sub (-r) (τ x⁻) (τ x⁺),250 show τ x⁻ - τ x⁺ = -(τ x⁺ - τ x⁻) from (neg_sub _ _).symm,251 smul_neg, neg_smul, neg_neg]252253variable254 (hτ_nn : ∀ x, 0 ≤ x → 0 ≤ τ x)255 (hτ_add : ∀ x y, 0 ≤ x → 0 ≤ y → τ (x + y) = τ x + τ y)256257/-- **Extension Lemma**: an additive map on the positive cone of a vector lattice258extends to a unique positive linear operator when the codomain is Archimedean.259The extension satisfies `T x = τ x⁺ − τ x⁻`. -/260noncomputable def extension : X →ₗ[ℝ] Y :=261 { toFun := fun x => τ x⁺ - τ x⁻262 map_add' := extFun_add hτ_nn hτ_add263 map_smul' := fun r x => by264 simp only [RingHom.id_apply]265 exact extFun_smul hτ_nn hτ_add r x }266267@[simp]268theorem extension_apply (x : X) :269 extension hτ_nn hτ_add x = τ x⁺ - τ x⁻ := rfl270271theorem extension_nonneg {x : X} (hx : 0 ≤ x) :272 extension hτ_nn hτ_add x = τ x := by273 rw [extension_apply, posPart_of_nonneg hx, negPart_of_nonneg hx,274 tau_zero hτ_add, sub_zero]275276theorem extension_positive : Positive (extension hτ_nn hτ_add) :=277 fun x hx => by278 rw [extension_nonneg hτ_nn hτ_add hx]; exact hτ_nn _ hx279280/-- The positive linear extension is the unique positive operator281extending τ on nonneg elements. -/282theorem extension_unique {f : X →ₗ[ℝ] Y} (_hf : Positive f)283 (hext : ∀ x, 0 ≤ x → f x = τ x) :284 f = extension hτ_nn hτ_add := by285 ext x286 simp only [extension_apply]287 rw [← hext _ (posPart_nonneg _), ← hext _ (negPart_nonneg _), ← map_sub]288 congr 1; exact (posPart_sub_negPart x).symm289290end ExtensionLemma291292/-! ## Automatic continuity on Banach lattices -/293294variable {X Y : Type*} [NormedAddCommGroup X] [NormedAddCommGroup Y]295 [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]296 [BanachLattice X] [NormedVectorLattice Y]297298private lemma norm_map_le_of_abs_le {f : X →ₗ[ℝ] Y} (hf : Positive f)299 {x y : X} (h : |x| ≤ y) : ‖f x‖ ≤ ‖f y‖ :=300 norm_le_norm_of_abs_le_abs <|301 (abs_le_map_abs hf x).trans <|302 ((monotone_iff.mpr hf) h).trans (le_abs_self _)303304/-- Every positive linear operator from a Banach lattice to a normed vector lattice305is continuous. -/306theorem continuous {f : X →ₗ[ℝ] Y} (hf : Positive f) : Continuous f := by307 by_contra hcont308 have hunb : ∀ C : ℝ, ∃ x : X, C * ‖x‖ < ‖f x‖ := by309 by_contra h; push Not at h; obtain ⟨C, hC⟩ := h310 exact hcont (continuous_of_linear_of_bound f.map_add f.map_smul hC)311 -- For each n, find xₙ with ‖xₙ‖ ≤ (1/2)ⁿ and n < ‖f xₙ‖312 have hseq : ∀ n : ℕ, ∃ x : X, ‖x‖ ≤ (1 / 2 : ℝ) ^ n ∧ (n : ℝ) < ‖f x‖ := by313 intro n314 obtain ⟨z, hz⟩ := hunb ((n : ℝ) * (2 : ℝ) ^ n)315 have hznz : z ≠ 0 := by intro h; simp [h] at hz316 refine ⟨((2 : ℝ) ^ n * ‖z‖)⁻¹ • z, ?_, ?_⟩317 · rw [norm_smul, Real.norm_of_nonneg (inv_nonneg.mpr (by positivity))]318 rw [inv_mul_le_iff₀ (by positivity : (0 : ℝ) < 2 ^ n * ‖z‖)]319 simp [one_div, mul_comm]320 · rw [map_smul, norm_smul, Real.norm_of_nonneg (inv_nonneg.mpr (by positivity))]321 rw [lt_inv_mul_iff₀ (by positivity : (0 : ℝ) < 2 ^ n * ‖z‖)]322 linarith [mul_comm ((n : ℝ) * (2 : ℝ) ^ n) ‖z‖]323 choose x hxn hxf using hseq324 have habs : Summable (fun n => |x n|) :=325 .of_norm_bounded (g := fun n => (1 / 2 : ℝ) ^ n)326 (summable_geometric_of_lt_one (by norm_num) (by norm_num))327 (fun n => by rw [norm_abs_eq_norm]; exact hxn n)328 set y := ∑' n, |x n|329 have hle : ∀ n, |x n| ≤ y := fun n => habs.le_tsum n (fun j _ => abs_nonneg _)330 obtain ⟨N, hN⟩ := exists_nat_gt ‖f y‖331 exact absurd (lt_of_lt_of_le (hxf N) (norm_map_le_of_abs_le hf (hle N)))332 (not_lt.mpr hN.le)333334end Positive335