On complemented subspaces of L1[0,1]L_1[0,1]

BanLat/Operators/OrderBounded.lean

All source files · Download exact source

SHA-256: a563efcec03e343455826da46e359b819a39a0b0e53de85d17fb76a6579842d2

1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Operators.Positive67/-!8# Order bounded operators910A linear map between vector lattices is **order bounded** if it maps order bounded11sets to order bounded sets. Equivalently, for every positive `x`, there exists a12positive `y` such that `|z| ≤ x` implies `|T z| ≤ y`. Every positive operator is13order bounded, and every order bounded operator from a Banach lattice to a normed14vector lattice is continuous. The bundled type `OrderBoundedHom X Y` carries15the basic algebraic and order instances.16-/1718variable {X Y : Type*} [AddCommGroup X] [AddCommGroup Y] [Lattice X] [Lattice Y]19  [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y]2021/-- A linear map is *order bounded* if for every positive `x`, the image of the22symmetric order interval `{z | |z| ≤ x}` is order bounded. -/23def IsOrderBounded (f : X →ₗ[ℝ] Y) : Prop :=24  ∀ x : X, 0 ≤ x → ∃ y : Y, 0 ≤ y ∧ ∀ z : X, |z| ≤ x → |f z| ≤ y2526namespace Positive2728/-- Every positive operator is order bounded. -/29theorem isOrderBounded {f : X →ₗ[ℝ] Y} (hf : Positive f) :30    IsOrderBounded f := by31  intro x hx32  refine ⟨f x, hf x hx, fun z hz => ?_⟩33  exact (abs_le_map_abs hf z).trans ((monotone_iff.mpr hf) hz)3435end Positive3637namespace IsOrderBounded3839/-- The sum of order bounded operators is order bounded. -/40theorem add {f g : X →ₗ[ℝ] Y} (hf : IsOrderBounded f)41    (hg : IsOrderBounded g) :42    IsOrderBounded (f + g) := by43  intro x hx44  obtain ⟨yf, hyf, hbf⟩ := hf x hx45  obtain ⟨yg, hyg, hbg⟩ := hg x hx46  refine ⟨yf + yg, add_nonneg hyf hyg, fun z hz => ?_⟩47  simp only [LinearMap.add_apply]48  exact (abs_add_le _ _).trans (add_le_add (hbf z hz) (hbg z hz))4950/-- The negation of an order bounded operator is order bounded. -/51theorem neg {f : X →ₗ[ℝ] Y} (hf : IsOrderBounded f) :52    IsOrderBounded (-f) := by53  intro x hx54  obtain ⟨y, hy, hb⟩ := hf x hx55  exact ⟨y, hy, fun z hz => by56    simp only [LinearMap.neg_apply, abs_neg]; exact hb z hz⟩5758/-- The difference of order bounded operators is order bounded. -/59theorem sub {f g : X →ₗ[ℝ] Y} (hf : IsOrderBounded f)60    (hg : IsOrderBounded g) :61    IsOrderBounded (f - g) := by62  rw [sub_eq_add_neg]; exact add hf (neg hg)6364/-- A scalar multiple of an order bounded operator is order65bounded. -/66theorem smul {f : X →ₗ[ℝ] Y} (hf : IsOrderBounded f)67    (r : ℝ) : IsOrderBounded (r • f) := by68  intro x hx69  obtain ⟨y, hy, hb⟩ := hf x hx70  refine ⟨|r| • y, smul_nonneg (abs_nonneg r) hy, fun z hz => ?_⟩71  simp only [LinearMap.smul_apply]72  rw [abs_smul' (f z) r]73  exact smul_le_smul_of_nonneg_left (hb z hz) (abs_nonneg r)7475variable {X Y : Type*} [NormedAddCommGroup X] [NormedAddCommGroup Y]76  [Lattice X] [Lattice Y] [IsOrderedAddMonoid X] [IsOrderedAddMonoid Y]77  [BanachLattice X] [NormedVectorLattice Y]7879/-- Every order bounded operator from a Banach lattice to a normed vector lattice80is continuous. -/81theorem continuous {f : X →ₗ[ℝ] Y} (hf : IsOrderBounded f) :82    Continuous f := by83  by_contra hcont84  have hunb : ∀ C : ℝ, ∃ x : X, C * ‖x‖ < ‖f x‖ := by85    by_contra h; push Not at h; obtain ⟨C, hC⟩ := h86    exact hcont (continuous_of_linear_of_bound f.map_add f.map_smul hC)87  have hseq : ∀ n : ℕ, ∃ x : X, ‖x‖ ≤ (1 / 2 : ℝ) ^ n ∧ (n : ℝ) < ‖f x‖ := by88    intro n89    obtain ⟨z, hz⟩ := hunb ((n : ℝ) * (2 : ℝ) ^ n)90    have hznz : z ≠ 0 := by intro h; simp [h] at hz91    refine ⟨((2 : ℝ) ^ n * ‖z‖)⁻¹ • z, ?_, ?_⟩92    · rw [norm_smul, Real.norm_of_nonneg (inv_nonneg.mpr (by positivity))]93      rw [inv_mul_le_iff₀ (by positivity : (0 : ℝ) < 2 ^ n * ‖z‖)]94      simp [one_div, mul_comm]95    · rw [map_smul, norm_smul, Real.norm_of_nonneg (inv_nonneg.mpr (by positivity))]96      rw [lt_inv_mul_iff₀ (by positivity : (0 : ℝ) < 2 ^ n * ‖z‖)]97      linarith [mul_comm ((n : ℝ) * (2 : ℝ) ^ n) ‖z‖]98  choose x hxn hxf using hseq99  have habs : Summable (fun n => |x n|) :=100    .of_norm_bounded (g := fun n => (1 / 2 : ℝ) ^ n)101      (summable_geometric_of_lt_one (by norm_num) (by norm_num))102      (fun n => by rw [norm_abs_eq_norm]; exact hxn n)103  set y := ∑' n, |x n|104  have hy : 0 ≤ y := tsum_nonneg (fun n => abs_nonneg _)105  have hle : ∀ n, |x n| ≤ y :=106    fun n => habs.le_tsum n (fun j _ => abs_nonneg _)107  obtain ⟨u, _hu, hbound⟩ := hf y hy108  obtain ⟨N, hN⟩ := exists_nat_gt ‖u‖109  have hfN : ‖f (x N)‖ ≤ ‖u‖ := by110    have hab : |f (x N)| ≤ u := hbound (x N) (hle N)111    exact norm_le_norm_of_abs_le_abs (hab.trans (le_abs_self u))112  exact absurd (lt_of_lt_of_le (hxf N) hfN) (not_lt.mpr hN.le)113114end IsOrderBounded115116/-! ### The space of order bounded operators -/117118/-- The type of order bounded linear operators from `X` to `Y`. -/119structure OrderBoundedHom (X : Type*) (Y : Type*)120    [AddCommGroup X] [AddCommGroup Y] [Lattice X]121    [Lattice Y] [IsOrderedAddMonoid X]122    [IsOrderedAddMonoid Y] [VectorLattice X]123    [VectorLattice Y] extends X →ₗ[ℝ] Y where124  isOrderBounded' : IsOrderBounded toLinearMap125126namespace OrderBoundedHom127128variable {X Y : Type*} [AddCommGroup X] [AddCommGroup Y]129  [Lattice X] [Lattice Y] [IsOrderedAddMonoid X]130  [IsOrderedAddMonoid Y] [VectorLattice X]131  [VectorLattice Y]132133/-- Coercion from `OrderBoundedHom` to functions. -/134instance instFunLike :135    FunLike (OrderBoundedHom X Y) X Y where136  coe f := f.toFun137  coe_injective := by138    intro f g h; cases f; cases g; congr 1139    exact LinearMap.ext (congrFun h)140141@[ext]142theorem ext {f g : OrderBoundedHom X Y}143    (h : ∀ x, f x = g x) : f = g :=144  DFunLike.coe_injective (funext h)145146@[simp]147theorem coe_toLinearMap (f : OrderBoundedHom X Y) :148    ⇑f.toLinearMap = ⇑f := rfl149150private theorem toLinearMap_injective :151    Function.Injective (OrderBoundedHom.toLinearMap :152      OrderBoundedHom X Y → X →ₗ[ℝ] Y) := fun _ _ h =>153  ext fun x => congrFun (congrArg DFunLike.coe h) x154155/-- Bundle a positive linear operator as an `OrderBoundedHom`. -/156def ofPositive (f : X →ₗ[ℝ] Y) (hf : Positive f) : OrderBoundedHom X Y :=157  ⟨f, hf.isOrderBounded⟩158159@[simp]160theorem ofPositive_apply (f : X →ₗ[ℝ] Y) (hf : Positive f) (x : X) :161    ofPositive f hf x = f x := rfl162163instance instZero : Zero (OrderBoundedHom X Y) :=164  ⟨ofPositive 0 fun _ _ => by simp⟩165166instance instAdd : Add (OrderBoundedHom X Y) :=167  ⟨fun f g => ⟨f.toLinearMap + g.toLinearMap,168    IsOrderBounded.add f.isOrderBounded' g.isOrderBounded'⟩⟩169170instance instNeg : Neg (OrderBoundedHom X Y) :=171  ⟨fun f => ⟨-f.toLinearMap,172    IsOrderBounded.neg f.isOrderBounded'⟩⟩173174instance instSub : Sub (OrderBoundedHom X Y) :=175  ⟨fun f g => ⟨f.toLinearMap - g.toLinearMap,176    IsOrderBounded.sub f.isOrderBounded' g.isOrderBounded'⟩⟩177178instance instSMulNat : SMul ℕ (OrderBoundedHom X Y) :=179  ⟨fun n f => ⟨n • f.toLinearMap, by180    rw [← Nat.cast_smul_eq_nsmul ℝ]181    exact IsOrderBounded.smul f.isOrderBounded' n⟩⟩182183instance instSMulInt : SMul ℤ (OrderBoundedHom X Y) :=184  ⟨fun n f => ⟨n • f.toLinearMap, by185    rw [← Int.cast_smul_eq_zsmul ℝ]186    exact IsOrderBounded.smul f.isOrderBounded' n⟩⟩187188noncomputable instance :189    AddCommGroup (OrderBoundedHom X Y) :=190  toLinearMap_injective.addCommGroup _191    rfl (fun _ _ => rfl) (fun _ => rfl)192    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)193194noncomputable instance :195    Module ℝ (OrderBoundedHom X Y) where196  smul r f := ⟨r • f.toLinearMap,197    IsOrderBounded.smul f.isOrderBounded' r⟩198  one_smul f := ext fun x => one_smul ℝ (f x)199  mul_smul r s f := ext fun x => mul_smul r s (f x)200  smul_zero r := ext fun _ => smul_zero r201  smul_add r f g := ext fun x => smul_add r (f x) (g x)202  add_smul r s f := ext fun x => add_smul r s (f x)203  zero_smul f := ext fun x => zero_smul ℝ (f x)204205noncomputable instance :206    PartialOrder (OrderBoundedHom X Y) :=207  PartialOrder.lift OrderBoundedHom.toLinearMap toLinearMap_injective208209/-- The operator ordering: `f ≤ g` iff for every `x ≥ 0` we have210`f x ≤ g x`. -/211theorem le_iff {f g : OrderBoundedHom X Y} :212    f ≤ g ↔ ∀ x : X, 0 ≤ x → f x ≤ g x :=213  Positive.le_iff214215instance :216    IsOrderedAddMonoid (OrderBoundedHom X Y) where217  add_le_add_left _ _ hab c := le_iff.mpr fun x hx =>218    add_le_add_left (le_iff.mp hab x hx) (c x)219220instance :221    PosSMulMono ℝ (OrderBoundedHom X Y) where222  smul_le_smul_of_nonneg_left _ hr _ _ hfg := le_iff.mpr fun x hx =>223    smul_le_smul_of_nonneg_left (le_iff.mp hfg x hx) hr224225end OrderBoundedHom226