ConditionalEventTV.lean

1 import KomorebiLSM.ContinuousTV
2 import Mathlib.Probability.ConditionalProbability
3 
4 /-! Eventwise comparison of the actual conditional probability measures.
5 Conditioning is used only when the common event has positive mass under both laws. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.ConditionalEventTV
8 open MeasureTheory ProbabilityTheory
9 open scoped ENNReal ProbabilityTheory
10 variable {Ω : Type*} [MeasurableSpace Ω]
11 
12 theorem event_error_le_tv (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
13     (S : Set Ω) (hS : MeasurableSet S) :
14     |P.real S-Q.real S|≤SequentialLowerCertificate.lawTV P Q := by
15   let φ : Ω → ℝ := S.indicator (fun _ => 1)
16   have hm : Measurable φ := measurable_const.indicator hS
17   have h0 : ∀ x,0≤φ x := by intro x; by_cases hx : x∈S <;> simp [φ,hx]
18   have h1 : ∀ x,φ x≤1 := by intro x; by_cases hx : x∈S <;> simp [φ,hx]
19   have h := SequentialLowerCertificate.bounded_test_integral_le_tv P Q φ hm h0 h1
20   simpa [φ,integral_indicator hS,Measure.real] using h
21 
22 theorem conditional_real (P : Measure Ω) (S T : Set Ω) (hS : MeasurableSet S) :
23     (ProbabilityTheory.cond P S).real T=P.real (S∩T)/P.real S := by
24   rw [Measure.real,ProbabilityTheory.cond_apply hS,ENNReal.toReal_mul,ENNReal.toReal_inv]
25   simp only [Measure.real,div_eq_mul_inv,mul_comm]
26 
27 /-- Scalar normalization uses both positive denominators and the actual event mass bound. -/
28 theorem ratio_error {a b p q δ : ℝ} (hp : 0<p) (hq : 0<q) (hb0 : 0≤b) (hb : b≤q)
29     (hδ : 0≤δ) (hab : |a-b|≤δ) (hpq : |p-q|≤δ) :
30     |a/p-b/q|≤2*δ/p := by
31   have hbq0 : 0≤b/q := div_nonneg hb0 hq.le
32   have hbq1 : b/q≤1 := (div_le_one hq).mpr hb
33   have he : a/p-b/q=(a-b)/p+(b/q)*((q-p)/p) := by field_simp; ring
34   rw [he]
35   calc |(a-b)/p+(b/q)*((q-p)/p)|≤|(a-b)/p|+|(b/q)*((q-p)/p)| := abs_add_le _ _
36     _ = |a-b|/p+(b/q)*(|p-q|/p) := by
37       rw [abs_mul,abs_div,abs_of_pos hp,abs_of_nonneg hbq0,abs_div,abs_of_pos hp,abs_sub_comm q p]
38     _ ≤ δ/p+(b/q)*(δ/p) := add_le_add (div_le_div_of_nonneg_right hab hp.le)
39       (mul_le_mul_of_nonneg_left (div_le_div_of_nonneg_right hpq hp.le) hbq0)
40     _ ≤ δ/p+δ/p := add_le_add le_rfl (by
41       simpa using mul_le_mul_of_nonneg_right hbq1 (div_nonneg hδ hp.le))
42     _ = 2*δ/p := by ring
43 
44 /-- The bound concerns literal normalized restrictions, with both event masses
45 strictly positive. It controls every measurable event under those measures. -/
46 theorem conditional_event_error (P Q : Measure Ω) [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
47     (S T : Set Ω) (hS : MeasurableSet S) (hT : MeasurableSet T)
48     (hp : 0<P.real S) (hq : 0<Q.real S) :
49     |(ProbabilityTheory.cond P S).real T-(ProbabilityTheory.cond Q S).real T|≤
50       min 1 (2*SequentialLowerCertificate.lawTV P Q/min (P.real S) (Q.real S)) := by
51   have hPnz : P S≠0 := by intro h; simp [Measure.real,h] at hp
52   have hQnz : Q S≠0 := by intro h; simp [Measure.real,h] at hq
53   have : IsProbabilityMeasure (ProbabilityTheory.cond P S) := ProbabilityTheory.cond_isProbabilityMeasure hPnz
54   have : IsProbabilityMeasure (ProbabilityTheory.cond Q S) := ProbabilityTheory.cond_isProbabilityMeasure hQnz
55   have h0P : 0≤(ProbabilityTheory.cond P S).real T := measureReal_nonneg
56   have h0Q : 0≤(ProbabilityTheory.cond Q S).real T := measureReal_nonneg
57   have h1P : (ProbabilityTheory.cond P S).real T≤1 := measureReal_le_one
58   have h1Q : (ProbabilityTheory.cond Q S).real T≤1 := measureReal_le_one
59   apply le_min
60   · exact abs_sub_le_iff.mpr ⟨by linarith,by linarith⟩
61   · rw [conditional_real P S T hS,conditional_real Q S T hS]
62     have hδ := SequentialLowerCertificate.lawTV_nonneg P Q
63     apply (ratio_error hp hq measureReal_nonneg
64       (measureReal_mono (Set.inter_subset_left : S∩T⊆S)) hδ
65       (event_error_le_tv P Q (S∩T) (hS.inter hT)) (event_error_le_tv P Q S hS)).trans
66     apply (div_le_div_iff₀ hp (lt_min hp hq)).mpr
67     exact mul_le_mul_of_nonneg_left (min_le_left _ _) (mul_nonneg (by norm_num) hδ)
68 
69 
70 section Records
71 open ContinuousRecords
72 variable {E A Y : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
73 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
74 variable [MeasurableSpace A] [MeasurableSpace Y] [Fintype A] [MeasurableSingletonClass A]
75 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y} [IsProbabilityMeasure μ]
76 
77 /-- The full-law budget controls every event of the actual conditional record
78 measures whenever the conditioning event has positive probability under both laws. -/
79 theorem record_conditional_event_error
80     (Ds Fs : ℕ → ContinuousInstrument.DensityInstrument (A := A) C μ)
81     (π : Policy (A := A) (Y := Y)) (u v : ContinuousInstrument.DensityInstrument.State C)
82     (ε : ℕ → ℝ) (hε0 : ∀ n,0≤ε n)
83     (hε : ∀ n a z,z∈C.base → (∫ y,C.value ((Ds n).op a y z-(Fs n).op a y z)∂μ)≤ε n)
84     (e0 : ℝ) (he0 : C.value (u.1-v.1)≤e0) (n : ℕ)
85     (S T : Set (History (A × Y) n)) (hS : MeasurableSet S) (hT : MeasurableSet T)
86     (hp : 0<(TimeRecords.recordLaw Ds π u.1 n).real S)
87     (hq : 0<(TimeRecords.recordLaw Fs π v.1 n).real S) :
88     |(ProbabilityTheory.cond (TimeRecords.recordLaw Ds π u.1 n) S).real T-
89       (ProbabilityTheory.cond (TimeRecords.recordLaw Fs π v.1 n) S).real T|≤
90       min 1 ((e0+∑ i∈Finset.range n,ε i)/
91         min ((TimeRecords.recordLaw Ds π u.1 n).real S) ((TimeRecords.recordLaw Fs π v.1 n).real S)) := by
92   have h := conditional_event_error (TimeRecords.recordLaw Ds π u.1 n)
93     (TimeRecords.recordLaw Fs π v.1 n) S T hS hT hp hq
94   apply h.trans
95   apply min_le_min le_rfl
96   apply div_le_div_of_nonneg_right _ (lt_min hp hq).le
97   have hTV := (ContinuousTV.record_lawTV_le Ds Fs π u v ε hε0 hε e0 he0 n).trans
98     (min_le_right _ _)
99   linarith
100 
101 end Records
102 end Komorebi.LSM.ConditionalEventTV

Back to source controls