feat: admissible e-processes, and the admissibility of the sub-Gaussian exponential e-process for nonatomic i.i.d. laws

LMLExplore/Analysis/Calculus/MeanValue.lean

@@ -6,20 +6,25 @@ Authors: LMLExplore contributors
 module
 
 public import Mathlib.Analysis.Calculus.Deriv.MeanValue
+import Mathlib.Analysis.Calculus.Deriv.Pow
 
 /-!
 # Comparing values of a function through the sign of its derivative
 
 Mathlib's `monotoneOn_of_hasDerivWithinAt_nonneg` and `antitoneOn_of_hasDerivWithinAt_nonpos`
 turn the sign of a derivative on an interval into monotonicity. This file packages the two-sided
 form used to prove that a point is a maximum: if the derivative of `f` is nonnegative to the left
-of `x₀` and nonpositive to its right, then `f x ≤ f x₀` for every `x`.
+of `x₀` and nonpositive to its right, then `f x ≤ f x₀` for every `x`. It also gives the
+second-order lower bound that a lower bound on the second derivative gives on a convex set.
 
 ## Main statements
 
 * `LMLExplore.apply_le_apply_of_hasDerivAt_of_nonneg_of_nonpos`: if `f` is continuous on the
   segment between `x` and `x₀` and has derivative `f' y` at each `y` strictly between them, with
   `f' ≥ 0` on `(x, x₀)` and `f' ≤ 0` on `(x₀, x)`, then `f x ≤ f x₀`.
+* `LMLExplore.add_mul_add_mul_sq_le_of_le_deriv2`: if `c ≤ f''` on a convex set `I` containing
+  `a`, then `f` lies above its second-order polynomial `f a + f' a (x - a) + c / 2 (x - a) ^ 2`
+  on `I`.
 -/
 
 public section
