ObservationPolicyTransport.lean

1 import KomorebiLSM.ObservationEquivalence
2 
3 set_option autoImplicit false
4 namespace Komorebi.LSM.ObservationEquivalence
5 open MeasureTheory ContinuousInstrument ContinuousRecords
6 noncomputable section
7 universe u
8 variable {Y Z : Type u} [MeasurableSpace Y] [MeasurableSpace Z]
9 variable {μ : Measure Y} {ν : Measure Z}
10 
11 theorem history_roundtrip (e : Y ≃ᵐ Z) (N : ℕ) (h : History Y N) :
12     historyEquiv e.symm N (historyEquiv e N h)=h := by
13   induction N with
14   | zero => cases h; rfl
15   | succ N ih => exact Prod.ext (ih h.1) (e.symm_apply_apply h.2)
16 
17 theorem history_roundtrip_reverse (e : Y ≃ᵐ Z) (N : ℕ) (h : History Z N) :
18     historyEquiv e N (historyEquiv e.symm N h)=h := by
19   exact history_roundtrip e.symm N h
20 
21 variable {A : Type*} [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
22 
23 omit [Fintype A] [MeasurableSingletonClass A] in
24 @[simp] theorem stepEquiv_symm (e : Y ≃ᵐ Z) :
25     stepEquiv (A := A) e.symm=(stepEquiv (A := A) e).symm := rfl
26 
27 omit [MeasurableSingletonClass A] in
28 theorem policy_ext (π ρ : Policy (A := A) (Y := Y))
29     (h : ∀ N x a,π.probability N x a=ρ.probability N x a) : π=ρ := by
30   rcases π with ⟨p,hp,sp⟩
31   rcases ρ with ⟨q,hq,sq⟩
32   have he : p=q := by funext N x a; exact h N x a
33   subst q
34   rfl
35 
36 omit [MeasurableSingletonClass A] in
37 /-- Inverse history recoding restores the same adaptive policy exactly. -/
38 theorem pullPolicy_roundtrip (e : Y ≃ᵐ Z) (π : Policy (A := A) (Y := Z)) :
39     pullPolicy e.symm (pullPolicy e π)=π := by
40   apply policy_ext
41   intro N h a
42   change π.probability N
43     (historyEquiv (stepEquiv (A := A) e) N (historyEquiv (stepEquiv (A := A) e.symm) N h)) a=π.probability N h a
44   rw [stepEquiv_symm,history_roundtrip_reverse]
45 
46 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
47 variable {C : BaseNorm.ProbabilityCone E}
48 
49 omit [MeasurableSingletonClass A] in
50 /-- A source fit and a target truth can be compared under exactly the same target history policy. -/
51 theorem forward_recordLaw (e : Y ≃ᵐ Z) (he : MeasurePreserving e μ ν) [IsFiniteMeasure ν]
52     (D : DensityInstrument (A := A) C μ) (π : Policy (A := A) (Y := Z)) (z : E) (N : ℕ) :
53     (recordLaw D (pullPolicy e π) z N).map (historyEquiv (stepEquiv (A := A) e) N)=
54       recordLaw (pullInstrument e.symm (he.symm e) D) π z N := by
55   have h := recordLaw_map e.symm (he.symm e) D (pullPolicy e π) z N
56   rw [pullPolicy_roundtrip] at h
57   have hm := congrArg (fun ρ : Measure (History (A × Y) N) =>
58     ρ.map (historyEquiv (stepEquiv (A := A) e) N)) h
59   rw [Measure.map_map (historyEquiv _ N).measurable (historyEquiv _ N).measurable] at hm
60   have hc : (historyEquiv (stepEquiv (A := A) e) N) ∘ (historyEquiv (stepEquiv (A := A) e.symm) N)=id := by
61     funext h
62     rw [stepEquiv_symm]
63     exact history_roundtrip_reverse _ N h
64   rw [hc,Measure.map_id] at hm
65   exact hm.symm
66 
67 end
68 end Komorebi.LSM.ObservationEquivalence

Back to source controls