PredictableResidualAffine.lean

1 import KomorebiLSM.PredictableResidual
2 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
3 
4 /-! Exact interval-affine transport of actual conditional residuals on
5 arbitrary probability spaces. Countability is used only to put all transport
6 identities on one common full-measure event. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.PredictableResidualAffine
9 open MeasureTheory
10 open scoped BigOperators
11 variable {Ω J : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
12 
13 /-- Conditional expectation commutes with every real affine map, including
14 zero scale, on an arbitrary probability sample space. -/
15 theorem condExp_affine_ae {m : MeasurableSpace Ω} (hm : m≤mΩ)
16     (X : Ω → ℝ) (hX : Integrable X μ) (a c : ℝ) :
17     (μ[fun ω => a+c*X ω | m])=ᵐ[μ] (fun ω => a+c*(μ[X | m]) ω) := by
18   have h := ContinuousLinearMap.comp_condExp_add_const_comm hm hX
19     (c • ContinuousLinearMap.id ℝ ℝ) a
20   simpa only [smul_apply,ContinuousLinearMap.id_apply,smul_eq_mul,add_comm] using h.symm
21 
22 omit [IsProbabilityMeasure μ] in
23 /-- A.e. equality of the actual observations transports their actual centered
24 sums, since conditional expectation respects a.e. equality. -/
25 theorem centeredSum_congr_ae (ℱ : Filtration ℕ mΩ) (X Y : ℕ → Ω → ℝ)
26     (hXY : ∀ i,X i=ᵐ[μ] Y i) (n : ℕ) :
27     PredictableResidual.centeredSum (μ:=μ) ℱ X n=ᵐ[μ]
28       PredictableResidual.centeredSum (μ:=μ) ℱ Y n := by
29   have hce : ∀ᵐ ω∂μ,∀ i,(μ[X i | ℱ i]) ω=(μ[Y i | ℱ i]) ω :=
30     ae_all_iff.mpr (fun i => condExp_congr_ae (hXY i))
31   have hobs : ∀ᵐ ω∂μ,∀ i,X i ω=Y i ω := ae_all_iff.mpr hXY
32   filter_upwards [hce,hobs] with ω hce hobs
33   apply Finset.sum_congr rfl
34   intro i _
35   rw [hobs i,hce i]
36 
37 /-- Every finite actual affine centered sum is exactly scaled a.e.; the
38 shift cancels inside the true conditional expectation. -/
39 theorem centeredSum_affine_ae (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
40     (hX : ∀ i,Integrable (X i) μ) (a c : ℝ) (n : ℕ) :
41     PredictableResidual.centeredSum (μ:=μ) ℱ (fun i ω => a+c*X i ω) n=ᵐ[μ]
42       (fun ω => c*PredictableResidual.centeredSum (μ:=μ) ℱ X n ω) := by
43   have hce : ∀ᵐ ω∂μ,∀ i,
44       (μ[fun ω => a+c*X i ω | ℱ i]) ω=a+c*(μ[X i | ℱ i]) ω :=
45     ae_all_iff.mpr (fun i => condExp_affine_ae (ℱ.le i) (X i) (hX i) a c)
46   filter_upwards [hce] with ω hce
47   simp only [PredictableResidual.centeredSum]
48   rw [Finset.mul_sum]
49   apply Finset.sum_congr rfl
50   intro i _
51   rw [hce i]
52   ring
53 
54 /-- Normalize every declared interval. The degenerate interval uses zero,
55 so zero width is covered without an invalid division. -/
56 noncomputable def normalizedProcess (lower width : J → ℝ) (X : J → ℕ → Ω → ℝ)
57     (j : J) (i : ℕ) (ω : Ω) : ℝ := by
58   classical
59   exact if width j=0 then 0 else (X j i ω-lower j)/width j
60 
61 theorem normalized_adapted (ℱ : Filtration ℕ mΩ)
62     (lower width : J → ℝ) (X : J → ℕ → Ω → ℝ)
63     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i)) :
64     ∀ j i,Measurable[ℱ (i+1)] (normalizedProcess lower width X j i) := by
65   intro j i
66   by_cases hw : width j=0
67   · have he : normalizedProcess lower width X j i=(fun _ : Ω => (0:ℝ)) := by
68       funext ω
69       exact ite_eq_left hw
70     rw [he]
71     exact measurable_const
72   · have he : normalizedProcess lower width X j i=(fun ω : Ω => (X j i ω-lower j)/width j) := by
73       funext ω
74       exact ite_eq_right hw
75     rw [he]
76     exact ((hX j i).sub_const (lower j)).div_const (width j)
77 
78 omit [IsProbabilityMeasure μ] in
79 theorem normalized_mem_unit_ae (lower width : J → ℝ) (X : J → ℕ → Ω → ℝ)
80     (hw : ∀ j,0≤width j)
81     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (lower j) (lower j+width j)) :
82     ∀ j i,∀ᵐ ω∂μ,normalizedProcess lower width X j i ω∈Set.Icc (0:ℝ) 1 := by
83   intro j i
84   by_cases hj : width j=0
85   · simp only [normalizedProcess,ite_eq_left hj,Set.mem_Icc]
86     exact Filter.Eventually.of_forall (fun _ => ⟨le_rfl,zero_le_one⟩)
87   · have hp : 0<width j := lt_of_le_of_ne (hw j) (Ne.symm hj)
88     filter_upwards [hb j i] with ω hω
89     simp only [normalizedProcess,ite_eq_right hj,Set.mem_Icc]
90     exact ⟨div_nonneg (sub_nonneg.mpr hω.1) hp.le,
91       (div_le_iff₀ hp).mpr (by linarith [hω.2])⟩
92 
93 omit [IsProbabilityMeasure μ] in
94 /-- The original observation equals its normalized affine representation,
95 including zero-width intervals, rather than merely sharing a range bound. -/
96 theorem affine_normalized_ae (lower width : J → ℝ) (X : J → ℕ → Ω → ℝ)
97     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (lower j) (lower j+width j)) :
98     ∀ j i,X j i=ᵐ[μ] (fun ω => lower j+width j*normalizedProcess lower width X j i ω) := by
99   intro j i
100   by_cases hj : width j=0
101   · filter_upwards [hb j i] with ω hω
102     simp only [normalizedProcess,hj,zero_mul,add_zero]
103     linarith [hω.1,hω.2]
104   · apply Filter.Eventually.of_forall
105     intro ω
106     simp only [normalizedProcess,ite_eq_right hj]
107     field_simp [hj]
108     ring
109 
110 /-- All actual interval-width centered sums and their unit-range versions
111 share one common full-measure transport event. -/
112 theorem centeredSum_normalized_ae [Countable J] (ℱ : Filtration ℕ mΩ)
113     (lower width : J → ℝ) (X : J → ℕ → Ω → ℝ)
114     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i)) (hw : ∀ j,0≤width j)
115     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (lower j) (lower j+width j)) :
116     ∀ᵐ ω∂μ,∀ j n,PredictableResidual.centeredSum (μ:=μ) ℱ (X j) n ω=
117       width j*PredictableResidual.centeredSum (μ:=μ) ℱ
118         (normalizedProcess lower width X j) n ω := by
119   have hunit := normalized_mem_unit_ae lower width X hw hb
120   have hadapt := normalized_adapted ℱ lower width X hX
121   have hi (j : J) (i : ℕ) : Integrable (normalizedProcess lower width X j i) μ :=
122     Integrable.of_mem_Icc (0:ℝ) 1 ((hadapt j i).mono (ℱ.le (i+1)) le_rfl).aemeasurable
123       (hunit j i)
124   have hobs := affine_normalized_ae lower width X hb
125   apply ae_all_iff.mpr
126   intro j
127   apply ae_all_iff.mpr
128   intro n
129   exact (centeredSum_congr_ae ℱ (X j)
130     (fun i ω => lower j+width j*normalizedProcess lower width X j i ω) (hobs j) n).trans
131       (centeredSum_affine_ae ℱ (normalizedProcess lower width X j) (hi j) (lower j) (width j) n)
132 
133 /-- On one full-measure event, every simultaneous positive-time bound for
134 the normalized process implies the width-scaled bound for the actual process. -/
135 theorem normalized_bound_transfer_ae [Countable J] (ℱ : Filtration ℕ mΩ)
136     (lower width : J → ℝ) (X : J → ℕ → Ω → ℝ)
137     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i)) (hw : ∀ j,0≤width j)
138     (hb : ∀ j i,∀ᵐ ω∂μ,X j i ω∈Set.Icc (lower j) (lower j+width j))
139     (boundary : J → ℕ → ℝ) :
140     ∀ᵐ ω∂μ,(∀ j n,|PredictableResidual.centeredSum (μ:=μ) ℱ
141       (normalizedProcess lower width X j) (n+1) ω|≤boundary j n) →
142       ∀ j n,|PredictableResidual.centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤width j*boundary j n := by
143   filter_upwards [centeredSum_normalized_ae ℱ lower width X hX hw hb] with ω he hall j n
144   rw [he j (n+1),abs_mul,abs_of_nonneg (hw j)]
145   exact mul_le_mul_of_nonneg_left (hall j n) (hw j)
146 
147 end Komorebi.LSM.PredictableResidualAffine

Back to source controls