AffineObservationTransport.lean

1 import KomorebiLSM.ObservationPolicyTransport
2 import KomorebiLSM.BernsteinKernel
3 import KomorebiLSM.UniformIntervalMoments
4 import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
5 
6 set_option autoImplicit false
7 namespace Komorebi.LSM.AffineObservationTransport
8 open MeasureTheory ContinuousInstrument ContinuousRecords ObservationEquivalence
9 noncomputable section
10 
11 /-- The actual affine observation equivalence, with its literal inverse. -/
12 def equiv : ℝ ≃ᵐ ℝ where
13   toFun v := 2*v-1
14   invFun u := (u+1)/2
15   left_inv v := by ring
16   right_inv u := by ring
17   measurable_toFun := by
18     change Measurable (fun v : ℝ => 2*v-1)
19     fun_prop
20   measurable_invFun := by
21     change Measurable (fun u : ℝ => (u+1)/2)
22     fun_prop
23 
24 @[simp] theorem equiv_apply (v : ℝ) : equiv v=2*v-1 := rfl
25 @[simp] theorem equiv_symm_apply (u : ℝ) : equiv.symm u=(u+1)/2 := rfl
26 
27 theorem preimage_interval : equiv ⁻¹' Set.Icc (-1 : ℝ) 1=Set.Icc (0 : ℝ) 1 := by
28   ext v
29   change (-1≤2*v-1 ∧ 2*v-1≤1) ↔ (0≤v ∧ v≤1)
30   constructor <;> rintro ⟨h0,h1⟩ <;> constructor <;> linarith
31 
32 /-- The factor one half is derived from actual Lebesgue scaling and translation. -/
33 theorem map_volume : volume.map equiv=ENNReal.ofReal (1/2 : ℝ) • volume := by
34   have he : (equiv : ℝ → ℝ)=(fun x : ℝ => x+(-1)) ∘ (fun v : ℝ => 2*v) := by
35     funext v
36     simp only [equiv_apply,Function.comp_apply]
37     ring
38   rw [he,← Measure.map_map (by fun_prop) (by fun_prop),
39     Real.map_volume_mul_left (by norm_num : (2 : ℝ)≠0),Measure.map_smul _ ((by fun_prop : Measurable (fun x : ℝ => x+(-1))).aemeasurable),
40     (measurePreserving_add_right volume (-1)).map_eq]
41   norm_num
42 
43 /-- The unit-interval Bernstein reference pushes forward to the actual normalized symmetric reference. -/
44 theorem measure_preserving : MeasurePreserving equiv BernsteinKernel.measure UniformIntervalMoments.measure := by
45   refine ⟨equiv.measurable,?_⟩
46   calc
47     BernsteinKernel.measure.map equiv = (volume.map equiv).restrict (Set.Icc (-1 : ℝ) 1) := by
48       rw [Measure.restrict_map equiv.measurable measurableSet_Icc,preimage_interval]
49       rfl
50     _ = (ENNReal.ofReal (1/2 : ℝ) • volume).restrict (Set.Icc (-1 : ℝ) 1) := by rw [map_volume]
51     _ = UniformIntervalMoments.measure := by
52       rw [Measure.restrict_smul]
53       unfold UniformIntervalMoments.measure AveragedCongruence.uniformInterval ProbabilityTheory.cond
54       rw [Real.volume_Ioc,restrict_Ioc_eq_restrict_Icc]
55       norm_num [ENNReal.ofReal_div_of_pos (by norm_num : (0 : ℝ)<2)]
56 
57 theorem inverse_measure_preserving :
58     MeasurePreserving equiv.symm UniformIntervalMoments.measure BernsteinKernel.measure :=
59   measure_preserving.symm equiv
60 
61 variable {E A : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
62 variable {C : BaseNorm.ProbabilityCone E}
63 
64 /-- Symmetric-interval densities pulled to the actual Bernstein reference. -/
65 def pullInstrument (D : DensityInstrument (A := A) C UniformIntervalMoments.measure) :
66     DensityInstrument (A := A) C BernsteinKernel.measure :=
67   ObservationEquivalence.pullInstrument equiv measure_preserving D
68 
69 @[simp] theorem pullInstrument_op (D : DensityInstrument (A := A) C UniformIntervalMoments.measure)
70     (a : A) (v : ℝ) : (pullInstrument D).op a v=D.op a (2*v-1) := rfl
71 
72 /-- Unit-interval fitted densities moved to the actual symmetric reference. -/
73 def pushInstrument (D : DensityInstrument (A := A) C BernsteinKernel.measure) :
74     DensityInstrument (A := A) C UniformIntervalMoments.measure :=
75   ObservationEquivalence.pullInstrument equiv.symm inverse_measure_preserving D
76 
77 @[simp] theorem pushInstrument_op (D : DensityInstrument (A := A) C BernsteinKernel.measure)
78     (a : A) (u : ℝ) : (pushInstrument D).op a u=D.op a ((u+1)/2) := rfl
79 
80 section Records
81 variable [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
82 
83 def pullPolicy (π : Policy (A := A) (Y := ℝ)) : Policy (A := A) (Y := ℝ) :=
84   ObservationEquivalence.pullPolicy equiv π
85 
86 def pushPolicy (π : Policy (A := A) (Y := ℝ)) : Policy (A := A) (Y := ℝ) :=
87   ObservationEquivalence.pullPolicy equiv.symm π
88 
89 omit [MeasurableSingletonClass A] in
90 theorem pull_recordLaw (D : DensityInstrument (A := A) C UniformIntervalMoments.measure)
91     (π : Policy (A := A) (Y := ℝ)) (z : E) (N : ℕ) :
92     (recordLaw (pullInstrument D) (pullPolicy π) z N).map
93       (historyEquiv (stepEquiv (A := A) equiv) N)=recordLaw D π z N :=
94   recordLaw_map equiv measure_preserving D π z N
95 
96 omit [MeasurableSingletonClass A] in
97 theorem push_recordLaw (D : DensityInstrument (A := A) C BernsteinKernel.measure)
98     (π : Policy (A := A) (Y := ℝ)) (z : E) (N : ℕ) :
99     (recordLaw (pushInstrument D) (pushPolicy π) z N).map
100       (historyEquiv (stepEquiv (A := A) equiv.symm) N)=recordLaw D π z N :=
101   recordLaw_map equiv.symm inverse_measure_preserving D π z N
102 
103 omit [MeasurableSingletonClass A] in
104 /-- The pushed fit uses the same target adaptive policy as the native symmetric-interval model. -/
105 theorem push_recordLaw_forward (D : DensityInstrument (A := A) C BernsteinKernel.measure)
106     (π : Policy (A := A) (Y := ℝ)) (z : E) (N : ℕ) :
107     (recordLaw D (pullPolicy π) z N).map (historyEquiv (stepEquiv (A := A) equiv) N)=
108       recordLaw (pushInstrument D) π z N :=
109   forward_recordLaw equiv measure_preserving D π z N
110 
111 end Records
112 end
113 end Komorebi.LSM.AffineObservationTransport

Back to source controls