[RemyDegenne]

This pull request proves a composite strong law of large numbers in stopping-time form. Take a set of integrable laws on ℝ whose centred first absolute moments are at most one constant c. For every α > 0, some stopping time of Filtration.piLE is finite on every sequence whose sample means do not converge, and finite with probability at most α under i.i.d. sampling from each law. On the way it proves Doob's upcrossing inequality with the initial term, and a maximal inequality and an upcrossing inequality for the sample means of an exchangeable sequence. It adds three new files and changes no existing file:

• LMLExplore/Probability/Martingale/Upcrossing.lean (85 lines)
• LMLExplore/Probability/Martingale/SampleMean.lean (285 lines)
• LMLExplore/EValues/CompositeStrongLaw.lean (258 lines)

Main declarations

• ProbabilityTheory.exists_isStoppingTime_lt_top_of_not_tendsto_mean, the composite strong law. It takes S : Set (Measure ℝ) with ∀ P ∈ S, Integrable id P and ∀ P ∈ S, ∫ x, |x - ∫ y, y ∂P| ∂P ≤ c, and a level 0 < α. It gives τ : (ℕ → ℝ) → WithTop ℕ such that:
  • IsStoppingTime (Filtration.piLE (X := fun _ : ℕ ↦ ℝ)) τ;
  • Measure.infinitePi (fun _ ↦ P) {ω | τ ω < ⊤} ≤ α for every P ∈ S;
  • τ ω < ⊤ for every ω such that (∑ i ∈ Finset.range n, ω i) / n has no limit in ℝ.
• ProbabilityTheory.mul_measure_exists_le_abs_sum_div_sub_le, the maximal inequality for sample means. Let μ be a finite exchangeable law on ℕ → ℝ (Tau Ceti's ExchangeableLaw) whose first coordinate is integrable. Then for every m : ℝ and L : ℝ≥0, L * μ {ω | ∃ n, L ≤ |(∑ i ∈ range (n + 1), ω i) / (n + 1) - m|} ≤ ENNReal.ofReal (∫ ω, |ω 0 - m| ∂μ).
• ProbabilityTheory.mul_lintegral_upcrossings_sum_div_le, the upcrossing inequality for sample means. Let μ be an exchangeable probability measure whose first coordinate is integrable, with mean m = ∫ ω, ω 0 ∂μ. Then ENNReal.ofReal (b - a) * ∫⁻ ω, upcrossings a b (sample means) ω ∂μ ≤ ENNReal.ofReal (∫ ω, |ω 0 - m| ∂μ). This holds for all a, b, and the bound does not depend on where [a, b] lies relative to m.
• MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_posPart_sub: (b - a) * 𝔼[upcrossingsBefore a b f N] ≤ 𝔼[(f N - a)⁺] - 𝔼[(f 0 - a)⁺], for every submartingale f and all a, b. Mathlib's Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part drops the last term.
• MeasureTheory.StronglyAdapted.adapted_upcrossingsBefore: the upcrossing counts of an adapted process are adapted. Mathlib's StronglyAdapted.measurable_upcrossingsBefore gives measurability only for the ambient σ-algebra.

Roadmap coverage (EValues, Layer 3, item 5)

Covered: the bullet "Instance, a composite strong law", in the stopping-time form that the bullet gives. The null is the set of i.i.d. laws Measure.infinitePi fun _ ↦ P, where P ranges over integrable laws with ∫ |x - ∫ y dP(y)| dP(x) ≤ c. The set A is the set of sequences whose sample means do not converge in ℝ. The theorem gives, for every α > 0, a stopping time of Filtration.piLE that is finite on A and finite with probability at most α under every member of the null.

Left: the statement ν A = 0. LMLExplore does not have the inverse capital outer measure ν of this item yet, so that statement waits for its definition. It follows from this theorem by the definition of ν. The rest of item 5 is not touched: ν and its outer-measure properties, [RLKR23, Theorems 3.1 and 3.7], and the truncated-Cauchy example.

Notes for reviewers

• How the proof goes.
  • Fix a horizon N. Under an exchangeable law, k ↦ X̄_{N - k} is a martingale for the σ-algebras of the events that are symmetric in the first N - k + 1 coordinates. Here X̄ₙ = (X₀ + ⋯ + Xₙ) / (n + 1) is the sample mean.
  • The maximal inequality is Doob's inequality for the submartingale |X̄_{N - k} - m|.
  • The upcrossing inequality starts from Tau Ceti's upcrossingsBefore_le_upcrossingsBefore_neg_revProcess_succ. It bounds the upcrossings of [a, b] by X̄ by the upcrossings of [-b, -a] by the negated reversed means.
  • The sharp Doob inequality bounds the mean of the latter by 𝔼(b - X₀)⁺ - 𝔼(b - X̄_N)⁺ ≤ 𝔼(b - X₀)⁺ - (b - m)⁺ ≤ 𝔼|X₀ - m|. Mathlib's form of Doob's inequality gives 𝔼(b - X₀)⁺, which grows with b - m, so it would not give a bound uniform over the null.
  • The stopping time is the first n at which, for some rational pair a < b, the means X̄₀, …, X̄ₙ have completed K (a, b) upcrossings of [a, b], or at which |X̄ₙ - X₀| ≥ 2L.
  • The thresholds K (a, b) come from summable positive weights on ℚ × ℚ (ENNReal.exists_pos_sum_of_countable).
  • A sequence on which the stopping time is infinite has convergent sample means, by Mathlib's tendsto_of_upcrossings_lt_top.
• Reuse. The reverse filtration is Tau Ceti's MeasureTheory.revFiltration, and the time reversal is Tau Ceti's revProcess, upcrossingsBefore_le_upcrossingsBefore_neg_revProcess_succ and upcrossingsBefore_succ_congr. The maximal inequality comes from Tau Ceti's Martingale.submartingale_norm and Submartingale.mul_measure_exists_mem_le_le. Exchangeability comes from Tau Ceti's ExchangeableLaw, ExchangeableLaw.measurePreserving_permReindex and exchangeableLaw_infinitePi_const. Integrals and measurability under products come from Statlib's integral_comp_eval_infinitePi and Filtration.measurable_piLE_apply. The symmetric σ-algebras and the sample means are private helpers.
• No published source. The roadmap cites the theorem to its own source, with no published proof, and states it in full. The two sample-mean inequalities are the classical reverse-martingale inequalities, stated here at the generality the proof gives.
• Deviations from the roadmap's wording.
  • The statement is in the stopping-time form, not ν A = 0; see above.
  • The null is given by its marginals S : Set (Measure ℝ), and the members are not assumed to be probability measures. The hypothesis ∀ P ∈ S, IsProbabilityMeasure P of the Conventions is dropped because the proof does not use it: for a P that is not a probability measure, Measure.infinitePi fun _ ↦ P is zero.
  • The roadmap's assumption mΩ = ⨆ n, ℱ n for item 5 is not needed for this statement.
• Generality of the auxiliary inequalities. The two sample-mean inequalities are stated for exchangeable laws on ℕ → ℝ, since the proof only uses the invariance of the law under swaps of coordinates. They are not restricted to i.i.d. laws. The maximal inequality holds for every centre m, not only the mean, and for finite measures.
• Overlaps with open pull requests. None. feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3] #413 adds lemmas on functions of the first n observations of an i.i.d. sequence, but this proof does not need them. No public name is shared with an open pull request.
• Placement. The two general results go next to the martingale material in Probability/Martingale/: the upcrossing inequality in Upcrossing.lean, the sample-mean inequalities in SampleMean.lean. Only the composite strong law is in EValues/.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R19

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM