Mixture confidence sequences

This file adds the measure-mixture exponential process used by the method of mixtures. The core analytic primitive is the conditional-expectation swap for a prior integral over tilts.

noncomputable def FormalSLT.AnytimeValid.mixtureExponentialProcess {Ω : Type u_1} [MeasurableSpace Ω] (X : ℕ → Ω → ℝ) (sigma2 b : ℝ) (ρ : MeasureTheory.Measure ℝ) (n : ℕ) (ω : Ω) : ℝ

Prior mixture of the fixed-tilt sub-Gamma exponential processes.

Equations

• FormalSLT.AnytimeValid.mixtureExponentialProcess X sigma2 b ρ n ω = ∫ (lam : ℝ), FormalSLT.AnytimeValid.subGammaExponentialProcess X sigma2 b lam n ω ∂ρ

noncomputable def FormalSLT.AnytimeValid.uniformTiltPrior (lam0 lam1 : ℝ) : MeasureTheory.Measure ℝ

Continuous uniform prior on a compact tilt interval.

Equations

• FormalSLT.AnytimeValid.uniformTiltPrior lam0 lam1 = MeasureTheory.volume[|Set.Icc lam0 lam1]

theorem FormalSLT.AnytimeValid.uniformTiltPrior_isProbabilityMeasure {lam0 lam1 : ℝ} (h : lam0 < lam1) : MeasureTheory.IsProbabilityMeasure (uniformTiltPrior lam0 lam1)

theorem FormalSLT.AnytimeValid.uniformTiltPrior_valid_tilt_support {b lam0 lam1 : ℝ} (h0 : 0 < lam0) (_h01 : lam0 < lam1) (h1 : lam1 < 3 / b) : ∀ᵐ (lam : ℝ) ∂uniformTiltPrior lam0 lam1, lam ∈ Set.Ioo 0 (3 / b)

theorem FormalSLT.AnytimeValid.ae_le_of_forall_subalgebra_setIntegral_le {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ m₀) [MeasureTheory.SigmaFinite (μ.trim hm)] {f g : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfm : MeasureTheory.StronglyMeasurable f) (hgm : MeasureTheory.StronglyMeasurable g) (hfg : ∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, f x ∂μ ≤ ∫ (x : Ω) in s, g x ∂μ) : f ≤ᵐ[μ] g

Order from testing set integrals on a sub-sigma-algebra. This is the inequality analogue of the conditional-expectation uniqueness principle.

theorem FormalSLT.AnytimeValid.condExp_mixture_swap {Ω : Type u_1} {m m₀ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ m₀) {ρ : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite ρ] {M : ℝ → ℕ → Ω → ℝ} {n : ℕ} (hM_int : MeasureTheory.Integrable (fun (p : ℝ × Ω) => M p.1 (n + 1) p.2) (ρ.prod μ)) (hM_int_restrict : ∀ {s : Set Ω}, MeasurableSet s → μ s < ⊤ → MeasureTheory.Integrable (fun (p : Ω × ℝ) => M p.2 (n + 1) p.1) ((μ.restrict s).prod ρ)) (hCE_int_restrict : ∀ {s : Set Ω}, MeasurableSet s → μ s < ⊤ → MeasureTheory.Integrable (fun (p : Ω × ℝ) => μ[M p.2 (n + 1) | m] p.1) ((μ.restrict s).prod ρ)) (hCE_meas : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => ∫ (lam : ℝ), μ[M lam (n + 1) | m] ω ∂ρ) μ) : μ[fun (ω : Ω) => ∫ (lam : ℝ), M lam (n + 1) ω ∂ρ | m] =ᵐ[μ] fun (ω : Ω) => ∫ (lam : ℝ), μ[M lam (n + 1) | m] ω ∂ρ

Conditional expectation commutes with the prior integral, under the product integrability and conditional-side measurability obligations needed for Fubini and the defining set-integral property of conditional expectation.

