diff --git a/LMLExplore/Bandits/Concentration.lean b/LMLExplore/Bandits/Concentration.lean index f6044ea7..b8265729 100644 --- a/LMLExplore/Bandits/Concentration.lean +++ b/LMLExplore/Bandits/Concentration.lean @@ -132,7 +132,7 @@ and 10.8] used in the regret analysis of KL-UCB for exponential families [GC11; public section -open MeasureTheory ProbabilityTheory Finset Real Set Learning Bandits +open MeasureTheory InformationTheory ProbabilityTheory Finset Real Set Learning Bandits open scoped NNReal diff --git a/LMLExplore/Bandits/KLUCB.lean b/LMLExplore/Bandits/KLUCB.lean index 5a8d1d63..a5e2ce3a 100644 --- a/LMLExplore/Bandits/KLUCB.lean +++ b/LMLExplore/Bandits/KLUCB.lean @@ -150,7 +150,7 @@ this limit to its Exercise 10.2. public section -open MeasureTheory ProbabilityTheory Finset Filter Topology Real Learning Bandits +open MeasureTheory InformationTheory ProbabilityTheory Finset Filter Topology Real Learning Bandits open scoped ENNReal NNReal diff --git a/LMLExplore/InformationTheory/KrichevskyTrofimov.lean b/LMLExplore/InformationTheory/KrichevskyTrofimov.lean index d4a97f9a..9a4b01b4 100644 --- a/LMLExplore/InformationTheory/KrichevskyTrofimov.lean +++ b/LMLExplore/InformationTheory/KrichevskyTrofimov.lean @@ -57,7 +57,7 @@ RemyDegenne/Garivier2016Optimal (commit 53ac67e4, directory `ForLMLExplore/`). public section -open MeasureTheory ProbabilityTheory Real Set +open MeasureTheory InformationTheory ProbabilityTheory Real Set namespace LMLExplore diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean b/LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean index 536f54b3..fb5e5a8f 100644 --- a/LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean +++ b/LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean @@ -11,6 +11,7 @@ public import Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog public import LMLExplore.Probability.Distributions.Bernoulli public import TauCeti.InformationTheory.KullbackLeibler.Basic public import TauCeti.InformationTheory.KullbackLeibler.Pinsker +public import Statlib.ForMathlib.InformationTheory.KullbackLeibler.Bernoulli public import Statlib.ForMathlib.InformationTheory.KullbackLeibler.ChainRule public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing public import TauCeti.InformationTheory.KullbackLeibler.Variational @@ -28,8 +29,10 @@ for `[0, 1]`-valued random variables, and the quantity in the KL-UCB index and i Lai–Robbins lower bound for Bernoulli bandits. We define `klBer p q : ℝ≥0∞` as `klDiv` of the two Bernoulli laws on `{0, 1} ⊆ ℝ`, so that it -takes the value `∞` exactly where `d(p, q)` does, and the real-valued `klBerReal p q` by the -closed form above. For `p, q ∈ [0, 1]`, the two agree wherever `klBer p q` is finite. +takes the value `∞` exactly where `d(p, q)` does. The real-valued closed form above is Statlib's +`InformationTheory.klBerReal p q`, whose basic API (`klBerReal_apply`, `klBerReal_self`, +`klBerReal_one_left`, `klBerReal_one_sub`, `klBerReal_eq_neg_binEntropy_sub`) comes from Statlib +too. For `p, q ∈ [0, 1]`, the two agree wherever `klBer p q` is finite. The upper confidence level `U(p, c)` is the largest `q ∈ [p, 1]` with `d(p, q) ≤ c`: evaluated at an empirical mean `p` and an exploration level `c` divided by a number of samples, it is the index @@ -41,7 +44,6 @@ smallest `q ∈ [0, p]` with `d(p, q) ≤ c`; together they are the confidence b * `LMLExplore.klBer p q`: the binary relative entropy in `ℝ≥0∞`, the arguments being clamped to `[0, 1]`. -* `LMLExplore.klBerReal p q`: the real number `p log (p / q) + (1 - p) log ((1 - p) / (1 - q))`. * `LMLExplore.klUpper p c`: the upper confidence level `U(p, c) = max {q ∈ [p, 1] | d(p, q) ≤ c}` of the KL-UCB algorithm, for `c : ℝ≥0∞`. * `LMLExplore.klLower p c`: the lower confidence level `L(p, c) = min {q ∈ [0, p] | d(p, q) ≤ c}`, @@ -61,8 +63,8 @@ smallest `q ∈ [0, p]` with `d(p, q) ≤ c`; together they are the confidence b is finite, `klBer p q` is given by the closed form `klBerReal p q`. * `LMLExplore.klBer_eq_zero_iff`: for `p, q ∈ [0, 1]`, `klBer p q = 0` if and only if `p = q`. `LMLExplore.klBerReal_eq_zero_iff` is its real-valued form for `q ∈ (0, 1)`. -* `LMLExplore.klBer_one_sub_one_sub`, `LMLExplore.klBerReal_one_sub_one_sub`: - `d(1 - p, 1 - q) = d(p, q)`. +* `LMLExplore.klBer_one_sub_one_sub`: `d(1 - p, 1 - q) = d(p, q)`, the `ℝ≥0∞`-valued form of + `InformationTheory.klBerReal_one_sub`. * `LMLExplore.ofReal_two_mul_sq_le_klBer`, `LMLExplore.two_mul_sq_le_klBerReal`: Pinsker's inequality `2 (p - q)² ≤ d(p, q)` for `p, q ∈ [0, 1]`. * `LMLExplore.klBer_le_ofReal_sq_sub_div`, `LMLExplore.klBerReal_le_sq_sub_div`: the reverse @@ -166,12 +168,6 @@ noncomputable def klBer (p q : ℝ) : ℝ≥0∞ := klDiv Ber((1 : ℝ), 0, Set.projIcc 0 1 zero_le_one p) Ber((1 : ℝ), 0, Set.projIcc 0 1 zero_le_one q) -/-- The real-valued binary relative entropy `p log (p / q) + (1 - p) log ((1 - p) / (1 - q))`. -For `p, q ∈ [0, 1]` it is the value of `klBer p q` whenever the latter is finite -(`LMLExplore.toReal_klBer`). -/ -noncomputable def klBerReal (p q : ℝ) : ℝ := - p * log (p / q) + (1 - p) * log ((1 - p) / (1 - q)) - variable {p q : ℝ} /-- The relative entropy between two Bernoulli laws on two distinct points `x ≠ y` of a measurable @@ -211,10 +207,6 @@ theorem klBer_def (p q : ℝ) : Ber((1 : ℝ), 0, Set.projIcc 0 1 zero_le_one q) := by rw [klBer] -theorem klBerReal_def (p q : ℝ) : - klBerReal p q = p * log (p / q) + (1 - p) * log ((1 - p) / (1 - q)) := by - rw [klBerReal] - /-- On `[0, 1]`, `klBer p q` is the relative entropy of the Bernoulli laws of parameters `p` and `q`. -/ theorem klBer_of_mem_Icc (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) : @@ -251,15 +243,6 @@ theorem klBer_integral_le_klDiv {μ ν : Measure ℝ} [IsProbabilityMeasure μ] theorem klBer_self (p : ℝ) : klBer p p = 0 := by rw [klBer_def, klDiv_self] -@[simp] -theorem klBerReal_self (p : ℝ) : klBerReal p p = 0 := by - simp [klBerReal_def] - -/-- `d(1, q) = -log q`. -/ -@[simp] -theorem klBerReal_one_left (q : ℝ) : klBerReal 1 q = -log q := by - simp [klBerReal_def] - /-- For `p, q ∈ [0, 1]`, `klBer p q` is finite if and only if `p` vanishes when `q` does and `p = 1` when `q = 1`. -/ theorem klBer_ne_top_iff (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) : @@ -290,7 +273,7 @@ theorem toReal_klBer (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) (h : klBe rw [klBer_of_mem_Icc hp hq] at h ⊢ obtain ⟨hac, hint⟩ := klDiv_ne_top_iff.1 h rw [toReal_klDiv hac hint, integral_bernoulliMeasure] - simp only [probReal_univ, add_sub_cancel_right, smul_eq_mul, klBerReal_def] + simp only [probReal_univ, add_sub_cancel_right, smul_eq_mul, klBerReal_apply] congr 1 · rcases eq_or_ne q 0 with rfl | hq0 · simp [h0 rfl] @@ -330,7 +313,8 @@ theorem two_mul_sq_le_klBerReal (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1 /-- For `p, q ∈ [0, 1]`, the real-valued binary relative entropy is nonnegative where `klBer p q` is finite. -/ -theorem klBerReal_nonneg (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) (h : klBer p q ≠ ∞) : +theorem klBerReal_nonneg_of_klBer_ne_top (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) + (h : klBer p q ≠ ∞) : 0 ≤ klBerReal p q := (by positivity : (0 : ℝ) ≤ 2 * (p - q) ^ 2).trans (two_mul_sq_le_klBerReal hp hq h) @@ -343,9 +327,9 @@ theorem klBer_eq_zero_iff (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Icc 0 1) : nlinarith [sq_nonneg (p - q)] /-- For `p ∈ [0, 1]` and `q ∈ (0, 1)`, the real-valued binary relative entropy vanishes only at -`p = q`. With `LMLExplore.klBerReal_nonneg`, `q` is the unique minimizer of `p ↦ d(p, q)` on -`[0, 1]` and, for `p ∈ (0, 1)`, `p` is the unique minimizer of `q ↦ d(p, q)` on `(0, 1)` -[LS, Lemma 10.2]. -/ +`p = q`. With `LMLExplore.klBerReal_nonneg_of_klBer_ne_top`, `q` is the unique minimizer of +`p ↦ d(p, q)` on `[0, 1]` and, for `p ∈ (0, 1)`, `p` is the unique minimizer of `q ↦ d(p, q)` on +`(0, 1)` [LS, Lemma 10.2]. -/ theorem klBerReal_eq_zero_iff (hp : p ∈ Set.Icc 0 1) (hq : q ∈ Set.Ioo 0 1) : klBerReal p q = 0 ↔ p = q := by rw [← toReal_klBer hp (Set.Ioo_subset_Icc_self hq) (klBer_ne_top hq), @@ -423,12 +407,6 @@ theorem klBer_one_sub_one_sub (p q : ℝ) : klBer (1 - p) (1 - q) = klBer p q := rw [klBer_def, klBer_def, ← symm_projIcc, ← symm_projIcc, h, h] exact klDiv_map_measurableEmbedding _ _ (MeasurableEquiv.subLeft (1 : ℝ)).measurableEmbedding -/-- The real-valued binary relative entropy is invariant under exchanging the roles of the two -outcomes. -/ -@[simp] -theorem klBerReal_one_sub_one_sub (p q : ℝ) : klBerReal (1 - p) (1 - q) = klBerReal p q := by - rw [klBerReal_def, klBerReal_def, sub_sub_cancel, sub_sub_cancel, add_comm] - /-! ### The maximum likelihood of a Bernoulli sample -/ /-- The frequency factor `(k / n) ^ k` of the maximum likelihood is positive for `n > 0`, including @@ -463,7 +441,7 @@ theorem mul_klBerReal_div_eq_log {k m n : ℕ} (hkm : k + m = n) (hn : 0 < n) rw [div_pow] exact (div_pos (div_pow_self_pos m hn) (pow_pos (sub_pos.2 hp.2) _)).ne' rw [mul_div_mul_comm, ← div_pow, ← div_pow, log_mul hk hm] - simp only [log_pow, klBerReal_def, h1] + simp only [log_pow, klBerReal_apply, h1] field_simp /-- The maximum likelihood of a Bernoulli sample: `u ^ k (1 - u) ^ m ≤ (k / n) ^ k (m / n) ^ m` @@ -494,23 +472,11 @@ theorem pow_mul_one_sub_pow_le_div_pow_mul_div_pow {k m n : ℕ} (hkm : k + m = have hq : 0 < u ^ k * (1 - u) ^ m := mul_pos (pow_pos hu0 _) (pow_pos (sub_pos.2 hu1) _) have hlog : 0 ≤ log (((k : ℝ) / n) ^ k * ((m : ℝ) / n) ^ m / (u ^ k * (1 - u) ^ m)) := by rw [← mul_klBerReal_div_eq_log hkm hn ⟨hu0, hu1⟩] - exact mul_nonneg hn'.le (klBerReal_nonneg hkn hu (klBer_ne_top ⟨hu0, hu1⟩)) + exact mul_nonneg hn'.le (klBerReal_nonneg_of_klBer_ne_top hkn hu (klBer_ne_top ⟨hu0, hu1⟩)) rwa [log_nonneg_iff (div_pos hR hq), one_le_div hq] at hlog /-! ### Continuity and monotonicity -/ -/-- Away from `q ∈ {0, 1}`, `klBerReal p q` is the binary cross-entropy -`-(p log q + (1 - p) log (1 - q))` minus the binary entropy of `p`. -/ -theorem klBerReal_eq_neg_binEntropy_sub (hq0 : q ≠ 0) (hq1 : q ≠ 1) : - klBerReal p q = -binEntropy p - (p * log q + (1 - p) * log (1 - q)) := by - have key {a b : ℝ} (hb : b ≠ 0) : a * log (a / b) = a * log a - a * log b := by - rcases eq_or_ne a 0 with rfl | ha - · simp - rw [log_div ha hb, mul_sub] - rw [klBerReal_def, key hq0, key (sub_ne_zero.2 hq1.symm)] - simp only [binEntropy_eq_negMulLog_add_negMulLog_one_sub, negMulLog_def] - ring - /-- The real-valued binary relative entropy is jointly continuous on `ℝ × (0, 1)`. -/ theorem continuousOn_klBerReal : ContinuousOn (Function.uncurry klBerReal) (Set.univ ×ˢ Set.Ioo 0 1) := by @@ -520,7 +486,7 @@ theorem continuousOn_klBerReal : (continuous_const.sub continuous_snd).continuousOn.log fun x hx ↦ (sub_pos.2 hx.2.2).ne' refine ContinuousOn.congr (f := fun x : ℝ × ℝ ↦ -binEntropy x.1 - (x.1 * log x.2 + (1 - x.1) * log (1 - x.2))) ?_ - fun x hx ↦ klBerReal_eq_neg_binEntropy_sub hx.2.1.ne' hx.2.2.ne + fun x hx ↦ (klBerReal_eq_neg_binEntropy_sub hx.2.1.ne' hx.2.2.ne).trans (sub_sub _ _ _) exact (binEntropy_continuous.comp continuous_fst).neg.continuousOn.sub ((continuous_fst.continuousOn.mul hlog).add ((continuous_const.sub continuous_fst).continuousOn.mul hlog')) @@ -572,7 +538,7 @@ theorem hasDerivAt_klBerReal (p : ℝ) (hq : q ∈ Set.Ioo 0 1) : · field_simp ring · filter_upwards [isOpen_Ioo.mem_nhds hq] with x hx - exact klBerReal_eq_neg_binEntropy_sub hx.1.ne' hx.2.ne + exact (klBerReal_eq_neg_binEntropy_sub hx.1.ne' hx.2.ne).trans (sub_sub _ _ _) /-- On the right of `p`, `q ↦ klBerReal p q` is strictly increasing on `(0, 1)`. -/ theorem strictMonoOn_klBerReal (p : ℝ) : @@ -613,7 +579,8 @@ theorem strictMonoOn_klBer (hp : p ∈ Set.Icc 0 1) : StrictMonoOn (klBer p) (Se have hq₂01 : q₂ ∈ Set.Ioo 0 1 := ⟨hq₁01.1.trans h, hq₂1⟩ rw [klBer_eq_ofReal_klBerReal hp hq₁' (klBer_ne_top hq₁01), klBer_eq_ofReal_klBerReal hp hq₂' (klBer_ne_top hq₂01), - ENNReal.ofReal_lt_ofReal_iff_of_nonneg (klBerReal_nonneg hp hq₁' (klBer_ne_top hq₁01))] + ENNReal.ofReal_lt_ofReal_iff_of_nonneg + (klBerReal_nonneg_of_klBer_ne_top hp hq₁' (klBer_ne_top hq₁01))] exact strictMonoOn_klBerReal p ⟨hq₁.1, hq₁01⟩ ⟨hq₂.1, hq₂01⟩ h /-- For `p ∈ [0, 1]`, `q ↦ klBer p q` is strictly decreasing on `[0, p]`. -/ @@ -660,7 +627,7 @@ theorem hasDerivAt_klBerReal_left (hp0 : p ≠ 0) (hp1 : p ≠ 1) (hq0 : q ≠ 0 (-(log (1 - p) - log p) - (1 * log q + -1 * log (1 - q))) p := (hasDerivAt_binEntropy hp0 hp1).neg.sub (((hasDerivAt_id' p).mul_const _).add (((hasDerivAt_id' p).const_sub 1).mul_const _)) - rw [funext fun x ↦ klBerReal_eq_neg_binEntropy_sub (p := x) hq0 hq1] + rw [funext fun x ↦ (klBerReal_eq_neg_binEntropy_sub (p := x) hq0 hq1).trans (sub_sub _ _ _)] exact h.congr_deriv (by ring) /-- For `q ∈ (0, 1)`, `p ↦ klBerReal p q` is strictly decreasing on `[0, q]`. -/ @@ -738,9 +705,10 @@ theorem klBer_add_klBer_le {r : ℝ} (hpq : p ≤ q) (hqr : q ≤ r) : klBer_eq_ofReal_klBerReal (Set.Ioo_subset_Icc_self hq') (Set.Ioo_subset_Icc_self hr') (klBer_ne_top hr'), klBer_eq_ofReal_klBerReal hp' (Set.Ioo_subset_Icc_self hr') (klBer_ne_top hr'), - ← ENNReal.ofReal_add (klBerReal_nonneg hp' (Set.Ioo_subset_Icc_self hq') (klBer_ne_top hq')) - (klBerReal_nonneg (Set.Ioo_subset_Icc_self hq') (Set.Ioo_subset_Icc_self hr') - (klBer_ne_top hr'))] + ← ENNReal.ofReal_add + (klBerReal_nonneg_of_klBer_ne_top hp' (Set.Ioo_subset_Icc_self hq') (klBer_ne_top hq')) + (klBerReal_nonneg_of_klBer_ne_top (Set.Ioo_subset_Icc_self hq') + (Set.Ioo_subset_Icc_self hr') (klBer_ne_top hr'))] refine ENNReal.ofReal_le_ofReal ?_ -- `d(p, r) - d(p, q)` is affine in `p`, with value `d(q, r)` at `p = q` and a nonpositive -- slope `(log q - log r) - (log (1 - q) - log (1 - r))` @@ -753,12 +721,11 @@ theorem klBer_add_klBer_le {r : ℝ} (hpq : p ≤ q) (hqr : q ≤ r) : (1 - p) * log ((1 - p) / (1 - q)) + (1 - p) * (log (1 - q) - log (1 - r)) := by rw [log_div (by linarith) (by linarith), log_div (by linarith) (by linarith)] ring - have h₃ : klBerReal q r = q * (log q - log r) + (1 - q) * (log (1 - q) - log (1 - r)) := by - rw [klBerReal_def, log_div hq'.1.ne' hr'.1.ne', log_div (by linarith) (by linarith)] + have h₃ := klBerReal_eq_of_ne (p := q) hr'.1.ne' hr'.2.ne have hA : log q - log r ≤ 0 := by linarith [log_le_log hq'.1 hqr.le] have hB : 0 ≤ log (1 - q) - log (1 - r) := by linarith [log_le_log (sub_pos.2 hr1) (by linarith : 1 - r ≤ 1 - q)] - rw [klBerReal_def p r, h₁, h₂, h₃, klBerReal_def p q] + rw [klBerReal_apply p r, h₁, h₂, h₃, klBerReal_apply p q] nlinarith [mul_nonneg (sub_nonneg.2 hpq.le) (sub_nonneg.2 (hA.trans hB))] rw [← klBer_projIcc p q, ← klBer_projIcc q r, ← klBer_projIcc p r] exact key (Set.projIcc 0 1 zero_le_one p).2.1 (Set.monotone_projIcc zero_le_one hpq) @@ -830,7 +797,8 @@ theorem strictConvexOn_klBerReal_left (hq : q ∈ Set.Ioo 0 1) : refine ⟨convex_Icc 0 1, fun x _ y _ a b _ _ hab ↦ le_of_eq ?_⟩ simp only [smul_eq_mul] linear_combination (log (1 - q)) * hab - rw [funext fun p ↦ klBerReal_eq_neg_binEntropy_sub (p := p) hq.1.ne' hq.2.ne] + rw [funext fun p ↦ + (klBerReal_eq_neg_binEntropy_sub (p := p) hq.1.ne' hq.2.ne).trans (sub_sub _ _ _)] exact strictConcave_binEntropy.neg.sub_concaveOn haff /-- For `p ∈ [0, 1]`, `q ↦ d(p, q)` is strictly convex on `(0, 1)` [LS, Lemma 10.2]: its @@ -890,7 +858,7 @@ theorem _root_.Measurable.klBer {α : Type*} {mα : MeasurableSpace α} {f g : /-- `d(p, 1 - p) = (1 - 2p) log ((1 - p) / p)`. -/ theorem klBerReal_one_sub_right (p : ℝ) : klBerReal p (1 - p) = (1 - 2 * p) * log ((1 - p) / p) := by - rw [klBerReal_def, sub_sub_cancel, ← inv_div (1 - p) p, Real.log_inv] + rw [klBerReal_apply, sub_sub_cancel, ← inv_div (1 - p) p, Real.log_inv] ring /-- For `p ∈ (0, 1)`, `d(p, 1 - p) = (1 - 2p) log ((1 - p) / p)`. -/ @@ -1053,7 +1021,7 @@ theorem tendsto_klBerReal_nhdsLT_one (hp0 : 0 ≤ p) (hp : p < 1) : nhdsWithin_le_nhds, eventually_nhdsWithin_of_forall fun q (hq : q < 1) ↦ sub_pos.2 hq⟩ refine ((tendsto_klBerReal_nhdsGT_zero (sub_pos.2 hp) (by linarith)).comp h).congr fun q ↦ ?_ - exact klBerReal_one_sub_one_sub p q + exact klBerReal_one_sub p q /-- **Lower bound on the binary relative entropy by `klFun`**: for `p ≤ 1`, `q ≠ 0` and `q < 1`, `q klFun (p / q) ≤ d(p, q)`, with `klFun x = x log x + 1 - x`. For `p, q ∈ (0, 1)` with `p / q` @@ -1077,7 +1045,7 @@ theorem mul_klFun_div_le_klBerReal (hp : p ≤ 1) (hq0 : q ≠ 0) (hq1 : q < 1) have h5 : q * (p / q * log (p / q) + 1 - p / q) = p * log (p / q) + (q - p) := by field_simp ring - rw [klBerReal_def, klFun_apply, h5] + rw [klBerReal_apply, klFun_apply, h5] linarith /-! ### The upper confidence level -/ diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Finite.lean b/LMLExplore/InformationTheory/KullbackLeibler/Finite.lean index 11725ceb..40294a4e 100644 --- a/LMLExplore/InformationTheory/KullbackLeibler/Finite.lean +++ b/LMLExplore/InformationTheory/KullbackLeibler/Finite.lean @@ -115,7 +115,7 @@ theorem sq_sum_abs_sub_le_two_mul_sum_mul_log_div {x z : α → ℝ} (hx : x ∈ ring -- the log-sum inequality on both blocks bounds the relative entropy below by `d(p, q)` have h_blocks : klBerReal p q ≤ ∑ a, x a * log (x a / z a) := by - rw [← sum_filter_add_sum_filter_not univ (fun a ↦ z a ≤ x a), klBerReal_def, ← hpc, ← hqc] + rw [← sum_filter_add_sum_filter_not univ (fun a ↦ z a ≤ x a), klBerReal_apply, ← hpc, ← hqc] exact add_le_add (sum_mul_log_div_sum_le_sum_mul_log_div _ (fun a _ ↦ hx0 a) (fun a _ ↦ hz0 a) fun a _ ↦ hxz a) diff --git a/LMLExplore/Probability/Distributions/ExponentialFamily/Bernoulli.lean b/LMLExplore/Probability/Distributions/ExponentialFamily/Bernoulli.lean index 8cd3eb8c..02863333 100644 --- a/LMLExplore/Probability/Distributions/ExponentialFamily/Bernoulli.lean +++ b/LMLExplore/Probability/Distributions/ExponentialFamily/Bernoulli.lean @@ -86,7 +86,7 @@ sampling law of Thompson sampling with the Jeffreys prior for Bernoulli arms [KK public section -open MeasureTheory ProbabilityTheory Real Set +open MeasureTheory InformationTheory ProbabilityTheory Real Set open scoped unitInterval ENNReal Topology @@ -225,7 +225,7 @@ theorem rateFunction_id_bernoulliMeasure (q : I) (hx : x ∈ Icc 0 1) : (fun h ↦ sub_ne_zero.2 (Ne.symm hq) (by rw [← hP]; exact (measureReal_eq_zero_iff).2 h)), hP, klBer_eq_ofReal_klBerReal hx q.2 ((klBer_ne_top_iff hx q.2).2 ⟨fun _ ↦ rfl, fun h ↦ absurd h hq⟩)] - simp [klBerReal_def] + simp [klBerReal_apply] rcases hx.2.eq_or_lt with rfl | hx1 · -- The level `1` is the essential supremum, of probability `q`. have hs : {z : ℝ | id z = 1} = {1} := by ext; simp diff --git a/LMLExplore/Probability/Moments/KLChernoff.lean b/LMLExplore/Probability/Moments/KLChernoff.lean index 34201304..8abf3e58 100644 --- a/LMLExplore/Probability/Moments/KLChernoff.lean +++ b/LMLExplore/Probability/Moments/KLChernoff.lean @@ -103,7 +103,7 @@ expected number of sample sizes `s` at which `s = 0`, `c ≤ μ̂_s` or `d(μ̂_ public section -open MeasureTheory ProbabilityTheory Filter Real Finset +open MeasureTheory InformationTheory ProbabilityTheory Filter Real Finset open scoped NNReal Topology unitInterval namespace LMLExplore @@ -278,7 +278,7 @@ theorem measureReal_sum_le_le_exp_klBerReal {X : ι → Ω → ℝ} (h_indep : i (fun i hi ↦ by simp [integral_sub (integrable_const 1) (.of_mem_Icc 0 1 (hXm i hi) (hX i hi))] linarith [hmean i hi]) - rw [← klBerReal_one_sub_one_sub, sub_zero, klBerReal_one_left, mul_neg, neg_neg, exp_nat_mul, + rw [← klBerReal_one_sub, sub_zero, klBerReal_one_left, mul_neg, neg_neg, exp_nat_mul, exp_log (sub_pos.2 hm)] refine le_of_eq_of_le ?_ h congr 1 @@ -388,7 +388,7 @@ theorem measureReal_klUpper_le_le {X : ι → Ω → ℝ} (h_indep : iIndepFun X rw [sub_sq_comm] exact ofReal_two_mul_sq_le_klBer hq' hm' refine ⟨x, ⟨hx.1, hxq.trans hqm⟩, (mul_div_cancel₀ _ hs0.ne').ge, ?_⟩ - exact (ENNReal.ofReal_le_ofReal_iff (klBerReal_nonneg hx hm' h_fin)).1 h_le + exact (ENNReal.ofReal_le_ofReal_iff (klBerReal_nonneg_of_klBer_ne_top hx hm' h_fin)).1 h_le _ ≤ exp (-(#s * (L / #s + 2 * (m - q) ^ 2))) := measureReal_exists_sum_le_and_le_klBerReal_le h_indep hXm hX hmean hm _ _ = exp (-L) * exp (-(2 * (m - q) ^ 2 * #s)) := by diff --git a/LMLExplore/SequentialLearning/BernoulliDeviation.lean b/LMLExplore/SequentialLearning/BernoulliDeviation.lean index b78d4624..dabdbb83 100644 --- a/LMLExplore/SequentialLearning/BernoulliDeviation.lean +++ b/LMLExplore/SequentialLearning/BernoulliDeviation.lean @@ -48,7 +48,7 @@ RemyDegenne/Garivier2016Optimal (commit 53ac67e4, directory `ForLMLExplore/`). public section -open MeasureTheory ProbabilityTheory Learning Finset Real unitInterval +open MeasureTheory InformationTheory ProbabilityTheory Learning Finset Real unitInterval open scoped ENNReal @@ -281,7 +281,7 @@ theorem measure_exists_log_two_mul_mul_lt_klBer_le ENNReal.ofReal_natCast] have hT_nonneg : ∀ {q : ℝ} {j N : ℕ}, q ∈ Set.Ioo 0 1 → j ≤ N → 0 ≤ (N : ℝ) * klBerReal (j / N) q := fun {q j N} hq hj ↦ - mul_nonneg (Nat.cast_nonneg _) (klBerReal_nonneg + mul_nonneg (Nat.cast_nonneg _) (klBerReal_nonneg_of_klBer_ne_top (div_mem (Nat.cast_nonneg _) (Nat.cast_nonneg _) (by exact_mod_cast hj)) ⟨hq.1.le, hq.2.le⟩ (klBer_ne_top hq)) rw [hmean hpa hja (by rw [empMean, hSa]), hmean hpb hjb (by rw [empMean, hSb]),