Skip to content

A few simple lemmas from the AlphaRAR project #220

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RemyDegenne merged 2 commits into from
Aug 23, 2026
Merged

A few simple lemmas from the AlphaRAR project #220

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4bade86
a few simple lemmas from AlphaRAR
RemyDegenne Aug 23, 2026
d668f0c
fix
RemyDegenne Aug 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
74 changes: 56 additions & 18 deletions LeanMachineLearning/SequentialLearning/Algorithm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,9 +143,6 @@ lemma history_succ (n : ℕ) :
symm
exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 × 𝓨) n).symm_apply_apply (history A Y (n + 1) ω)

section IsAlgEnvSeq


/-- An algorithm-environment sequence: a sequence of actions and feedbacks generated
by an algorithm interacting with an environment. -/
structure IsAlgEnvSeq
Expand Down Expand Up @@ -253,10 +250,12 @@ lemma IsAlgEnvSeq.hasLaw_history_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (
have hY := h.measurable_feedback
exact (Measure.map_map (by fun_prop) (by fun_prop)).symm

end IsAlgEnvSeq
section Filtration

namespace IsAlgEnvSeq

/-- Filtration generated by the history up to time `n`. -/
def IsAlgEnvSeq.filtration (h : IsAlgEnvSeq A Y alg env P) :
def filtration (h : IsAlgEnvSeq A Y alg env P) :
Filtration ℕ mΩ where
seq i := MeasurableSpace.comap (history A Y i) inferInstance
mono' i j hij := by
Expand All @@ -269,11 +268,11 @@ def IsAlgEnvSeq.filtration (h : IsAlgEnvSeq A Y alg env P) :
rw [← measurable_iff_comap_le]
exact Learning.measurable_history h.measurable_action h.measurable_feedback i

lemma IsAlgEnvSeq.adapted_history (h : IsAlgEnvSeq A Y alg env P) :
lemma adapted_history (h : IsAlgEnvSeq A Y alg env P) :
Adapted h.filtration (history A Y) :=
fun _ ↦ measurable_iff_comap_le.mpr le_rfl

lemma IsAlgEnvSeq.adapted_step (h : IsAlgEnvSeq A Y alg env P) :
lemma adapted_step (h : IsAlgEnvSeq A Y alg env P) :
Adapted h.filtration (step A Y) := by
intro n
have : step A Y n = (fun h ↦ (h ⟨n, by simp⟩)) ∘ (history A Y n) := by
Expand All @@ -282,7 +281,7 @@ lemma IsAlgEnvSeq.adapted_step (h : IsAlgEnvSeq A Y alg env P) :
rw [this]
exact measurable_comp_comap _ (by fun_prop)

lemma IsAlgEnvSeq.adapted_action (h : IsAlgEnvSeq A Y alg env P) :
lemma adapted_action (h : IsAlgEnvSeq A Y alg env P) :
Adapted h.filtration A := by
intro n
have : A n = (fun h ↦ (h ⟨n, by simp⟩).1) ∘ (history A Y n) := by
Expand All @@ -291,7 +290,7 @@ lemma IsAlgEnvSeq.adapted_action (h : IsAlgEnvSeq A Y alg env P) :
rw [this]
exact measurable_comp_comap _ (by fun_prop)

lemma IsAlgEnvSeq.adapted_feedback (h : IsAlgEnvSeq A Y alg env P) :
lemma adapted_feedback (h : IsAlgEnvSeq A Y alg env P) :
Adapted h.filtration Y := by
intro n
have : Y n = (fun h ↦ (h ⟨n, by simp⟩).2) ∘ (history A Y n) := by
Expand All @@ -301,10 +300,10 @@ lemma IsAlgEnvSeq.adapted_feedback (h : IsAlgEnvSeq A Y alg env P) :
exact measurable_comp_comap _ (by fun_prop)

/-- Filtration generated by the history at time `n-1` together with the action at time `n`. -/
def IsAlgEnvSeq.filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
def filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
Filtration ℕ mΩ where
seq n := if n = 0 then MeasurableSpace.comap (A 0) inferInstance
else IsAlgEnvSeq.filtration h (n - 1) ⊔ MeasurableSpace.comap (A n) inferInstance
else h.filtration (n - 1) ⊔ MeasurableSpace.comap (A n) inferInstance
mono' n m hnm := by
simp only
by_cases hn : n = 0
Expand All @@ -313,23 +312,23 @@ def IsAlgEnvSeq.filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
· simp only [hn, ↓reduceIte, hm]
refine le_sup_of_le_left ?_
rw [← measurable_iff_comap_le]
suffices Measurable[IsAlgEnvSeq.filtration h 0] (A 0) from
this.mono ((IsAlgEnvSeq.filtration h).mono zero_le) le_rfl
suffices Measurable[h.filtration 0] (A 0) from
this.mono ((h.filtration).mono zero_le) le_rfl
exact adapted_action h 0
have hm : m ≠ 0 := by grind
simp only [hn, hm, ↓reduceIte]
have hnm' : n - 1 ≤ m - 1 := by grind
simp only [sup_le_iff]
constructor
· refine le_sup_of_le_left ?_
exact (IsAlgEnvSeq.filtration h).mono hnm'
exact (h.filtration).mono hnm'
· rcases eq_or_lt_of_le hnm with rfl | hlt
· exact le_sup_of_le_right le_rfl
refine le_sup_of_le_left ?_
rw [← measurable_iff_comap_le]
have h_le : n ≤ m - 1 := by grind
suffices Measurable[h.filtration n] (A n) from
this.mono ((IsAlgEnvSeq.filtration h).mono h_le) le_rfl
this.mono ((h.filtration).mono h_le) le_rfl
exact adapted_action h n
le' n := by
by_cases hn : n = 0
Expand All @@ -342,17 +341,56 @@ def IsAlgEnvSeq.filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
· rw [← measurable_iff_comap_le]
exact h.measurable_action n

lemma IsAlgEnvSeq.filtrationAction_zero_eq_comap {h : IsAlgEnvSeq A Y alg env P} :
lemma filtrationAction_zero_eq_comap (h : IsAlgEnvSeq A Y alg env P) :
h.filtrationAction 0 = MeasurableSpace.comap (A 0) inferInstance := by
simp [filtrationAction]

lemma IsAlgEnvSeq.filtrationAction_eq_comap
{h : IsAlgEnvSeq A Y alg env P} (n : ℕ) (hn : n ≠ 0) :
lemma filtrationAction_eq_comap (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) (hn : n ≠ 0) :
h.filtrationAction n =
MeasurableSpace.comap (fun ω ↦ (history A Y (n - 1) ω, A n ω)) inferInstance := by
simp only [filtrationAction, filtration, ← MeasurableSpace.comap_prodMk, hn, ↓reduceIte]
rfl

@[fun_prop]
lemma measurable_history_filtrationAction_add_one (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
Measurable[h.filtrationAction (n + 1)] (history A Y n) := by
rw [h.filtrationAction_eq_comap (n + 1) (Nat.succ_ne_zero n)]
exact measurable_fst.comp (measurable_iff_comap_le.mpr le_rfl)

lemma filtration_le_filtrationAction_succ (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
h.filtration n ≤ h.filtrationAction (n + 1) :=
measurable_iff_comap_le.mp (h.measurable_history_filtrationAction_add_one n)

lemma filtrationAction_le_filtration (h : IsAlgEnvSeq A Y alg env P) (n : ℕ) :
h.filtrationAction n ≤ h.filtration n := by
cases n with
| zero =>
rw [h.filtrationAction_zero_eq_comap]
exact measurable_iff_comap_le.mp (h.adapted_action 0)
| succ m =>
rw [h.filtrationAction_eq_comap (m + 1) (Nat.succ_ne_zero m), ← measurable_iff_comap_le]
exact ((h.adapted_history m).mono (h.filtration.mono m.le_succ) le_rfl).prodMk
(h.adapted_action (m + 1))

lemma adapted_action_filtrationAction (h : IsAlgEnvSeq A Y alg env P) :
Adapted h.filtrationAction A := fun n ↦ by
cases n with
| zero => rw [h.filtrationAction_zero_eq_comap]; exact measurable_iff_comap_le.mpr le_rfl
| succ m =>
rw [h.filtrationAction_eq_comap (m + 1) (Nat.succ_ne_zero m)]
exact measurable_snd.comp (measurable_iff_comap_le.mpr le_rfl)

lemma measurable_feedback_filtrationAction_of_lt (h : IsAlgEnvSeq A Y alg env P)
{m n : ℕ} (hmn : m < n) :
Measurable[h.filtrationAction n] (Y m) := by
obtain ⟨j, rfl⟩ : ∃ j, n = j + 1 := ⟨n - 1, by lia⟩
exact (h.adapted_feedback.measurable_le (by lia)).mono
(filtration_le_filtrationAction_succ h j) le_rfl

end IsAlgEnvSeq

end Filtration

end IsAlgEnvSeq

end Learning
9 changes: 8 additions & 1 deletion LeanMachineLearning/SequentialLearning/FiniteActions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -651,7 +651,7 @@ lemma isStoppingTime_stepsUntil_filtrationAction [MeasurableSingletonClass 𝓐]
· subst hn
simp only [WithTop.coe_zero]
exact measurableSet_stepsUntil_eq_zero a m
· rw [IsAlgEnvSeq.filtrationAction_eq_comap _ hn]
· rw [h.filtrationAction_eq_comap _ hn]
exact measurableSet_stepsUntil_eq h a m n

end Measurability
Expand Down Expand Up @@ -767,6 +767,13 @@ lemma sum_comp_pullCount [Fintype 𝓐] [AddCommMonoid R] (f : ℕ → R) (t :
· simp [sum_range_succ]
· simp

lemma sum_pullCount' [Fintype 𝓐] (n : ℕ) (h : Iic n → 𝓐 × ℝ) : ∑ a, pullCount' n h a = n + 1 := by
simp_rw [pullCount'_eq_sum]
rw [Finset.sum_comm]
have hcol (s : Iic n) : ∑ a, (if (h s).1 = a then (1 : ℕ) else 0) = 1 := by
simp [Finset.sum_ite_eq univ (h s).1 (fun _ ↦ (1 : ℕ))]
simp [hcol]

section SumRewards

/-- Sum of rewards obtained when pulling action `a` up to time `t` (exclusive). -/
Expand Down