BaseNormTopology.lean

1 import KomorebiLSM.BaseNorm
2 
3 /-! Finite-dimensional closed cones with strict mass have compact bases.
4 The infimum construction is consequently nondegenerate. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.BaseNorm.ProbabilityCone
7 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
8 variable [FiniteDimensional ℝ E] (C : ProbabilityCone E)
9 
10 /-- A uniform cone bound is derived by minimizing mass on the unit cone slice. -/
11 theorem exists_cone_bound : ∃ R > 0, ∀ x ∈ C.carrier, ‖x‖ ≤ R*C.mass x := by
12   let S := Metric.sphere (0 : E) 1 ∩ C.carrier
13   have hcompact : IsCompact S := (isCompact_sphere (0 : E) 1).inter_right C.closed
14   have hunit : ∀ x : E, x ∈ C.carrier → x ≠ 0 → (‖x‖⁻¹ : ℝ) • x ∈ S := by
15     intro x hx hn
16     have hp : 0 < ‖x‖ := norm_pos_iff.mpr hn
17     refine ⟨?_,C.smul_mem (inv_nonneg.mpr (norm_nonneg x)) hx⟩
18     change dist ((‖x‖⁻¹ : ℝ) • x) 0 = 1
19     simp only [dist_zero_right,norm_smul,Real.norm_eq_abs,abs_inv,abs_norm,
20       inv_mul_cancel₀ (ne_of_gt hp)]
21   by_cases hs : S.Nonempty
22   · obtain ⟨y,hy,hmin⟩ := hcompact.exists_isMinOn hs C.mass.continuous_of_finiteDimensional.continuousOn
23     have hny : ‖y‖=1 := by simpa only [Metric.mem_sphere,dist_zero_right] using hy.1
24     have hyne : y ≠ 0 := by intro h; simp [h] at hny
25     have hd : 0 < C.mass y := C.mass_pos hy.2 hyne
26     refine ⟨(C.mass y)⁻¹,inv_pos.mpr hd,?_⟩
27     intro x hx
28     by_cases hn : x=0
29     · simp [hn]
30     have hp : 0<‖x‖ := norm_pos_iff.mpr hn
31     have hm := hmin (hunit x hx hn)
32     change C.mass y ≤ C.mass ((‖x‖⁻¹ : ℝ) • x) at hm
33     simp only [map_smul,smul_eq_mul] at hm
34     have hm' : C.mass y ≤ C.mass x/‖x‖ := by simpa only [div_eq_mul_inv,mul_comm] using hm
35     have he := (le_div_iff₀ hp).mp hm'
36     have ht : ‖x‖ ≤ C.mass x / C.mass y := (le_div_iff₀ hd).mpr (by nlinarith)
37     simpa only [div_eq_mul_inv,mul_comm] using ht
38   · refine ⟨1,by norm_num,?_⟩
39     intro x hx
40     have hn : x=0 := by
41       by_contra h
42       exact hs ⟨_,hunit x hx h⟩
43     simp [hn]
44 
45 theorem base_closed : IsClosed C.base :=
46   C.closed.inter (isClosed_eq C.mass.continuous_of_finiteDimensional continuous_const)
47 
48 /-- Compactness follows from the structural cone assumptions. -/
49 theorem base_compact : IsCompact C.base := by
50   obtain ⟨R,_,hR⟩ := C.exists_cone_bound
51   apply Metric.isCompact_of_isClosed_isBounded C.base_closed
52   apply (Metric.isBounded_iff_subset_closedBall (0 : E)).mpr
53   refine ⟨R,?_⟩
54   intro x hx
55   have h := hR x hx.1
56   rw [hx.2,mul_one] at h
57   simpa only [Metric.mem_closedBall,dist_zero_right] using h
58 
59 omit [FiniteDimensional ℝ E] in
60 theorem base_convex : Convex ℝ C.base := by
61   intro x hx y hy a b ha hb hab
62   refine ⟨C.add_mem (C.smul_mem ha hx.1) (C.smul_mem hb hy.1),?_⟩
63   simp only [map_add,map_smul,smul_eq_mul,hx.2,hy.2,mul_one,hab]
64 
65 /-- The original ambient norm is bounded by a fixed multiple of the base norm. -/
66 theorem exists_norm_le_value : ∃ R > 0, ∀ x : E, ‖x‖ ≤ R*C.value x := by
67   obtain ⟨R,hRp,hR⟩ := C.exists_cone_bound
68   refine ⟨R,hRp,?_⟩
69   intro x
70   have h : ‖x‖/R ≤ C.value x := by
71     apply C.le_value
72     intro u hu v hv hx
73     apply (div_le_iff₀ hRp).mpr
74     have ht := norm_sub_le u v
75     rw [hx]
76     nlinarith [hR u hu,hR v hv]
77   have hm := (div_le_iff₀ hRp).mp h
78   simpa only [mul_comm] using hm
79 
80 @[simp] theorem value_eq_zero_iff (x : E) : C.value x=0 ↔ x=0 := by
81   constructor
82   · intro h
83     obtain ⟨R,_,hR⟩ := C.exists_norm_le_value
84     have hb := hR x
85     rw [h,mul_zero] at hb
86     exact norm_eq_zero.mp (le_antisymm hb (norm_nonneg x))
87   · intro h; simp [h]
88 
89 /-- The actual infimum has every real norm law, including nondegeneracy. -/
90 theorem base_norm_laws :
91     (∀ x, 0 ≤ C.value x) ∧
92     (∀ x, C.value x=0 ↔ x=0) ∧
93     (∀ x y, C.value (x+y) ≤ C.value x+C.value y) ∧
94     (∀ a x, C.value (a • x)=|a| * C.value x) :=
95   ⟨C.value_nonneg,C.value_eq_zero_iff,C.value_add_le,C.value_smul⟩
96 
97 /-- The infimum, packaged as an actual real seminorm. -/
98 noncomputable def seminorm : Seminorm ℝ E where
99   toFun := C.value
100   map_zero' := C.value_zero
101   add_le' := C.value_add_le
102   neg' := C.value_neg
103   smul' := fun a x => by simpa only [Real.norm_eq_abs] using C.value_smul a x
104 
105 /-- Nondegeneracy makes the same infimum an additive group norm. -/
106 noncomputable def groupNorm : AddGroupNorm E where
107   toFun := C.value
108   map_zero' := C.value_zero
109   add_le' := C.value_add_le
110   neg' := C.value_neg
111   eq_zero_of_map_eq_zero' := fun x hx => (C.value_eq_zero_iff x).mp hx
112 
113 omit [FiniteDimensional ℝ E] in
114 @[simp] theorem seminorm_apply (x : E) : C.seminorm x=C.value x := rfl
115 @[simp] theorem groupNorm_apply (x : E) : C.groupNorm x=C.value x := rfl
116 
117 end Komorebi.LSM.BaseNorm.ProbabilityCone

Back to source controls