RobustFiniteDomains.lean

1 import KomorebiLSM.PositiveLiftTopology
2 
3 /-! P40: convex sets of complete operator families and history-dependent
4 selection. Mixing takes place across whole families, retaining the mass law. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.RobustDomains
7 open scoped BigOperators
8 open FiniteInstruments PositiveLift
9 variable {E A O : Type*} [AddCommGroup E] [Module ℝ E] [Fintype O]
10 
11 def ValidFamily (C : Set E) (l : E →ₗ[ℝ] ℝ) (B : A × O → E →ₗ[ℝ] E) : Prop :=
12   (∀ s x, x ∈ C → B s x ∈ C) ∧ (∀ a x, ∑ o, l (B (a,o) x) = l x)
13 
14 /-- A single convex coefficient is shared by every branch of a complete family. -/
15 theorem validFamily_convex (C : Set E) (hc : Convex ℝ C) (l : E →ₗ[ℝ] ℝ) :
16     Convex ℝ {B : A × O → E →ₗ[ℝ] E | ValidFamily C l B} := by
17   intro B hB D hD a b ha hb hab
18   constructor
19   · intro s x hx
20     exact hc (hB.1 s x hx) (hD.1 s x hx) ha hb hab
21   · intro u x
22     change ∑ o, l (a • B (u,o) x + b • D (u,o) x) = l x
23     simp only [map_add,map_smul,smul_eq_mul,Finset.sum_add_distrib,← Finset.mul_sum,
24       hB.2,hD.2,← add_mul,hab,one_mul]
25 
26 /-- Membership in the actual convex hull, not merely a list of tested parameters. -/
27 theorem robust_convex_hull {I : Type*} (C : Set E) (hc : Convex ℝ C)
28     (l : E →ₗ[ℝ] ℝ) (families : I → A × O → E →ₗ[ℝ] E)
29     (hv : ∀ i, ValidFamily C l (families i)) :
30     ∀ B ∈ convexHull ℝ (Set.range families), ValidFamily C l B := by
31   apply convexHull_min _ (validFamily_convex C hc l)
32   rintro _ ⟨i,rfl⟩
33   exact hv i
34 
35 /-- Nonnegative vertex witnesses establish validity on the full uncertainty hull. -/
36 theorem robust_positive_lift {I J : Type*} [Fintype J] [DecidableEq J]
37     (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
38     (families : I → A × O → E →ₗ[ℝ] E)
39     (M : I → A × O → Matrix J J ℝ)
40     (hp : ∀ i s j k, 0 ≤ M i s j k)
41     (he : ∀ i s, (families i s).comp V = V.comp (M i s).mulVecLin)
42     (hm : ∀ i a x, ∑ o, l (families i (a,o) x) = l x) :
43     ∀ B ∈ convexHull ℝ (Set.range families), ValidFamily (hull V) l B := by
44   apply robust_convex_hull (hull V) (hull_convex V) l families
45   intro i
46   exact ⟨fun s => (positive_lift_iff V (families i s)).mpr ⟨M i s,hp i s,he i s⟩,hm i⟩
47 
48 /-- Explicit mixed lifts retain intertwining, including redundant generators. -/
49 theorem mixed_lift {I J : Type*} [Fintype I] [Fintype J]
50     (V : (J → ℝ) →ₗ[ℝ] E) (B : I → E →ₗ[ℝ] E) (M : I → Matrix J J ℝ)
51     (he : ∀ i, (B i).comp V = V.comp (M i).mulVecLin) (θ : I → ℝ) :
52     (∑ i, θ i • B i).comp V = V.comp (∑ i, θ i • (M i).mulVecLin) := by
53   apply LinearMap.ext
54   intro x
55   simp only [LinearMap.comp_apply,LinearMap.sum_apply,LinearMap.smul_apply,map_sum,map_smul]
56   apply Finset.sum_congr rfl
57   intro i _
58   exact congrArg (θ i • ·) (congrArg (fun F : (J → ℝ) →ₗ[ℝ] E => F x) (he i))
59 
60 omit [Fintype O] in
61 theorem mixed_entries_nonnegative {I J : Type*} [Fintype I]
62     (M : I → Matrix J J ℝ) (hp : ∀ i j k, 0 ≤ M i j k)
63     (θ : I → ℝ) (hθ : ∀ i, 0 ≤ θ i) : ∀ j k, 0 ≤ (∑ i, θ i • M i) j k := by
64   intro j k
65   simp only [Matrix.sum_apply,Matrix.smul_apply,smul_eq_mul]
66   exact Finset.sum_nonneg (fun i _ => mul_nonneg (hθ i) (hp i j k))
67 
68 /-- A chronological word can use a different family after every observed prefix. -/
69 def adaptiveWord (B : List (A × O) → A × O → E →ₗ[ℝ] E) :
70     List (A × O) → List (A × O) → E → E
71   | _, [], x => x
72   | h, s::w, x => adaptiveWord B (h ++ [s]) w (B h s x)
73 
74 theorem adaptiveWord_in_cone (C : Set E) (l : E →ₗ[ℝ] ℝ)
75     (B : List (A × O) → A × O → E →ₗ[ℝ] E)
76     (hv : ∀ h, ValidFamily C l (B h)) (h w : List (A × O)) {x : E} (hx : x ∈ C) :
77     adaptiveWord B h w x ∈ C := by
78   induction w generalizing h x with
79   | nil => exact hx
80   | cons s w ih => exact ih _ ((hv h).1 s x hx)
81 
82 theorem adaptiveWord_nonnegative (C : Set E) (l : E →ₗ[ℝ] ℝ)
83     (hC : ∀ x ∈ C, 0 ≤ l x) (B : List (A × O) → A × O → E →ₗ[ℝ] E)
84     (hv : ∀ h, ValidFamily C l (B h)) (h w : List (A × O)) {x : E} (hx : x ∈ C) :
85     0 ≤ l (adaptiveWord B h w x) :=
86   hC _ (adaptiveWord_in_cone C l B hv h w hx)
87 
88 theorem adaptiveWord_mass_le (C : Set E) (l : E →ₗ[ℝ] ℝ)
89     (hC : ∀ x ∈ C, 0 ≤ l x) (B : List (A × O) → A × O → E →ₗ[ℝ] E)
90     (hv : ∀ h, ValidFamily C l (B h)) (h w : List (A × O)) {x : E} (hx : x ∈ C) :
91     l (adaptiveWord B h w x) ≤ l x := by
92   induction w generalizing h x with
93   | nil => exact le_rfl
94   | cons s w ih =>
95     apply (ih (h ++ [s]) ((hv h).1 s x hx)).trans
96     rw [← (hv h).2 s.1 x]
97     exact Finset.single_le_sum (fun o _ => hC _ ((hv h).1 (s.1,o) x hx)) (Finset.mem_univ s.2)
98 
99 /-- Full observation-tree mass for an arbitrary deterministic history-based policy. -/
100 noncomputable def adaptiveTreeMass (B : List (A × O) → A × O → E →ₗ[ℝ] E)
101     (l : E →ₗ[ℝ] ℝ) (policy : List (A × O) → A) : ℕ → List (A × O) → E → ℝ
102   | 0, _, x => l x
103   | n+1, h, x => ∑ o, adaptiveTreeMass B l policy n (h ++ [(policy h,o)]) (B h (policy h,o) x)
104 
105 theorem adaptiveTreeMass_eq (C : Set E) (l : E →ₗ[ℝ] ℝ)
106     (B : List (A × O) → A × O → E →ₗ[ℝ] E)
107     (hv : ∀ h, ValidFamily C l (B h)) (policy : List (A × O) → A)
108     (n : ℕ) (h : List (A × O)) (x : E) : adaptiveTreeMass B l policy n h x = l x := by
109   induction n generalizing h x with
110   | zero => rfl
111   | succ n ih =>
112     simp only [adaptiveTreeMass,ih]
113     exact (hv h).2 (policy h) x
114 
115 end Komorebi.LSM.RobustDomains

Back to source controls