[RemyDegenne]

This pull request proves the almost sure form of the optimal growth rate against an i.i.d. null: for every sequence of n-sample e-variables for the null, and so for every e-process, limsup (1/n) log is almost surely at most the bipolar rate under the i.i.d. law of the alternative. It adds one new file, LMLExplore/EValues/BipolarRate/AlmostSure.lean (831 lines), and changes no existing file.

Main declarations

• ae_limsup_log_div_le_bipolarRate: for M : (n : ℕ) → (Fin n → 𝓧) → ℝ≥0∞ with every M n an e-variable for {P ^ n | P ∈ S₁}, ∀ᵐ ω ∂Measure.infinitePi (fun _ ↦ Q₁), limsup (fun n ↦ ENNReal.log (M n (initSeg n ω)) / n) atTop ≤ bipolarRate Q₁ S₁.
• ae_limsup_log_div_le_bipolarRate_of_dependsOn: the same bound for measurable F n : (ℕ → 𝓧) → ℝ≥0∞ that depend only on the first n coordinates and have ∫⁻ ω, F n ω ∂Measure.infinitePi (fun _ ↦ P) ≤ 1 for every P ∈ S₁. These hypotheses are those of eintegral_log_le_maxLogGrowth_of_dependsOn on main. The other two theorems follow from this one.
• IsEProcess.ae_limsup_log_div_le_bipolarRate: for an e-process E for Filtration.piLE and the i.i.d. null, limsup (fun n ↦ ENNReal.log (E n ω) / (n + 1)) atTop ≤ bipolarRate Q₁ S₁ almost surely. It is the almost sure counterpart of IsEProcess.limsup_eintegral_log_div_le_bipolarRate (feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3] #413), and divides by the number n + 1 of observations seen, as feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3] #413 does.

The only hypothesis on the null is that its members are probability measures. Nothing is assumed on Q₁: if it is not a probability measure, Measure.infinitePi (fun _ ↦ Q₁) = 0 and the statements hold trivially.

Roadmap coverage (EValues, Layer 6, item 1)

Covered: the first half of the bullet "Almost surely under Q, every sequence of n-sample e-variables M n for the i.i.d. null, evaluated at the first n observations, in particular every e-process for the null, has limsup (1/n) log (M n) ≤ d", with no assumption on S₁ or Q₁.

Not covered: the second half of the same bullet ("and the numeraires attain the rate: (1/n) log of Statlib's numeraire ... tends to d almost surely, also when d = ∞"). It belongs to another item of the paper project and is not part of this pull request. The bound by KL_inf(Q₁, S₁) that the bullet mentions [WSJ26, Proposition 2.2] is the composition with bipolarRate_le_iInf_klDiv, which is already on main, so it gets no theorem of its own. The rest of item 1 is untouched.

The roadmap cites this bound as [EVR26, Note 01], which has no published source. The proof here is the Lean proof from the paper project, rewritten on main's API.

Notes for reviewers

• Proof route. The roadmap's sketch compares each G n with the numeraire X* n by Markov's inequality and the Borel–Cantelli lemma. That reduces the bound to the almost sure upper bound limsup (1/n) log X* n ≤ d for the numeraires themselves, and that bound needs the same covering argument used here, plus an ergodic theorem. This pull request applies the covering argument directly to the given sequence and never uses numeraires, which is the shorter route with what main has. It has two steps, both in the module docstring:

  • Covering. Suppose G n ≥ exp (n L) holds infinitely often almost surely, where each G n is a function of the first n observations with null expectation at most one. Then L ≤ d. The covering mixture of N observations bets half on skipping one observation and half on a block of k observations (weight 1 / (k (k + 1)), bet G k), then recurses on the rest. It is again such a function, so its expected logarithm is at most maxLogGrowth Q₁ S₁ N ≤ N d. A greedy parse bounds its logarithm from below pointwise. The classical argument would use the ergodic theorem and Fatou's lemma here. Instead, the number of "bad" positions is bounded in expectation: by stationarity, its mean is N times the probability of the bad event.
  • Zero-one law. Suppose M n ≥ exp (n L) infinitely often with positive probability. The mixture over shifts ∑ s < n, 2⁻¹ ^ (s + 1) M (n - s) ∘ shift^[s] then exceeds exp (n L') infinitely often on an event that contains its own preimage under the shift. Since the Bernoulli shift is ergodic, that event has probability one.

• Reuse.

  • Tau Ceti: the path shift TauCeti.Probability.shift and its iterates, which LMLExplore's Markov chain files already use, and MeasureTheory.Measure.ergodic_shift_infinitePi_const (TauCeti.Probability.Ergodic.BernoulliShift, imported by LMLExplore for the first time).
  • Mathlib: Ergodic.ae_empty_or_univ_of_preimage_ae_le for the zero-one law.
  • LMLExplore main: initSeg, exists_measurable_eq_comp_initSeg, measurePreserving_initSeg, dependsOn_comp_initSeg, eintegral_log_le_maxLogGrowth_of_dependsOn and maxLogGrowth_le_mul_bipolarRate. Neither maxLogGrowth nor bipolarRate is unfolded.

• Private helpers. All other declarations (30) are private, and none is API:

  • the measure preservation of the shift iterates;
  • lintegral_mul_comp_shift_iterate: under an i.i.d. law, a function of the first t observations is independent of a function of the observations after them;
  • the covering mixture, the good event, the count of bad positions and the mixture over shifts.

  The other half of the same paper item (the Wald inequality at stopping times and the lower bound on the expected number of observations) is being ported at the same time in a separate pull request, which needs the same independence fact. Here it stays private, so the two pull requests share no public name and do not depend on each other. Whichever lands second can move one copy to LMLExplore/Probability/ProductMeasure.lean and delete the other.

• Order of quantifiers. The theorems fix the sequence first and then hold almost surely, which is how the roadmap's "almost surely, every sequence" has to be read: the exceptional null event depends on the sequence. This is also the order of the expectation bound in feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3] #413.

• Dropped hypothesis. [IsProbabilityMeasure Q₁] is not assumed, as explained above. The e-process statement uses IsEProcess because the roadmap names e-processes. Its proof uses only adaptedness and the e-variable property at fixed times, and the _of_dependsOn form states exactly those hypotheses.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R10

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM