PL1/LatticeStrictPositive.lean

All source files · Download exact source

SHA-256: 0548013e214d7e56472aea3781770a53288766bd4f16435db48a44a91c590f99

1import PL1.SchurLattice2import BanLat.Dual34/-!5# Strictly positive functionals on separable normed lattices67The positive functional constructed here detects every nonzero positive8vector. It is obtained from positive Hahn--Banach functionals on a dense9sequence in the positive cone, using a norm-convergent geometric series.10-/1112noncomputable section13open Filter TopologicalSpace14open scoped Topology1516namespace PL1.SchurLattice1718variable {E : Type*} [NormedAddCommGroup E] [Lattice E]19  [IsOrderedAddMonoid E] [NormedVectorLattice E]2021/-- Positivity is strict on all nonzero positive vectors. -/22def IsStrictlyPositive (φ : E →L[ℝ] ℝ) : Prop :=23  ∀ x : E, 0 < x → 0 < φ x2425theorem IsStrictlyPositive.nonneg {φ : E →L[ℝ] ℝ} (hφ : IsStrictlyPositive φ) :26    0 ≤ φ := by27  apply StrongDual.nonneg_iff.mpr28  intro x hx29  by_cases h : x = 030  · simp [h]31  · exact (hφ x (lt_of_le_of_ne hx (Ne.symm h))).le3233theorem IsStrictlyPositive.eq_zero_of_nonneg {φ : E →L[ℝ] ℝ}34    (hφ : IsStrictlyPositive φ) {x : E} (hx : 0 ≤ x) (hz : φ x = 0) : x = 0 := by35  by_contra h36  have hp := hφ x (lt_of_le_of_ne hx (Ne.symm h))37  exact (ne_of_gt hp) hz3839/-- Separability supplies a strictly positive continuous functional. The40result does not require completeness or a separable continuous dual. -/41theorem exists_strictlyPositive [SeparableSpace E] :42    ∃ φ : E →L[ℝ] ℝ, 0 ≤ φ ∧ IsStrictlyPositive φ := by43  classical44  let C := Set.Ici (0 : E)45  let : Nonempty C := ⟨⟨0, le_rfl⟩⟩46  let d : ℕ → C := denseSeq C47  choose g hg hgn hgd using fun n =>48    StrongDual.exists_positive_dual_norming (d n).property49  let w : ℕ → ℝ := fun n => (1 / 2 : ℝ) ^ n50  have hw : Summable w := summable_geometric_of_lt_one (by norm_num) (by norm_num)51  have hsum : Summable (fun n => w n • g n) := by52    apply hw.of_norm_bounded53    intro n54    rw [norm_smul, Real.norm_of_nonneg (by positivity : 0 ≤ w n)]55    exact mul_le_of_le_one_right (by positivity : 0 ≤ w n) (hgn n)56  let φ : E →L[ℝ] ℝ := ∑' n, w n • g n57  have hφ (x : E) : φ x = ∑' n, w n * g n x := by58    simpa [φ] using (ContinuousLinearMap.apply ℝ ℝ x).map_tsum hsum59  have hscalar (x : E) : Summable (fun n => w n * g n x) := by60    simpa using hsum.mapL (ContinuousLinearMap.apply ℝ ℝ x)61  have hpos : 0 ≤ φ := by62    apply StrongDual.nonneg_iff.mpr63    intro x hx64    rw [hφ]65    exact tsum_nonneg (fun n => mul_nonneg (by positivity)66      (StrongDual.apply_nonneg_of_nonneg (hg n) hx))67  refine ⟨φ, hpos, ?_⟩68  intro x hx69  have hx0 : x ≠ 0 := ne_of_gt hx70  have hxnorm : 0 < ‖x‖ := norm_pos_iff.mpr hx071  obtain ⟨n, hn⟩ := (denseRange_denseSeq C).exists_dist_lt (⟨x, hx.le⟩ : C)72    (show 0 < ‖x‖ / 3 from by positivity)73  have hdist : ‖x - (d n : E)‖ < ‖x‖ / 3 := by74    simpa [d, Subtype.dist_eq, dist_eq_norm] using hn75  have hdual : |g n x - ‖(d n : E)‖| ≤ ‖x - (d n : E)‖ := by76    have hb := (g n).le_opNorm (x - (d n : E))77    rw [map_sub, hgd] at hb78    exact hb.trans (mul_le_of_le_one_left (norm_nonneg _) (hgn n))79  have htriangle : ‖x‖ ≤ ‖x - (d n : E)‖ + ‖(d n : E)‖ := by80    simpa only [sub_add_cancel] using norm_add_le (x - (d n : E)) (d n : E)81  have hgnx : 0 < g n x := by82    have hb := (abs_le.mp hdual).183    linarith84  rw [hφ]85  exact (hscalar x).tsum_pos (fun k => mul_nonneg (by positivity)86    (StrongDual.apply_nonneg_of_nonneg (hg k) hx.le)) n87    (mul_pos (by positivity) hgnx)8889end PL1.SchurLattice90