[RemyDegenne]

This PR proves the large deviation principle for the empirical means of a run whose numbers of pulls stay within k of T w almost surely, and derives from it the error exponent of the static proportions families of fixed-budget identification. It is the Identification roadmap's Layer 8.3 (Large deviations under static allocations), second bullet: "Deduce that the static-proportions algorithm recommending i*(μ̂), for a task asking about the means (Layer 1.1), has error exponent the infimum of ∑_a w_a I_a(x_a) over the vectors of means x for which i*(μ) is not correct [GJ04]". The first bullet (the product principle hasLDP_pi_cramer, #369) handles fixed numbers of samples. Here the numbers of pulls are random and may depend on the rewards, so the law of μ̂_T is not a product, and the first bullet's principle has to be carried over to runs.

Roadmap: Identification
Paper: RemyDegenne/Degenne2023Existence
Item: R12

New file LMLExplore/SequentialLearning/StaticAllocation.lean (namespace LMLExplore):

• hasLDP_empMean_of_abs_pullCount_sub_le: the main theorem [GJ04; D23, Theorem 12]. Take families of runs IsAlgEnvSeq (O T) (A T) (R T) (alg T) (Environment.bandit ν) (P T) with |N_{T,a} - T w a| ≤ k almost surely, and per-arm empirical-mean laws that satisfy LDPs with good rate functions I a. Then the laws of μ̂_T satisfy HasLDP with speed 1 / T and rate function x ↦ ∑ a, w a I a (x a). hasLDP_empMean_rateFunction_of_abs_pullCount_sub_le is the Cramér instance, for arms whose cgf is finite near 0.
• measure_empMean_mem_le_streamMeasure and streamMeasure_le_measure_empMean_mem transfer events about μ̂_T between the run and LML's reward stream, in both directions, when the pull counts lie a.s. in a set S. The upper direction comes from measure_exists_pullCount_armObs_pi_le and needs no measurability. The lower direction goes through the rewards by count (hasLaw_rewardByCount_streamMeasure).
• eventually_streamMeasure_mean_mem_le_exp and exists_eventually_le_streamMeasure_forall_mean_mem give exponential upper and lower bounds for the stream means, uniformly over a window of sample counts. The upper bound picks a violating count vector for each T and applies hasLDP_pi_comp_of_tendsto_div to that sequence. The lower bound asks the first ⌈T w a - k⌉₊ entries of each row to have a mean near the target and the next 2k entries to lie in a fixed ball, and uses the product lower bound at a box.
• Measure.infinitePi_mean_mem_and_forall_mem: for an i.i.d. sequence, the mean of the first n terms and the next m terms are independent.

Additions to existing files:

• SequentialLearning/SumRewards.lean: streamMeasure_map_mean (the law of the vector of stream means is Measure.pi of the per-arm laws) and streamMeasure_forall_row_mem (events about different rows of the stream are independent), next to their siblings. streamMeasure_forall_mean_mem is now re-proved as the box case of streamMeasure_map_mean, with its statement unchanged.
• Probability/LargeDeviations/Pi.lean: neg_sum_le_liminf_log_pi was private and is now public. It is the product lower bound, which needs no goodness, and the window lower bound uses it.
• Identification/StaticProportions.lean: IsStaticProportions.hasLDP_empMean, then IsStaticProportions.limsup_log_errorProb_div_le and IsStaticProportions.neg_le_liminf_log_errorProb_div. These bound (1/T) log p_{θ,T} between -inf of ∑ w_a I_a over the closure and over the interior of {x | rec x ∉ correct θ}. When the two infima agree, IsStaticProportions.tendsto_log_errorProb_div gives the exact exponent and IsStaticProportions.tendsto_errorComplexity the limit of the error complexity. The rule rec is arbitrary (not necessarily measurable), and the model needs only a measurable set of correct answers.

No public declaration is removed or renamed; neg_sum_le_liminf_log_pi is the only visibility change.

The statements and proofs are adapted from the formalization of [D23] in the paper project RemyDegenne/Degenne2023Existence (same author; credited in the module docstring). That formalization works in LML's array model for trajectory measures. Here the results hold for every algorithm-environment sequence against the bandit, the transfer goes through the rewards by count, and the fixed-count bounds come from LMLExplore's product principle rather than a separate compact-cover argument.

What remains of Layer 8.3 bullet 2 after this PR is its exponential-family form [D23, Theorems 1, 12]. Under the regularity of the task, the closure and interior infima coincide and equal inf_{λ ∈ ¬i*(μ)} ∑_a w_a d(λ_a, μ_a) (alternative first), which is what staticDifficulty uses. Bullet 3 (two arms, [KCG16, Theorems 12–13]) is separate.

Local checks (tauceti-local-checks verify --policy ordinary) passed: scope: scoped: against a4fdeb88b5aeb10c0dca836626263ee24dc2ee9c; local-axioms: checked 4 changed module(s), 124 declaration(s); 0 violation(s); whole-library lake build --iofail green, module-system, header-style and changed-module environment lint passed. These are local checks; CI verifies the pushed PR.

