BaseNormModels.lean

1 import KomorebiLSM.InstrumentContraction
2 import KomorebiLSM.FiniteTV
3 
4 /-! The constructed norm is connected to the previously checked finite lifts.
5 Injective synthesis gives the exact coefficient l1 norm; redundancy gives only an upper bound. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.BaseNorm
8 open scoped BigOperators
9 open FiniteInstruments FiniteBayes PositiveLift
10 variable {E J : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
11 variable [FiniteDimensional ℝ E] [Fintype J] [DecidableEq J]
12 
13 /-- Every normalized full-row-rank positive-lift domain supplies the norm construction. -/
14 noncomputable def finiteCone (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
15     (hn : l.comp V=mass) (hs : Function.Surjective V) : ProbabilityCone E where
16   carrier := hull V
17   zero_mem := hull_zero V
18   add_mem := hull_add V
19   smul_mem := hull_smul V
20   spans := hull_spans V hs
21   mass := l
22   mass_pos := fun hx hne => hull_strict_mass V l hn _ hx hne
23   closed := hull_closed V l hn
24 
25 theorem finiteCone_base (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
26     (hn : l.comp V=mass) (hs : Function.Surjective V) :
27     (finiteCone V l hn hs).base=convexHull ℝ (Set.range (generator V)) :=
28   normalizedHull_eq_convexHull V l hn
29 
30 omit [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [DecidableEq J] in
31 theorem positive_negative_parts (x : J → ℝ) :
32     x=(fun j => max (x j) 0)-(fun j => max (-x j) 0) ∧
33     mass (fun j => max (x j) 0)+mass (fun j => max (-x j) 0)=FiniteTV.l1 x := by
34   constructor
35   · funext j
36     change x j=max (x j) 0-max (-x j) 0
37     by_cases hx : 0 ≤ x j
38     · rw [max_eq_left hx,max_eq_right (neg_nonpos.mpr hx)]; ring
39     · have hn : x j ≤ 0 := le_of_not_ge hx
40       rw [max_eq_right hn,max_eq_left (neg_nonneg.mpr hn)]; ring
41   · rw [mass_apply,mass_apply,← Finset.sum_add_distrib]
42     apply Finset.sum_congr rfl
43     intro j _
44     by_cases hx : 0 ≤ x j
45     · rw [max_eq_left hx,max_eq_right (neg_nonpos.mpr hx),abs_of_nonneg hx]; ring
46     · have hn : x j ≤ 0 := le_of_not_ge hx
47       rw [max_eq_right hn,max_eq_left (neg_nonneg.mpr hn),abs_of_nonpos hn]; ring
48 
49 /-- Any signed coefficient representation gives an upper bound, not necessarily the minimum. -/
50 theorem value_synthesis_le_l1 (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
51     (hn : l.comp V=mass) (hs : Function.Surjective V) (x : J → ℝ) :
52     (finiteCone V l hn hs).value (V x) ≤ FiniteTV.l1 x := by
53   obtain ⟨he,hm⟩ := positive_negative_parts x
54   let a : J → ℝ := fun j => max (x j) 0
55   let b : J → ℝ := fun j => max (-x j) 0
56   have ha : V a ∈ (finiteCone V l hn hs).carrier := ⟨a,fun j => le_max_right _ _,rfl⟩
57   have hb : V b ∈ (finiteCone V l hn hs).carrier := ⟨b,fun j => le_max_right _ _,rfl⟩
58   have h := (finiteCone V l hn hs).value_le_cost (x := V x) ha hb
59     (by rw [← map_sub]; exact congrArg V he)
60   have hma : l (V a)=mass a := by simpa only [← mass_apply] using normalized_mass V l hn a
61   have hmb : l (V b)=mass b := by simpa only [← mass_apply] using normalized_mass V l hn b
62   change _ ≤ l (V a)+l (V b) at h
63   rw [hma,hmb] at h
64   exact h.trans_eq hm
65 
66 /-- Injective synthesis makes the upper bound an equality. -/
67 theorem value_synthesis_eq_l1 (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
68     (hn : l.comp V=mass) (hs : Function.Surjective V) (hi : Function.Injective V) (x : J → ℝ) :
69     (finiteCone V l hn hs).value (V x)=FiniteTV.l1 x := by
70   apply le_antisymm (value_synthesis_le_l1 V l hn hs x)
71   apply (finiteCone V l hn hs).le_value
72   rintro u ⟨a,ha,rfl⟩ v ⟨b,hb,rfl⟩ he
73   have hx : x=a-b := hi (by rw [map_sub]; exact he)
74   have h := FiniteTV.l1_sub_le a b
75   rw [FiniteTV.l1_of_nonneg a ha,FiniteTV.l1_of_nonneg b hb] at h
76   change FiniteTV.l1 x ≤ l (V a)+l (V b)
77   rw [normalized_mass V l hn,normalized_mass V l hn]
78   simpa only [hx,mass_apply] using h
79 
80 /-- The manuscript's invertible-atlas formula, using its actual inverse. -/
81 theorem value_invertible_synthesis (V : (J → ℝ) ≃ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
82     (hn : l.comp V.toLinearMap=mass) (x : E) :
83     (finiteCone V.toLinearMap l hn V.surjective).value x=FiniteTV.l1 (V.symm x) := by
84   simpa only [LinearEquiv.coe_coe,LinearEquiv.apply_symm_apply] using
85     value_synthesis_eq_l1 V.toLinearMap l hn V.surjective V.injective (V.symm x)
86 
87 /-- The ordinary orthant, constructed through the finite positive-lift interface. -/
88 noncomputable def orthant (J : Type*) [Fintype J] [DecidableEq J] : ProbabilityCone (J → ℝ) :=
89   finiteCone LinearMap.id mass (by simp) Function.surjective_id
90 
91 @[simp] theorem orthant_carrier (x : J → ℝ) : x ∈ (orthant J).carrier ↔ ∀ j, 0 ≤ x j := by
92   constructor
93   · rintro ⟨a,ha,he⟩; simpa only [LinearMap.id_apply] using he ▸ ha
94   · intro hx; exact ⟨x,hx,rfl⟩
95 
96 @[simp] theorem orthant_value (x : J → ℝ) : (orthant J).value x=FiniteTV.l1 x := by
97   simpa only [orthant,LinearMap.id_apply] using
98     value_synthesis_eq_l1 (LinearMap.id : (J → ℝ) →ₗ[ℝ] (J → ℝ)) mass
99       (by simp) Function.surjective_id Function.injective_id x
100 
101 /-- A scalar probability cone for exact record-law examples. -/
102 noncomputable def scalarCone : ProbabilityCone ℝ where
103  carrier := {x : ℝ | 0 ≤ x}
104  zero_mem := by change (0 : ℝ) ≤ 0; exact le_rfl
105  add_mem := by
106   intro x y hx hy
107   change (0 : ℝ) ≤ x at hx
108   change (0 : ℝ) ≤ y at hy
109   change (0 : ℝ) ≤ x+y
110   exact add_nonneg hx hy
111  smul_mem := by
112   intro a ha x hx
113   change (0 : ℝ) ≤ x at hx
114   change (0 : ℝ) ≤ a*x
115   exact mul_nonneg ha hx
116  spans := by
117   apply top_unique
118   intro x _
119   have h : (1 : ℝ) ∈ Submodule.span ℝ {x : ℝ | 0 ≤ x} := Submodule.subset_span (by norm_num)
120   simpa using Submodule.smul_mem (Submodule.span ℝ {x : ℝ | 0 ≤ x}) x h
121  mass := LinearMap.id
122  mass_pos := by
123   intro x hx hn
124   change (0 : ℝ) ≤ x at hx
125   change (0 : ℝ) < x
126   exact lt_of_le_of_ne hx (Ne.symm hn)
127  closed := isClosed_le continuous_const continuous_id
128 
129 @[simp] theorem scalar_value (x : ℝ) : scalarCone.value x=|x| := by
130   by_cases hx : 0 ≤ x
131   · exact (scalarCone.value_on_cone hx).trans (abs_of_nonneg hx).symm
132   · have hn : 0 ≤ -x := neg_nonneg.mpr (le_of_not_ge hx)
133     have h := scalarCone.value_on_cone hn
134     rw [scalarCone.value_neg] at h
135     exact h.trans (abs_of_neg (lt_of_not_ge hx)).symm
136 
137 end Komorebi.LSM.BaseNorm

Back to source controls