Import order continuity for free p-convex Banach lattices

LeanPool/FBLOrderContinuity.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026 Raúl E. Pariente-Martín, Pedro Tradacete. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Raúl E. Pariente-Martín, Pedro Tradacete
+-/
+
+
+
+module
+
+public import LeanPool.FBLOrderContinuity.Parameters
+
+/-!
+# Order continuity of induced homomorphisms between free Banach lattices
+
+Source: arxiv:2611.00451, url:https://github.com/pedrotradacete/FBLOrderContinuousLH/tree/ee3cde5070125ff2356b7144ff7a940a8dff2a54
+Authors: Raúl E. Pariente-Martín, Pedro Tradacete, David Muñoz-Lahoz
+Status: verified
+Main declarations: `FBLOrderContinuousLH.intro_infty`, `FBLOrderContinuousLH.intro_poe`,
+  `FBLOrderContinuousLH.cross_parameter_inclusion`
+Tags: banach-lattices, free-banach-lattices, order-continuity, operator-extensions
+MSC: 46B42, 46A40, 47B60
+-/
+
+/-!
+## Attribution and dependency scope
+
+The main formalization is preserved from
+`pedrotradacete/FBLOrderContinuousLH` at
+`ee3cde5070125ff2356b7144ff7a940a8dff2a54` (Apache-2.0).
+The completed proof commit is `167b82ad69724d2ddb2a701fc932e52d445faecc`,
+dated October 30, 2026, 22:05:46 UTC. The accompanying manuscript,
+[arXiv:2611.00451](https://arxiv.org/abs/2611.00451), was submitted on
+October 30 at 23:06:06 UTC. Its declaration on AI use credits GPT-6 Astra
+and GPT-6 Sol for the Lean formalization, under the authors’ mathematical
+direction; this import records AI provenance for the implementation.
+
+David Muñoz-Lahoz’s BanLat at
+`33c4b73fce845c4295614326193d4e52111be762` supplies the additional
+free-lattice, duality, quotient, AM-space representation and functional-calculus
+prerequisites, also under Apache-2.0. The existing BanLat core in
+`LeanPool.OrderClosures` is reused. The added subtype, weak-convergence and finite-product
+modules restore the interfaces needed by this dependency closure without
+copying that core. The original mathematical namespaces and theorem statements
+are retained. The main paper’s acknowledgments credit Timur Oikhberg for
+discussions and a simplification of Lemma 4.11.
+-/

LeanPool/FBLOrderContinuity/BanLat/AMSpace/Basic.lean

@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2026 David Muñoz-Lahoz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Muñoz-Lahoz
+-/
+
+module
+
+/-
+Authors: David Muñoz-Lahoz
+-/
+
+public import LeanPool.FBLOrderContinuity.BanLat.Sublattice
+public import LeanPool.OrderClosures.BanLat.Substructures.Ideal
+public import Mathlib.Order.Filter.AtTopBot.Basic
+
+
+
+/-!
+# AM-spaces
+
+This file introduces AM-spaces and AM-spaces with unit. An `AMSpace` is a
+Banach lattice whose norm satisfies the AM-axiom on disjoint elements. An
+`AMSpaceWithUnit` is an AM-space equipped with a strong order unit whose gauge
+norm agrees with the original norm.
+
+The main structural result is that every principal ideal, equipped with its
+gauge norm, is an AM-space with unit; conversely, in an AM-space with unit,
+the unit generates the whole space as a principal ideal.
+-/
+
+@[expose] public section
+
+/-! ### AM-spaces -/
+
+/-- An **AM-space** is a Banach lattice whose norm satisfies the AM-axiom on
+disjoint elements: if `x ⊓ y = 0`, then `‖x + y‖ = max ‖x‖ ‖y‖`. The
+positivity of `x` and `y` is automatic from `x ⊓ y = 0`. -/
+class AMSpace (X : Type*) [NormedAddCommGroup X] [Lattice X]
+    [IsOrderedAddMonoid X] extends BanachLattice X where
+  norm_add_eq_max_of_inf_eq_zero {x y : X} (hxy : x ⊓ y = 0) :
+    ‖x + y‖ = max ‖x‖ ‖y‖
+
+namespace AMSpace
+
+variable {X : Type*} [NormedAddCommGroup X] [Lattice X]
+  [IsOrderedAddMonoid X] [AMSpace X]
+
+/-- For disjoint elements in an AM-space, the norm of the supremum is the
+maximum of the norms. -/
+theorem norm_sup_eq_max_of_inf_eq_zero {x y : X} (hxy : x ⊓ y = 0) :
+    ‖x ⊔ y‖ = max ‖x‖ ‖y‖ := by
+  have hx : 0 ≤ x := by
+    rw [← hxy]
+    exact inf_le_left
+  have hy : 0 ≤ y := by
+    rw [← hxy]
+    exact inf_le_right
+  have hadd : x + y = x ⊔ y := by
+    calc
+      x + y = x + (y - x)⁺ := by
+        rw [← sub_inf_eq_posPart y x, inf_comm, hxy, sub_zero]
+      _ = x ⊔ y := (sup_eq_add_posPart x y).symm
+  rw [← hadd]
+  exact AMSpace.norm_add_eq_max_of_inf_eq_zero hxy
+
+end AMSpace
+
+/-! ### AM-spaces with unit -/
+
+/-- An **AM-space with unit** is an AM-space equipped with a strong order unit
+whose gauge norm agrees with the original norm. -/
+class AMSpaceWithUnit (X : Type*) [NormedAddCommGroup X] [Lattice X]
+    [IsOrderedAddMonoid X] extends AMSpace X where
+  /-- The distinguished strong order unit. -/
+  unit : X
+  strongOrderUnit_unit : StrongOrderUnit unit
+  norm_eq_gaugeNorm : ∀ x : X, ‖x‖ = OrderIdeal.gaugeNorm unit x
+
+namespace AMSpaceWithUnit
+
+variable {X : Type*} [NormedAddCommGroup X] [Lattice X]
+  [IsOrderedAddMonoid X] [AMSpaceWithUnit X]
+
+/-- The distinguished unit of an AM-space with unit is non-negative. -/
+theorem unit_nonneg : 0 ≤ (AMSpaceWithUnit.unit : X) :=
+  AMSpaceWithUnit.strongOrderUnit_unit.1
+
+/-- In an AM-space with unit, the distinguished unit is a strong order unit. -/
+theorem strongOrderUnit_unit' : StrongOrderUnit (AMSpaceWithUnit.unit : X) :=
+  AMSpaceWithUnit.strongOrderUnit_unit
+
+/-- In an AM-space with unit, the principal ideal generated by the unit is the
+whole space. -/
+theorem principal_unit_eq_top : OrderIdeal.principal (AMSpaceWithUnit.unit : X) = ⊤ :=
+  (OrderIdeal.strongOrderUnit_iff_principal_eq_top.mp
+    AMSpaceWithUnit.strongOrderUnit_unit).2
+
+end AMSpaceWithUnit
+
+/-! ### Principal ideals -/
+
+namespace OrderIdeal
+
+variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]
+  [VectorLattice X]
+
+theorem principal_strongOrderUnit [IsVLArchimedean X] {e : X} (he : 0 ≤ e) :
+    letI : NormedAddCommGroup ↥(principal e) := principalNormedAddCommGroup e
+    letI : Lattice ↥(principal e) := instLatticePrincipal e
+    letI : IsOrderedAddMonoid ↥(principal e) := instIsOrderedAddMonoidPrincipal e
+    letI : NormedVectorLattice ↥(principal e) := principalNormedVectorLattice e
+    StrongOrderUnit (⟨e, self_mem_principal e⟩ : ↥(principal e)) := by
+  let : NormedAddCommGroup ↥(principal e) := principalNormedAddCommGroup e
+  let : Lattice ↥(principal e) := instLatticePrincipal e
+  let : IsOrderedAddMonoid ↥(principal e) := instIsOrderedAddMonoidPrincipal e
+  let : NormedVectorLattice ↥(principal e) := principalNormedVectorLattice e
+  refine ⟨he, ?_⟩
+  intro x
+  obtain ⟨c, hc, hcx⟩ := mem_principal.mp x.2
+  refine ⟨c, hc, ?_⟩
+  change |(x : X)| ≤ c • e
+  rwa [abs_of_nonneg he] at hcx
+
+theorem principal_norm_eq_gaugeNorm_unit [IsVLArchimedean X] {e : X} :
+    letI : NormedAddCommGroup ↥(principal e) := principalNormedAddCommGroup e
+    letI : Lattice ↥(principal e) := instLatticePrincipal e
+    letI : IsOrderedAddMonoid ↥(principal e) := instIsOrderedAddMonoidPrincipal e
+    letI : NormedVectorLattice ↥(principal e) := principalNormedVectorLattice e
+    ∀ x : ↥(principal e),
+      ‖x‖ = gaugeNorm (⟨e, self_mem_principal e⟩ : ↥(principal e)) x := by
+  let : NormedAddCommGroup ↥(principal e) := principalNormedAddCommGroup e
+  let : Lattice ↥(principal e) := instLatticePrincipal e
+  let : IsOrderedAddMonoid ↥(principal e) := instIsOrderedAddMonoidPrincipal e
+  let : NormedVectorLattice ↥(principal e) := principalNormedVectorLattice e
+  intro x
+  change gaugeNorm e (x : X) = gaugeNorm (⟨e, self_mem_principal e⟩ : ↥(principal e)) x
+  rfl
+
+theorem principal_norm_add_eq_max_of_inf_eq_zero [IsVLArchimedean X]
+    {e : X} (he : 0 ≤ e) :
+    letI : NormedAddCommGroup ↥(principal e) := principalNormedAddCommGroup e
+    letI : Lattice ↥(principal e) := instLatticePrincipal e
+    letI : IsOrderedAddMonoid ↥(principal e) := instIsOrderedAddMonoidPrincipal e
+    letI : NormedVectorLattice ↥(principal e) := principalNormedVectorLattice e
+    ∀ {x y : ↥(principal e)}, x ⊓ y = 0 → ‖x + y‖ = max ‖x‖ ‖y‖ := by
+  let : NormedAddCommGroup ↥(principal e) := principalNormedAddCommGroup e
+  let : Lattice ↥(principal e) := instLatticePrincipal e
+  let : IsOrderedAddMonoid ↥(principal e) := instIsOrderedAddMonoidPrincipal e
+  let : NormedVectorLattice ↥(principal e) := principalNormedVectorLattice e
+  intro x y hxy
+  have hx : 0 ≤ x := by rw [← hxy]; exact inf_le_left
+  have hy : 0 ≤ y := by rw [← hxy]; exact inf_le_right
+  have hsum_nonneg : 0 ≤ x + y := add_nonneg hx hy
+  have hsup : x + y = x ⊔ y :=
+    add_eq_sup_of_isVLDisjoint_of_nonneg hx hy (isVLDisjoint_of_inf_eq_zero hxy)
+  apply le_antisymm
+  · let M : ℝ := max ‖x‖ ‖y‖
+    have hM_nonneg : 0 ≤ M := le_max_of_le_left (norm_nonneg x)
+    have hx_bound : (x : X) ≤ M • e := by
+      have hx_abs : |(x : X)| ≤ ‖x‖ • |e| := by
+        change |(x : X)| ≤ gaugeNorm e (x : X) • |e|
+        exact abs_le_gaugeNorm_smul_abs e x.2
+      calc (x : X) ≤ |(x : X)| := le_abs_self _
+        _ ≤ ‖x‖ • |e| := hx_abs
+        _ ≤ M • |e| := smul_le_smul_of_nonneg_right (le_max_left _ _) (abs_nonneg e)
+        _ = M • e := by rw [abs_of_nonneg he]
+    have hy_bound : (y : X) ≤ M • e := by
+      have hy_abs : |(y : X)| ≤ ‖y‖ • |e| := by
+        change |(y : X)| ≤ gaugeNorm e (y : X) • |e|
+        exact abs_le_gaugeNorm_smul_abs e y.2
+      calc (y : X) ≤ |(y : X)| := le_abs_self _
+        _ ≤ ‖y‖ • |e| := hy_abs
+        _ ≤ M • |e| := smul_le_smul_of_nonneg_right (le_max_right _ _) (abs_nonneg e)
+        _ = M • e := by rw [abs_of_nonneg he]
+    have hsum_bound : ((x + y : ↥(principal e)) : X) ≤ M • e := by
+      have hsup_val : (x : X) + (y : X) = (x : X) ⊔ (y : X) := by
+        have hsup_sub :
+            ((x + y : ↥(principal e)) : X) = ((x ⊔ y : ↥(principal e)) : X) :=
+          congrArg Subtype.val hsup
+        change (x : X) + (y : X) = (x : X) ⊔ (y : X) at hsup_sub
+        exact hsup_sub
+      change (x : X) + (y : X) ≤ M • e
+      rw [hsup_val]
+      exact sup_le hx_bound hy_bound
+    change gaugeNorm e ((x + y : ↥(principal e)) : X) ≤ M
+    exact gaugeNorm_le_of_abs_le e hM_nonneg (by
+      rw [abs_of_nonneg (show 0 ≤ ((x + y : ↥(principal e)) : X) from hsum_nonneg),
+        abs_of_nonneg he]
+      exact hsum_bound)
+  · refine max_le ?_ ?_
+    · apply norm_le_norm_of_abs_le_abs
+      rw [abs_of_nonneg hx, abs_of_nonneg hsum_nonneg]
+      exact le_add_of_nonneg_right hy
+    · apply norm_le_norm_of_abs_le_abs
+      rw [abs_of_nonneg hy, abs_of_nonneg hsum_nonneg]
+      exact le_add_of_nonneg_left hx
+
+/-- In an Archimedean vector lattice, a complete principal ideal,
+equipped with its gauge norm and inherited vector lattice structure, is an
+AM-space with unit. -/
+@[reducible]
+noncomputable def principalAMSpaceWithUnit [IsVLArchimedean X] {e : X} (he : 0 ≤ e)
+    (hcomplete :
+      letI : NormedAddCommGroup ↥(principal e) := principalNormedAddCommGroup e
+      CompleteSpace ↥(principal e)) :
+    @AMSpaceWithUnit ↥(principal e)
+      (principalNormedAddCommGroup e)
+      (instLatticePrincipal e)
+      (instIsOrderedAddMonoidPrincipal e) := by
+  letI : NormedAddCommGroup ↥(principal e) := principalNormedAddCommGroup e
+  letI : Lattice ↥(principal e) := instLatticePrincipal e
+  letI : IsOrderedAddMonoid ↥(principal e) := instIsOrderedAddMonoidPrincipal e
+  letI : NormedVectorLattice ↥(principal e) := principalNormedVectorLattice e
+  letI : CompleteSpace ↥(principal e) := hcomplete
+  letI : BanachLattice ↥(principal e) := { }
+  refine { (inferInstance : BanachLattice ↥(principal e)) with
+    unit := ⟨e, self_mem_principal e⟩
+    strongOrderUnit_unit := principal_strongOrderUnit he
+    norm_eq_gaugeNorm := principal_norm_eq_gaugeNorm_unit
+    norm_add_eq_max_of_inf_eq_zero := principal_norm_add_eq_max_of_inf_eq_zero he }
+
+end OrderIdeal