PL1/LatticeBridge.lean

All source files · Download exact source

SHA-256: f8222f4351f5044bc658e3132232b5b53a3883478fcee2122885a99956cee35b

1import PL1.LatticeDefinitions2import BanLat.Normed3import Mathlib.Analysis.Normed.Module.Seminorm.Norm4import Mathlib.Analysis.Normed.Operator.Basic5import Mathlib.Order.Lattice67/-!8Transporting a Banach lattice norm along a continuous linear equivalence shows9that the renorming obstruction covers target lattices in every universe.10-/1112noncomputable section1314universe u v1516namespace PL11718variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]19  {F : Type v} [NormedAddCommGroup F] [Lattice F]20  [IsOrderedAddMonoid F] [BanachLattice F]2122/-- Any real linear Banach-space isomorphism with a Banach lattice pulls back23an equivalent solid lattice norm, irrespective of the target's universe. -/24theorem hasEquivalentRealLatticeNorm_of_continuousLinearEquiv25    (e : E ≃L[ℝ] F) : HasEquivalentRealLatticeNorm E := by26  let : Lattice E := e.toEquiv.lattice27  let : IsOrderedAddMonoid E := {28    add_le_add_left := by29      intro x y h z30      change e (x + z) ≤ e (y + z)31      change e x ≤ e y at h32      simpa only [map_add] using add_le_add h (le_refl (e z)) }33  let : PosSMulMono ℝ E := {34    smul_le_smul_of_nonneg_left := by35      intro a ha x y h36      change e (a • x) ≤ e (a • y)37      change e x ≤ e y at h38      simpa only [map_smul] using smul_le_smul_of_nonneg_left h ha }39  have h_abs (x : E) : e |x| = |e x| := by40    change e (e.symm (e x ⊔ e (-x))) = |e x|41    simp only [e.apply_symm_apply, map_neg, abs]42  refine ⟨inferInstance, inferInstance, inferInstance,43    (normSeminorm ℝ F).comp e.toLinearMap, ?_,44    (‖e.symm.toContinuousLinearMap‖ + 1)⁻¹,45    ‖e.toContinuousLinearMap‖ + 1, ?_, ?_, ?_⟩46  · intro x y h47    change ‖e x‖ ≤ ‖e y‖48    apply norm_le_norm_of_abs_le_abs49    change e |x| ≤ e |y| at h50    simpa only [h_abs] using h51  · positivity52  · positivity53  · intro x54    change (‖e.symm.toContinuousLinearMap‖ + 1)⁻¹ * ‖x‖ ≤ ‖e x‖ ∧55      ‖e x‖ ≤ (‖e.toContinuousLinearMap‖ + 1) * ‖x‖56    constructor57    · have h := e.symm.toContinuousLinearMap.le_opNorm (e x)58      have hbound : ‖x‖ ≤ (‖e.symm.toContinuousLinearMap‖ + 1) * ‖e x‖ := by59        simpa only [ContinuousLinearEquiv.coe_coe, e.symm_apply_apply] using60          h.trans (mul_le_mul_of_nonneg_right (le_add_of_nonneg_right zero_le_one)61            (norm_nonneg (e x)))62      have hpos : 0 < ‖e.symm.toContinuousLinearMap‖ + 1 := by positivity63      rw [inv_mul_eq_div, div_le_iff₀ hpos]64      simpa only [mul_comm] using hbound65    · exact (e.toContinuousLinearMap.le_opNorm x).trans66        (mul_le_mul_of_nonneg_right (le_add_of_nonneg_right zero_le_one) (norm_nonneg x))6768/-- Negating the renorming predicate rules out every real Banach lattice69target, with no restriction on its carrier universe. -/70theorem not_nonempty_continuousLinearEquiv_of_not_hasEquivalentRealLatticeNorm71    (hE : ¬ HasEquivalentRealLatticeNorm E) : ¬ Nonempty (E ≃L[ℝ] F) := by72  rintro ⟨e⟩73  exact hE (hasEquivalentRealLatticeNorm_of_continuousLinearEquiv e)7475end PL176