Skip to content

Commit bdec6f4

Browse files
RemyDegenneRemyDegenne
authored
Cleanup: Ionescu-Tulcea space (#104)
2 parents 5c8a661 + a42c1ca commit bdec6f4

7 files changed

Lines changed: 69 additions & 130 deletions

File tree

‎LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,11 +5,11 @@ Authors: Rémy Degenne, Paulo Rauber
55
-/
66
module
77

8+
public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel
89
public import LeanMachineLearning.Probability.Independence.CondIndepFun
910
public import LeanMachineLearning.Probability.Independence.IndepFun
1011
public import LeanMachineLearning.Probability.Independence.IndepInfinitePi
1112
public import LeanMachineLearning.Probability.Integrable
12-
public import LeanMachineLearning.MeasureTheory.Constructions.Polish.StandardBorel
1313
public import LeanMachineLearning.SequentialLearning.FiniteActions
1414
public import LeanMachineLearning.SequentialLearning.StationaryEnv
1515
public import Mathlib.Probability.Independence.Integration

‎LeanMachineLearning/Online/Bandit/SumRewards.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ module
88
public import LeanMachineLearning.Online.Bandit.ArrayProbSpace
99
public import LeanMachineLearning.Online.Bandit.Regret
1010
public import LeanMachineLearning.Probability.Moments.SubGaussian
11+
public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
1112

1213
/-! # Law of the sum of rewards
1314
-/

‎LeanMachineLearning/SequentialLearning/Algorithm.lean‎

Lines changed: 0 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -25,14 +25,6 @@ interacting with an environment.
2525
* `IsAlgEnvSeqUntil A R' alg env P N`: `A` and `R'` form an algorithm-environment sequence until
2626
time `N`.
2727
28-
## Main statements
29-
30-
* `isAlgEnvSeq_unique`: the law of the sequence of actions and observations generated by an
31-
algorithm-environment pair is unique: it does not depend on the probability space used.
32-
If `A₁`, `R₁` and `A₂`, `R₂` are two algorithm-environment sequences generated by the same
33-
algorithm-environment pair on probability spaces `(Ω, P)` and `(Ω', P')`, then
34-
`P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω))`.
35-
3628
## Notes
3729
3830
The `ANCHOR` comments are used to mark code that appears in the tutorials.
@@ -312,61 +304,4 @@ lemma IsAlgEnvSeq.filtrationAction_eq_comap
312304

313305
end IsAlgEnvSeq
314306

315-
/-- Measure on the sequence of actions and observations generated by the algorithm/environment. -/
316-
noncomputable
317-
def trajMeasure (alg : Algorithm α R) (env : Environment α R) :
318-
Measure (ℕ → α × R) :=
319-
Kernel.trajMeasure (alg.p0 ⊗ₘ env.ν0) (stepKernel alg env)
320-
deriving IsProbabilityMeasure
321-
322-
section ModelEquivalence
323-
324-
variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
325-
[StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
326-
{alg : Algorithm α R} {env : Environment α R}
327-
{P : Measure Ω} [IsProbabilityMeasure P] {P' : Measure Ω'} [IsProbabilityMeasure P']
328-
{A₁ : ℕ → Ω → α} {R₁ : ℕ → Ω → R} {A₂ : ℕ → Ω' → α} {R₂ : ℕ → Ω' → R} {N : ℕ}
329-
330-
theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) :
331-
P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = trajMeasure alg env := by
332-
rw [trajMeasure]
333-
have h := Kernel.eq_trajMeasure (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) (P := P)
334-
(μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) (fun n ↦ ?_) ?_ (fun n ↦ ?_)
335-
· exact h
336-
· have hA := h.measurable_A n
337-
have hR := h.measurable_R n
338-
fun_prop
339-
· simp only
340-
exact h.hasLaw_step_zero
341-
· exact h.hasCondDistrib_step n
342-
343-
lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
344-
(h : IsAlgEnvSeqUntil A₁ R₁ alg env P N) :
345-
P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
346-
(trajMeasure alg env).map (Preorder.frestrictLe N) := by
347-
rw [trajMeasure]
348-
have h := Kernel.eq_trajMeasure_map_frestrictLe (Y := fun n ω ↦ (A₁ n ω, R₁ n ω))
349-
(P := P) (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) ?_ (fun n hn ↦ ?_) (N := N)
350-
· exact h
351-
· exact h.hasLaw_step_zero
352-
· exact h.hasCondDistrib_step n hn
353-
354-
/-- The law of the sequence of actions and observations generated by an algorithm-environment pair
355-
is unique: it does not depend on the probability space used. -/
356-
-- ANCHOR: isAlgEnvSeq_unique
357-
theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
358-
(h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
359-
P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by
360-
-- ANCHOR_END: isAlgEnvSeq_unique
361-
rw [eq_trajMeasure_of_isAlgEnvSeq h1, eq_trajMeasure_of_isAlgEnvSeq h2]
362-
363-
theorem isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
364-
(h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) :
365-
P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
366-
P'.map (fun ω (n : Iic N) ↦ (A₂ n ω, R₂ n ω)) := by
367-
rw [eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h1,
368-
eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h2]
369-
370-
end ModelEquivalence
371-
372307
end Learning

‎LeanMachineLearning/SequentialLearning/Deterministic.lean‎

Lines changed: 1 addition & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Rémy Degenne
66
module
77

88
public import LeanMachineLearning.Probability.Kernel.Basic
9-
public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
9+
public import LeanMachineLearning.SequentialLearning.Algorithm
1010

1111
/-!
1212
# Deterministic algorithms and environments
@@ -308,31 +308,4 @@ lemma action_detAlgorithm_ae_eq
308308

309309
end IsAlgEnvSeqUntil
310310

311-
namespace IT
312-
313-
local notation "𝔓" => trajMeasure (detAlgorithm nextA h_next action0) env
314-
315-
lemma HasLaw_action_zero_detAlgorithm : HasLaw (IT.action 0) (Measure.dirac action0) 𝔓 where
316-
map_eq := (IT.hasLaw_action_zero _ _).map_eq
317-
318-
lemma action_zero_detAlgorithm [MeasurableSingletonClass α] :
319-
IT.action 0 =ᵐ[𝔓] fun _ ↦ action0 := by
320-
have h_eq : ∀ᵐ x ∂((𝔓).map (IT.action 0)), x = action0 := by
321-
rw [(IT.hasLaw_action_zero _ _).map_eq]
322-
simp [detAlgorithm]
323-
exact ae_of_ae_map (by fun_prop) h_eq
324-
325-
lemma action_detAlgorithm_ae_eq [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R]
326-
[Nonempty R] (n : ℕ) : IT.action (n + 1) =ᵐ[𝔓] fun h ↦ nextA n (IT.hist n h) :=
327-
ae_eq_of_condDistrib_eq_deterministic (by fun_prop) (by fun_prop) (by fun_prop)
328-
(IT.condDistrib_action (detAlgorithm nextA h_next action0) env n)
329-
330-
lemma action_detAlgorithm_ae_all_eq
331-
[StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] :
332-
∀ᵐ h ∂𝔓, IT.action 0 h = action0 ∧ ∀ n, IT.action (n + 1) h = nextA n (IT.hist n h) := by
333-
rw [eventually_and, ae_all_iff]
334-
exact ⟨action_zero_detAlgorithm, action_detAlgorithm_ae_eq⟩
335-
336-
end IT
337-
338311
end Learning

‎LeanMachineLearning/SequentialLearning/IonescuTulceaSpace.lean‎

Lines changed: 64 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,13 @@ a sequence of random variables representing the actions and feedback generated b
1515
of the algorithm and the environment.
1616
The main ingredient of the construction is the Ionescu-Tulcea theorem.
1717
18-
TODO: actually, the probability measure is already defined in the Algorithm file. Reorganize?
18+
## Main statements
19+
20+
* `isAlgEnvSeq_unique`: the law of the sequence of actions and observations generated by an
21+
algorithm-environment pair is unique: it does not depend on the probability space used.
22+
If `A₁`, `R₁` and `A₂`, `R₂` are two algorithm-environment sequences generated by the same
23+
algorithm-environment pair on probability spaces `(Ω, P)` and `(Ω', P')`, then
24+
`P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω))`.
1925
2026
-/
2127

@@ -29,6 +35,63 @@ namespace Learning
2935

3036
variable {α R Ω : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω}
3137

38+
/-- Measure on the sequence of actions and observations generated by the algorithm/environment. -/
39+
noncomputable
40+
def trajMeasure (alg : Algorithm α R) (env : Environment α R) :
41+
Measure (ℕ → α × R) :=
42+
Kernel.trajMeasure (alg.p0 ⊗ₘ env.ν0) (stepKernel alg env)
43+
deriving IsProbabilityMeasure
44+
45+
section ModelEquivalence
46+
47+
variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
48+
[StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
49+
{alg : Algorithm α R} {env : Environment α R}
50+
{P : Measure Ω} [IsProbabilityMeasure P] {P' : Measure Ω'} [IsProbabilityMeasure P']
51+
{A₁ : ℕ → Ω → α} {R₁ : ℕ → Ω → R} {A₂ : ℕ → Ω' → α} {R₂ : ℕ → Ω' → R} {N : ℕ}
52+
53+
theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) :
54+
P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = trajMeasure alg env := by
55+
rw [trajMeasure]
56+
have h := Kernel.eq_trajMeasure (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) (P := P)
57+
(μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) (fun n ↦ ?_) ?_ (fun n ↦ ?_)
58+
· exact h
59+
· have hA := h.measurable_A n
60+
have hR := h.measurable_R n
61+
fun_prop
62+
· simp only
63+
exact h.hasLaw_step_zero
64+
· exact h.hasCondDistrib_step n
65+
66+
lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
67+
(h : IsAlgEnvSeqUntil A₁ R₁ alg env P N) :
68+
P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
69+
(trajMeasure alg env).map (Preorder.frestrictLe N) := by
70+
rw [trajMeasure]
71+
have h := Kernel.eq_trajMeasure_map_frestrictLe (Y := fun n ω ↦ (A₁ n ω, R₁ n ω))
72+
(P := P) (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) ?_ (fun n hn ↦ ?_) (N := N)
73+
· exact h
74+
· exact h.hasLaw_step_zero
75+
· exact h.hasCondDistrib_step n hn
76+
77+
/-- The law of the sequence of actions and observations generated by an algorithm-environment pair
78+
is unique: it does not depend on the probability space used. -/
79+
-- ANCHOR: isAlgEnvSeq_unique
80+
theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
81+
(h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
82+
P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by
83+
-- ANCHOR_END: isAlgEnvSeq_unique
84+
rw [eq_trajMeasure_of_isAlgEnvSeq h1, eq_trajMeasure_of_isAlgEnvSeq h2]
85+
86+
theorem isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N)
87+
(h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) :
88+
P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) =
89+
P'.map (fun ω (n : Iic N) ↦ (A₂ n ω, R₂ n ω)) := by
90+
rw [eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h1,
91+
eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h2]
92+
93+
end ModelEquivalence
94+
3295
namespace IT
3396

3497
/-- Action and reward at step `n`. -/

‎LeanMachineLearning/SequentialLearning/StationaryEnv.lean‎

Lines changed: 1 addition & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Rémy Degenne, Paulo Rauber
66
module
77

88
public import LeanMachineLearning.Probability.Kernel.Composition.MapComap
9-
public import LeanMachineLearning.SequentialLearning.IonescuTulceaSpace
9+
public import LeanMachineLearning.SequentialLearning.Algorithm
1010

1111
/-!
1212
# Oblivious and stationary environments
@@ -230,37 +230,4 @@ lemma condIndepFun_reward_hist_action_action' [StandardBorelSpace Ω]
230230

231231
end IsAlgEnvSeq
232232

233-
namespace IT
234-
235-
local notation "𝔓" => trajMeasure alg (stationaryEnv ν)
236-
237-
/-- The conditional distribution of the reward at time `n` given the action at time `n` is `ν`. -/
238-
lemma condDistrib_reward_stationaryEnv (n : ℕ) :
239-
condDistrib (IT.reward n) (IT.action n) 𝔓 =ᵐ[(𝔓).map (IT.action n)] ν :=
240-
IsAlgEnvSeq.condDistrib_reward_stationaryEnv
241-
(IT.isAlgEnvSeq_trajMeasure alg (stationaryEnv ν)) n
242-
243-
/-- The reward at time `n + 1` is conditionally independent of the history up to time `n`
244-
given the action at time `n + 1`. -/
245-
lemma condIndepFun_reward_hist_action (n : ℕ) :
246-
IT.reward (n + 1) ⟂ᵢ[IT.action (n + 1), IT.measurable_action _ ; 𝔓] IT.hist n :=
247-
IsAlgEnvSeq.condIndepFun_reward_hist_action
248-
(IT.isAlgEnvSeq_trajMeasure alg (stationaryEnv ν)) n
249-
250-
lemma condIndepFun_reward_hist_action_action
251-
{alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) :
252-
reward (n + 1) ⟂ᵢ[action (n + 1), measurable_action (n + 1); trajMeasure alg (stationaryEnv ν)]
253-
(fun ω ↦ (hist n ω, action (n + 1) ω)) :=
254-
IsAlgEnvSeq.condIndepFun_reward_hist_action_action
255-
(IT.isAlgEnvSeq_trajMeasure alg (stationaryEnv ν)) n
256-
257-
lemma condIndepFun_reward_hist_action_action'
258-
{alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ) (hn : n ≠ 0) :
259-
reward n ⟂ᵢ[action n, measurable_action n; trajMeasure alg (stationaryEnv ν)]
260-
(fun ω ↦ (hist (n - 1) ω, action n ω)) :=
261-
IsAlgEnvSeq.condIndepFun_reward_hist_action_action'
262-
(IT.isAlgEnvSeq_trajMeasure alg (stationaryEnv ν)) n hn
263-
264-
end IT
265-
266233
end Learning

‎tutorial/Manual/Pages/DefiningAlgorithm.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ All spaces of interest in machine learning are standard Borel, so this is not a
115115
Given any algorithm and environment, there always exists a sequence of actions and feedback that satisfies `IsAlgEnvSeq` by the Ionescu-Tulcea theorem.
116116
However other constructions of such sequences are possible, and it is easier to work with generic sequences satisfying `IsAlgEnvSeq` than with a specific construction.
117117
Which sequence we choose does not matter for the results we prove, since all such sequences are equal in distribution, as stated by the following theorem.
118-
```anchor isAlgEnvSeq_unique (module := LeanMachineLearning.SequentialLearning.Algorithm)
118+
```anchor isAlgEnvSeq_unique (module := LeanMachineLearning.SequentialLearning.IonescuTulceaSpace)
119119
theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P)
120120
(h2 : IsAlgEnvSeq A₂ R₂ alg env P') :
121121
P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by

0 commit comments

Comments
 (0)