ContinuousReferenceChange.lean

1 import KomorebiLSM.ContinuousInstrument
2 
3 /-! P52 reference changes: the new reference and reciprocal operator density
4 are constructed explicitly; equality of kernels follows by cancellation. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.ContinuousInstrument
7 open MeasureTheory ProbabilityTheory
8 open scoped ENNReal
9 variable {E A Y : Type*} [MeasurableSpace Y]
10 
11 /-- A strictly positive, normalized density for a change of reference. -/
12 structure ReferenceDensity (μ : Measure Y) where
13   weight : Y → ℝ
14   measurable_weight : Measurable weight
15   positive : ∀ᵐ y∂μ,0<weight y
16   integral_one : (∫ y,weight y∂μ)=1
17 
18 namespace ReferenceDensity
19 variable {μ : Measure Y} (R : ReferenceDensity μ)
20 
21 theorem integrable_weight : Integrable R.weight μ := integrable_of_integral_eq_one R.integral_one
22 
23 noncomputable def measure : Measure Y := μ.withDensity (fun y => ENNReal.ofReal (R.weight y))
24 
25 instance measure_probability : IsProbabilityMeasure R.measure := by
26   constructor
27   rw [measure,withDensity_apply _ MeasurableSet.univ,Measure.restrict_univ,
28     ← ofReal_integral_eq_lintegral_ofReal R.integrable_weight (R.positive.mono fun _ h => h.le),
29     R.integral_one]
30   exact ENNReal.ofReal_one
31 
32 theorem measure_ac : R.measure ≪ μ := withDensity_absolutelyContinuous _ _
33 
34 theorem original_ac : μ ≪ R.measure :=
35   withDensity_absolutelyContinuous' R.measurable_weight.ennreal_ofReal.aemeasurable
36     (R.positive.mono fun _ h => by simpa using h)
37 
38 theorem ae_iff {p : Y → Prop} : (∀ᵐ y∂R.measure,p y) ↔ ∀ᵐ y∂μ,p y :=
39   ⟨fun h => R.original_ac.ae_le h,fun h => R.measure_ac.ae_le h⟩
40 
41 variable [NormedAddCommGroup E] [NormedSpace ℝ E]
42 
43 /-- Reciprocal-density cancellation is an actual Bochner integral identity,
44 valid for every integrable vector-valued quantity. -/
45 theorem integral_reciprocal {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
46     (g : Y → F) :
47     (∫ y,(R.weight y)⁻¹ • g y∂R.measure)=∫ y,g y∂μ := by
48   rw [measure,integral_withDensity_eq_integral_toReal_smul R.measurable_weight.ennreal_ofReal
49     (ae_of_all _ fun y => ENNReal.ofReal_lt_top)]
50   apply integral_congr_ae
51   filter_upwards [R.positive] with y hy
52   rw [ENNReal.toReal_ofReal hy.le,smul_smul,mul_inv_cancel₀ hy.ne',one_smul]
53 
54 theorem integrable_reciprocal {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
55     {g : Y → F} (hg : Integrable g μ) :
56     Integrable (fun y => (R.weight y)⁻¹ • g y) R.measure := by
57   rw [measure,integrable_withDensity_iff_integrable_smul' R.measurable_weight.ennreal_ofReal
58     (ae_of_all _ fun y => ENNReal.ofReal_lt_top)]
59   apply hg.congr
60   filter_upwards [R.positive] with y hy
61   rw [ENNReal.toReal_ofReal hy.le,smul_smul,mul_inv_cancel₀ hy.ne',one_smul]
62 
63 end ReferenceDensity
64 
65 namespace DensityInstrument
66 variable [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
67 variable [MeasurableSpace E] [BorelSpace E]
68 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y}
69 variable (D : DensityInstrument (A := A) C μ) (R : ReferenceDensity μ)
70 
71 /-- The changed operator is B/r against the changed reference r μ. -/
72 noncomputable def reweighted : DensityInstrument (A := A) C R.measure where
73   op a y := (R.weight y)⁻¹ • D.op a y
74   measurable_op a := R.measurable_weight.inv.smul (D.measurable_op a)
75   integrable_op a := R.integrable_reciprocal (D.integrable_op a)
76   positive a := by
77     apply R.ae_iff.mpr
78     filter_upwards [R.positive,D.positive a] with y hy hp
79     intro z hz
80     exact C.smul_mem (inv_nonneg.mpr hy.le) (hp z hz)
81   mass_preserving a z := by
82     rw [R.integral_reciprocal]
83     exact D.mass_preserving a z
84 
85 omit [MeasurableSpace E] [BorelSpace E] in
86 theorem reweighted_density (a : A) (y : Y) (z : E) :
87     (D.reweighted R).density a y z=(R.weight y)⁻¹*D.density a y z := by
88   exact map_smul C.mass (R.weight y)⁻¹ (D.op a y z)
89 
90 
91 /-- The changed reference and changed density define exactly the same kernel. -/
92 theorem reweighted_kernel [IsProbabilityMeasure μ] (a : A) :
93     (D.reweighted R).kernel a=D.kernel a := by
94   apply DFunLike.ext
95   intro z
96   rw [(D.reweighted R).kernel_apply a z,D.kernel_apply a z]
97   have hg : Measurable (fun y => ENNReal.ofReal ((D.reweighted R).density a y z.1)) :=
98     (((D.reweighted R).density_measurable a).comp
99       (measurable_const.prodMk measurable_id)).ennreal_ofReal
100   change (μ.withDensity (fun y => ENNReal.ofReal (R.weight y))).withDensity
101     (fun y => ENNReal.ofReal ((D.reweighted R).density a y z.1))=
102       μ.withDensity (fun y => ENNReal.ofReal (D.density a y z.1))
103   rw [← withDensity_mul μ R.measurable_weight.ennreal_ofReal hg]
104   apply withDensity_congr_ae
105   filter_upwards [R.positive] with y hy
106   change ENNReal.ofReal (R.weight y)*ENNReal.ofReal ((D.reweighted R).density a y z.1)=_
107   rw [← ENNReal.ofReal_mul hy.le,D.reweighted_density R a y z.1]
108   congr 1
109   rw [← mul_assoc,mul_inv_cancel₀ hy.ne',one_mul]
110 
111 omit [MeasurableSpace E] [BorelSpace E] in
112 /-- Reciprocal rescaling cancels inside every normalized positive-density update. -/
113 theorem reweighted_normalized (a : A) (y : Y) (z : E) (hy : 0<R.weight y) :
114     ((D.reweighted R).density a y z)⁻¹ • (D.reweighted R).op a y z=
115       (D.density a y z)⁻¹ • D.op a y z := by
116   rw [D.reweighted_density R a y z]
117   change ((R.weight y)⁻¹*D.density a y z)⁻¹ • ((R.weight y)⁻¹ • D.op a y z)=_
118   rw [smul_smul,mul_inv_rev,inv_inv,mul_assoc,mul_inv_cancel₀ hy.ne',mul_one]
119 
120 omit [MeasurableSpace E] [BorelSpace E] in
121 /-- With the same fixed fallback, measurable update versions agree almost
122 surely under either equivalent reference measure. -/
123 theorem reweighted_update_ae (fallback : State C) (a : A) (z : State C) :
124     ∀ᵐ y∂μ,(D.reweighted R).update fallback a z y=D.update fallback a z y := by
125   have hN : ∀ᵐ y∂μ,y∉D.exceptional a :=
126     ae_iff.mpr (by simpa using D.exceptional_null a)
127   have hN' : ∀ᵐ y∂μ,y∉(D.reweighted R).exceptional a :=
128     R.ae_iff.mp (ae_iff.mpr (by simpa using (D.reweighted R).exceptional_null a))
129   filter_upwards [R.positive,hN,hN'] with y hy hN hN'
130   have hp : 0<(D.reweighted R).density a y z.1 ↔ 0<D.density a y z.1 := by
131     rw [D.reweighted_density R a y z.1]
132     exact mul_pos_iff_of_pos_left (inv_pos.mpr hy)
133   apply Subtype.ext
134   change (D.reweighted R).updateValue fallback a z y=D.updateValue fallback a z y
135   unfold updateValue
136   simp only [hN,hN',not_false_eq_true,true_and,hp]
137   split_ifs
138   · exact D.reweighted_normalized R a y z.1 hy
139   · rfl
140 
141 theorem reweighted_event [IsProbabilityMeasure μ] (a : A) (z : State C) (S : Set Y) :
142     ((D.reweighted R).kernel a z).real S=(D.kernel a z).real S := by
143   rw [D.reweighted_kernel R a]
144 
145 omit [MeasurableSpace E] [BorelSpace E] in
146 theorem reweighted_update_ae_changed (fallback : State C) (a : A) (z : State C) :
147     ∀ᵐ y∂R.measure,(D.reweighted R).update fallback a z y=D.update fallback a z y :=
148   R.ae_iff.mpr (D.reweighted_update_ae R fallback a z)
149 
150 end DensityInstrument
151 end Komorebi.LSM.ContinuousInstrument

Back to source controls