PL1/ALRenorming.lean
All source files · Download exact source
SHA-256: 11cacb1c0331644012e7df10171b7a70ab15900eb0364f8fb758737846e735a0
1import PL1.LatticeRenorming2import BanLat.RieszDec3import BanLat.Operators.Positive45/-!6# Positive decomposition renorming78The finite estimate in this file quantifies over every positive family. It is9stronger than a disjoint-family estimate; no implication between those two10estimates is assumed or asserted here. Its positive-decomposition supremum11constructs a genuine equivalent AL norm.12-/1314noncomputable section15open scoped BigOperators1617namespace PL1.ALRenorming1819variable {E : Type*} [NormedAddCommGroup E] [Lattice E]20 [IsOrderedAddMonoid E] [NormedVectorLattice E]2122/-- The original norm is additive on the positive cone. -/23def IsALNorm (E : Type*) [NormedAddCommGroup E] [Lattice E] : Prop :=24 ∀ x y : E, 0 ≤ x → 0 ≤ y → ‖x + y‖ = ‖x‖ + ‖y‖2526/-- A uniform lower-one estimate for all positive finite families. -/27def PositiveLowerOne (C : ℝ) : Prop :=28 0 ≤ C ∧ ∀ (n : ℕ) (x : Fin n → E), (∀ i, 0 ≤ x i) →29 ∑ i, ‖x i‖ ≤ C * ‖∑ i, x i‖3031def decompositionValues (u : E) : Set ℝ :=32 {r | ∃ (n : ℕ) (x : Fin n → E), (∀ i, 0 ≤ x i) ∧33 (∑ i, x i) ≤ u ∧ r = ∑ i, ‖x i‖}3435def variation (u : E) : ℝ := sSup (decompositionValues u)3637omit [IsOrderedAddMonoid E] [NormedVectorLattice E] in38theorem zero_mem_decompositionValues {u : E} (hu : 0 ≤ u) :39 0 ∈ decompositionValues u :=40 ⟨0, Fin.elim0, fun i => i.elim0, by simpa using hu, by simp⟩4142theorem decompositionValues_bddAbove {C : ℝ} (hC : PositiveLowerOne (E := E) C)43 {u : E} (hu : 0 ≤ u) : BddAbove (decompositionValues u) := by44 refine ⟨C * ‖u‖, ?_⟩45 rintro r ⟨n, x, hx, hxu, rfl⟩46 exact (hC.2 n x hx).trans (mul_le_mul_of_nonneg_left47 (norm_le_norm_of_abs_le_abs (by48 simpa only [abs_of_nonneg (Finset.sum_nonneg fun i _ => hx i),49 abs_of_nonneg hu] using hxu)) hC.1)5051theorem variation_nonneg {C : ℝ} (hC : PositiveLowerOne (E := E) C)52 {u : E} (hu : 0 ≤ u) : 0 ≤ variation u :=53 le_csSup (decompositionValues_bddAbove hC hu) (zero_mem_decompositionValues hu)5455theorem variation_le {C : ℝ} (hC : PositiveLowerOne (E := E) C)56 {u : E} (hu : 0 ≤ u) : variation u ≤ C * ‖u‖ := by57 apply csSup_le ⟨0, zero_mem_decompositionValues hu⟩58 rintro r ⟨n, x, hx, hxu, rfl⟩59 exact (hC.2 n x hx).trans (mul_le_mul_of_nonneg_left60 (norm_le_norm_of_abs_le_abs (by61 simpa only [abs_of_nonneg (Finset.sum_nonneg fun i _ => hx i),62 abs_of_nonneg hu] using hxu)) hC.1)6364theorem norm_le_variation {C : ℝ} (hC : PositiveLowerOne (E := E) C)65 {u : E} (hu : 0 ≤ u) : ‖u‖ ≤ variation u := by66 apply le_csSup (decompositionValues_bddAbove hC hu)67 exact ⟨1, fun _ => u, fun _ => hu, by simp, by simp⟩6869theorem variation_mono {C : ℝ} (hC : PositiveLowerOne (E := E) C)70 {u v : E} (hu : 0 ≤ u) (huv : u ≤ v) : variation u ≤ variation v := by71 apply csSup_le ⟨0, zero_mem_decompositionValues hu⟩72 rintro r ⟨n, x, hx, hxu, hr⟩73 exact le_csSup (decompositionValues_bddAbove hC (hu.trans huv))74 ⟨n, x, hx, hxu.trans huv, hr⟩7576theorem variation_add {C : ℝ} (hC : PositiveLowerOne (E := E) C)77 (u v : E) (hu : 0 ≤ u) (hv : 0 ≤ v) :78 variation (u + v) = variation u + variation v := by79 classical80 apply le_antisymm81 · apply csSup_le ⟨0, zero_mem_decompositionValues (add_nonneg hu hv)⟩82 rintro r ⟨n, x, hx, hsum, rfl⟩83 obtain ⟨a, b, ha, hb, has, hbs, hx'⟩ :=84 riesz_decomposition_sum_le x u v hx hu hv hsum85 calc86 ∑ i, ‖x i‖ ≤ ∑ i, (‖a i‖ + ‖b i‖) :=87 Finset.sum_le_sum fun i _ => by rw [hx' i]; exact norm_add_le _ _88 _ = (∑ i, ‖a i‖) + ∑ i, ‖b i‖ := Finset.sum_add_distrib89 _ ≤ variation u + variation v := add_le_add90 (le_csSup (decompositionValues_bddAbove hC hu) ⟨n, a, ha, has, rfl⟩)91 (le_csSup (decompositionValues_bddAbove hC hv) ⟨n, b, hb, hbs, rfl⟩)92 · apply le_of_forall_lt_imp_le_of_dense93 intro r hr94 have hr' : r - variation v < variation u := by linarith95 obtain ⟨a, ha, hbr⟩ := exists_lt_of_lt_csSup96 ⟨0, zero_mem_decompositionValues hu⟩ hr'97 have hr'' : r - a < variation v := by linarith98 obtain ⟨b, hb, hab⟩ := exists_lt_of_lt_csSup99 ⟨0, zero_mem_decompositionValues hv⟩ hr''100 obtain ⟨m, x, hx, hxu, rfl⟩ := ha101 obtain ⟨n, y, hy, hyv, rfl⟩ := hb102 have hm : (∑ i, ‖x i‖) + ∑ i, ‖y i‖ ∈ decompositionValues (u + v) := by103 refine ⟨m + n, Fin.addCases x y, ?_, ?_, ?_⟩104 · intro i105 exact Fin.addCases (fun j => by simpa using hx j)106 (fun j => by simpa using hy j) i107 · simpa [Fin.sum_univ_add] using add_le_add hxu hyv108 · simp [Fin.sum_univ_add]109 exact (by linarith : r ≤ (∑ i, ‖x i‖) + ∑ i, ‖y i‖).trans110 (le_csSup (decompositionValues_bddAbove hC (add_nonneg hu hv)) hm)111112/-- The positive-decomposition gauge extends to a positive real functional. -/113def variationLinear {C : ℝ} (hC : PositiveLowerOne (E := E) C) : E →ₗ[ℝ] ℝ :=114 Positive.extension (fun _ hu => variation_nonneg hC hu) (variation_add hC)115116theorem variationLinear_nonneg {C : ℝ} (hC : PositiveLowerOne (E := E) C)117 {u : E} (hu : 0 ≤ u) : variationLinear hC u = variation u :=118 Positive.extension_nonneg _ _ hu119120theorem variationLinear_positive {C : ℝ} (hC : PositiveLowerOne (E := E) C) :121 Positive (variationLinear hC) := Positive.extension_positive _ _122123/-- The solid AL seminorm associated to the constructed functional. -/124def seminorm {C : ℝ} (hC : PositiveLowerOne (E := E) C) : Seminorm ℝ E :=125 Seminorm.of (fun x => variationLinear hC |x|)126 (fun x y => by127 rw [← map_add]128 exact (Positive.monotone_iff.mpr (variationLinear_positive hC)) (abs_add_le x y))129 (fun a x => by simp only [abs_smul', map_smul, smul_eq_mul, Real.norm_eq_abs])130131theorem seminorm_bounds {C : ℝ} (hC : PositiveLowerOne (E := E) C) (x : E) :132 ‖x‖ ≤ seminorm hC x ∧ seminorm hC x ≤ C * ‖x‖ := by133 change ‖x‖ ≤ variationLinear hC |x| ∧ variationLinear hC |x| ≤ C * ‖x‖134 rw [variationLinear_nonneg hC (abs_nonneg x)]135 simpa only [norm_abs_eq_norm] using136 And.intro (norm_le_variation hC (abs_nonneg x)) (variation_le hC (abs_nonneg x))137138theorem seminorm_solid {C : ℝ} (hC : PositiveLowerOne (E := E) C)139 (x y : E) (hxy : |x| ≤ |y|) : seminorm hC x ≤ seminorm hC y :=140 (Positive.monotone_iff.mpr (variationLinear_positive hC)) hxy141142theorem seminorm_add_of_nonneg {C : ℝ} (hC : PositiveLowerOne (E := E) C)143 (x y : E) (hx : 0 ≤ x) (hy : 0 ≤ y) :144 seminorm hC (x + y) = seminorm hC x + seminorm hC y := by145 change variationLinear hC |x + y| = variationLinear hC |x| + variationLinear hC |y|146 rw [abs_of_nonneg (add_nonneg hx hy), abs_of_nonneg hx, abs_of_nonneg hy, map_add]147148theorem seminorm_separates {C : ℝ} (hC : PositiveLowerOne (E := E) C)149 (x : E) (hx : seminorm hC x = 0) : x = 0 := by150 exact norm_eq_zero.mp (le_antisymm (hx ▸ (seminorm_bounds hC x).1) (norm_nonneg x))151152/-- The actual vector-space copy carrying the constructed AL norm. -/153abbrev Space {C : ℝ} (hC : PositiveLowerOne (E := E) C) :=154 LatticeRenorming.Space (seminorm hC) (seminorm_separates hC)155156def equiv {C : ℝ} (hC : PositiveLowerOne (E := E) C) : E ≃L[ℝ] Space hC :=157 LatticeRenorming.equiv _ _ 1 C (by norm_num)158 (fun x => by simpa only [one_mul] using seminorm_bounds hC x)159160@[reducible] def normedVectorLattice {C : ℝ} (hC : PositiveLowerOne (E := E) C) :161 NormedVectorLattice (Space hC) :=162 LatticeRenorming.normedVectorLattice _ _ (seminorm_solid hC)163164theorem completeSpace [CompleteSpace E] {C : ℝ}165 (hC : PositiveLowerOne (E := E) C) : CompleteSpace (Space hC) :=166 LatticeRenorming.completeSpace _ _ 1 C (by norm_num)167 (fun x => by simpa only [one_mul] using seminorm_bounds hC x)168169theorem separableSpace [TopologicalSpace.SeparableSpace E] {C : ℝ}170 (hC : PositiveLowerOne (E := E) C) : TopologicalSpace.SeparableSpace (Space hC) :=171 LatticeRenorming.separableSpace _ _ 1 C (by norm_num)172 (fun x => by simpa only [one_mul] using seminorm_bounds hC x)173174theorem isALNorm {C : ℝ} (hC : PositiveLowerOne (E := E) C) : IsALNorm (Space hC) :=175 seminorm_add_of_nonneg hC176177end PL1.ALRenorming178