theorem FormalSLT.AnytimeValid.mixture_condExp_step_of_fixed_tilt_steps {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} {sigma2 b : ℝ} {ρ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ρ] (h_adapted_mix : MeasureTheory.StronglyAdapted ℱ (mixtureExponentialProcess X sigma2 b ρ)) (h_integrable_mix : ∀ (n : ℕ), MeasureTheory.Integrable (mixtureExponentialProcess X sigma2 b ρ n) μ) (hM_int_next : ∀ (n : ℕ), MeasureTheory.Integrable (fun (p : ℝ × Ω) => subGammaExponentialProcess X sigma2 b p.1 (n + 1) p.2) (ρ.prod μ)) (hM_int_next_restrict : ∀ (n : ℕ) {s : Set Ω}, MeasurableSet s → μ s < ⊤ → MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 (n + 1) p.1) ((μ.restrict s).prod ρ)) (hM_int_current : ∀ (n : ℕ), MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 n p.1) (μ.prod ρ)) (hM_int_current_restrict : ∀ (n : ℕ) {s : Set Ω}, MeasurableSet s → μ s < ⊤ → MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 n p.1) ((μ.restrict s).prod ρ)) (hfixed_step : ∀ (n : ℕ), ∀ᵐ (lam : ℝ) ∂ρ, μ[fun (ω : Ω) => subGammaExponentialProcess X sigma2 b lam (n + 1) ω | ↑ℱ n] ≤ᵐ[μ] fun (ω : Ω) => subGammaExponentialProcess X sigma2 b lam n ω) (n : ℕ) : μ[mixtureExponentialProcess X sigma2 b ρ (n + 1) | ↑ℱ n] ≤ᵐ[μ] mixtureExponentialProcess X sigma2 b ρ n

One mixture supermartingale step from fixed-tilt conditional steps, proved by testing on F_n-measurable sets. This avoids needing joint measurability of the chosen conditional-expectation versions in the tilt parameter.

theorem FormalSLT.AnytimeValid.mixture_is_supermartingale {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} {sigma2 b : ℝ} {ρ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ρ] (hb : 0 < b) (hσ : 0 ≤ sigma2) (hsupport : ∀ᵐ (lam : ℝ) ∂ρ, lam ∈ Set.Ioo 0 (3 / b)) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (hX_int : ∀ (k : ℕ), MeasureTheory.Integrable (X k) μ) (h_adapted_lam : ∀ (lam : ℝ), MeasureTheory.StronglyAdapted ℱ (subGammaExponentialProcess X sigma2 b lam)) (h_adapted : MeasureTheory.StronglyAdapted ℱ (mixtureExponentialProcess X sigma2 b ρ)) (h_integrable : ∀ (n : ℕ), MeasureTheory.Integrable (mixtureExponentialProcess X sigma2 b ρ n) μ) (hM_int : ∀ (n : ℕ), MeasureTheory.Integrable (fun (p : ℝ × Ω) => subGammaExponentialProcess X sigma2 b p.1 (n + 1) p.2) (ρ.prod μ)) (hM_int_restrict : ∀ (n : ℕ) {s : Set Ω}, MeasurableSet s → μ s < ⊤ → MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 (n + 1) p.1) ((μ.restrict s).prod ρ)) (hM_int_step : ∀ (n : ℕ), MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 n p.1) (μ.prod ρ)) (hM_int_step_restrict : ∀ (n : ℕ) {s : Set Ω}, MeasurableSet s → μ s < ⊤ → MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 n p.1) ((μ.restrict s).prod ρ)) (hbound : ∀ (k : ℕ), ∀ᵐ (ω : Ω) ∂μ, |X k ω| ≤ b) (hcenter : ∀ (k : ℕ), μ[X k | ↑ℱ k] =ᵐ[μ] 0) (hvar : ∀ (k : ℕ), μ[fun (ω : Ω) => X k ω ^ 2 | ↑ℱ k] ≤ᵐ[μ] fun (x : Ω) => sigma2) : MeasureTheory.Supermartingale (mixtureExponentialProcess X sigma2 b ρ) ℱ μ ∧ ∀ (n : ℕ) (ω : Ω), 0 ≤ mixtureExponentialProcess X sigma2 b ρ n ω

The mixture process is a nonnegative supermartingale once the conditional expectation swap and the resulting integral one-step inequality are available.

theorem FormalSLT.AnytimeValid.atTop_time_uniform_confidence_sequence_subGamma_mixture {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} {sigma2 b delta : ℝ} {ρ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ρ] (hδ : 0 < delta) (hb : 0 < b) (hσ : 0 ≤ sigma2) (hsupport : ∀ᵐ (lam : ℝ) ∂ρ, lam ∈ Set.Ioo 0 (3 / b)) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (hX_int : ∀ (k : ℕ), MeasureTheory.Integrable (X k) μ) (h_adapted_lam : ∀ (lam : ℝ), MeasureTheory.StronglyAdapted ℱ (subGammaExponentialProcess X sigma2 b lam)) (h_adapted_mix : MeasureTheory.StronglyAdapted ℱ (mixtureExponentialProcess X sigma2 b ρ)) (h_integrable_mix : ∀ (n : ℕ), MeasureTheory.Integrable (mixtureExponentialProcess X sigma2 b ρ n) μ) (hM_int : ∀ (n : ℕ), MeasureTheory.Integrable (fun (p : ℝ × Ω) => subGammaExponentialProcess X sigma2 b p.1 (n + 1) p.2) (ρ.prod μ)) (hM_int_restrict : ∀ (n : ℕ) {s : Set Ω}, MeasurableSet s → μ s < ⊤ → MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 (n + 1) p.1) ((μ.restrict s).prod ρ)) (hM_int_step : ∀ (n : ℕ), MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 n p.1) (μ.prod ρ)) (hM_int_step_restrict : ∀ (n : ℕ) {s : Set Ω}, MeasurableSet s → μ s < ⊤ → MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 n p.1) ((μ.restrict s).prod ρ)) (hbound : ∀ (k : ℕ), ∀ᵐ (ω : Ω) ∂μ, |X k ω| ≤ b) (hcenter : ∀ (k : ℕ), μ[X k | ↑ℱ k] =ᵐ[μ] 0) (hvar : ∀ (k : ℕ), μ[fun (ω : Ω) => X k ω ^ 2 | ↑ℱ k] ≤ᵐ[μ] fun (x : Ω) => sigma2) : μ.real {ω : Ω | ∃ (n : ℕ), 0 < n ∧ 1 / delta ≤ mixtureExponentialProcess X sigma2 b ρ n ω} ≤ delta

Countable-time Ville bound for the mixture exponential process.

Discharging the measurability / integrability package for the uniform prior

The headline atTop_time_uniform_confidence_sequence_subGamma_mixture carries six measurability / integrability obligations. For the concrete uniformTiltPrior (a probability measure supported on the compact interval [lam0, lam1]) they are all discharged from the increment model alone, with no free hypotheses:

• joint measurability of (λ, ω) ↦ subGammaExponentialProcess λ n ω in the product σ-algebra;
• the pointwise process bound M ≤ exp (lam1 · n · b) valid on the bounded-increment, admissible-tilt region, which yields product-integrability over [lam0, lam1] × Ω (and its restricted variants) via Integrable.of_bound, since the product of two finite measures is finite;
• adaptedness of each fixed-tilt process and of the prior integral, from adaptedness of X.

theorem FormalSLT.AnytimeValid.measurable_subGammaExponentialProcess_prod {Ω : Type u_1} [MeasurableSpace Ω] (X : ℕ → Ω → ℝ) (sigma2 b : ℝ) (n : ℕ) (hX_meas : ∀ (k : ℕ), Measurable (X k)) : Measurable fun (p : ℝ × Ω) => subGammaExponentialProcess X sigma2 b p.1 n p.2

Joint measurability of the parameterized sub-Gamma exponential process in the product σ-algebra, from measurability of each increment.

theorem FormalSLT.AnytimeValid.subGammaExponentialProcess_le_of_bound {Ω : Type u_1} (X : ℕ → Ω → ℝ) (sigma2 b lam lam1 : ℝ) (n : ℕ) (ω : Ω) (hb : 0 < b) (hσ : 0 ≤ sigma2) (hlam0 : 0 ≤ lam) (hlam1 : lam ≤ lam1) (hblam : b * lam < 3) (hbound : ∀ i ∈ Finset.range n, |X i ω| ≤ b) : subGammaExponentialProcess X sigma2 b lam n ω ≤ Real.exp (lam1 * ↑n * b)

