diff --git a/LMLRoadmaps/Bandits/README.md b/LMLRoadmaps/Bandits/README.md index 9fbcbbb..3b139ac 100644 --- a/LMLRoadmaps/Bandits/README.md +++ b/LMLRoadmaps/Bandits/README.md @@ -153,7 +153,7 @@ dependency versions used to check the interfaces (LML `53be244`, Mathlib `2e318f | Convex analysis | LML [`Bregman/Basic.lean`][lml-breg] (`bregDiv`, notation `D_[f](x, y, J)`, `bregDiv_three_point`), [`Subgradient/`][lml-subgrad]; Tau Ceti [`Conjugate.lean`][tc-conj] (`fenchelConjugate`, for a bilinear pairing), [`Strong.lean`][tc-strong] (`StrongConvexOn.add_add_le_of_hasFDerivWithinAt`); Mathlib `StrongConvexOn`, `PiLp`; LMLExplore `simplex` (`Analysis/Convex/Simplex.lean`) | | Linear algebra | Mathlib `ContinuousLinearMap.IsPositive` and its Loewner order, `LinearMap.det`, `Matrix.det_one_add_replicateCol_mul_replicateRow`, `Matrix.add_mul_mul_inv_eq_sub`; Tau Ceti [`Frame.lean`][tc-frame] (`frameOperator`), [`AffineNormalization.lean`][tc-affine] (`IsCompact.exists_affineBasis_abs_coord_le_one`) and [`MoorePenrose.lean`][tc-mp] (`LinearMap.moorePenroseInverse`, `LinearMap.IsMoorePenroseInverse`, `LinearEquiv.moorePenroseInverse_eq_symm`) | | Designs | Mathlib `Convexity.StdSimplex` (finitely supported probability weights; `StdSimplex.map`, `StdSimplex.range_toFun_comp_weights`) | -| LMLExplore material that the general forms below extend | exponential families (`Probability/Distributions/ExponentialFamily/`: `Measure.expFamily`, `expFamilyMeans`, `natParam`, `expFamilyDiv`), MGF domination (`MGFDominatedAbove`, `MGFDominatedBelow`, `mgfDominatedAbove_bernoulliMeasure`, `mgfDominatedBelow_bernoulliMeasure`), the Bandits algorithms `ucbF`, `klucb`, `gaussianTS`, `exp3`, `exp3IX`, `exp4` and the lower-bound files, follow-the-perturbed-leader policies (`perturbedLeaderAlgorithm`, `PerturbedLeader.lintegral_pullCount_le`), the FTRL lemma `sum_apply_sub_le_ftrl` (time-varying regularizers), `ConvexOn.exists_mem_segment_apply_sub_sub_bregDiv_div_le` (second-order Bregman bound), `softmax_regret_le`, `IsUnbiasedRound`, `designOp`, `ridgeEstimate` | +| LMLExplore material that the general forms below extend | exponential families (`Probability/Distributions/ExponentialFamily/`: `Measure.expFamily`, `expFamilyMeans`, `natParam`, `expFamilyDiv`), MGF domination (`MGFDominatedOn`, `mgfDominatedOn_Ici_bernoulliMeasure`, `mgfDominatedOn_Iic_bernoulliMeasure`), the Bandits algorithms `ucbF`, `klucb`, `gaussianTS`, `exp3`, `exp3IX`, `exp4` and the lower-bound files, follow-the-perturbed-leader policies (`perturbedLeaderAlgorithm`, `PerturbedLeader.lintegral_pullCount_le`), the FTRL lemma `sum_apply_sub_le_ftrl` (time-varying regularizers), `ConvexOn.exists_mem_segment_apply_sub_sub_bregDiv_div_le` (second-order Bregman bound), `softmax_regret_le`, `IsUnbiasedRound`, `designOp`, `ridgeEstimate` | The [Kiefer–Wolfowitz formalization in `colt-2026-83`][kw] (Apache-2.0, no `sorry`) proves the existence of G-optimal designs for compact spanning subsets of `EuclideanSpace ℝ ι` @@ -263,8 +263,8 @@ against an environment with a single arm is $0$. supermartingale $\exp(\lambda S_t-\psi(\lambda)N_t)$ of a sum sampled along a predictable sequence, and Ville's inequality, as in the proof of [GC11, Theorem 10]) is that roadmap's Layer 4.2. Prove here the bounded instance: a random variable with values in $[0,1]$ whose - conditional mean given a σ-algebra is at most (at least) $m$ is conditionally dominated above - (below) by $\mathcal B(m)$ [GC11, Lemma 9; LS, Note 10.3.1], and the rate function of + conditional mean given a σ-algebra is at most (at least) $m$ is conditionally dominated by + $\mathcal B(m)$ on $[0,\infty)$ (on $(-\infty,0]$) [GC11, Lemma 9; LS, Note 10.3.1], and the rate function of $\mathcal B(m)$ at a level $p\in[0,1]$ is `klBer p m`. Deduce for i.i.d. $X_i\in[0,1]$ with mean $\mu$ [LS, Lemma 10.3]: $P(\hat\mu_n\ge\mu+\varepsilon)\le\exp(-n\,d(\mu+\varepsilon,\mu))$ for $\varepsilon\in[0,1-\mu]$ and the lower tail, the boundary levels $0$ and $1$ included, and @@ -320,10 +320,10 @@ $\eta_\rho(q)=$ `ρ.natParam id q`), the divergence $d_\rho(x,q)=$ `ρ.expFamily $M_\rho\times M_\rho$, and its extension $\bar d_\rho(x,q)\in[0,\infty]$ to every level $x\in\mathbb R$, the Cramér–Chernoff rate function of $\rho_{(q)}$ at $x$. Each arm $a$ has its own family $\rho_a$. Arm $a$ is *dominated by its family* if its mean $\mu_a$ lies in -$M_{\rho_a}$ and its law $\nu_a$ is MGF-dominated above and below by $\rho_{a,(\mu_a)}$ -(LMLExplore's `MGFDominatedAbove`, `MGFDominatedBelow`). Laws on $[0,1]$ with mean in $(0,1)$ are -dominated by the Bernoulli family (`mgfDominatedAbove_bernoulliMeasure`, -`mgfDominatedBelow_bernoulliMeasure`), σ²-sub-Gaussian laws by the Gaussian family of variance +$M_{\rho_a}$ and its law $\nu_a$ is MGF-dominated by $\rho_{a,(\mu_a)}$ on $\mathbb R$ +(LMLExplore's `MGFDominatedOn` with `Set.univ`). Laws on $[0,1]$ with mean in $(0,1)$ are +dominated by the Bernoulli family (`mgfDominatedOn_Ici_bernoulliMeasure`, +`mgfDominatedOn_Iic_bernoulliMeasure`), σ²-sub-Gaussian laws by the Gaussian family of variance $\sigma^2$ (Identification roadmap, Layer 4.2), and the members of a family by the family itself. 1. **Upper confidence levels.** For a family $\rho$, $x\in\mathbb R$ and $c\in[0,\infty]$, define diff --git a/LMLRoadmaps/Identification/README.md b/LMLRoadmaps/Identification/README.md index bd29691..b0db7bc 100644 --- a/LMLRoadmaps/Identification/README.md +++ b/LMLRoadmaps/Identification/README.md @@ -64,7 +64,7 @@ generating functions with its exponential supermartingales (Layer 4.2). | Conditional means of the feedback and their martingale | LML `SequentialLearning/Means.lean` (`Environment.means`, `IsAlgEnvSeq.condExp_feedback`), `FeedbackMartingale.lean` (`noiseSum`, `IsAlgEnvSeq.martingale_noiseSum`) | | KL divergence of histories at a fixed horizon | LML `SequentialLearning/DivergenceDecomposition.lean` (`IsAlgEnvSeq.klDiv_map_history_stepKernel`, for any two algorithm-environment pairs); LMLExplore `Learning.IsAlgEnvSeq.klDiv_map_history_eq_sum_pullCount`, `Learning.klDiv_stoppedHistMeasure_le` | | Binary relative entropy, Bretagnolle–Huber, Ville's inequality, mixtures of supermartingales, time-uniform sub-Gaussian bounds, Chernoff bounds in relative-entropy form | LMLExplore (Bandits roadmap, Layers 0.2, 1 and 4): `klBer`, `klBerReal`, `exp_neg_klDiv_div_two_le`, `MeasureTheory.Supermartingale.measure_exists_le_le`, `supermartingale_integral_of_integrable`, `supermartingale_exp_sum_mul_of_hasCondSubgaussianMGF`, `measureReal_sum_ge_le_exp_klBerReal` | -| Sub-Gaussian and sub-exponential random variables, unconditional and conditional | Mathlib `Probability/Moments/SubGaussian.lean` (`HasSubgaussianMGF`, `Kernel.HasSubgaussianMGF`, `HasCondSubgaussianMGF`), LML `ForMathlib/Probability/Moments/SubExponential.lean` (`HasSubexponentialMGF`, `HasCondSubexponentialMGF`); LMLExplore `Probability/Moments/MGFDominated.lean` (`MGFDominatedAbove`, `MGFDominatedBelow`) | +| Sub-Gaussian and sub-exponential random variables, unconditional and conditional | Mathlib `Probability/Moments/SubGaussian.lean` (`HasSubgaussianMGF`, `Kernel.HasSubgaussianMGF`, `HasCondSubgaussianMGF`), LML `ForMathlib/Probability/Moments/SubExponential.lean` (`HasSubexponentialMGF`, `HasCondSubexponentialMGF`); LMLExplore `Probability/Moments/MGF/Dominated.lean` (`MGFDominatedOn`) | | Design operators, self-normalized bounds, G-optimal designs | Bandits roadmap, Layer 8 (`designOp`, the design operator $V(\pi)$ of a design, the self-normalized bound, the Kiefer–Wolfowitz theorem); Tau Ceti `Analysis/InnerProductSpace/Frame.lean` (`frameOperator`) | | Exponential weights, regret of online linear optimization | Bandits roadmap, Layer 6 | | KL divergence, chain rule, data processing, exponential tilting, cumulant generating functions | Mathlib `InformationTheory/KullbackLeibler/`, `MeasureTheory/Measure/Tilted.lean`, `MeasureTheory/Measure/LogLikelihoodRatio.lean`, `Probability/Moments/` (`cgf`, `integrableExpSet`, `deriv_cgf`, `iteratedDeriv_two_cgf`) | @@ -363,16 +363,16 @@ forms above, and that development may be adapted to them. Layer 1.4). Prove that $\bar d$ is continuous on (closure of the means)$\times$(means) as an `ℝ≥0∞`-valued function. - Prove the Cramér–Chernoff bound with the rate function: for independent real random variables - $X_i$, $i\in s$, each dominated above by a real random variable $X$ (LMLExplore's - `MGFDominatedAbove`, the Refactors roadmap's Layer 0.3 form), every $x\ge\mathbb E[X]$ and - every real $r\le I_X(x)$, $P\big(\sum_{i\in s}X_i\ge\#s\,x\big)\le\exp(-\#s\,r)$; and the lower - tail for variables dominated below and $x\le\mathbb E[X]$. For $X$ the statistic under the + $X_i$, $i\in s$, each dominated on $[0,\infty)$ by a real random variable $X$ (LMLExplore's + `MGFDominatedOn X_i P X Q (Set.Ici 0)`), every $x\ge\mathbb E[X]$ and every real + $r\le I_X(x)$, $P\big(\sum_{i\in s}X_i\ge\#s\,x\big)\le\exp(-\#s\,r)$; and the lower tail for + variables dominated on $(-\infty,0]$ and $x\le\mathbb E[X]$. For $X$ the statistic under the member of mean $\mu$, this is the bound $\exp(-\#s\,\bar d(x,\mu))$ at every level $x\ge\mu$, not only at the means; it contains LMLExplore's `iIndepFun.measureReal_sum_ge_le_exp_expFamilyDiv` and the Bandits roadmap's Layer 1.4 bound, boundary levels included. - Deduce the two-sided bound $P\big(\#s\,\bar d(\hat\mu_s,\mu)\ge z\big)\le2e^{-z}$ for every - $z\ge0$, for the empirical mean $\hat\mu_s$ of variables dominated above and below by the + $z\ge0$, for the empirical mean $\hat\mu_s$ of variables dominated on $\mathbb R$ by the member of mean $\mu$. - Prove the sub-Gaussian comparison: $d(\mu,\mu')\ge(\mu-\mu')^2/(2\sigma^2)$ when the family has variance at most $\sigma^2$ on the segment. @@ -695,14 +695,14 @@ alternatives, and Gaussian costs with arm-dependent variances in design-operator and LML's `HasCondSubexponentialMGF m hm X V b μ` the case $\psi(t)=Vt^2/2$ on $\{t:b|t|\le1\}$; - the unconditional version with $\psi$ the cumulant generating function of a real random - variable $Y$ on $[0,\infty)\cap$ `integrableExpSet Y Q` is LMLExplore's - `MGFDominatedAbove X P Y Q` (and on $(-\infty,0]$, `MGFDominatedBelow`); the Chernoff bounds - of Layer 1.2 hold under the conditional version along a filtration; + variable $Y$ on $\Lambda\cap$ `integrableExpSet Y Q` is LMLExplore's + `MGFDominatedOn X P Y Q Λ` (`mgfDominatedOn_iff_hasMGFBound`); the Chernoff bounds of + Layer 1.2 hold under the conditional version along a filtration; - $\psi$ the cumulant generating function of the statistic under a member of an exponential family on $[0,\infty)$ or $(-\infty,0]$ (the domination of $[0,1]$-valued variables by Bernoulli laws is the Bandits roadmap's Layer 1.4); - - if $X-\mu$ is conditionally σ²-sub-Gaussian, then $X$ is conditionally dominated above and - below by the member of mean $\mu$ of the Gaussian family of variance σ², so that the + - if $X-\mu$ is conditionally σ²-sub-Gaussian, then $X$ is conditionally dominated on + $\mathbb R$ by the member of mean $\mu$ of the Gaussian family of variance σ², so that the Gaussian-family inequalities below apply to σ²-sub-Gaussian rewards. - **Exponential supermartingales.** For a filtration $\mathcal F$, a process $(X_k)$ with $X_k$ $\mathcal F_{k+1}$-measurable and with moment generating function conditionally bounded by diff --git a/LMLRoadmaps/Identification/Suggested.lean b/LMLRoadmaps/Identification/Suggested.lean index ac045c1..edcb551 100644 --- a/LMLRoadmaps/Identification/Suggested.lean +++ b/LMLRoadmaps/Identification/Suggested.lean @@ -374,8 +374,8 @@ structure Kernel.HasCGFBound (X : Ω → ℝ) (ψ : ℝ → ℝ) (Λ : Set ℝ) mgf_le : ∀ᵐ ω' ∂ν, ∀ t ∈ Λ, mgf X (κ ω') t ≤ exp (ψ t) /-- The moment generating function of `X` under `P` is bounded by `exp ψ` on `Λ`. With `ψ` the -cumulant generating function of `Y` under `Q` on `[0, ∞) ∩ integrableExpSet Y Q`, this is -LMLExplore's `MGFDominatedAbove X P Y Q`. -/ +cumulant generating function of `Y` under `Q` on `Λ ∩ integrableExpSet Y Q`, this is +LMLExplore's `MGFDominatedOn X P Y Q Λ`. -/ structure HasCGFBound (X : Ω → ℝ) (ψ : ℝ → ℝ) (Λ : Set ℝ) (P : Measure Ω) : Prop where integrable_exp_mul : ∀ t ∈ Λ, Integrable (fun ω ↦ exp (t * X ω)) P mgf_le : ∀ t ∈ Λ, mgf X P t ≤ exp (ψ t) @@ -407,7 +407,7 @@ theorem supermartingale_exp_sum_of_hasCondCGFBound [StandardBorelSpace Ω] {P : sorry /-- **Cramér–Chernoff bound with the rate function** (README Layer 1.2), at every level above -the mean, for independent variables dominated above by `Y`. -/ +the mean, for independent variables dominated by `Y` on `[0, ∞)`. -/ theorem measureReal_sum_ge_le_exp_of_le_rateFunction {P : Measure Ω} [IsProbabilityMeasure P] {Q : Measure Ω'} [IsProbabilityMeasure Q] {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} (hY : Integrable Y Q) (h_indep : iIndepFun X P)