PL1/PrincipalIdealDual.lean
All source files · Download exact source
SHA-256: 76c1479447c319a86c43ef59d136942da23f80edf3ed3f0325623473ba1b5aaf
1import BanLat.Dual23/-!4# Principal-ideal localization of positive functionals56This public helper reproduces the private witness construction in the pinned7BanLat/Operators/RieszKantorovich.lean (David Muñoz-Lahoz). Its proofs use8Riesz decomposition and the positive-cone extension lemma. No principal9projection in the domain, completeness of the domain, or Schur hypothesis10is assumed. Keeping the helper separate preserves the imported BanLat port.11-/1213noncomputable section1415namespace PL1.PrincipalIdealDual16open OrderBoundedHom1718variable {X Y : Type*} [AddCommGroup X] [AddCommGroup Y]19 [Lattice X] [ConditionallyCompleteLattice Y] [IsOrderedAddMonoid X]20 [IsOrderedAddMonoid Y] [VectorLattice X] [VectorLattice Y]2122private lemma obZero_apply (x : X) : (0 : OrderBoundedHom X Y) x = (0 : Y) := rfl23private lemma obToLinearMap_apply (f : OrderBoundedHom X Y) (x : X) :24 f.toLinearMap x = f x := rfl2526lemma f_mono_of_nonneg {f : OrderBoundedHom X Y}27 (hf : (0 : OrderBoundedHom X Y) ≤ f) : Monotone f.toLinearMap :=28 Positive.monotone_iff.mpr fun y hy => by29 have := le_iff.mp hf y hy30 simpa only [obZero_apply, obToLinearMap_apply] using this313233lemma f_apply_nonneg {f : OrderBoundedHom X Y}34 (hf : (0 : OrderBoundedHom X Y) ≤ f) {y : X} (hy : 0 ≤ y) : 0 ≤ f y := by35 have := le_iff.mp hf y hy36 simpa only [obZero_apply] using this3738/-- The value of the witness operator on the positive cone:39`witFun f x₀ y = sup_n f (y ⊓ n • x₀)`. Defaults to `0` outside the regime where40the supremum exists. -/41noncomputable def witFun (f : OrderBoundedHom X Y) (x₀ y : X) : Y :=42 sSup (Set.range fun n : ℕ => f (y ⊓ n • x₀))4344lemma witFun_isLUB {f : OrderBoundedHom X Y}45 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}46 (_hx₀ : 0 ≤ x₀) (_hy : 0 ≤ y) :47 IsLUB (Set.range fun n : ℕ => f (y ⊓ n • x₀)) (witFun f x₀ y) := by48 refine isLUB_csSup ⟨_, 0, rfl⟩ ⟨f y, ?_⟩49 rintro _ ⟨n, rfl⟩50 exact f_mono_of_nonneg hf inf_le_left5152lemma witFun_le_f {f : OrderBoundedHom X Y}53 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}54 (hx₀ : 0 ≤ x₀) (hy : 0 ≤ y) : witFun f x₀ y ≤ f y := by55 apply (witFun_isLUB hf hx₀ hy).256 rintro _ ⟨n, rfl⟩57 exact f_mono_of_nonneg hf inf_le_left5859lemma witFun_nonneg {f : OrderBoundedHom X Y}60 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}61 (hx₀ : 0 ≤ x₀) (hy : 0 ≤ y) : 0 ≤ witFun f x₀ y := by62 refine (witFun_isLUB hf hx₀ hy).1 ⟨0, ?_⟩63 change f (y ⊓ (0 : ℕ) • x₀) = 064 rw [zero_nsmul, inf_of_le_right hy]65 exact map_zero f.toLinearMap6667lemma witFun_eq_at {f : OrderBoundedHom X Y}68 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :69 witFun f x₀ x₀ = f x₀ := by70 refine le_antisymm (witFun_le_f hf hx₀ hx₀) ?_71 refine (witFun_isLUB hf hx₀ hx₀).1 ⟨1, ?_⟩72 change f (x₀ ⊓ (1 : ℕ) • x₀) = f x₀73 rw [one_nsmul, inf_idem]7475lemma witFun_zero_of_disjoint {f : OrderBoundedHom X Y}76 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}77 (hx₀ : 0 ≤ x₀) (hy : 0 ≤ y) (hd : y ⊓ x₀ = 0) :78 witFun f x₀ y = 0 := by79 have hyn : ∀ n : ℕ, y ⊓ n • x₀ = 0 := by80 intro n81 induction n with82 | zero => rw [zero_nsmul, inf_of_le_right hy]83 | succ n ih =>84 have hle : y ⊓ (n + 1) • x₀ ≤ y ⊓ (n • x₀) + y ⊓ x₀ := by85 rw [succ_nsmul]86 exact inf_le_inf_add_inf_of_nonneg y (n • x₀) x₀ hy87 (nsmul_nonneg hx₀ n) hx₀88 rw [ih, hd, add_zero] at hle89 exact le_antisymm hle (le_inf hy (nsmul_nonneg hx₀ (n + 1)))90 refine le_antisymm ?_ (witFun_nonneg hf hx₀ hy)91 apply (witFun_isLUB hf hx₀ hy).292 rintro _ ⟨n, rfl⟩93 change f (y ⊓ n • x₀) ≤ 094 rw [hyn n]95 exact (map_zero f.toLinearMap).le9697lemma witFun_add {f : OrderBoundedHom X Y}98 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y₁ y₂ : X}99 (hx₀ : 0 ≤ x₀) (hy₁ : 0 ≤ y₁) (hy₂ : 0 ≤ y₂) :100 witFun f x₀ (y₁ + y₂) = witFun f x₀ y₁ + witFun f x₀ y₂ := by101 refine le_antisymm ?_ ?_102 · apply (witFun_isLUB hf hx₀ (add_nonneg hy₁ hy₂)).2103 rintro _ ⟨n, rfl⟩104 have hznn : 0 ≤ (y₁ + y₂) ⊓ n • x₀ :=105 le_inf (add_nonneg hy₁ hy₂) (nsmul_nonneg hx₀ n)106 have hzy : (y₁ + y₂) ⊓ n • x₀ ≤ y₁ + y₂ := inf_le_left107 obtain ⟨z₁, z₂, hz₁nn, hz₁y₁, hz₂nn, hz₂y₂, hzeq⟩ :=108 riesz_decomposition (x := (y₁ + y₂) ⊓ n • x₀) y₁ y₂ hznn hy₁ hy₂ hzy109 have hz_le : (y₁ + y₂) ⊓ n • x₀ ≤ n • x₀ := inf_le_right110 have hz₁_nx : z₁ ≤ n • x₀ :=111 ((le_add_of_nonneg_right hz₂nn).trans hzeq.symm.le).trans hz_le112 have hz₂_nx : z₂ ≤ n • x₀ :=113 ((le_add_of_nonneg_left hz₁nn).trans hzeq.symm.le).trans hz_le114 have hz₁_inf : z₁ ≤ y₁ ⊓ n • x₀ := le_inf hz₁y₁ hz₁_nx115 have hz₂_inf : z₂ ≤ y₂ ⊓ n • x₀ := le_inf hz₂y₂ hz₂_nx116 calc f ((y₁ + y₂) ⊓ n • x₀)117 = f (z₁ + z₂) := by rw [hzeq]118 _ = f z₁ + f z₂ := map_add f.toLinearMap z₁ z₂119 _ ≤ f (y₁ ⊓ n • x₀) + f (y₂ ⊓ n • x₀) :=120 add_le_add (f_mono_of_nonneg hf hz₁_inf) (f_mono_of_nonneg hf hz₂_inf)121 _ ≤ witFun f x₀ y₁ + witFun f x₀ y₂ :=122 add_le_add ((witFun_isLUB hf hx₀ hy₁).1 ⟨n, rfl⟩)123 ((witFun_isLUB hf hx₀ hy₂).1 ⟨n, rfl⟩)124 · have step1 : ∀ n m : ℕ,125 f (y₁ ⊓ n • x₀) + f (y₂ ⊓ m • x₀) ≤ witFun f x₀ (y₁ + y₂) := by126 intro n m127 have hsum : (y₁ ⊓ n • x₀) + (y₂ ⊓ m • x₀) ≤ (y₁ + y₂) ⊓ ((n + m) • x₀) := by128 refine le_inf (add_le_add inf_le_left inf_le_left) ?_129 rw [add_nsmul]; exact add_le_add inf_le_right inf_le_right130 calc f (y₁ ⊓ n • x₀) + f (y₂ ⊓ m • x₀)131 = f ((y₁ ⊓ n • x₀) + (y₂ ⊓ m • x₀)) :=132 (map_add f.toLinearMap _ _).symm133 _ ≤ f ((y₁ + y₂) ⊓ (n + m) • x₀) := f_mono_of_nonneg hf hsum134 _ ≤ witFun f x₀ (y₁ + y₂) :=135 (witFun_isLUB hf hx₀ (add_nonneg hy₁ hy₂)).1 ⟨n + m, rfl⟩136 have step2 : ∀ m : ℕ,137 witFun f x₀ y₁ + f (y₂ ⊓ m • x₀) ≤ witFun f x₀ (y₁ + y₂) := by138 intro m139 have hub : witFun f x₀ (y₁ + y₂) - f (y₂ ⊓ m • x₀) ∈140 upperBounds (Set.range fun n : ℕ => f (y₁ ⊓ n • x₀)) := by141 rintro _ ⟨n, rfl⟩142 exact le_sub_iff_add_le.mpr (step1 n m)143 exact le_sub_iff_add_le.mp ((witFun_isLUB hf hx₀ hy₁).2 hub)144 have hub : witFun f x₀ (y₁ + y₂) - witFun f x₀ y₁ ∈145 upperBounds (Set.range fun n : ℕ => f (y₂ ⊓ n • x₀)) := by146 rintro _ ⟨m, rfl⟩147 rw [le_sub_iff_add_le, add_comm]; exact step2 m148 have h := (witFun_isLUB hf hx₀ hy₂).2 hub149 have h2 := le_sub_iff_add_le.mp h150 rwa [add_comm] at h2151152/-- The witness linear map for `f` and `x₀ ≥ 0`. -/153noncomputable def witLin {f : OrderBoundedHom X Y}154 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :155 X →ₗ[ℝ] Y := by156 haveI : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice157 exact Positive.extension158 (fun y hy => witFun_nonneg hf hx₀ hy)159 (fun y₁ y₂ hy₁ hy₂ => witFun_add hf hx₀ hy₁ hy₂)160161lemma witLin_apply_nonneg {f : OrderBoundedHom X Y}162 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X}163 (hx₀ : 0 ≤ x₀) (hy : 0 ≤ y) : witLin hf hx₀ y = witFun f x₀ y := by164 have : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice165 exact Positive.extension_nonneg _ _ hy166167lemma witLin_positive {f : OrderBoundedHom X Y}168 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :169 Positive (witLin hf hx₀) := by170 have : IsVLArchimedean Y := IsVLArchimedean_of_sigmaConditionallyCompleteLattice171 exact Positive.extension_positive _ _172173/-- The witness operator as an `OrderBoundedHom`. -/174noncomputable def witOp {f : OrderBoundedHom X Y}175 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :176 OrderBoundedHom X Y :=177 ⟨witLin hf hx₀, Positive.isOrderBounded (witLin_positive hf hx₀)⟩178179lemma witOp_apply {f : OrderBoundedHom X Y}180 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) (y : X) :181 witOp hf hx₀ y = witLin hf hx₀ y := rfl182183lemma witOp_nonneg {f : OrderBoundedHom X Y}184 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :185 (0 : OrderBoundedHom X Y) ≤ witOp hf hx₀ :=186 le_iff.mpr fun y hy => by187 have h := witLin_positive hf hx₀ y hy188 change (0 : Y) ≤ witLin hf hx₀ y at h189 simpa only [obZero_apply, witOp_apply] using h190191lemma witOp_le_f {f : OrderBoundedHom X Y}192 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :193 witOp hf hx₀ ≤ f :=194 le_iff.mpr fun y hy => by195 change witLin hf hx₀ y ≤ f y196 rw [witLin_apply_nonneg hf hx₀ hy]197 exact witFun_le_f hf hx₀ hy198199lemma witOp_apply_self {f : OrderBoundedHom X Y}200 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ : X} (hx₀ : 0 ≤ x₀) :201 witOp hf hx₀ x₀ = f x₀ := by202 change witLin hf hx₀ x₀ = f x₀203 rw [witLin_apply_nonneg hf hx₀ hx₀, witFun_eq_at hf hx₀]204205lemma witOp_apply_disjoint {f : OrderBoundedHom X Y}206 (hf : (0 : OrderBoundedHom X Y) ≤ f) {x₀ y : X} (hx₀ : 0 ≤ x₀)207 (hy : 0 ≤ y) (hd : y ⊓ x₀ = 0) : witOp hf hx₀ y = 0 := by208 change witLin hf hx₀ y = 0209 rw [witLin_apply_nonneg hf hx₀ hy, witFun_zero_of_disjoint hf hx₀ hy hd]210211212end PL1.PrincipalIdealDual213