🤖 Prepared with Claude Code

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The run-level LDP under a.s. bounded deviation of pull counts from T w, the closure/interior error-exponent bounds, and the exact-exponent and error-complexity corollaries faithfully state [GJ04; D23, Theorem 12], with the window hypothesis discharged by the existing IsStaticProportions.ae_abs_pullCount_sub_le field (k = card α). Helper lemmas (window bounds, transfers, i.i.d. split, stream product formulas) have correct quantifiers and non-vacuous hypotheses, and errorProb_eq correctly links the error event to the empirical-means set for arbitrary rec.
✅	reuse	approved	claude/claude-opus-5-5	The new declarations (window LDP bounds, run-to-stream transfers, stream row/mean product formulas, the infinite-product split, the bounded-distance limit lemma) have no located counterparts in Mathlib or LMLExplore, and the proofs reuse the existing LDP helpers, hasLDP_pi_comp_of_tendsto_div, the stream-model law lemmas and Mathlib's infinitePi/independence API. streamMeasure_forall_mean_mem is now derived from streamMeasure_map_mean rather than duplicating it.
✅	scope	approved	claude/claude-opus-5-5	The PR proves the error exponent of static-proportions families and the large deviation principle it rests on, which is Identification Layer 8.3 bullet 2 (roadmap README.md:966-971), so the target itself advances. The new helpers (the ratio limit, the i.i.d. split, the stream row independence and mean law, and the transfer and window bounds) and the one visibility change are all used on that path, so the PR is a single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	StaticAllocation.lean and the StaticProportions.lean additions credit [GJ04], [D23, Theorem 12], [LS, §4.6] and the adapted RemyDegenne/Degenne2023Existence formalization; the roadmap is credited only in the PR description. The new helpers (ratio limit, i.i.d. block independence) are routine and follow no identifiable source.
✅	api-design	approved	claude/claude-opus-5-5	The new public surface is the Layer 8.3 bullet-2 results plus general helpers placed in their natural files (Analysis/SpecificLimits/Basic, Probability/ProductMeasure, SequentialLearning/SumRewards), and making neg_sum_le_liminf_log_pi public is justified by its new consumer. The private lemmas serve only the window argument, and the PR adds no definitions, exposed bodies or compatibility artifacts.
✅	generality	approved	claude/claude-opus-5-5	The run LDP is proved for arbitrary good rate functions, with the Cramér and static-proportions results derived from it, and goodness is assumed only where hasLDP_pi_comp_of_tendsto_div and isGoodRateFunction_sum_mul need it. streamMeasure_forall_mean_mem is now a corollary of streamMeasure_map_mean, so no special case duplicates a proof.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration lives in the file matching its topic and dependencies (ratio limit in Analysis/SpecificLimits/Basic, infinitePi split in Probability/ProductMeasure, stream lemmas in SumRewards, run LDP in SequentialLearning/StaticAllocation, error exponent in Identification/StaticProportions). New imports are all used and none is overly broad.
✅	naming	approved	claude/claude-opus-5-5	The earlier finding is fixed: the row-independence lemma is now streamMeasure_forall_arm_mem, matching its arm siblings in SumRewards.lean. All new public names describe their conclusions in standard terms, sit in the right namespaces (Measure.infinitePi_fin_mem_and_forall_add_mem under MeasureTheory.Measure), and the PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	Every new file has an accurate module docstring and every new public declaration is documented consistently with its statement, with valid cross-references. No overclaiming or process narrative in file docstrings.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are well-structured: window arithmetic is factored into private lemmas, and the long lower-bound and LDP proofs are commented stage by stage. The single rfl in infinitePi_fin_mem_and_forall_add_mem is a documented Subtype.val-of-constructor step; no undocumented defeq, change/show, or brittle rewrite chains remain.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head e8f17ce. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $4.60.}

[RemyDegenne]

🟡 placement — request_changes claude/claude-opus-5-5

The new Measure.infinitePi lemma is in the finite-product file MeasureTheory/Constructions/Pi.lean, which now publicly imports Mathlib.Probability.Independence.InfinitePi and passes it on to everything that imports the file. All other new material and imports are where they belong.

• LMLExplore/MeasureTheory/Constructions/Pi.lean:109 — infinitePi_fin_mem_and_forall_add_mem concerns Measure.infinitePi and needs independence, but it lives in the finite Measure.pi file. That forces a new public import Mathlib.Probability.Independence.InfinitePi (line 10) on the file and on every file that imports it. Fix: Move the lemma to a new LMLExplore/Probability/ProductMeasure.lean, mirroring Mathlib's infinitePi home. Import that file from StaticAllocation.lean, drop the Independence.InfinitePi import and the infinitePi docstring lines from Constructions/Pi.lean, and remove the old declaration there.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 40s · 241.9k in (227k cache read, 14.9k cache write) / 3.5k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}