CoveredActionBoundaries.lean

1 import KomorebiLSM.CoveredAdaptiveActions
2 import Mathlib.Probability.Distributions.Bernoulli
3 
4 /-! Exact probability-kernel boundaries for covered adaptive evidence. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.CoveredAdaptiveActions.Boundaries
7 open MeasureTheory ProbabilityTheory
8 
9 noncomputable def neverPolicy : Kernel Unit Bool :=
10   Kernel.deterministic (fun _ => false) measurable_const
11 
12 noncomputable def observations (tag : Bool) : Kernel (Unit × Bool) Bool :=
13   Kernel.deterministic (fun h => if h.2 then tag else false) (measurable_of_countable _)
14 
15 instance neverPolicy_markov : IsMarkovKernel neverPolicy := by
16   unfold neverPolicy
17   infer_instance
18 
19 instance observations_markov (tag : Bool) : IsMarkovKernel (observations tag) := by
20   unfold observations
21   infer_instance
22 
23 def oneTest : Unit × Bool → ℝ := fun _ => 1
24 
25 theorem target_propensity_zero : propensity neverPolicy true ()=0 := by
26   simp [propensity,neverPolicy,Kernel.deterministic_apply,Measure.real]
27 
28 theorem unobserved_evidence_zero (r : Bool × Bool) :
29     weightedTest neverPolicy oneTest true ((),r)=0 := by
30   simp [weightedTest,oneTest,target_propensity_zero]
31 
32 theorem unobserved_mean_one : targetMean (observations true) oneTest true ()=1 := by
33   change (∫ _ : Bool,(1:ℝ)∂observations true ((),true))=1
34   rw [integral_const,probReal_univ,one_smul]
35 
36 /-- Two genuine probability experiments have the same complete observed pair
37 law while disagreeing on the never-selected target action. -/
38 theorem unobserved_joint_law_agreement :
39     (neverPolicy ⊗ₖ observations false) ()=(neverPolicy ⊗ₖ observations true) () := by
40   ext s hs
41   simp only [observations,Kernel.compProd_deterministic_apply _ hs,
42     neverPolicy,Kernel.deterministic_apply]
43   simp only [Measure.dirac_apply]
44   rfl
45 
46 def responseTest : Unit × Bool → ℝ := fun p => if p.2 then 1 else 0
47 
48 theorem unobserved_kernel_means_disagree :
49     targetMean (observations false) responseTest true ()=0 ∧
50     targetMean (observations true) responseTest true ()=1 := by
51   simp [targetMean,observations,Kernel.deterministic_apply,responseTest]
52 
53 noncomputable def halfPolicy : Kernel Unit Bool :=
54   Kernel.const Unit (bernoulliMeasure true false ⟨1/2,by constructor <;> norm_num⟩)
55 
56 instance halfPolicy_markov : IsMarkovKernel halfPolicy := by
57   unfold halfPolicy
58   infer_instance
59 
60 theorem half_propensity : propensity halfPolicy true ()=1/2 := by
61   norm_num [propensity,halfPolicy,Kernel.const_apply,
62     bernoulliMeasure_real_apply _ (measurableSet_singleton true),unitInterval.toNNReal]
63   rfl
64 
65 theorem covered_weight_two : weightedTest halfPolicy oneTest true ((),(true,true))=2 := by
66   norm_num [weightedTest,oneTest,half_propensity]
67 
68 /-- The value two occurs with positive probability in the actual randomized
69 action/observation experiment; it is not an off-support test point. -/
70 theorem covered_pair_mass : ((halfPolicy ⊗ₖ observations true) ()).real {(true,true)}=1/2 := by
71   unfold Measure.real
72   rw [observations,Kernel.compProd_deterministic_apply _ (measurableSet_singleton _)]
73   have hs : {b : Bool | (b,if b then true else false)∈({(true,true)} : Set (Bool × Bool))}={true} := by
74     ext b
75     cases b <;> simp
76   rw [hs]
77   exact half_propensity
78 
79 end Komorebi.LSM.CoveredAdaptiveActions.Boundaries

Back to source controls