VilleInequality.lean

1 import Mathlib.Probability.Martingale.OptionalStopping
2 import Mathlib.MeasureTheory.Measure.Continuity
3 
4 /-! The actual crossing event of a nonnegative supermartingale. Finite stopped
5 expectations are controlled before passing to every natural-number time. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.VilleInequality
8 open MeasureTheory ProbabilityTheory Set
9 open scoped ENNReal
10 variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
11 variable (F : Filtration ℕ ‹MeasurableSpace Ω›) (M : ℕ → Ω → ℝ)
12 
13 def crossingUpTo (c : ℝ) (N : ℕ) : Set Ω := {ω | ∃ n≤N,c≤M n ω}
14 def crossing (c : ℝ) : Set Ω := {ω | ∃ n,c≤M n ω}
15 
16 omit [IsProbabilityMeasure μ] in
17 theorem crossingUpTo_measurable (hM : Supermartingale M F μ) (c : ℝ) (N : ℕ) :
18     MeasurableSet (crossingUpTo M c N) := by
19   have he : crossingUpTo M c N=⋃ n : ℕ,⋃ _h : n≤N,{ω | c≤M n ω} := by
20     ext ω
21     simp only [crossingUpTo,mem_ofPred_eq,mem_iUnion,exists_prop]
22   rw [he]
23   exact MeasurableSet.iUnion fun n => MeasurableSet.iUnion fun _ =>
24     measurableSet_le measurable_const ((hM.stronglyMeasurable n).measurable.le (F.le n))
25 
26 omit [IsProbabilityMeasure μ] in
27 theorem crossing_measurable (hM : Supermartingale M F μ) (c : ℝ) :
28     MeasurableSet (crossing M c) := by
29   have he : crossing M c=⋃ n : ℕ,{ω | c≤M n ω} := by ext ω; simp [crossing]
30   rw [he]
31   exact MeasurableSet.iUnion fun n =>
32     measurableSet_le measurable_const ((hM.stronglyMeasurable n).measurable.le (F.le n))
33 
34 /-- Bounded hitting and optional stopping give the finite crossing bound. -/
35 theorem finite_crossing_bound (hM : Supermartingale M F μ)
36     (h0 : ∀ n ω,0≤M n ω) (hinitial : (∫ ω,M 0 ω ∂μ)≤1)
37     (c : ℝ) (hc : 0<c) (N : ℕ) : μ (crossingUpTo M c N)≤ENNReal.ofReal (1/c) := by
38   let τ : Ω → WithTop ℕ := fun ω => (hittingBtwn M (Ici c) 0 N ω : ℕ)
39   have hτ : IsStoppingTime F τ :=
40     hM.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici
41   have hb : ∀ ω,τ ω≤N := fun ω => by
42     change ((hittingBtwn M (Ici c) 0 N ω : ℕ) : WithTop ℕ)≤(N : WithTop ℕ)
43     exact_mod_cast hittingBtwn_le (u := M) (s := Ici c) (n := 0) (m := N) ω
44   have hint : Integrable (stoppedValue M τ) μ := integrable_stoppedValue ℕ hτ hM.integrable hb
45   have hstop : (∫ ω,stoppedValue M τ ω ∂μ)≤∫ ω,M 0 ω ∂μ := by
46     have he := hM.neg.expected_stoppedValue_mono (isStoppingTime_const F 0) hτ
47       (fun ω => by change (0 : WithTop ℕ)≤τ ω; exact bot_le) hb
48     change (∫ ω,-M 0 ω ∂μ)≤∫ ω,-stoppedValue M τ ω ∂μ at he
49     rw [integral_neg,integral_neg,neg_le_neg_iff] at he
50     exact he
51   have hhit (ω : Ω) (hω : ω∈crossingUpTo M c N) : c≤stoppedValue M τ ω := by
52     apply stoppedValue_hittingBtwn_mem
53     obtain ⟨n,hn,hval⟩ := hω
54     exact ⟨n,⟨Nat.zero_le _,hn⟩,hval⟩
55   have hs := crossingUpTo_measurable μ F M hM c N
56   have hl := setIntegral_ge_of_const_le_real hs (measure_ne_top μ _) hhit hint.integrableOn
57   have hn : 0≤ᵐ[μ] stoppedValue M τ := ae_of_all _ fun ω => h0 _ _
58   have hu := (setIntegral_le_integral hint hn (s := crossingUpTo M c N)).trans (hstop.trans hinitial)
59   have hr : μ.real (crossingUpTo M c N)≤1/c := (le_div_iff₀ hc).mpr (by nlinarith)
60   simpa only [Measure.real,ENNReal.ofReal_toReal (measure_ne_top μ _)] using ENNReal.ofReal_le_ofReal hr
61 
62 /-- Ville's inequality for the literal event of ever crossing the threshold. -/
63 theorem crossing_bound (hM : Supermartingale M F μ)
64     (h0 : ∀ n ω,0≤M n ω) (hinitial : (∫ ω,M 0 ω ∂μ)≤1)
65     (c : ℝ) (hc : 0<c) : μ (crossing M c)≤ENNReal.ofReal (1/c) := by
66   have hmono : Monotone (crossingUpTo M c) := by
67     intro n k hnk ω hω
68     obtain ⟨i,hi,hval⟩ := hω
69     exact ⟨i,hi.trans hnk,hval⟩
70   have he : crossing M c=⋃ N : ℕ,crossingUpTo M c N := by
71     ext ω
72     constructor
73     · rintro ⟨n,hn⟩
74       exact mem_iUnion.mpr ⟨n,n,le_rfl,hn⟩
75     · intro h
76       obtain ⟨N,n,_,hn⟩ := mem_iUnion.mp h
77       exact ⟨n,hn⟩
78   rw [he,hmono.measure_iUnion]
79   exact iSup_le fun N => finite_crossing_bound μ F M hM h0 hinitial c hc N
80 
81 /-- Every data-selected natural time is covered by the same actual event. -/
82 theorem selected_time_bound (hM : Supermartingale M F μ)
83     (h0 : ∀ n ω,0≤M n ω) (hinitial : (∫ ω,M 0 ω ∂μ)≤1)
84     (c : ℝ) (hc : 0<c) (t : Ω → ℕ) :
85     μ {ω | c≤M (t ω) ω}≤ENNReal.ofReal (1/c) := by
86   have hs : {ω | c≤M (t ω) ω}⊆crossing M c := by
87     intro ω hω
88     exact ⟨t ω,hω⟩
89   exact (measure_mono hs).trans (crossing_bound μ F M hM h0 hinitial c hc)
90 
91 end Komorebi.LSM.VilleInequality

Back to source controls