PositiveLiftTopology.lean

1 import KomorebiLSM.PositiveLift
2 import Mathlib.Analysis.Convex.Combination
3 import Mathlib.Topology.Algebra.Module.FiniteDimension
4 import Mathlib.Topology.Order.Compact
5 import Mathlib.Topology.Maps.Proper.Basic
6 
7 /-! Closedness is derived for normalized finite generators, including redundant
8 ones. Compactifying coefficient witnesses avoids assuming a closed linear image. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.PositiveLift
11 open scoped BigOperators
12 open FiniteBayes FiniteInstruments
13 variable {E J : Type*} [AddCommGroup E] [Module ℝ E] [Fintype J]
14 variable [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
15 variable [T2Space E] [FiniteDimensional ℝ E]
16 
17 /-- Nonnegative prior coordinates lie in the finite unit box. -/
18 theorem prior_box {a : J → ℝ} (ha : IsPrior a) : ∀ j, a j ∈ Set.Icc (0 : ℝ) 1 := by
19   intro j
20   refine ⟨ha.1 j, ?_⟩
21   rw [← ha.2]
22   exact Finset.single_le_sum (fun i _ => ha.1 i) (Finset.mem_univ j)
23 
24 omit [T2Space E] [FiniteDimensional ℝ E] in
25 /-- The actual finite probability simplex is compact. -/
26 theorem priors_compact : IsCompact {a : J → ℝ | IsPrior a} := by
27   have he : {a : J → ℝ | IsPrior a} =
28       {a | ∀ j, a j ∈ Set.Icc (0 : ℝ) 1} ∩ {a | ∑ j, a j = 1} := by
29     ext a
30     constructor
31     · intro ha; exact ⟨prior_box ha,ha.2⟩
32     · rintro ⟨ha,hs⟩; exact ⟨fun j => (ha j).1,hs⟩
33   rw [he]
34   exact (isCompact_pi_infinite (fun _ => isCompact_Icc)).inter_right
35     (isClosed_eq (by fun_prop) continuous_const)
36 
37 omit [T2Space E] [FiniteDimensional ℝ E] in
38 theorem normalizedHull_compact (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
39     (hn : l.comp V = mass) : IsCompact (normalizedHull V l) := by
40   rw [normalizedHull_eq_prior_image V l hn]
41   exact priors_compact.image V.continuous_of_finiteDimensional
42 
43 omit [Fintype J] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] in
44 theorem normalizedHull_convex (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
45     Convex ℝ (normalizedHull V l) := by
46   intro x hx y hy a b ha hb hab
47   refine ⟨hull_convex V hx.1 hy.1 ha hb hab, ?_⟩
48   simpa only [map_add,map_smul,smul_eq_mul,hx.2,hy.2,mul_one] using hab
49 
50 /-- Normalized generators keep coefficient witnesses in a compact unit box. -/
51 theorem hull_closed (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
52     (hn : l.comp V = mass) : IsClosed (hull V) := by
53   let K : Set (J → ℝ) := {a | ∀ j, a j ∈ Set.Icc (0 : ℝ) 1}
54   have hk : IsCompact K := isCompact_pi_infinite (fun _ => isCompact_Icc)
55   let : CompactSpace K := isCompact_iff_compactSpace.mp hk
56   let F : Set (E × K) := {z | (1 + l z.1) • V z.2.val = z.1}
57   have hf : IsClosed F := isClosed_eq
58     ((continuous_const.add (l.continuous_of_finiteDimensional.comp continuous_fst)).smul
59       (V.continuous_of_finiteDimensional.comp (continuous_subtype_val.comp continuous_snd)))
60     continuous_fst
61   have he : hull V = {x | 0 ≤ l x} ∩ (Prod.fst '' F) := by
62     ext x
63     constructor
64     · intro hx
65       have hm : 0 ≤ l x := hull_mass_nonneg V l hn hx
66       obtain ⟨a,ha,haV⟩ := hx
67       have hpos : 0 < 1 + l x := by linarith
68       let b : J → ℝ := (1 + l x)⁻¹ • a
69       have hb : b ∈ K := by
70         intro j
71         change 0 ≤ (1 + l x)⁻¹ * a j ∧ (1 + l x)⁻¹ * a j ≤ 1
72         refine ⟨mul_nonneg (inv_nonneg.mpr hpos.le) (ha j), ?_⟩
73         rw [mul_comm,← div_eq_mul_inv]
74         apply (div_le_one hpos).mpr
75         have hle : a j ≤ ∑ i, a i :=
76           Finset.single_le_sum (fun i _ => ha i) (Finset.mem_univ j)
77         have hsum : ∑ i, a i = l x := (normalized_mass V l hn a).symm.trans (congrArg l haV)
78         rw [hsum] at hle
79         linarith
80       refine ⟨hm,⟨(x,⟨b,hb⟩),?_,rfl⟩⟩
81       change (1+l x) • V ((1+l x)⁻¹ • a) = x
82       rw [map_smul,smul_smul,mul_inv_cancel₀ (ne_of_gt hpos),one_smul,haV]
83     · rintro ⟨hx,⟨⟨y,b⟩,hF,hxy⟩⟩
84       change y = x at hxy
85       subst y
86       change 0 ≤ l x at hx
87       refine ⟨(1+l x) • b.val,fun j => mul_nonneg (by linarith) (b.property j).1, ?_⟩
88       rw [map_smul]
89       exact hF
90   rw [he]
91   exact (isClosed_le continuous_const l.continuous_of_finiteDimensional).inter
92     (isClosedMap_fst_of_compactSpace F hf)
93 
94 omit [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] [FiniteDimensional ℝ E] in
95 /-- The normalized base is precisely the convex hull of the supplied generators. -/
96 theorem normalizedHull_eq_convexHull [DecidableEq J]
97     (V : (J → ℝ) →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) (hn : l.comp V = mass) :
98     normalizedHull V l = convexHull ℝ (Set.range (generator V)) := by
99   apply Set.Subset.antisymm
100   · intro x hx
101     rw [normalizedHull_eq_prior_image V l hn] at hx
102     obtain ⟨a,ha,rfl⟩ := hx
103     rw [synthesis_sum]
104     exact (convex_convexHull ℝ _).sum_mem (fun j _ => ha.1 j) ha.2
105       (fun j _ => subset_convexHull ℝ _ ⟨j,rfl⟩)
106   · apply convexHull_min _ (normalizedHull_convex V l)
107     rintro _ ⟨j,rfl⟩
108     exact ⟨generator_mem V j,mass_generator V l hn j⟩
109 
110 end Komorebi.LSM.PositiveLift

Back to source controls