PL1/LatticeRenorming.lean
All source files · Download exact source
SHA-256: 8cd1effbdfa84fa8ce905dadd5ef8ae67be75bc552e4871966b29437e06aca10
1import PL1.LatticeBridge2import Mathlib.Topology.UniformSpace.Equiv3import Mathlib.Topology.Bases45/-!+# Realization of equivalent lattice norms67The predicate in `LatticeDefinitions` is realized by a separate type carrying8the new norm. The equivalence retains the original addition and real action.9No order-completeness or atomicity assertion is used here.10-/1112noncomputable section13open TopologicalSpace14universe u1516namespace PL1.LatticeRenorming1718variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]1920/-- A copy of the original vector space on which a separating seminorm is used21as the norm. Keeping a separate type prevents changing the source norm. -/22def Space (p : Seminorm ℝ E) (_hsep : ∀ x, p x = 0 → x = 0) : Type u := E2324variable (p : Seminorm ℝ E) (hsep : ∀ x, p x = 0 → x = 0)2526instance : AddCommGroup (Space p hsep) := inferInstanceAs (AddCommGroup E)27instance : Module ℝ (Space p hsep) := inferInstanceAs (Module ℝ E)2829instance : NormedAddCommGroup (Space p hsep) :=30 (show AddGroupNorm (Space p hsep) from31 { p.toAddGroupSeminorm with eq_zero_of_map_eq_zero' := hsep }).toNormedAddCommGroup3233@[simp] theorem norm_eq (x : Space p hsep) : ‖x‖ = p x := rfl3435instance : NormedSpace ℝ (Space p hsep) where36 norm_smul_le a x := (map_smul_eq_mul p a x).le3738/-- The unchanged linear coordinates between the original and renormed spaces. -/39def linearEquiv : E ≃ₗ[ℝ] Space p hsep :=40 { toFun := fun x => x41 invFun := fun x => x42 left_inv := fun _ => rfl43 right_inv := fun _ => rfl44 map_add' := fun _ _ => rfl45 map_smul' := fun _ _ => rfl }4647@[simp] theorem linearEquiv_symm_apply (x : Space p hsep) :48 (linearEquiv p hsep).symm x = (show E from x) := rfl4950/-- Equivalence of norms gives a continuous linear equivalence to the new norm. -/51def equiv (a b : ℝ) (ha : 0 < a)52 (hbounds : ∀ x : E, a * ‖x‖ ≤ p x ∧ p x ≤ b * ‖x‖) :53 E ≃L[ℝ] Space p hsep :=54 { linearEquiv p hsep with55 continuous_toFun := ((linearEquiv p hsep).toLinearMap.mkContinuous b56 (fun x => (hbounds x).2)).continuous57 continuous_invFun := ((linearEquiv p hsep).symm.toLinearMap.mkContinuous a⁻¹58 (fun x => by59 change _ ≤ a⁻¹ * p x60 rw [← div_eq_inv_mul]61 apply (le_div_iff₀ ha).mpr62 convert (hbounds ((linearEquiv p hsep).symm x)).1 using 1 <;>63 first | rfl | exact mul_comm (_ : ℝ) _)).continuous }6465theorem completeSpace [CompleteSpace E] (a b : ℝ) (ha : 0 < a)66 (hbounds : ∀ x : E, a * ‖x‖ ≤ p x ∧ p x ≤ b * ‖x‖) :67 CompleteSpace (Space p hsep) := by68 let e := equiv p hsep a b ha hbounds69 let e' : E ≃ᵤ Space p hsep :=70 { e.toEquiv with71 uniformContinuous_toFun := e.toContinuousLinearMap.uniformContinuous72 uniformContinuous_invFun := e.symm.toContinuousLinearMap.uniformContinuous }73 exact e'.completeSpace_iff.mp inferInstance7475theorem separableSpace [SeparableSpace E] (a b : ℝ) (ha : 0 < a)76 (hbounds : ∀ x : E, a * ‖x‖ ≤ p x ∧ p x ≤ b * ‖x‖) :77 SeparableSpace (Space p hsep) := by78 let e := equiv p hsep a b ha hbounds79 exact e.surjective.denseRange.separableSpace e.continuous8081instance [Lattice E] : Lattice (Space p hsep) := inferInstanceAs (Lattice E)82instance [Lattice E] [IsOrderedAddMonoid E] : IsOrderedAddMonoid (Space p hsep) :=83 inferInstanceAs (IsOrderedAddMonoid E)84instance [Lattice E] [PosSMulMono ℝ E] : PosSMulMono ℝ (Space p hsep) :=85 inferInstanceAs (PosSMulMono ℝ E)8687/-- The assumed solid seminorm becomes an actual normed vector lattice. -/88@[reducible] def normedVectorLattice [Lattice E] [IsOrderedAddMonoid E] [PosSMulMono ℝ E]89 (hsolid : ∀ x y : E, |x| ≤ |y| → p x ≤ p y) :90 NormedVectorLattice (Space p hsep) where91 solid := fun {x y} hxy => hsolid x y hxy92 norm_smul := fun a x => map_smul_eq_mul p a x9394end PL1.LatticeRenorming9596namespace PL19798variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]99100/-- Existence of an actual BanLat Banach lattice continuously linearly101equivalent to the given real normed space, in the same universe. -/102def HasBanachLatticeModel (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] : Prop :=103 ∃ (F : Type u) (nF : NormedAddCommGroup F),104 letI := nF105 ∃ lF : Lattice F,106 letI := lF107 ∃ oF : IsOrderedAddMonoid F,108 letI := oF109 ∃ bF : BanachLattice F,110 letI := bF111 Nonempty (E ≃L[ℝ] F)112113/-- The reviewed equivalent-norm predicate really produces an actual Banach114lattice, preserving the vector-space operations and completeness. -/115theorem HasEquivalentRealLatticeNorm.hasBanachLatticeModel [CompleteSpace E]116 (h : HasEquivalentRealLatticeNorm E) : HasBanachLatticeModel E := by117 obtain ⟨lE, ho, hs, p, hsolid, a, b, ha, _hb, hbounds⟩ := h118 let : Lattice E := lE119 let : IsOrderedAddMonoid E := ho120 let : PosSMulMono ℝ E := hs121 have hsep : ∀ x : E, p x = 0 → x = 0 := by122 intro x hx123 apply norm_eq_zero.mp124 have hl := (hbounds x).1125 rw [hx] at hl126 have hle : ‖x‖ ≤ 0 := by nlinarith [norm_nonneg x]127 exact le_antisymm hle (norm_nonneg x)128 let : NormedVectorLattice (LatticeRenorming.Space p hsep) :=129 LatticeRenorming.normedVectorLattice p hsep hsolid130 let : CompleteSpace (LatticeRenorming.Space p hsep) :=131 LatticeRenorming.completeSpace p hsep a b ha hbounds132 let : BanachLattice (LatticeRenorming.Space p hsep) := {}133 exact ⟨LatticeRenorming.Space p hsep, inferInstance, inferInstance, inferInstance,134 inferInstance, ⟨LatticeRenorming.equiv p hsep a b ha hbounds⟩⟩135136/-- Exact equivalence between the reviewed predicate and existence of an137isomorphic BanLat model. Completeness is assumed only for the forward direction. -/138theorem hasEquivalentRealLatticeNorm_iff_hasBanachLatticeModel [CompleteSpace E] :139 HasEquivalentRealLatticeNorm E ↔ HasBanachLatticeModel E := by140 constructor141 · exact HasEquivalentRealLatticeNorm.hasBanachLatticeModel142 · rintro ⟨F, nF, lF, oF, bF, ⟨e⟩⟩143 let := nF144 let := lF145 let := oF146 let := bF147 exact hasEquivalentRealLatticeNorm_of_continuousLinearEquiv e148149/-- A separable source transfers its separability to any Banach lattice model.150This form allows applying isomorphism-invariant conclusions without exporting151an auxiliary choice of norm or lattice order on the original type. -/152theorem HasEquivalentRealLatticeNorm.elim_separable [CompleteSpace E] [SeparableSpace E]153 (h : HasEquivalentRealLatticeNorm E) {P : Prop}154 (hP : ∀ (F : Type u) [NormedAddCommGroup F] [Lattice F] [IsOrderedAddMonoid F]155 [BanachLattice F] [SeparableSpace F], (E ≃L[ℝ] F) → P) : P := by156 obtain ⟨F, nF, lF, oF, bF, ⟨e⟩⟩ := h.hasBanachLatticeModel157 let := nF158 let := lF159 let := oF160 let := bF161 let : SeparableSpace F := e.surjective.denseRange.separableSpace e.continuous162 exact hP F e163164end PL1165