TestTopology.lean

1 import KomorebiLSM.TestCones
2 import Mathlib.Topology.Algebra.Module.FiniteDimension
3 import Mathlib.Topology.Order.Compact
4 
5 /-! Finite-dimensional probability-domain topology. The compactness proof uses
6 an actual closed observation embedding, not a boundedness assumption. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.TestDomains
9 open scoped BigOperators
10 open FiniteInstruments
11 variable {E S : Type*} [AddCommGroup E] [Module ℝ E]
12 variable [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
13 variable [T2Space E] [FiniteDimensional ℝ E]
14 
15 theorem allTests_closed (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
16     IsClosed (allTests B l) := by
17   have he : allTests B l = ⋂ w, {x | 0 ≤ l (wordAction B w x)} := by
18     ext x; simp only [allTests,Set.mem_ofPred_eq,Set.mem_iInter,observe_apply]
19   rw [he]
20   exact isClosed_iInter (fun w => isClosed_le continuous_const
21     (l.comp (wordAction B w)).continuous_of_finiteDimensional)
22 
23 theorem testLevel_closed (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) (h : ℕ) :
24     IsClosed (testLevel B l h) := by
25   have he : testLevel B l h = ⋂ w, ⋂ (_ : w.length ≤ h), {x | 0 ≤ l (wordAction B w x)} := by
26     ext x; simp only [testLevel,Set.mem_ofPred_eq,Set.mem_iInter,observe_apply]
27   rw [he]
28   exact isClosed_iInter (fun w => isClosed_iInter (fun _ => isClosed_le continuous_const
29     (l.comp (wordAction B w)).continuous_of_finiteDimensional))
30 
31 theorem base_closed (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ) :
32     IsClosed (base B l) :=
33   (allTests_closed B l).inter (isClosed_eq l.continuous_of_finiteDimensional continuous_const)
34 
35 /-- A finite observable linear space embeds as a closed subspace of all tests. -/
36 theorem observe_closedEmbedding (B : S → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
37     (ho : Function.Injective (observe B l)) : Topology.IsClosedEmbedding (observe B l) :=
38   LinearMap.isClosedEmbedding_of_injective (LinearMap.ker_eq_bot.mpr ho)
39 
40 section Causal
41 variable {A O : Type*} [Fintype O]
42 variable (B : A × O → E →ₗ[ℝ] E) (l : E →ₗ[ℝ] ℝ)
43 variable (hm : ∀ a x, ∑ o, l (B (a,o) x) = l x)
44 include hm
45 
46 /-- Closed finite-dimensional observation range plus bounded tests gives compactness. -/
47 theorem base_compact (ho : Function.Injective (observe B l)) :
48     IsCompact (base B l) := by
49   let K : Set (List (A × O) → ℝ) :=
50     {v | (∀ w, v w ∈ Set.Icc (0 : ℝ) 1) ∧ v [] = 1}
51   have hk : IsCompact K :=
52     (isCompact_pi_infinite (fun _ => isCompact_Icc)).inter_right
53       (isClosed_eq (continuous_apply []) continuous_const)
54   have he : base B l = observe B l ⁻¹' K := by
55     ext x
56     constructor
57     · intro hx
58       exact ⟨base_test_bounds B l hm hx,hx.2⟩
59     · rintro ⟨hx,he⟩
60       exact ⟨fun w => (hx w).1,he⟩
61   rw [he]
62   exact (observe_closedEmbedding B l ho).isCompact_preimage hk
63 
64 end Causal
65 end Komorebi.LSM.TestDomains

Back to source controls