ObservationEquivalence.lean

1 import KomorebiLSM.ContinuousRecords
2 import Mathlib.MeasureTheory.Integral.Lebesgue.Map
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.ObservationEquivalence
6 open MeasureTheory ContinuousInstrument ContinuousRecords
7 open scoped ENNReal
8 noncomputable section
9 
10 universe u
11 variable {Y Z : Type u} [MeasurableSpace Y] [MeasurableSpace Z]
12 variable {μ : Measure Y} {ν : Measure Z}
13 
14 /-- A measurable observation equivalence transports an actual density measure. -/
15 theorem map_withDensity (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν) (f : Z → ℝ≥0∞) :
16     (μ.withDensity (fun y => f (e y))).map e = ν.withDensity f := by
17   ext S hS
18   rw [Measure.map_apply e.measurable hS,withDensity_apply _ (e.measurable hS),withDensity_apply _ hS]
19   exact he.setLIntegral_comp_preimage_emb e.measurableEmbedding f S
20 
21 /-- The equivalence is applied in chronological order to every coordinate of a history. -/
22 def historyEquiv (e : Y ≃ᵐ Z) : (N : ℕ) → History Y N ≃ᵐ History Z N
23   | 0 => MeasurableEquiv.refl _
24   | N+1 => (historyEquiv e N).prodCongr e
25 
26 theorem historyEquiv_eq_mapHistory (e : Y ≃ᵐ Z) (N : ℕ) (h : History Y N) :
27     historyEquiv e N h=mapHistory e N h := by
28   induction N with
29   | zero => cases h; rfl
30   | succ N ih => exact Prod.ext (ih h.1) rfl
31 
32 theorem history_preserving (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν) [IsFiniteMeasure μ] :
33     (N : ℕ) → MeasurePreserving (historyEquiv e N) (reference μ N) (reference ν N)
34   | 0 => by
35     change MeasurePreserving (id : PUnit → PUnit) (Measure.dirac PUnit.unit) (Measure.dirac PUnit.unit)
36     exact MeasurePreserving.id _
37   | N+1 => (history_preserving e he N).prod he
38 
39 variable {E A : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
40 variable {C : BaseNorm.ProbabilityCone E}
41 
42 /-- Pullback changes the actual operator density and derives all instrument fields. -/
43 def pullInstrument (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν)
44     (D : DensityInstrument (A := A) C ν) : DensityInstrument (A := A) C μ where
45   op a y := D.op a (e y)
46   measurable_op a := (D.measurable_op a).comp e.measurable
47   integrable_op a := he.integrable_comp_of_integrable (D.integrable_op a)
48   positive a := he.quasiMeasurePreserving.ae (D.positive a)
49   mass_preserving a z := by
50     rw [he.integral_comp' (D.op a)]
51     exact D.mass_preserving a z
52 
53 @[simp] theorem pullInstrument_op (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν)
54     (D : DensityInstrument (A := A) C ν) (a : A) (y : Y) :
55     (pullInstrument e he D).op a y=D.op a (e y) := rfl
56 
57 section Records
58 variable [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
59 
60 /-- Actions are retained, and only the observation component is recoded. -/
61 def stepEquiv (e : Y ≃ᵐ Z) : (A × Y) ≃ᵐ (A × Z) :=
62   (MeasurableEquiv.refl A).prodCongr e
63 
64 omit [MeasurableSingletonClass A] in
65 theorem step_preserving (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν) [IsFiniteMeasure μ] :
66     MeasurePreserving (stepEquiv (A := A) e) (stepReference (A := A) μ) (stepReference (A := A) ν) :=
67   (MeasurePreserving.id Measure.count).prod he
68 
69 /-- The pulled policy sees exactly the corresponding recoded full history. -/
70 def pullPolicy (e : Y ≃ᵐ Z) (π : Policy (A := A) (Y := Z)) : Policy (A := A) (Y := Y) where
71   probability N h a := π.probability N (historyEquiv (stepEquiv (A := A) e) N h) a
72   measurable_probability N a := (π.measurable_probability N a).comp (historyEquiv _ N).measurable
73   sum_one N _h := π.sum_one N _
74 
75 omit [MeasurableSingletonClass A] in
76 theorem pullPolicy_weight (e : Y ≃ᵐ Z) (π : Policy (A := A) (Y := Z)) (N : ℕ)
77     (h : History (A × Y) N) :
78     (pullPolicy e π).weight N h=π.weight N (historyEquiv (stepEquiv (A := A) e) N h) := by
79   induction N with
80   | zero => rfl
81   | succ N ih =>
82     change (pullPolicy e π).weight N h.1 * π.probability N
83       (historyEquiv (stepEquiv (A := A) e) N h.1) h.2.1 =
84       π.weight N (historyEquiv (stepEquiv (A := A) e) N h.1) * π.probability N
85         (historyEquiv (stepEquiv (A := A) e) N h.1) h.2.1
86     rw [ih]
87 
88 omit [Fintype A] [MeasurableSingletonClass A] in
89 theorem pull_run (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν)
90     (D : DensityInstrument (A := A) C ν) (z : E) (N : ℕ) (h : History (A × Y) N) :
91     run (pullInstrument e he D) z N h=run D z N (historyEquiv (stepEquiv (A := A) e) N h) := by
92   induction N with
93   | zero => rfl
94   | succ N ih =>
95     change D.op h.2.1 (e h.2.2) (run (pullInstrument e he D) z N h.1) =
96       D.op h.2.1 (e h.2.2) (run D z N (historyEquiv (stepEquiv (A := A) e) N h.1))
97     rw [ih]
98 
99 omit [MeasurableSingletonClass A] in
100 theorem pull_recordDensity (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν)
101     (D : DensityInstrument (A := A) C ν) (π : Policy (A := A) (Y := Z))
102     (z : E) (N : ℕ) (h : History (A × Y) N) :
103     recordDensity (pullInstrument e he D) (pullPolicy e π) z N h=
104       recordDensity D π z N (historyEquiv (stepEquiv (A := A) e) N h) := by
105   unfold recordDensity
106   rw [pullPolicy_weight,pull_run]
107 
108 omit [MeasurableSingletonClass A] in
109 /-- The actual finite full record law is pushed forward, with the corresponding history policy. -/
110 theorem recordLaw_map (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν) [IsFiniteMeasure μ]
111     (D : DensityInstrument (A := A) C ν) (π : Policy (A := A) (Y := Z)) (z : E) (N : ℕ) :
112     (recordLaw (pullInstrument e he D) (pullPolicy e π) z N).map
113       (historyEquiv (stepEquiv (A := A) e) N)=recordLaw D π z N := by
114   have hd : recordDensity (pullInstrument e he D) (pullPolicy e π) z N=
115       fun h => recordDensity D π z N (historyEquiv (stepEquiv (A := A) e) N h) := by
116     funext h
117     exact pull_recordDensity e he D π z N h
118   unfold recordLaw
119   rw [hd]
120   exact map_withDensity _ (history_preserving (stepEquiv (A := A) e) (step_preserving e he) N) _
121 
122 end Records
123 end
124 end Komorebi.LSM.ObservationEquivalence

Back to source controls