Pointwise upper bound M_n ≤ exp (lam1 · n · b) on the fixed-tilt exponential process when the increments are bounded (|X_i ω| ≤ b for i < n) and the tilt is admissible (0 ≤ lam ≤ lam1, b · lam < 3). The negative cumulant term only helps, so it is dropped.

theorem FormalSLT.AnytimeValid.uniformTiltPrior_ae_mem_Icc {lam0 lam1 : ℝ} : ∀ᵐ (lam : ℝ) ∂uniformTiltPrior lam0 lam1, lam ∈ Set.Icc lam0 lam1

For the uniform prior, almost every tilt lies in the closed parameter interval.

theorem FormalSLT.AnytimeValid.integrable_subGammaExponentialProcess_prod_uniformPrior {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} {sigma2 b lam0 lam1 : ℝ} (n : ℕ) (hb : 0 < b) (hσ : 0 ≤ sigma2) (hlam0 : 0 ≤ lam0) (h01 : lam0 < lam1) (hlam1 : b * lam1 < 3) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (hbound : ∀ (k : ℕ), ∀ᵐ (ω : Ω) ∂μ, |X k ω| ≤ b) : MeasureTheory.Integrable (fun (p : ℝ × Ω) => subGammaExponentialProcess X sigma2 b p.1 n p.2) ((uniformTiltPrior lam0 lam1).prod μ)

Product integrability for subGammaExponentialProcess under (uniformTiltPrior …).prod μ. The integrand is a.e. bounded by exp (lam1 · n · b) and the product of two probability measures is finite, so Integrable.of_bound applies.

theorem FormalSLT.AnytimeValid.integrable_subGammaExponentialProcess_omegaProd_uniformPrior {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure ν] {X : ℕ → Ω → ℝ} {sigma2 b lam0 lam1 : ℝ} (n : ℕ) (hb : 0 < b) (hσ : 0 ≤ sigma2) (hlam0 : 0 ≤ lam0) (h01 : lam0 < lam1) (hlam1 : b * lam1 < 3) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (hbound : ∀ (k : ℕ), ∀ᵐ (ω : Ω) ∂ν, |X k ω| ≤ b) : MeasureTheory.Integrable (fun (p : Ω × ℝ) => subGammaExponentialProcess X sigma2 b p.2 n p.1) (ν.prod (uniformTiltPrior lam0 lam1))

Product integrability in the Ω × ℝ orientation under ν.prod (uniformTiltPrior …), for any finite measure ν on Ω carrying a ν-a.e. increment bound. This single statement covers both the full measure (ν = μ) and the filtration-restricted measure (ν = μ.restrict s) variants the supermartingale step needs.

