ContinuousRecordReference.lean

1 import KomorebiLSM.ContinuousRecords
2 import KomorebiLSM.ContinuousReferenceChange
3 
4 /-! P52 reference cancellation for actual complete finite record measures,
5 including arbitrary common measurable randomized policies. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.ContinuousRecordReference
8 open MeasureTheory ProbabilityTheory ContinuousInstrument ContinuousRecords
9 open scoped ENNReal
10 variable {X : Type*} [MeasurableSpace X]
11 
12 noncomputable def referenceWeight (f : X → ℝ≥0∞) : (n : ℕ) → History X n → ℝ≥0∞
13   | 0, _ => 1
14   | n+1, h => referenceWeight f n h.1*f h.2
15 
16 noncomputable def realWeight (r : X → ℝ) : (n : ℕ) → History X n → ℝ
17   | 0, _ => 1
18   | n+1, h => realWeight r n h.1*r h.2
19 
20 theorem referenceWeight_measurable (f : X → ℝ≥0∞) (hf : Measurable f) :
21     (n : ℕ) → Measurable (referenceWeight f n)
22   | 0 => measurable_const
23   | n+1 => ((referenceWeight_measurable f hf n).comp measurable_fst).mul (hf.comp measurable_snd)
24 
25 theorem realWeight_measurable (r : X → ℝ) (hr : Measurable r) :
26     (n : ℕ) → Measurable (realWeight r n)
27   | 0 => measurable_const
28   | n+1 => ((realWeight_measurable r hr n).comp measurable_fst).mul (hr.comp measurable_snd)
29 
30 /-- Changing every factor of the actual finite product reference multiplies
31 its density by the literal product of the reference densities. -/
32 theorem reference_withDensity (ν : Measure X) [IsFiniteMeasure ν]
33     (r : X → ℝ) (hr : Measurable r) : (n : ℕ) →
34     reference (ν.withDensity (fun x => ENNReal.ofReal (r x))) n=
35       (reference ν n).withDensity (referenceWeight (fun x => ENNReal.ofReal (r x)) n)
36   | 0 => by simp [reference,referenceWeight]
37   | n+1 => by
38     rw [reference,reference,reference_withDensity ν r hr n]
39     exact prod_withDensity (referenceWeight_measurable _ hr.ennreal_ofReal n) hr.ennreal_ofReal
40 
41 /-- All scalar factors are positive on one product-reference full-measure set. -/
42 theorem weight_valid_ae (ν : Measure X) [IsFiniteMeasure ν]
43     (r : X → ℝ) (hr : Measurable r) (hp : ∀ᵐ x∂ν,0<r x) : (n : ℕ) →
44     ∀ᵐ h∂reference ν n,
45       referenceWeight (fun x => ENNReal.ofReal (r x)) n h=ENNReal.ofReal (realWeight r n h) ∧
46         0<realWeight r n h
47   | 0 => by simp [referenceWeight,realWeight]
48   | n+1 => by
49     change ∀ᵐ h∂(reference ν n).prod ν,_
50     have hm : MeasurableSet {h : History X (n+1) |
51         referenceWeight (fun x => ENNReal.ofReal (r x)) (n+1) h=
52           ENNReal.ofReal (realWeight r (n+1) h) ∧ 0<realWeight r (n+1) h} :=
53       (measurableSet_eq_fun (referenceWeight_measurable _ hr.ennreal_ofReal (n+1))
54         (realWeight_measurable r hr (n+1)).ennreal_ofReal).inter
55           (measurableSet_lt measurable_const (realWeight_measurable r hr (n+1)))
56     apply (Measure.ae_prod_iff_ae_ae hm).mpr
57     filter_upwards [weight_valid_ae ν r hr hp n] with h hh
58     filter_upwards [hp] with x hx
59     exact ⟨by rw [referenceWeight,realWeight,hh.1,ENNReal.ofReal_mul hh.2.le],mul_pos hh.2 hx⟩
60 
61 variable {E A Y : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
62 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
63 variable [MeasurableSpace Y] [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A]
64 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y}
65 variable (D : DensityInstrument (A := A) C μ) (R : ReferenceDensity μ)
66 
67 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A] [Fintype A]
68   [MeasurableSingletonClass A] in
69 /-- The actual operator product carries the reciprocal product reference factor. -/
70 theorem run_reweighted (z : E) : (n : ℕ) → ∀ h : History (A × Y) n,
71     run (D.reweighted R) z n h=
72       (realWeight (fun s : A × Y => R.weight s.2) n h)⁻¹ • run D z n h
73   | 0, _ => by simp [run,realWeight]
74   | n+1, h => by
75     change (R.weight h.2.2)⁻¹ • D.op h.2.1 h.2.2 (run (D.reweighted R) z n h.1)=_
76     rw [run_reweighted z n h.1]
77     simp only [map_smul,smul_smul,realWeight,run,mul_inv_rev]
78 
79 omit [Fintype A] [MeasurableSingletonClass A] in
80 theorem stepReference_reweighted [SFinite μ] :
81     stepReference (A := A) R.measure=
82       (stepReference (A := A) μ).withDensity (fun s => ENNReal.ofReal (R.weight s.2)) := by
83   exact prod_withDensity_right R.measurable_weight.ennreal_ofReal
84 
85 omit [Fintype A] [MeasurableSingletonClass A] in
86 theorem step_weight_positive_ae [SFinite μ] :
87     ∀ᵐ s∂stepReference (A := A) μ,0<R.weight s.2 := by
88   apply (Measure.ae_prod_iff_ae_ae
89     (measurableSet_lt measurable_const (R.measurable_weight.comp measurable_snd))).mpr
90   exact Filter.Eventually.of_forall (fun _ => R.positive)
91 
92 /-- Every future event has the same probability after reciprocal reference
93 rescaling, for the same arbitrary measurable history policy. -/
94 theorem recordLaw_reweighted [IsProbabilityMeasure μ]
95     (π : Policy (A := A) (Y := Y)) (z : E) (n : ℕ) :
96     recordLaw (D.reweighted R) π z n=recordLaw D π z n := by
97   simp only [recordLaw]
98   rw [stepReference_reweighted R,reference_withDensity (stepReference (A := A) μ)
99     (fun s : A × Y => R.weight s.2) (R.measurable_weight.comp measurable_snd) n]
100   have hf : Measurable (referenceWeight (fun s : A × Y => ENNReal.ofReal (R.weight s.2)) n) :=
101     referenceWeight_measurable (fun s : A × Y => ENNReal.ofReal (R.weight s.2))
102       (R.measurable_weight.comp measurable_snd).ennreal_ofReal n
103   rw [← withDensity_mul _ hf (recordDensity_measurable (D.reweighted R) π z n)]
104   apply withDensity_congr_ae
105   filter_upwards [weight_valid_ae (stepReference (A := A) μ)
106     (fun s : A × Y => R.weight s.2) (R.measurable_weight.comp measurable_snd)
107     (step_weight_positive_ae R) n] with h hh
108   change referenceWeight _ n h*(π.weight n h*ENNReal.ofReal (C.mass (run (D.reweighted R) z n h)))=_
109   rw [run_reweighted D R z n h,map_smul,smul_eq_mul,hh.1]
110   rw [mul_left_comm,← ENNReal.ofReal_mul hh.2.le]
111   rw [← mul_assoc,mul_inv_cancel₀ hh.2.ne',one_mul]
112   rfl
113 
114 omit [MeasurableSpace E] [BorelSpace E] [MeasurableSpace A] [Fintype A]
115   [MeasurableSingletonClass A] in
116 theorem observationRun_reweighted (actions : ℕ → A) (z : E) :
117     (n : ℕ) → ∀ h : History Y n,
118     observationRun (D.reweighted R) actions z n h=
119       (realWeight R.weight n h)⁻¹ • observationRun D actions z n h
120   | 0, _ => by simp [observationRun,realWeight]
121   | n+1, h => by
122     change (R.weight h.2)⁻¹ • D.op (actions n) h.2
123       (observationRun (D.reweighted R) actions z n h.1)=_
124     rw [observationRun_reweighted actions z n h.1]
125     simp only [map_smul,smul_smul,realWeight,observationRun,mul_inv_rev]
126 
127 omit [MeasurableSpace A] [Fintype A] [MeasurableSingletonClass A] in
128 /-- The prescribed-action full observation law also stays exactly unchanged. -/
129 theorem observationLaw_reweighted [IsProbabilityMeasure μ]
130     (actions : ℕ → A) (z : E) (n : ℕ) :
131     observationLaw (D.reweighted R) actions z n=observationLaw D actions z n := by
132   simp only [observationLaw]
133   change (reference (μ.withDensity (fun y => ENNReal.ofReal (R.weight y))) n).withDensity _=_
134   rw [reference_withDensity μ R.weight R.measurable_weight n]
135   rw [← withDensity_mul _
136     (referenceWeight_measurable _ R.measurable_weight.ennreal_ofReal n)
137     (observationDensity_measurable (D.reweighted R) actions z n)]
138   apply withDensity_congr_ae
139   filter_upwards [weight_valid_ae μ R.weight R.measurable_weight R.positive n] with h hh
140   change referenceWeight _ n h*ENNReal.ofReal
141     (C.mass (observationRun (D.reweighted R) actions z n h))=_
142   rw [observationRun_reweighted D R actions z n h,map_smul,smul_eq_mul,hh.1]
143   rw [← ENNReal.ofReal_mul hh.2.le,← mul_assoc,mul_inv_cancel₀ hh.2.ne',one_mul]
144   rfl
145 
146 end Komorebi.LSM.ContinuousRecordReference

Back to source controls