@@ -50,4 +55,48 @@ theorem apply_le_apply_of_hasDerivAt_of_nonneg_of_nonpos {f f' : ℝ → ℝ} {x
     rw [interior_Icc]
     exact hpos
 
+/-- **Second-order lower bound.** If `c ≤ f''` on a convex set `I` containing `a`, then
+`f a + f' a * (x - a) + c / 2 * (x - a) ^ 2 ≤ f x` on `I`. -/
+theorem add_mul_add_mul_sq_le_of_le_deriv2 {f f' f'' : ℝ → ℝ} {I : Set ℝ} (hI : Convex ℝ I)
+    {a c : ℝ} (ha : a ∈ I) (hf : ∀ x, HasDerivAt f (f' x) x)
+    (hf' : ∀ x, HasDerivAt f' (f'' x) x) (hc : ∀ x ∈ I, c ≤ f'' x) {x : ℝ} (hx : x ∈ I) :
+    f a + f' a * (x - a) + c / 2 * (x - a) ^ 2 ≤ f x := by
+  set g := fun y ↦ f y - (f a + f' a * (y - a) + c / 2 * (y - a) ^ 2) with hg_def
+  set g' := fun y ↦ f' y - (f' a + c * (y - a)) with hg'_def
+  have h1 (y : ℝ) : HasDerivAt (fun y ↦ f a + f' a * (y - a) + c / 2 * (y - a) ^ 2)
+      (f' a + c * (y - a)) y := by
+    have h := (hasDerivAt_id y).sub_const a
+    exact (((h.const_mul (f' a)).const_add (f a)).add ((h.pow 2).const_mul (c / 2))).congr_deriv
+      (by simp only [id, Nat.cast_ofNat]; ring)
+  have hg (y : ℝ) : HasDerivAt g (g' y) y := (hf y).sub (h1 y)
+  have hg' (y : ℝ) : HasDerivAt g' (f'' y - c) y :=
+    (hf' y).sub (((((hasDerivAt_id y).sub_const a).const_mul c).const_add (f' a)).congr_deriv
+      (by simp))
+  have hmono : MonotoneOn g' I :=
+    monotoneOn_of_hasDerivWithinAt_nonneg hI
+      (fun y _ ↦ (hg' y).continuousAt.continuousWithinAt) (fun y _ ↦ (hg' y).hasDerivWithinAt)
+      fun y hy ↦ sub_nonneg.2 (hc y (interior_subset hy))
+  have hga : g a = 0 := by simp [g]
+  have hg'a : g' a = 0 := by simp [g']
+  suffices 0 ≤ g x by simp only [g] at this; linarith
+  rcases le_total a x with hax | hxa
+  · have h : MonotoneOn g (I ∩ Set.Ici a) :=
+      monotoneOn_of_hasDerivWithinAt_nonneg (hI.inter (convex_Ici a))
+        (fun y _ ↦ (hg y).continuousAt.continuousWithinAt) (fun y _ ↦ (hg y).hasDerivWithinAt)
+        fun y hy ↦ by
+          have hy' := interior_subset hy
+          rw [← hg'a]
+          exact hmono ha hy'.1 hy'.2
+    rw [← hga]
+    exact h ⟨ha, Set.mem_Ici.2 le_rfl⟩ ⟨hx, hax⟩ hax
+  · have h : AntitoneOn g (I ∩ Set.Iic a) :=
+      antitoneOn_of_hasDerivWithinAt_nonpos (hI.inter (convex_Iic a))
+        (fun y _ ↦ (hg y).continuousAt.continuousWithinAt) (fun y _ ↦ (hg y).hasDerivWithinAt)
+        fun y hy ↦ by
+          have hy' := interior_subset hy
+          rw [← hg'a]
+          exact hmono hy'.1 ha hy'.2
+    rw [← hga]
+    exact h ⟨hx, hxa⟩ ⟨ha, Set.mem_Iic.2 le_rfl⟩ hxa
+
 end LMLExplore

LMLExplore/EValues/BipolarRate/EProcess.lean

@@ -6,7 +6,7 @@ Authors: LMLExplore contributors
 module
 
 public import LMLExplore.EValues.BipolarRate.Basic
-public import LMLExplore.EValues.EProcess
+public import LMLExplore.EValues.EProcess.Basic
 public import LMLExplore.Probability.ProductMeasure
 
 /-!

LMLExplore/EValues/EProcess/Admissible.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import LMLExplore.EValues.EProcess.Basic
+
+/-!
+# Admissible e-processes
+
+An e-process `F` for a null `S` dominates an e-process `E` when `E n ≤ F n` almost surely under
+every member of `S`, at every time `n`, and dominates it strictly when moreover `E n < F n` with
+positive probability under some member of `S` at some time. An e-process is admissible when no
+e-process dominates it strictly [RRLK, §4.2]: every e-process that dominates it is equal to it at
+every time, almost surely under every member of the null. This is the sequential form of
+admissible e-variables (`ProbabilityTheory.IsAdmissibleEVar`).
+
+An e-process is admissible as soon as every event of time `n` charged by some member of the null
+is charged by a member under which `E n` has expectation one: under such a member, an e-process
+that dominates `E` has expectation at most that of `E n` at time `n`, so it is equal to `E n`
+almost surely there.
+
+## Main definitions
+
+* `ProbabilityTheory.IsAdmissibleEProcess E ℱ S`: `E` is an admissible e-process for the null `S`
+  and the filtration `ℱ`.
+
+## Main statements
+
+* `ProbabilityTheory.isAdmissibleEProcess_iff_measure_lt_eq_zero`: an e-process is admissible
+  exactly when no e-process dominates it strictly, the definition of [RRLK, §4.2].
+* `ProbabilityTheory.IsEProcess.isAdmissibleEProcess_of_exists_lintegral_eq`: an e-process such
+  that every event of time `n` charged by a member of the null is charged by a member under which
+  `E n` has expectation `P univ` is admissible.
+
+## References
+
+* [RRLK] A. Ramdas, J. Ruf, M. Larsson and W. M. Koolen, *Admissible anytime-valid sequential
+  inference must rely on nonnegative martingales*, arXiv:2009.03167v3: §4.2.
+-/
+
+public section
+
+open MeasureTheory Set
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {ℱ : Filtration ℕ mΩ} {S : Set (Measure Ω)}
+  {P : Measure Ω} {E F : ℕ → Ω → ℝ≥0∞}
+
+/-- An e-process `E` for the null `S` and the filtration `ℱ` is **admissible** when every
+e-process `F` that dominates it, `E n ≤ F n` almost surely under every member of `S` at every time
+`n`, is at most `E` at every time, almost surely under every member of `S`: no e-process dominates
+`E` strictly [RRLK, §4.2] (`isAdmissibleEProcess_iff_measure_lt_eq_zero`). -/
+structure IsAdmissibleEProcess (E : ℕ → Ω → ℝ≥0∞) (ℱ : Filtration ℕ mΩ) (S : Set (Measure Ω)) :
+    Prop extends IsEProcess E ℱ S where
+  ae_le_of_ae_le : ∀ F, IsEProcess F ℱ S → (∀ P ∈ S, ∀ n, E n ≤ᵐ[P] F n) →
+    ∀ P ∈ S, ∀ n, F n ≤ᵐ[P] E n
+
+namespace IsAdmissibleEProcess
+
+/-- An e-process that dominates an admissible e-process is at most it at every time, almost
+surely under every member of the null. -/
+theorem ae_le (hE : IsAdmissibleEProcess E ℱ S) (hF : IsEProcess F ℱ S)
+    (hEF : ∀ P ∈ S, ∀ n, E n ≤ᵐ[P] F n) (hP : P ∈ S) (n : ℕ) : F n ≤ᵐ[P] E n :=
+  hE.ae_le_of_ae_le F hF hEF P hP n
+
+/-- An e-process that dominates an admissible e-process is equal to it at every time, almost
+surely under every member of the null. -/
+theorem ae_eq (hE : IsAdmissibleEProcess E ℱ S) (hF : IsEProcess F ℱ S)
+    (hEF : ∀ P ∈ S, ∀ n, E n ≤ᵐ[P] F n) (hP : P ∈ S) (n : ℕ) : F n =ᵐ[P] E n :=
+  (hE.ae_le hF hEF hP n).antisymm (hEF P hP n)
+
+/-- An adapted process equal to an admissible e-process at every time, almost surely under every
+member of the null, is an admissible e-process. -/
+theorem congr (hE : IsAdmissibleEProcess E ℱ S) (hF : Adapted ℱ F)
+    (hEF : ∀ P ∈ S, ∀ n, E n =ᵐ[P] F n) : IsAdmissibleEProcess F ℱ S where
+  adapted := hF
+  isEVar_stoppedValue τ hτ := (hE.isEVar_stoppedValue τ hτ).congr
+    (hF.measurable_apply_stoppingTime hτ) fun P hP ↦ by
+      filter_upwards [ae_all_iff.2 (hEF P hP)] with ω hω using hω (τ ω)
+  ae_le_of_ae_le _ hG hFG P hP n :=
+    (hE.ae_le hG (fun P hP n ↦ (hEF P hP n).le.trans (hFG P hP n)) hP n).trans (hEF P hP n).le
+
+end IsAdmissibleEProcess
+
+/-- An e-process is admissible exactly when no e-process dominates it strictly: for every
+e-process `F` with `E n ≤ F n` almost surely under every member of the null at every time, the
+event `E n < F n` is null under every member of the null at every time [RRLK, §4.2]. -/
+theorem isAdmissibleEProcess_iff_measure_lt_eq_zero :
+    IsAdmissibleEProcess E ℱ S ↔ IsEProcess E ℱ S ∧ ∀ F, IsEProcess F ℱ S →
+      (∀ P ∈ S, ∀ n, E n ≤ᵐ[P] F n) → ∀ P ∈ S, ∀ n, P {ω | E n ω < F n ω} = 0 := by
+  have key (F : ℕ → Ω → ℝ≥0∞) (P : Measure Ω) (n : ℕ) :
+      F n ≤ᵐ[P] E n ↔ P {ω | E n ω < F n ω} = 0 := by
+    simp only [Filter.EventuallyLE, ae_iff, not_le]
+  exact ⟨fun h ↦ ⟨h.toIsEProcess, fun F hF hEF P hP n ↦ (key F P n).1 (h.ae_le hF hEF hP n)⟩,
+    fun h ↦ ⟨h.1, fun F hF hEF P hP n ↦ (key F P n).2 (h.2 F hF hEF P hP n)⟩⟩
+
+/-- **A sufficient condition for admissibility.** For a null of finite measures, an e-process `E`
+such that every `ℱ n`-measurable set charged by a member of the null is charged by a member `P`
+under which `E n` has expectation `P univ` is admissible. -/
+theorem IsEProcess.isAdmissibleEProcess_of_exists_lintegral_eq
+    (hS : ∀ P ∈ S, IsFiniteMeasure P) (hE : IsEProcess E ℱ S)
+    (h : ∀ n A, MeasurableSet[ℱ n] A → (∃ P ∈ S, P A ≠ 0) →
+      ∃ P ∈ S, P A ≠ 0 ∧ ∫⁻ ω, E n ω ∂P = P univ) :
+    IsAdmissibleEProcess E ℱ S := by
+  refine isAdmissibleEProcess_iff_measure_lt_eq_zero.2 ⟨hE, fun F hF hEF P₀ hP₀ n ↦ ?_⟩
+  by_contra hP₀A
+  -- under a member of the null that charges `{E n < F n}` and under which `E n` has expectation
+  -- `P univ`, the expectation of `F n` is at most that of `E n`
+  obtain ⟨P, hP, hPA, hPE⟩ := h n _
+    (measurableSet_lt (hE.adapted n) (hF.adapted n)) ⟨P₀, hP₀, hP₀A⟩
+  have := hS P hP
+  have h_eq : E n =ᵐ[P] F n := ae_eq_of_ae_le_of_lintegral_le (hEF P hP n)
+    (by rw [hPE]; exact measure_ne_top P univ) (hF.measurable n).aemeasurable
+    (by rw [hPE]; exact (hF.isEVar n).lintegral_le_measure_univ P hP)
+  exact hPA (measure_mono_null (fun ω hω ↦ (hω : E n ω < F n ω).ne) h_eq)
+
+end ProbabilityTheory