def FormalSLT.AnytimeValid.IncrementAdapted {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (ℱ : MeasureTheory.Filtration ℕ mΩ) (X : ℕ → Ω → ℝ) : Prop

Predictable-increment (martingale-difference) adaptedness.

The increment X_k is revealed at time k + 1, i.e. each X_k is ℱ (k+1)-strongly-measurable. This is the correct admissibility for a martingale-difference sequence whose centering and conditional variance are taken with respect to the past ℱ k: it lets X_k be a genuine nonconstant increment while keeping μ[X k | ℱ k] = 0 non-vacuous.

Conditioning the present (StronglyAdapted ℱ X, i.e. each X_k is ℱ k-measurable) together with μ[X k | ℱ k] = 0 would force X_k =ᵐ 0 by condExp_of_stronglyMeasurable, leaving only the zero process admissible. The +1 shift is what avoids that collapse. The running sum S_n remains ℱ n-measurable because it only involves X_0, …, X_{n-1}, each ℱ n-measurable since i < n ⟹ i + 1 ≤ n.

Equations

• FormalSLT.AnytimeValid.IncrementAdapted ℱ X = ∀ (k : ℕ), MeasureTheory.StronglyMeasurable (X k)

theorem FormalSLT.AnytimeValid.stronglyAdapted_subGammaExponentialProcess_of_adapted {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} (sigma2 b lam : ℝ) (hX_adapted : IncrementAdapted ℱ X) : MeasureTheory.StronglyAdapted ℱ (subGammaExponentialProcess X sigma2 b lam)

Each fixed-tilt exponential process is ℱ-adapted once the increment process is predictable-increment adapted (X_k is ℱ (k+1)-measurable). The running sum S_n is ℱ n-measurable because it only involves X_0, …, X_{n-1} and i < n ⟹ i + 1 ≤ n.

theorem FormalSLT.AnytimeValid.stronglyMeasurable_filtration_prod_subGamma {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} (sigma2 b : ℝ) (n : ℕ) (hX_adapted : IncrementAdapted ℱ X) : MeasureTheory.StronglyMeasurable (Function.uncurry fun (ω : Ω) (lam : ℝ) => subGammaExponentialProcess X sigma2 b lam n ω)

Joint strong-measurability of the parameterized process in the ℱ n-product σ-algebra, from adaptedness of the increment process. This is the input to the integral-over-tilt adaptedness.

theorem FormalSLT.AnytimeValid.stronglyAdapted_mixtureExponentialProcess_of_adapted {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} (sigma2 b : ℝ) (ρ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ρ] (hX_adapted : IncrementAdapted ℱ X) : MeasureTheory.StronglyAdapted ℱ (mixtureExponentialProcess X sigma2 b ρ)

The prior integral preserves ℱ n-strong-measurability, so the mixture process is adapted to ℱ whenever the increment process is.

theorem FormalSLT.AnytimeValid.mixture_confidence_sequence_uniformPrior {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {X : ℕ → Ω → ℝ} {sigma2 b delta lam0 lam1 : ℝ} (hδ : 0 < delta) (hb : 0 < b) (hσ : 0 ≤ sigma2) (hlam0 : 0 < lam0) (h01 : lam0 < lam1) (hlam1 : lam1 < 3 / b) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (hX_int : ∀ (k : ℕ), MeasureTheory.Integrable (X k) μ) (hX_adapted : IncrementAdapted ℱ X) (hbound : ∀ (k : ℕ), ∀ᵐ (ω : Ω) ∂μ, |X k ω| ≤ b) (hcenter : ∀ (k : ℕ), μ[X k | ↑ℱ k] =ᵐ[μ] 0) (hvar : ∀ (k : ℕ), μ[fun (ω : Ω) => X k ω ^ 2 | ↑ℱ k] ≤ᵐ[μ] fun (x : Ω) => sigma2) : μ.real {ω : Ω | ∃ (n : ℕ), 0 < n ∧ 1 / delta ≤ mixtureExponentialProcess X sigma2 b (uniformTiltPrior lam0 lam1) n ω} ≤ delta

The mixture confidence sequence for the continuous uniform tilt prior, with no free measurability or integrability hypotheses. The increment model on X is a genuine martingale-difference sequence: each increment X_k is revealed at time k + 1 (IncrementAdapted ℱ X, i.e. X_k is ℱ (k+1)-strongly-measurable), is bounded |X_k| ≤ b, is conditionally centered with respect to the past μ[X_k | F_k] = 0, and has conditional second moment μ[X_k² | F_k] ≤ σ². With an admissible compact tilt interval [lam0, lam1] ⊆ (0, 3/b), the prior-mixture exponential process is an anytime-valid confidence sequence:

μ.real {ω | ∃ n > 0, 1/δ ≤ ∫ lam, M_λ(n, ω) ∂Unif[lam0,lam1]} ≤ δ.

The +1 increment shift is essential for non-vacuity: pairing the present-conditioning StronglyAdapted ℱ X with μ[X_k | F_k] = 0 would force X_k =ᵐ 0 (by condExp_of_stronglyMeasurable), admitting only the zero process. With the shift the centering is genuine and the running sum S_n is still ℱ n-measurable (it uses only X_0, …, X_{n-1}).

Every measurability / integrability obligation of atTop_time_uniform_confidence_sequence_subGamma_mixture is discharged internally for the concrete uniform prior: joint measurability from hX_meas, the four product-integrability conditions from the process bound M ≤ exp (lam1 · n · b) via Integrable.of_bound, and both adaptedness conditions from hX_adapted.