BanLat/Dual.lean
All source files · Download exact source
SHA-256: 9d2254f8c8dab409a223ffa01e7a66cf044278039c82f995c286ad2e38f65cd3
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Operators.Regular6import BanLat.Operators.RieszKantorovich7import Mathlib.Analysis.Convex.Cone.Dual89/-!10# The order dual and strong dual of a vector or Banach lattice1112The **order dual** `OrderDualSpace X` of a vector lattice `X` is the space of order13bounded real-valued linear functionals on `X`. Since `ℝ` is order complete, the14Riesz–Kantorovich machinery equips it with a canonical order complete vector15lattice structure. The **strong dual** `StrongDual ℝ X` of a normed vector lattice16`X` is the mathlib abbreviation for the space `X →L[ℝ] ℝ` of continuous linear17functionals. For a Banach lattice the two duals coincide as sets — every18continuous functional is order bounded and every order bounded functional is19automatically continuous — and the strong dual inherits the structure of a20Banach lattice.21-/2223/-! ### The order dual -/2425/-- The **order dual** of a vector lattice: order bounded real-valued26linear functionals. -/27abbrev OrderDualSpace (X : Type*) [AddCommGroup X] [Lattice X]28 [IsOrderedAddMonoid X] [VectorLattice X] : Type _ :=29 OrderBoundedHom X ℝ3031namespace OrderDualSpace3233variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]34 [VectorLattice X]3536/-- Order on the order dual: `φ ≤ ψ` iff `φ x ≤ ψ x` for all positive `x`. -/37theorem le_iff {φ ψ : OrderDualSpace X} :38 φ ≤ ψ ↔ ∀ x : X, 0 ≤ x → φ x ≤ ψ x :=39 OrderBoundedHom.le_iff4041/-- A dual element is positive iff it sends positive elements of `X` to42non-negative reals. -/43theorem nonneg_iff {φ : OrderDualSpace X} :44 0 ≤ φ ↔ ∀ x : X, 0 ≤ x → 0 ≤ φ x :=45 OrderBoundedHom.le_iff4647/-- Riesz–Kantorovich: positive part of a dual functional at a positive48element is the supremum of `φ y` over `0 ≤ y ≤ x`. -/49theorem isLUB_posPart_apply {φ : OrderDualSpace X} {x : X} (hx : 0 ≤ x) :50 IsLUB {r : ℝ | ∃ y, 0 ≤ y ∧ y ≤ x ∧ r = φ y} (φ⁺ x) :=51 OrderBoundedHom.isLUB_posPart_apply hx5253/-- Negative part of a dual functional at a positive element. -/54theorem isLUB_negPart_apply {φ : OrderDualSpace X} {x : X} (hx : 0 ≤ x) :55 IsLUB {r : ℝ | ∃ y, 0 ≤ y ∧ y ≤ x ∧ r = -(φ y)} (φ⁻ x) :=56 OrderBoundedHom.isLUB_negPart_apply hx5758/-- Modulus of a dual functional at a positive element. -/59theorem isLUB_abs_apply {φ : OrderDualSpace X} {x : X} (hx : 0 ≤ x) :60 IsLUB {r : ℝ | ∃ y, |y| ≤ x ∧ r = |φ y|} (|φ| x) :=61 OrderBoundedHom.isLUB_abs_apply hx6263/-- Riesz–Kantorovich formula for the supremum of two dual functionals. -/64theorem isLUB_sup_apply {φ ψ : OrderDualSpace X} {x : X} (hx : 0 ≤ x) :65 IsLUB66 {r : ℝ | ∃ y z, 0 ≤ y ∧ 0 ≤ z ∧ y + z = x ∧ r = φ y + ψ z}67 ((φ ⊔ ψ) x) :=68 OrderBoundedHom.isLUB_sup_apply hx6970/-- Riesz–Kantorovich formula for the infimum of two dual functionals. -/71theorem isGLB_inf_apply {φ ψ : OrderDualSpace X} {x : X} (hx : 0 ≤ x) :72 IsGLB73 {r : ℝ | ∃ y z, 0 ≤ y ∧ 0 ≤ z ∧ y + z = x ∧ r = φ y + ψ z}74 ((φ ⊓ ψ) x) :=75 OrderBoundedHom.isGLB_inf_apply hx7677/-- Every order dual element is regular: it can be written as a difference of78two positive functionals. -/79theorem isRegularOp (φ : OrderDualSpace X) :80 IsRegularOp φ.toLinearMap :=81 IsOrderBounded.isRegularOp φ.isOrderBounded'8283variable (X) in84/-- The order dual separates points of `X`: every nonzero element is detected by85some order bounded functional. -/86def SeparatesPoints : Prop :=87 ∀ x : X, (∀ φ : OrderDualSpace X, φ x = 0) → x = 08889/-- Suprema in the order dual are supplied by the Riesz-Kantorovich90order-completeness theorem for order bounded operators. -/91noncomputable instance instSupSet : SupSet (OrderDualSpace X) where92 sSup S := by93 classical94 exact if h : S.Nonempty ∧ BddAbove S then95 (OrderBoundedHom.exists_isLUB h.1 h.2).choose96 else 09798/-- The chosen supremum in the order dual is the least upper bound of every99non-empty bounded-above set. -/100theorem isLUB_sSup (S : Set (OrderDualSpace X)) (hbdd : BddAbove S)101 (hne : S.Nonempty) : IsLUB S (sSup S) := by102 classical103 change IsLUB S (if h : S.Nonempty ∧ BddAbove S then104 (OrderBoundedHom.exists_isLUB h.1 h.2).choose105 else 0)106 rw [dif_pos ⟨hne, hbdd⟩]107 exact (OrderBoundedHom.exists_isLUB hne hbdd).choose_spec108109/-- The order dual is conditionally complete. -/110noncomputable instance instConditionallyCompleteLattice :111 ConditionallyCompleteLattice (OrderDualSpace X) :=112 conditionallyCompleteLatticeOfLatticeOfsSup _ isLUB_sSup113114end OrderDualSpace115116/-! ### The strong dual -/117118namespace StrongDual119120section NormedVectorLattice121122variable {X : Type*} [NormedAddCommGroup X] [Lattice X]123 [IsOrderedAddMonoid X] [NormedVectorLattice X]124125/-- Every continuous linear functional on a normed vector lattice is order126bounded. -/127theorem isOrderBounded (φ : StrongDual ℝ X) :128 IsOrderBounded φ.toLinearMap := by129 intro x hx130 refine ⟨‖φ‖ * ‖x‖, mul_nonneg (norm_nonneg _) (norm_nonneg _), fun z hz => ?_⟩131 have hzx : ‖z‖ ≤ ‖x‖ :=132 norm_le_norm_of_abs_le_abs (by rw [abs_of_nonneg hx]; exact hz)133 have h1 : |φ.toLinearMap z| = ‖φ z‖ := (Real.norm_eq_abs _).symm134 rw [h1]135 exact (φ.le_opNorm z).trans (by gcongr)136137/-- The order bounded functional underlying a continuous linear functional. -/138def toOrderDualSpace (φ : StrongDual ℝ X) : OrderDualSpace X where139 toLinearMap := φ.toLinearMap140 isOrderBounded' := isOrderBounded φ141142@[simp]143theorem toOrderDualSpace_apply (φ : StrongDual ℝ X) (x : X) :144 toOrderDualSpace φ x = φ x := rfl145146/-- Bundling `toOrderDualSpace` as a real-linear map. -/147def toOrderDualSpaceLinear : StrongDual ℝ X →ₗ[ℝ] OrderDualSpace X where148 toFun := toOrderDualSpace149 map_add' _ _ := by ext; rfl150 map_smul' _ _ := by ext; rfl151152/-- Order on the strong dual, transported through the order dual. -/153instance instLE : LE (StrongDual ℝ X) where154 le f g := toOrderDualSpace f ≤ toOrderDualSpace g155156instance instLT : LT (StrongDual ℝ X) where157 lt f g := toOrderDualSpace f < toOrderDualSpace g158159/-- Order on the strong dual: `φ ≤ ψ` iff `φ x ≤ ψ x` for all positive `x`. -/160theorem le_iff {φ ψ : StrongDual ℝ X} :161 φ ≤ ψ ↔ ∀ x : X, 0 ≤ x → φ x ≤ ψ x := by162 change toOrderDualSpace φ ≤ toOrderDualSpace ψ ↔ ∀ x : X, 0 ≤ x → φ x ≤ ψ x163 simpa [toOrderDualSpace_apply] using OrderDualSpace.le_iff (φ := toOrderDualSpace φ)164 (ψ := toOrderDualSpace ψ)165166/-- A continuous linear functional is positive iff it sends positive elements167of `X` to non-negative reals. -/168theorem nonneg_iff {φ : StrongDual ℝ X} :169 0 ≤ φ ↔ ∀ x : X, 0 ≤ x → 0 ≤ φ x := by170 simpa using (le_iff (φ := 0) (ψ := φ))171172/-- A positive continuous linear functional is non-negative on positive elements. -/173theorem apply_nonneg_of_nonneg {φ : StrongDual ℝ X}174 (hφ : 0 ≤ φ) {x : X} (hx : 0 ≤ x) : 0 ≤ φ x :=175 (nonneg_iff.mp hφ) x hx176177/-- A positive continuous linear functional is monotone. -/178theorem apply_le_apply_of_nonneg {φ : StrongDual ℝ X}179 (hφ : 0 ≤ φ) {x y : X} (hxy : x ≤ y) : φ x ≤ φ y :=180 (Positive.monotone_iff.mpr (nonneg_iff.mp hφ)) hxy181182/-- A positive continuous linear functional is dominated by its value on the modulus. -/183theorem abs_apply_le_apply_abs {φ : StrongDual ℝ X}184 (hφ : 0 ≤ φ) (x : X) : |φ x| ≤ φ |x| :=185 Positive.abs_le_map_abs (nonneg_iff.mp hφ) x186187private theorem toOrderDualSpace_injective :188 Function.Injective (toOrderDualSpace (X := X)) := by189 intro f g h190 ext x191 have := congrArg (fun (ψ : OrderDualSpace X) => ψ x) h192 simpa using this193194private theorem toOrderDualSpace_le {f g : StrongDual ℝ X} :195 toOrderDualSpace f ≤ toOrderDualSpace g ↔ f ≤ g := Iff.rfl196197private theorem toOrderDualSpace_lt {f g : StrongDual ℝ X} :198 toOrderDualSpace f < toOrderDualSpace g ↔ f < g := Iff.rfl199200end NormedVectorLattice201202section WeakConvergence203204variable {X : Type*} [NormedAddCommGroup X] [Lattice X]205 [IsOrderedAddMonoid X] [NormedVectorLattice X]206207/-- Every positive element of a normed vector lattice attains its norm at a208positive continuous linear functional of norm at most one. -/209theorem exists_positive_dual_norming {x : X} (hx : 0 ≤ x) :210 ∃ φ : StrongDual ℝ X, 0 ≤ φ ∧ ‖φ‖ ≤ 1 ∧ φ x = ‖x‖ := by211 by_cases hx0 : x = 0212 · refine ⟨0, ?_, by simp, by simp [hx0]⟩213 exact nonneg_iff.mpr fun _ _ => by simp214 · let N : X → ℝ := fun y => ‖y⁺‖215 have hN_hom : ∀ c : ℝ, 0 < c → ∀ y : X, N (c • y) = c * N y := by216 intro c hc y217 simp [N, posPart_smul_nonneg hc.le y, norm_smul, Real.norm_of_nonneg hc.le]218 have hN_add : ∀ y z : X, N (y + z) ≤ N y + N z := by219 intro y z220 have hle : |(y + z)⁺| ≤ |y⁺ + z⁺| := by221 rw [abs_of_nonneg (posPart_nonneg (y + z)),222 abs_of_nonneg (add_nonneg (posPart_nonneg y) (posPart_nonneg z))]223 exact posPart_add_le y z224 exact (norm_le_norm_of_abs_le_abs hle).trans (norm_add_le y⁺ z⁺)225 let p : Subspace ℝ X := ℝ ∙ x226 let coord : StrongDual ℝ p := ContinuousLinearEquiv.coord ℝ x hx0227 let f : p →L[ℝ] ℝ := (‖x‖ : ℝ) • coord228 have hf_le : ∀ y : (⟨p, f⟩ : X →ₗ.[ℝ] ℝ).domain,229 (⟨p, f⟩ : X →ₗ.[ℝ] ℝ) y ≤ N y := by230 intro y231 let a : ℝ := coord y232 have hy_eq : (y : X) = a • x := by233 dsimp [a, coord]234 exact (congrArg Subtype.val235 ((ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ x hx0).apply_symm_apply y)).symm236 by_cases ha : 0 ≤ a237 · have hpos : ((y : X))⁺ = a • x := by238 rw [hy_eq, posPart_smul_nonneg ha, posPart_of_nonneg hx]239 simp [f, a, N, hpos, norm_smul, Real.norm_of_nonneg ha, mul_comm]240 · have ha' : a ≤ 0 := le_of_not_ge ha241 have hnonpos : (y : X) ≤ 0 := by242 rw [hy_eq]243 exact smul_nonpos_of_nonpos_of_nonneg ha' hx244 have hpos : ((y : X))⁺ = 0 := posPart_eq_zero.mpr hnonpos245 have hleft : (⟨p, f⟩ : X →ₗ.[ℝ] ℝ) y = ‖x‖ * a := by246 simp [f, a]247 rw [hleft]248 change ‖x‖ * a ≤ ‖((y : X))⁺‖249 rw [hpos, norm_zero]250 exact mul_nonpos_of_nonneg_of_nonpos (norm_nonneg x) ha'251 obtain ⟨g, hg_eq, hg_le⟩ :=252 exists_extension_of_le_sublinear (⟨p, f⟩ : X →ₗ.[ℝ] ℝ) N hN_hom hN_add hf_le253 have hg_abs : ∀ y : X, |g y| ≤ ‖y‖ := by254 intro y255 refine abs_le.mpr ⟨?_, ?_⟩256 · have hneg := hg_le (-y)257 have hNneg : N (-y) ≤ ‖y‖ := by258 exact (NormedVectorLattice.norm_posPart_le (-y)).trans (by rw [norm_neg])259 have : g (-y) ≤ ‖y‖ := hneg.trans hNneg260 rwa [map_neg, neg_le] at this261 · exact (hg_le y).trans (NormedVectorLattice.norm_posPart_le y)262 let φ : StrongDual ℝ X := g.mkContinuous 1 fun y => by263 simpa [one_mul] using hg_abs y264 refine ⟨φ, ?_, ?_, ?_⟩265 · exact nonneg_iff.mpr fun y hy => by266 have hneg := hg_le (-y)267 have hNneg : N (-y) = 0 := by268 simp [N, posPart_eq_zero.mpr (neg_nonpos.mpr hy)]269 rw [hNneg, map_neg] at hneg270 simpa [φ] using (show 0 ≤ g y by linarith)271 · exact g.mkContinuous_norm_le zero_le_one fun y => by272 simpa [one_mul] using hg_abs y273 · have hxmem : x ∈ p := Submodule.mem_span_singleton_self x274 have hval := hg_eq (⟨x, hxmem⟩ : (⟨p, f⟩ : X →ₗ.[ℝ] ℝ).domain)275 have hcoord : coord (⟨x, hxmem⟩ : p) = 1 := by276 change (ContinuousLinearEquiv.coord ℝ x hx0) (⟨x, hxmem⟩ : ℝ ∙ x) = 1277 exact ContinuousLinearEquiv.coord_self (𝕜 := ℝ) x hx0278 simpa [φ, f, coord, hcoord] using hval279280/-- **Dini's theorem**: a monotone net in a normed lattice that converges weakly281converges in norm. -/282theorem tendsto_of_monotone_weak_tendsto {ι : Type*} [Preorder ι]283 [IsDirected ι (· ≤ ·)] [Nonempty ι] {u : ι → X} {x : X}284 (hmono : Monotone u ∨ Antitone u)285 (hweak : Filter.Tendsto (fun i => (toWeakSpace ℝ X) (u i)) Filter.atTop286 (nhds ((toWeakSpace ℝ X) x))) :287 Filter.Tendsto u Filter.atTop (nhds x) :=288 NormedVectorLattice.tendsto_of_monotone_weak_tendsto hmono hweak289290end WeakConvergence291292section BanachLattice293294variable {X : Type*} [NormedAddCommGroup X] [Lattice X]295 [IsOrderedAddMonoid X] [BanachLattice X]296297/-- For a Banach lattice, every order bounded functional is continuous. -/298noncomputable def ofOrderDualSpace (f : OrderDualSpace X) : StrongDual ℝ X :=299 ⟨f.toLinearMap, IsOrderBounded.continuous f.isOrderBounded'⟩300301@[simp]302theorem ofOrderDualSpace_apply (f : OrderDualSpace X) (x : X) :303 ofOrderDualSpace f x = f x := rfl304305/-- For a Banach lattice, the order dual and the strong dual are linearly306equivalent: continuous functionals are exactly the order bounded ones. -/307noncomputable def equivOrderDualSpace : StrongDual ℝ X ≃ₗ[ℝ] OrderDualSpace X where308 toFun := toOrderDualSpace309 invFun := ofOrderDualSpace310 left_inv _ := by ext; rfl311 right_inv _ := by ext; rfl312 map_add' _ _ := by ext; rfl313 map_smul' _ _ := by ext; rfl314315noncomputable instance instMax : Max (StrongDual ℝ X) where316 max f g := ofOrderDualSpace (toOrderDualSpace f ⊔ toOrderDualSpace g)317318noncomputable instance instMin : Min (StrongDual ℝ X) where319 min f g := ofOrderDualSpace (toOrderDualSpace f ⊓ toOrderDualSpace g)320321private theorem toOrderDualSpace_sup (f g : StrongDual ℝ X) :322 toOrderDualSpace (f ⊔ g) = toOrderDualSpace f ⊔ toOrderDualSpace g := by323 ext x; rfl324325private theorem toOrderDualSpace_inf (f g : StrongDual ℝ X) :326 toOrderDualSpace (f ⊓ g) = toOrderDualSpace f ⊓ toOrderDualSpace g := by327 ext x; rfl328329/-- The induced lattice structure on the strong dual: `φ ≤ ψ` iff `φ x ≤ ψ x`330for all positive `x`, with sup/inf transported from the order dual. -/331noncomputable instance instLattice : Lattice (StrongDual ℝ X) :=332 toOrderDualSpace_injective.lattice _ toOrderDualSpace_le333 toOrderDualSpace_lt toOrderDualSpace_sup toOrderDualSpace_inf334335/-- Suprema in the strong dual are transported from the order dual. -/336noncomputable instance instSupSet : SupSet (StrongDual ℝ X) where337 sSup S := ofOrderDualSpace (sSup (toOrderDualSpace '' S : Set (OrderDualSpace X)))338339/-- The chosen supremum in the strong dual is the least upper bound of every340non-empty bounded-above set. -/341theorem isLUB_sSup (S : Set (StrongDual ℝ X)) (hbdd : BddAbove S)342 (hne : S.Nonempty) : IsLUB S (sSup S) := by343 change IsLUB S (ofOrderDualSpace344 (sSup (toOrderDualSpace '' S : Set (OrderDualSpace X))))345 have hne' : (toOrderDualSpace '' S : Set (OrderDualSpace X)).Nonempty :=346 hne.image _347 have hbdd' : BddAbove (toOrderDualSpace '' S : Set (OrderDualSpace X)) := by348 obtain ⟨u, hu⟩ := hbdd349 exact ⟨toOrderDualSpace u, by350 rintro _ ⟨v, hv, rfl⟩351 exact hu hv⟩352 have hLUB' := OrderDualSpace.isLUB_sSup353 (toOrderDualSpace '' S : Set (OrderDualSpace X)) hbdd' hne'354 have hround : toOrderDualSpace355 (ofOrderDualSpace (sSup (toOrderDualSpace '' S : Set (OrderDualSpace X)))) =356 sSup (toOrderDualSpace '' S : Set (OrderDualSpace X)) := by357 ext x358 rfl359 constructor360 · intro a ha361 change toOrderDualSpace a ≤ toOrderDualSpace362 (ofOrderDualSpace (sSup (toOrderDualSpace '' S : Set (OrderDualSpace X))))363 rw [hround]364 exact hLUB'.1 ⟨a, ha, rfl⟩365 · intro u hu366 change toOrderDualSpace367 (ofOrderDualSpace (sSup (toOrderDualSpace '' S : Set (OrderDualSpace X)))) ≤368 toOrderDualSpace u369 rw [hround]370 exact hLUB'.2 (by371 rintro _ ⟨a, ha, rfl⟩372 exact hu ha)373374/-- The strong dual is conditionally complete. -/375noncomputable instance instConditionallyCompleteLattice :376 ConditionallyCompleteLattice (StrongDual ℝ X) :=377 conditionallyCompleteLatticeOfLatticeOfsSup _ isLUB_sSup378379private theorem toOrderDualSpace_add (f g : StrongDual ℝ X) :380 toOrderDualSpace (f + g) = toOrderDualSpace f + toOrderDualSpace g := by381 ext; rfl382383private theorem toOrderDualSpace_smul (r : ℝ) (f : StrongDual ℝ X) :384 toOrderDualSpace (r • f) = r • toOrderDualSpace f := by385 ext; rfl386387/-- The strong dual of a Banach lattice is an ordered additive group. -/388instance instIsOrderedAddMonoid : IsOrderedAddMonoid (StrongDual ℝ X) where389 add_le_add_left f g hfg c := by390 change toOrderDualSpace f ≤ toOrderDualSpace g at hfg391 change toOrderDualSpace (f + c) ≤ toOrderDualSpace (g + c)392 rw [toOrderDualSpace_add, toOrderDualSpace_add]393 exact IsOrderedAddMonoid.add_le_add_left _ _ hfg c.toOrderDualSpace394395instance instPosSMulMono : PosSMulMono ℝ (StrongDual ℝ X) where396 smul_le_smul_of_nonneg_left {r} hr {f g} hfg := by397 change toOrderDualSpace f ≤ toOrderDualSpace g at hfg398 change toOrderDualSpace (r • f) ≤ toOrderDualSpace (r • g)399 rw [toOrderDualSpace_smul, toOrderDualSpace_smul]400 exact smul_le_smul_of_nonneg_left hfg hr401402/-- The strong dual of a Banach lattice is a vector lattice. -/403noncomputable instance instVectorLattice : VectorLattice (StrongDual ℝ X) where404405private theorem coe_abs_apply (φ : StrongDual ℝ X) (x : X) :406 (|φ| : StrongDual ℝ X) x = |toOrderDualSpace φ| x := rfl407408private theorem abs_apply_le_abs_apply_abs (φ : StrongDual ℝ X) (x : X) :409 |φ x| ≤ (|φ| : StrongDual ℝ X) (|x|) := by410 rw [coe_abs_apply]411 exact (OrderBoundedHom.isLUB_abs_apply (f := toOrderDualSpace φ)412 (abs_nonneg x)).1 ⟨x, le_refl _, rfl⟩413414private theorem abs_apply_nonneg (φ : StrongDual ℝ X) {x : X} (hx : 0 ≤ x) :415 0 ≤ (|φ| : StrongDual ℝ X) x := by416 rw [coe_abs_apply]417 exact (OrderBoundedHom.isLUB_abs_apply (f := toOrderDualSpace φ) hx).1418 ⟨0, by simp [hx], by simp⟩419420/-- For a positive `x`, `|φ| x` is bounded by `‖φ‖ * ‖x‖`. -/421private theorem abs_apply_le_norm_mul (φ : StrongDual ℝ X) {x : X} (hx : 0 ≤ x) :422 (|φ| : StrongDual ℝ X) x ≤ ‖φ‖ * ‖x‖ := by423 rw [coe_abs_apply]424 refine (OrderBoundedHom.isLUB_abs_apply (f := toOrderDualSpace φ) hx).2 ?_425 rintro _ ⟨y, hyx, rfl⟩426 have hy : ‖y‖ ≤ ‖x‖ :=427 norm_le_norm_of_abs_le_abs (by rw [abs_of_nonneg hx]; exact hyx)428 calc |φ y| = ‖φ y‖ := (Real.norm_eq_abs _).symm429 _ ≤ ‖φ‖ * ‖y‖ := φ.le_opNorm y430 _ ≤ ‖φ‖ * ‖x‖ := by gcongr431432/-- The strong dual carries a solid lattice norm: `|φ| ≤ |ψ|` implies433`‖φ‖ ≤ ‖ψ‖`. -/434instance instHasSolidNorm : HasSolidNorm (StrongDual ℝ X) where435 solid {φ ψ} hφψ := by436 refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_437 have h1 : |φ x| ≤ (|φ| : StrongDual ℝ X) (|x|) :=438 abs_apply_le_abs_apply_abs φ x439 have hOD : (|φ| : StrongDual ℝ X) (|x|) ≤ (|ψ| : StrongDual ℝ X) (|x|) := by440 exact le_iff.mp hφψ _ (abs_nonneg x)441 have h2 : (|ψ| : StrongDual ℝ X) (|x|) ≤ ‖ψ‖ * ‖x‖ := by442 have := abs_apply_le_norm_mul ψ (abs_nonneg x)443 rwa [norm_abs_eq_norm] at this444 calc ‖φ x‖ = |φ x| := Real.norm_eq_abs _445 _ ≤ (|ψ| : StrongDual ℝ X) (|x|) := h1.trans hOD446 _ ≤ ‖ψ‖ * ‖x‖ := h2447448/-- The strong dual of a Banach lattice is itself a normed vector lattice. -/449noncomputable instance instNormedVectorLattice :450 NormedVectorLattice (StrongDual ℝ X) where451 norm_smul := norm_smul452453/-- The strong dual of a Banach lattice is a Banach lattice. -/454noncomputable instance instBanachLattice : BanachLattice (StrongDual ℝ X) where455456/-- The dual norm of the modulus equals the dual norm: `‖|φ|‖ = ‖φ‖`. -/457theorem norm_abs (φ : StrongDual ℝ X) : ‖|φ|‖ = ‖φ‖ :=458 le_antisymm459 (HasSolidNorm.solid (by rw [abs_abs]))460 (HasSolidNorm.solid (by rw [abs_abs]))461462/-- For a positive functional, the dual norm is the supremum of `φ x` over the463intersection of the unit ball with the positive cone. -/464theorem norm_of_nonneg {φ : StrongDual ℝ X} (hφ : 0 ≤ φ) :465 ‖φ‖ = sSup ((φ : X → ℝ) '' ({x | ‖x‖ ≤ 1} ∩ {x | 0 ≤ x})) := by466 set S := (φ : X → ℝ) '' ({x | ‖x‖ ≤ 1} ∩ {x | 0 ≤ x})467 have hpos : ∀ {x : X}, 0 ≤ x → 0 ≤ φ x := fun {x} hx =>468 nonneg_iff.mp hφ x hx469 have habs_eq : (|φ| : StrongDual ℝ X) = φ := abs_of_nonneg hφ470 have hub : ∀ s ∈ S, s ≤ ‖φ‖ := by471 rintro _ ⟨x, ⟨hx1, hx0⟩, rfl⟩472 have h1 : ‖φ x‖ ≤ ‖φ‖ * ‖x‖ := φ.le_opNorm x473 have h2 : φ x = ‖φ x‖ := by474 rw [Real.norm_eq_abs, abs_of_nonneg (hpos hx0)]475 rw [h2]476 exact h1.trans (by simpa using mul_le_mul_of_nonneg_left hx1 (norm_nonneg _))477 have hbdd : BddAbove S := ⟨‖φ‖, hub⟩478 have hne : S.Nonempty := ⟨0, 0, ⟨by simp, le_refl _⟩, by simp⟩479 have hsup_nn : 0 ≤ sSup S :=480 Real.sSup_nonneg (by rintro _ ⟨y, ⟨_, hy0⟩, rfl⟩; exact hpos hy0)481 apply le_antisymm482 · refine ContinuousLinearMap.opNorm_le_bound _ hsup_nn fun x => ?_483 -- ‖φ x‖ ≤ φ |x| (positivity)484 have hbound : ‖φ x‖ ≤ φ (|x|) := by485 rw [Real.norm_eq_abs]486 have h := abs_apply_le_abs_apply_abs φ x487 rw [habs_eq] at h; exact h488 by_cases hx0 : x = 0489 · subst hx0490 simp only [map_zero, norm_zero, mul_zero]491 exact le_refl _492 -- normalise493 have hxn : (0 : ℝ) < ‖x‖ := norm_pos_iff.mpr hx0494 set y : X := ‖x‖⁻¹ • |x|495 have hy_nn : 0 ≤ y := smul_nonneg (inv_nonneg.mpr hxn.le) (abs_nonneg x)496 have hy_norm : ‖y‖ ≤ 1 := by497 rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_nonneg hxn.le,498 norm_abs_eq_norm]499 exact (inv_mul_cancel₀ hxn.ne').le500 have hyS : φ y ∈ S := ⟨y, ⟨hy_norm, hy_nn⟩, rfl⟩501 have hyS_le : φ y ≤ sSup S := le_csSup hbdd hyS502 have hφy : φ y = ‖x‖⁻¹ * φ (|x|) := by503 change φ.toLinearMap (‖x‖⁻¹ • |x|) = _504 rw [map_smul]; rfl505 have hφabs : φ (|x|) ≤ ‖x‖ * sSup S := by506 have h1 := mul_le_mul_of_nonneg_left hyS_le hxn.le507 rw [hφy, ← mul_assoc, mul_inv_cancel₀ hxn.ne', one_mul] at h1508 exact h1509 exact hbound.trans (hφabs.trans (by rw [mul_comm]))510 · exact csSup_le hne hub511512/-- For a Banach lattice, the order dual separates points. -/513theorem orderDual_separatesPoints :514 OrderDualSpace.SeparatesPoints X := by515 intro x hx516 refine SeparatingDual.eq_zero_of_forall_dual_eq_zero (R := ℝ) fun f => ?_517 simpa using hx (toOrderDualSpace f)518519end BanachLattice520521end StrongDual522