From a1f5d81cbcf10cca6ee5cbddb957947996fa8735 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 26 Jan 2026 13:43:02 +0100 Subject: [PATCH 1/3] martingale lemmas --- LeanBandits/Bandit/SumRewards.lean | 32 ++++++++ LeanBandits/ForMathlib/SubGaussian.lean | 76 +++++++++++++++++++ LeanBandits/SequentialLearning/Algorithm.lean | 21 +++++ .../SequentialLearning/FiniteActions.lean | 55 ++++++++++++++ 4 files changed, 184 insertions(+) diff --git a/LeanBandits/Bandit/SumRewards.lean b/LeanBandits/Bandit/SumRewards.lean index 81ec80a3..bd23d6e4 100644 --- a/LeanBandits/Bandit/SumRewards.lean +++ b/LeanBandits/Bandit/SumRewards.lean @@ -488,6 +488,38 @@ lemma probReal_sumRewards_le_sumRewards_le [Fintype α] (h : IsAlgEnvSeq A R alg section Subgaussian +open Real + +lemma superMartingale_exp_sumRewards_sub (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {c : ℝ≥0} + (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) c (ν a)) (t : ℝ) : + Supermartingale (fun n ω ↦ + exp (t * (sumRewards A R a (n + 1) ω - pullCount A a (n + 1) ω * (ν a)[id]))) + (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R) P := by + refine supermartingale_nat (fun n ↦ ?_) (fun n ↦ ?_) (fun n ↦ ?_) + · change StronglyMeasurable[IsAlgEnvSeq.filtration h.measurable_A h.measurable_R _] (exp ∘ _) + refine StronglyMeasurable.comp_measurable (by fun_prop) ?_ + refine Measurable.const_mul ?_ _ + refine Measurable.sub ?_ ?_ + · exact (h.adapted_sumRewards_add_one a n).measurable + · have := adapted_pullCount_add_one h.measurable_A h.measurable_R a n + fun_prop + · sorry + · simp_rw [sumRewards_sub_pullCount_mul_eq_sum (n := n + 1) (fun a ↦ (ν a)[id]), + sum_range_succ (n := n + 1), + ← sumRewards_sub_pullCount_mul_eq_sum (n := n) (fun a ↦ (ν a)[id]), mul_add, exp_add] + calc P[fun ω ↦ exp (t * (sumRewards A R a (n + 1) ω - pullCount A a (n + 1) ω * (ν a)[id])) * + exp (t * if A (n + 1) ω = a then R (n + 1) ω - (ν a)[id] else 0)| + IsAlgEnvSeq.filtration h.measurable_A h.measurable_R n] + _ =ᵐ[P] (fun ω ↦ exp (t * (sumRewards A R a (n + 1) ω - pullCount A a (n + 1) ω * (ν a)[id]))) * + P[fun ω ↦ exp (t * if A (n + 1) ω = a then R (n + 1) ω - (ν a)[id] else 0)| + IsAlgEnvSeq.filtration h.measurable_A h.measurable_R n] := by + apply condExp_mul_of_aestronglyMeasurable_left + · sorry + · sorry + · sorry + _ ≤ᵐ[P] fun ω ↦ exp (t * (sumRewards A R a (n + 1) ω - pullCount A a (n + 1) ω * (ν a)[id])) := + sorry + omit [DecidableEq α] [StandardBorelSpace α] in lemma probReal_sum_le_sum_streamMeasure [Fintype α] {c : ℝ≥0} (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) c (ν a)) (a : α) (m : ℕ) : diff --git a/LeanBandits/ForMathlib/SubGaussian.lean b/LeanBandits/ForMathlib/SubGaussian.lean index 658dd237..df72520c 100644 --- a/LeanBandits/ForMathlib/SubGaussian.lean +++ b/LeanBandits/ForMathlib/SubGaussian.lean @@ -10,6 +10,82 @@ open scoped ENNReal NNReal namespace ProbabilityTheory +namespace HasCondSubgaussianMGF + +variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] + {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → ℝ} {c : ℝ≥0} + +lemma ae_trim_condExp_exp_sub_le_one (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) : + ∀ᵐ ω' ∂(μ.trim hm), (μ[fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)|m]) ω' ≤ 1 := by + have h_le : ∀ᵐ ω' ∂(μ.trim hm), μ[fun ω ↦ exp (t * X ω)|m] ω' ≤ exp (c * t ^ 2 / 2) := + h.ae_trim_condExp_le t + have h_eq : μ[fun ω ↦ exp (t * X ω) / exp (c * t ^ 2 / 2)|m] =ᵐ[μ.trim hm] + fun ω ↦ μ[fun ω ↦ exp (t * X ω)|m] ω / exp (c * t ^ 2 / 2) := by + refine ae_eq_trim_of_measurable _ ?_ ?_ ?_ + · exact stronglyMeasurable_condExp.measurable + · refine Measurable.div_const ?_ _ + exact stronglyMeasurable_condExp.measurable + simp_rw [div_eq_inv_mul] + refine condExp_mul_of_stronglyMeasurable_left ?_ ?_ ?_ + · fun_prop + · refine Integrable.const_mul ?_ _ + exact h.integrable_exp_mul _ + · exact h.integrable_exp_mul _ + filter_upwards [h_le, h_eq] with ω hω_le hω_eq + simp_rw [exp_sub, hω_eq] + rwa [div_le_one (by positivity)] + +lemma ae_condExp_exp_sub_le_one (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) : + ∀ᵐ ω' ∂μ, (μ[fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)|m]) ω' ≤ 1 := + ae_of_ae_trim hm (h.ae_trim_condExp_exp_sub_le_one t) + +lemma memLp_exp_mul_sub (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) (p : ℝ≥0) : + MemLp (fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)) p μ := by + have h_lp := h.memLp_exp_mul t p + simp_rw [sub_eq_add_neg, exp_add] + exact h_lp.mul_const _ + +lemma integrable_exp_mul_sub (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) : + Integrable (fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)) μ := by + have h_int := h.integrable_exp_mul t + simp_rw [exp_sub] + exact h_int.div_const _ + +lemma aux {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥0} {ℱ : Filtration ℕ mΩ} + {p : ℕ → Ω → Prop} [∀ n, DecidablePred (p n)] + (h0 : HasSubgaussianMGF (X 0) (c 0) μ) + (h_subG : ∀ n, HasCondSubgaussianMGF (ℱ n) (ℱ.le n) (X (n + 1)) (c (n + 1)) μ) + (hp : IsPredictable ℱ p) (t : ℝ) (n : ℕ) : + ∀ q, 1 < q → MemLp (fun ω ↦ exp (∑ i ∈ Finset.range n, + t * if p i ω then (X i ω - c i * t ^ 2 / 2) else 0)) q μ := by + induction n with + | zero => + simp only [Finset.range_zero, mul_ite, mul_zero, Finset.sum_empty, exp_zero] + exact fun _ _ ↦ memLp_const _ + | succ n hn => + intro q hq + simp_rw [Finset.sum_range_succ, exp_add] + obtain ⟨p1, p2, hp1, hp2, h_triple⟩ : + ∃ p1 p2, 1 < p1 ∧ 1 < p2 ∧ ENNReal.HolderTriple p1 p2 q := by + refine ⟨2 * q, 2 * q, ?_, ?_, ?_⟩ + · sorry + · sorry + · constructor + sorry + refine MemLp.mul (q := p2) ?_ (hn p1 hp1) + sorry + +lemma todo_supermartingale_optional {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥0} {ℱ : Filtration ℕ mΩ} + {p : ℕ → Ω → Prop} [∀ n, DecidablePred (p n)] + (h0 : HasSubgaussianMGF (X 0) (c 0) μ) + (h_subG : ∀ n, HasCondSubgaussianMGF (ℱ n) (ℱ.le n) (X (n + 1)) (c (n + 1)) μ) + (hp : IsPredictable ℱ p) (t : ℝ) : + Supermartingale (fun n ω ↦ exp (∑ i ∈ Finset.range n, + t * if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) ℱ μ := + sorry + +end HasCondSubgaussianMGF + namespace HasSubgaussianMGF variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X Y : Ω → ℝ} {c cX cY : ℝ≥0} diff --git a/LeanBandits/SequentialLearning/Algorithm.lean b/LeanBandits/SequentialLearning/Algorithm.lean index c3638035..2abf3222 100644 --- a/LeanBandits/SequentialLearning/Algorithm.lean +++ b/LeanBandits/SequentialLearning/Algorithm.lean @@ -192,6 +192,27 @@ lemma IsAlgEnvSeq.measurable_action_filtration rw [this] exact measurable_comp_comap _ (by fun_prop) +lemma IsAlgEnvSeq.adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] + [SecondCountableTopology α] [OpensMeasurableSpace α] + (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) : + Adapted (filtration hA hR') A := + fun n ↦ (IsAlgEnvSeq.measurable_action_filtration hA hR' n).stronglyMeasurable + +lemma IsAlgEnvSeq.measurable_reward_filtration + (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (n : ℕ) : + Measurable[IsAlgEnvSeq.filtration hA hR' n] (R' n) := by + have : R' n = (fun h ↦ (h ⟨n, by simp⟩).2) ∘ (hist A R' n) := by + ext ω : 1 + simp [IsAlgEnvSeq.hist] + rw [this] + exact measurable_comp_comap _ (by fun_prop) + +lemma IsAlgEnvSeq.adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R] + [SecondCountableTopology R] [OpensMeasurableSpace R] + (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) : + Adapted (filtration hA hR') R' := + fun n ↦ (IsAlgEnvSeq.measurable_reward_filtration hA hR' n).stronglyMeasurable + /-- Filtration generated by the history at time `n-1` together with the action at time `n`. -/ def IsAlgEnvSeq.filtrationAction (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) : diff --git a/LeanBandits/SequentialLearning/FiniteActions.lean b/LeanBandits/SequentialLearning/FiniteActions.lean index 527db1f6..12b550a0 100644 --- a/LeanBandits/SequentialLearning/FiniteActions.lean +++ b/LeanBandits/SequentialLearning/FiniteActions.lean @@ -767,6 +767,14 @@ noncomputable def empMean' (n : ℕ) (h : Iic n → α × ℝ) (a : α) := (sumRewards' n h a) / (pullCount' n h a) +@[simp] +lemma sumRewards_zero {R' : ℕ → Ω → ℝ} : sumRewards A R' a 0 = 0 := by ext; simp [sumRewards] + +lemma sumRewards_add_one {R' : ℕ → Ω → ℝ} : + sumRewards A R' a (t + 1) ω = sumRewards A R' a t ω + if A t ω = a then R' t ω else 0 := by + unfold sumRewards + rw [sum_range_succ] + lemma sumRewards_eq_pullCount_mul_empMean {R' : ℕ → Ω → ℝ} {ω : Ω} (h_pull : pullCount A a t ω ≠ 0) : sumRewards A R' a t ω = pullCount A a t ω * empMean A R' a t ω := by unfold empMean; field_simp @@ -811,6 +819,25 @@ lemma empMean_eq_empMean' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} (hn : n unfold empMean empMean' rw [sumRewards_eq_sumRewards' hn, pullCount_eq_pullCount' hn] +lemma sumRewards_sub_pullCount_mul_eq_sum {R' : ℕ → Ω → ℝ} (c : α → ℝ) : + sumRewards A R' a (n + 1) ω - pullCount A a (n + 1) ω * c a = + ∑ i ∈ range (n + 1), (if A i ω = a then R' i ω - c a else 0) := by + induction n with + | zero => + simp_rw [sumRewards_add_one, pullCount_add_one] + simp only [sumRewards_zero, Pi.zero_apply, zero_add, pullCount_zero, Nat.cast_ite, Nat.cast_one, + CharP.cast_eq_zero, ite_mul, one_mul, zero_mul, range_one, sum_singleton] + grind + | succ n hn => + simp_rw [sumRewards_add_one (t := n + 1), pullCount_add_one (t := n + 1)] + split_ifs with ha + · conv_rhs => rw [sum_range_succ] + simp only [Nat.cast_add, Nat.cast_one, ha, ↓reduceIte, add_mul, one_mul] + grind + · simp only [add_zero, hn] + conv_rhs => rw [sum_range_succ] + simp [ha] + @[fun_prop] lemma measurable_sumRewards [MeasurableSingletonClass α] {R' : ℕ → Ω → ℝ} (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (t : ℕ) : @@ -843,6 +870,34 @@ lemma measurable_empMean' [MeasurableSingletonClass α] (n : ℕ) (a : α) : unfold empMean' fun_prop +lemma IsAlgEnvSeq.isPredictable_sumRewards [StandardBorelSpace α] [Nonempty α] {R' : ℕ → Ω → ℝ} + {alg : Algorithm α ℝ} {env : Environment α ℝ} + (h : IsAlgEnvSeq A R' alg env P) (a : α) : + IsPredictable (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R) (sumRewards A R' a) := by + rw [isPredictable_iff_measurable_add_one] + constructor + · simp only [sumRewards_zero] + fun_prop + refine fun n ↦ measurable_fun_sum _ fun i hi ↦ Measurable.ite ?_ ?_ (by fun_prop) + · refine (measurableSet_singleton a).preimage ?_ + have h_meas_i := IsAlgEnvSeq.measurable_action_filtration h.measurable_A h.measurable_R i + simp only [mem_range] at hi + exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_A h.measurable_R).mono (by lia)) + le_rfl + · have h_meas_i := IsAlgEnvSeq.measurable_reward_filtration h.measurable_A h.measurable_R i + simp only [mem_range] at hi + exact h_meas_i.mono ((IsAlgEnvSeq.filtration h.measurable_A h.measurable_R).mono (by lia)) + le_rfl + +lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace α] [Nonempty α] {R' : ℕ → Ω → ℝ} + {alg : Algorithm α ℝ} {env : Environment α ℝ} + (h : IsAlgEnvSeq A R' alg env P) (a : α) : + Adapted (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R) + (fun n ↦ sumRewards A R' a (n + 1)) := by + have h_predictable := h.isPredictable_sumRewards a + rw [isPredictable_iff_measurable_add_one] at h_predictable + exact fun n ↦ Measurable.stronglyMeasurable (h_predictable.2 n) + end SumRewards end Learning From 66ca67b64e7704e4cabd9bce70a1783ef3facdcd Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 26 Jan 2026 13:44:40 +0100 Subject: [PATCH 2/3] fix --- LeanBandits/ForMathlib/SubGaussian.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBandits/ForMathlib/SubGaussian.lean b/LeanBandits/ForMathlib/SubGaussian.lean index df72520c..5c142119 100644 --- a/LeanBandits/ForMathlib/SubGaussian.lean +++ b/LeanBandits/ForMathlib/SubGaussian.lean @@ -81,7 +81,7 @@ lemma todo_supermartingale_optional {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥ (h_subG : ∀ n, HasCondSubgaussianMGF (ℱ n) (ℱ.le n) (X (n + 1)) (c (n + 1)) μ) (hp : IsPredictable ℱ p) (t : ℝ) : Supermartingale (fun n ω ↦ exp (∑ i ∈ Finset.range n, - t * if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) ℱ μ := + if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) ℱ μ := sorry end HasCondSubgaussianMGF From 1895aec727ba98e43bd55c545681b3442938a951 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 19 Mar 2026 20:27:17 +0100 Subject: [PATCH 3/3] wip --- LeanBandits/Bandit/SumRewards.lean | 53 +++++++++------ LeanBandits/ForMathlib/SubGaussian.lean | 66 ++++++++++++++++--- .../SequentialLearning/FiniteActions.lean | 49 +++++++++++--- 3 files changed, 131 insertions(+), 37 deletions(-) diff --git a/LeanBandits/Bandit/SumRewards.lean b/LeanBandits/Bandit/SumRewards.lean index 07fb446e..536e3a7b 100644 --- a/LeanBandits/Bandit/SumRewards.lean +++ b/LeanBandits/Bandit/SumRewards.lean @@ -457,35 +457,50 @@ section Subgaussian open Real -lemma superMartingale_exp_sumRewards_sub (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {c : ℝ≥0} +lemma superMartingale_exp_sumNoises (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {c : ℝ≥0} (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) c (ν a)) (t : ℝ) : Supermartingale (fun n ω ↦ - exp (t * (sumRewards A R a (n + 1) ω - pullCount A a (n + 1) ω * (ν a)[id]))) + exp (t * (sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω) + - t ^ 2 * c * pullCount A a (n + 1) ω / 2)) (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R) P := by refine supermartingale_nat (fun n ↦ ?_) (fun n ↦ ?_) (fun n ↦ ?_) - · change StronglyMeasurable[IsAlgEnvSeq.filtration h.measurable_A h.measurable_R _] (exp ∘ _) - refine StronglyMeasurable.comp_measurable (by fun_prop) ?_ - refine Measurable.const_mul ?_ _ - refine Measurable.sub ?_ ?_ - · exact (h.adapted_sumRewards_add_one a n).measurable - · have := adapted_pullCount_add_one h.measurable_A h.measurable_R a n - fun_prop + · have h1 := h.adapted_sumNoises_add_one a n (μ := fun a ↦ (ν a)[id]) + have h2 := adapted_pullCount_add_one h.measurable_A h.measurable_R a n + fun_prop · sorry - · simp_rw [sumRewards_sub_pullCount_mul_eq_sum (n := n + 1) (fun a ↦ (ν a)[id]), - sum_range_succ (n := n + 1), - ← sumRewards_sub_pullCount_mul_eq_sum (n := n) (fun a ↦ (ν a)[id]), mul_add, exp_add] - calc P[fun ω ↦ exp (t * (sumRewards A R a (n + 1) ω - pullCount A a (n + 1) ω * (ν a)[id])) * - exp (t * if A (n + 1) ω = a then R (n + 1) ω - (ν a)[id] else 0)| + · simp_rw [sumNoises_add_one (t := n + 1), pullCount_add_one (t := n + 1)] + have h_ae_eq ω : + (t * (sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω + + if A (n + 1) ω = a then R (n + 1) ω - (ν a)[id] else 0)) - + t ^ 2 * c * ↑(pullCount A a (n + 1) ω + if A (n + 1) ω = a then 1 else 0) / 2 = + (t * sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω - + t ^ 2 * c * (pullCount A a (n + 1) ω) / 2) + + if A (n + 1) ω = a then t * (R (n + 1) ω - (ν a)[id]) - t ^ 2 * c / 2 else 0 := by + simp only [id_eq, Nat.cast_add, Nat.cast_ite, Nat.cast_one, CharP.cast_eq_zero] + split_ifs with hA <;> ring + simp_rw [h_ae_eq, exp_add] + calc P[fun ω ↦ exp (t * sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω - + t ^ 2 * c * (pullCount A a (n + 1) ω) / 2) * + exp (if A (n + 1) ω = a then t * (R (n + 1) ω - (ν a)[id]) - t ^ 2 * c / 2 else 0)| IsAlgEnvSeq.filtration h.measurable_A h.measurable_R n] - _ =ᵐ[P] (fun ω ↦ exp (t * (sumRewards A R a (n + 1) ω - pullCount A a (n + 1) ω * (ν a)[id]))) * - P[fun ω ↦ exp (t * if A (n + 1) ω = a then R (n + 1) ω - (ν a)[id] else 0)| + _ =ᵐ[P] (fun ω ↦ exp (t * (sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω) - + t ^ 2 * c * (pullCount A a (n + 1) ω) / 2)) * + P[fun ω ↦ exp (if A (n + 1) ω = a then t * (R (n + 1) ω - (ν a)[id]) - t ^ 2 * c / 2 else 0)| IsAlgEnvSeq.filtration h.measurable_A h.measurable_R n] := by apply condExp_mul_of_aestronglyMeasurable_left + · have h1 := h.adapted_sumNoises_add_one a n (μ := fun a ↦ (ν a)[id]) + have h2 := adapted_pullCount_add_one h.measurable_A h.measurable_R a n + fun_prop · sorry · sorry - · sorry - _ ≤ᵐ[P] fun ω ↦ exp (t * (sumRewards A R a (n + 1) ω - pullCount A a (n + 1) ω * (ν a)[id])) := - sorry + _ ≤ᵐ[P] fun ω ↦ exp (t * sumNoises A R (fun a ↦ (ν a)[id]) a (n + 1) ω - + t ^ 2 * c * (pullCount A a (n + 1) ω) / 2) := by + suffices P[fun ω ↦ exp (if A (n + 1) ω = a then t * (R (n + 1) ω - (ν a)[id]) - t ^ 2 * c / 2 + else 0) | IsAlgEnvSeq.filtration h.measurable_A h.measurable_R n] ≤ᵐ[P] 1 by + filter_upwards [this] with ω hω + simp only [id_eq, Pi.mul_apply, Pi.one_apply] at ⊢ hω + exact mul_le_of_le_one_right (by positivity) hω + sorry omit [DecidableEq α] [StandardBorelSpace α] in lemma probReal_sum_le_sum_streamMeasure [Fintype α] {c : ℝ≥0} diff --git a/LeanBandits/ForMathlib/SubGaussian.lean b/LeanBandits/ForMathlib/SubGaussian.lean index 5c142119..7a535278 100644 --- a/LeanBandits/ForMathlib/SubGaussian.lean +++ b/LeanBandits/ForMathlib/SubGaussian.lean @@ -10,6 +10,25 @@ open scoped ENNReal NNReal namespace ProbabilityTheory +namespace HasSubgaussianMGF + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} + {μ : Measure Ω} {X : Ω → ℝ} {c : ℝ≥0} + +lemma memLp_exp_mul_sub (h : HasSubgaussianMGF X c μ) (t : ℝ) (p : ℝ≥0) : + MemLp (fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)) p μ := by + have h_lp := h.memLp_exp_mul t p + simp_rw [sub_eq_add_neg, exp_add] + exact h_lp.mul_const _ + +lemma integrable_exp_mul_sub (h : HasSubgaussianMGF X c μ) (t : ℝ) : + Integrable (fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)) μ := by + have h_int := h.integrable_exp_mul t + simp_rw [exp_sub] + exact h_int.div_const _ + +end HasSubgaussianMGF + namespace HasCondSubgaussianMGF variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] @@ -57,10 +76,10 @@ lemma aux {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥0} {ℱ : Filtration ℕ m (h_subG : ∀ n, HasCondSubgaussianMGF (ℱ n) (ℱ.le n) (X (n + 1)) (c (n + 1)) μ) (hp : IsPredictable ℱ p) (t : ℝ) (n : ℕ) : ∀ q, 1 < q → MemLp (fun ω ↦ exp (∑ i ∈ Finset.range n, - t * if p i ω then (X i ω - c i * t ^ 2 / 2) else 0)) q μ := by + if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) q μ := by induction n with | zero => - simp only [Finset.range_zero, mul_ite, mul_zero, Finset.sum_empty, exp_zero] + simp only [Finset.range_zero, Finset.sum_empty, exp_zero] exact fun _ _ ↦ memLp_const _ | succ n hn => intro q hq @@ -68,21 +87,50 @@ lemma aux {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥0} {ℱ : Filtration ℕ m obtain ⟨p1, p2, hp1, hp2, h_triple⟩ : ∃ p1 p2, 1 < p1 ∧ 1 < p2 ∧ ENNReal.HolderTriple p1 p2 q := by refine ⟨2 * q, 2 * q, ?_, ?_, ?_⟩ - · sorry - · sorry + · conv_lhs => rw [← one_mul 1] + gcongr + simp + · conv_lhs => rw [← one_mul 1] + gcongr + simp · constructor - sorry + rw [ENNReal.mul_inv (by simp) (by simp), ← ENNReal.div_eq_inv_mul, ENNReal.add_halves] refine MemLp.mul (q := p2) ?_ (hn p1 hp1) - sorry + cases n with + | zero => + have h_Lp := h0.memLp_exp_mul_sub t p2.toNNReal + sorry + | succ n => + have h_Lp := (h_subG n).memLp_exp_mul_sub t p2.toNNReal + sorry lemma todo_supermartingale_optional {X : ℕ → Ω → ℝ} {c : ℕ → ℝ≥0} {ℱ : Filtration ℕ mΩ} - {p : ℕ → Ω → Prop} [∀ n, DecidablePred (p n)] + {p : ℕ → Ω → Prop} [∀ n, DecidablePred (p n)] (hX : Adapted ℱ X) (h0 : HasSubgaussianMGF (X 0) (c 0) μ) (h_subG : ∀ n, HasCondSubgaussianMGF (ℱ n) (ℱ.le n) (X (n + 1)) (c (n + 1)) μ) (hp : IsPredictable ℱ p) (t : ℝ) : Supermartingale (fun n ω ↦ exp (∑ i ∈ Finset.range n, - if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) ℱ μ := - sorry + if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) ℱ μ := by + refine supermartingale_nat (fun n ↦ ?_) (fun n ↦ ?_) (fun n ↦ ?_) + · sorry + · sorry + · simp_rw [Finset.sum_range_succ, exp_add] + calc μ[fun ω ↦ exp (∑ i ∈ Finset.range n, if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0) * + exp (if p n ω then t * X n ω - c n * t ^ 2 / 2 else 0) | ℱ n] + _ =ᵐ[μ] (fun ω ↦ exp (∑ i ∈ Finset.range n, + if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0)) * + μ[fun ω ↦ exp (if p n ω then t * X n ω - c n * t ^ 2 / 2 else 0) | ℱ n] := by + apply condExp_mul_of_aestronglyMeasurable_left + · sorry + · sorry + · sorry + _ ≤ᵐ[μ] fun ω ↦ exp (∑ i ∈ Finset.range n, + if p i ω then (t * X i ω - c i * t ^ 2 / 2) else 0) := by + suffices μ[fun ω ↦ exp (if p n ω then t * X n ω - c n * t ^ 2 / 2 else 0) | ℱ n] ≤ᵐ[μ] 1 by + filter_upwards [this] with ω hω + simp only [Pi.mul_apply, Pi.one_apply] at ⊢ hω + exact mul_le_of_le_one_right (by positivity) hω + sorry end HasCondSubgaussianMGF diff --git a/LeanBandits/SequentialLearning/FiniteActions.lean b/LeanBandits/SequentialLearning/FiniteActions.lean index b46415be..69b211b5 100644 --- a/LeanBandits/SequentialLearning/FiniteActions.lean +++ b/LeanBandits/SequentialLearning/FiniteActions.lean @@ -749,6 +749,9 @@ noncomputable def empMean' (n : ℕ) (h : Iic n → α × ℝ) (a : α) := (sumRewards' n h a) / (pullCount' n h a) +def sumNoises (A : ℕ → Ω → α) (R' : ℕ → Ω → ℝ) (μ : α → ℝ) (a : α) (t : ℕ) (ω : Ω) : ℝ := + ∑ s ∈ range t, if A s ω = a then R' s ω - μ a else 0 + @[simp] lemma sumRewards_zero {R' : ℕ → Ω → ℝ} : sumRewards A R' a 0 = 0 := by ext; simp [sumRewards] @@ -757,6 +760,12 @@ lemma sumRewards_add_one {R' : ℕ → Ω → ℝ} : unfold sumRewards rw [sum_range_succ] +lemma sumNoises_add_one {R' : ℕ → Ω → ℝ} (μ : α → ℝ) : + sumNoises A R' μ a (t + 1) ω = + sumNoises A R' μ a t ω + if A t ω = a then R' t ω - μ a else 0 := by + unfold sumNoises + rw [sum_range_succ] + lemma sumRewards_eq_of_pullCount_eq {R' : ℕ → Ω → ℝ} {s t : ℕ} (h_eq : pullCount A a s ω = pullCount A a t ω) : sumRewards A R' a s ω = sumRewards A R' a t ω := by @@ -816,17 +825,13 @@ lemma empMean_eq_empMean' {R' : ℕ → Ω → ℝ} {n : ℕ} {ω : Ω} (hn : n unfold empMean empMean' rw [sumRewards_eq_sumRewards' hn, pullCount_eq_pullCount' hn] -lemma sumRewards_sub_pullCount_mul_eq_sum {R' : ℕ → Ω → ℝ} (c : α → ℝ) : - sumRewards A R' a (n + 1) ω - pullCount A a (n + 1) ω * c a = - ∑ i ∈ range (n + 1), (if A i ω = a then R' i ω - c a else 0) := by +lemma sumRewards_sub_pullCount_mul_eq_sumNoises {R' : ℕ → Ω → ℝ} (c : α → ℝ) : + sumRewards A R' a n ω - pullCount A a n ω * c a = sumNoises A R' c a n ω := by + unfold sumNoises induction n with - | zero => - simp_rw [sumRewards_add_one, pullCount_add_one] - simp only [sumRewards_zero, Pi.zero_apply, zero_add, pullCount_zero, Nat.cast_ite, Nat.cast_one, - CharP.cast_eq_zero, ite_mul, one_mul, zero_mul, range_one, sum_singleton] - grind + | zero => simp | succ n hn => - simp_rw [sumRewards_add_one (t := n + 1), pullCount_add_one (t := n + 1)] + simp_rw [sumRewards_add_one (t := n), pullCount_add_one (t := n)] split_ifs with ha · conv_rhs => rw [sum_range_succ] simp only [Nat.cast_add, Nat.cast_one, ha, ↓reduceIte, add_mul, one_mul] @@ -835,6 +840,12 @@ lemma sumRewards_sub_pullCount_mul_eq_sum {R' : ℕ → Ω → ℝ} (c : α → conv_rhs => rw [sum_range_succ] simp [ha] + +lemma sumRewards_sub_pullCount_mul_eq_sumNoises' {R' : ℕ → Ω → ℝ} (c : α → ℝ) : + (fun ω ↦ sumRewards A R' a n ω - pullCount A a n ω * c a) = sumNoises A R' c a n := by + ext ω + exact sumRewards_sub_pullCount_mul_eq_sumNoises c + @[fun_prop] lemma measurable_sumRewards [MeasurableSingletonClass α] {R' : ℕ → Ω → ℝ} (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (a : α) (t : ℕ) : @@ -852,6 +863,13 @@ lemma measurable_empMean [MeasurableSingletonClass α] {R' : ℕ → Ω → ℝ} unfold empMean fun_prop +@[fun_prop] +lemma measurable_sumNoises [MeasurableSingletonClass α] {R' : ℕ → Ω → ℝ} + (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) (μ : α → ℝ) (a : α) (n : ℕ) : + Measurable (sumNoises A R' μ a n) := by + simp_rw [← sumRewards_sub_pullCount_mul_eq_sumNoises'] + fun_prop + @[fun_prop] lemma measurable_sumRewards' [MeasurableSingletonClass α] (n : ℕ) (a : α) : Measurable (fun h ↦ sumRewards' n h a) := by @@ -895,6 +913,19 @@ lemma IsAlgEnvSeq.adapted_sumRewards_add_one [StandardBorelSpace α] [Nonempty rw [isPredictable_iff_measurable_add_one] at h_predictable exact h_predictable.2 +lemma IsAlgEnvSeq.adapted_sumNoises_add_one [StandardBorelSpace α] [Nonempty α] {R' : ℕ → Ω → ℝ} + {alg : Algorithm α ℝ} {env : Environment α ℝ} {μ : α → ℝ} + (h : IsAlgEnvSeq A R' alg env P) (a : α) : + Adapted (IsAlgEnvSeq.filtration h.measurable_A h.measurable_R) + (fun n ↦ sumNoises A R' μ a (n + 1)) := by + simp_rw [← sumRewards_sub_pullCount_mul_eq_sumNoises'] + have h1 := h.adapted_sumRewards_add_one a + have h2 := adapted_pullCount_add_one h.measurable_A h.measurable_R a + refine h1.sub (Adapted.mul ?_ (adapted_const _ _)) + intro n + specialize h2 n + fun_prop + section CopiedFromPR open Set