From 580750cdb55f257c0a176fd4b851ff9ea1cd4303 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:20:19 +0100 Subject: [PATCH 1/4] feat: test martingales for a convex i.i.d. null have no power against its linear span MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For a convex set `S₁` of measures and a probability measure `Q₁` with `Q₁ + ∑ i, b i • P i = ∑ i, c i • P i` for finitely many probability measures `P i ∈ S₁`, a test martingale for the i.i.d. laws of `S₁` whose initial value has expectation `1` under the null, for a filtration each of whose σ-algebras depends on finitely many observations, is a test martingale under the i.i.d. law of `Q₁`, so its `limsup` is almost surely finite there. For the null of the two point masses on `Bool`, some test martingale tends to `∞` almost surely under i.i.d. fair coin flips, so convexity is needed (EValues roadmap, Layer 6.2, power one). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- .../EValues/PowerOne/TestMartingale.lean | 440 ++++++++++++++++++ 1 file changed, 440 insertions(+) create mode 100644 LMLExplore/EValues/PowerOne/TestMartingale.lean diff --git a/LMLExplore/EValues/PowerOne/TestMartingale.lean b/LMLExplore/EValues/PowerOne/TestMartingale.lean new file mode 100644 index 00000000..2744008e --- /dev/null +++ b/LMLExplore/EValues/PowerOne/TestMartingale.lean @@ -0,0 +1,440 @@ +/- +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.TestSupermartingale +public import Mathlib.Analysis.Convex.Basic +public import Mathlib.Probability.ProductMeasure +import LMLExplore.Probability.Martingale.OptionalStopping +import Mathlib.Analysis.Analytic.Constructions +import Mathlib.Analysis.Analytic.Uniqueness +import Mathlib.MeasureTheory.Function.FactorsThrough + +/-! +# Test martingales for convex i.i.d. nulls have no power against the span of the null + +The observations are the coordinates of `ℕ → 𝓧`. For a set `S₁` of probability measures on `𝓧`, +the i.i.d. null is the set of the laws `Measure.infinitePi fun _ ↦ P` with `P ∈ S₁`. Zhang, Ramdas +and Wang conjecture that if a test martingale for the i.i.d. null has power one against the i.i.d. +law of `Q₁`, then `Q₁` lies outside the linear span of `S₁`, perhaps under additional conditions +[ZRW24, §7]. + +For a convex `S₁` this holds, for every filtration each of whose σ-algebras depends on finitely +many observations. Let `Q₁` be a probability measure in the linear span of `S₁`, written as +`Q₁ + ∑ i, b i • P i = ∑ i, c i • P i` with finitely many `P i ∈ S₁` and `b i, c i ≥ 0`. Then every +test martingale for the i.i.d. null whose initial value has expectation `1` under the null is a +test martingale under the i.i.d. law of `Q₁`. In particular its `limsup` is almost surely finite +under that law: it does not have power one against `Q₁`. + +Convexity is needed. For the null of the two point masses on `Bool`, the fair coin is the midpoint +of the null, yet the process equal to `1` while all observations agree, and to `2 ^ n` at time `n` +once two different ones have been seen, is a test martingale for the i.i.d. null that tends to `∞` +almost surely under i.i.d. fair coin flips. + +## Main statements + +* `ProbabilityTheory.isTestMartingale_infinitePi_of_add_sum_eq_sum`: for a convex null, a test + martingale for the i.i.d. null with initial expectation `1` is a test martingale under the i.i.d. + law of every probability measure in the linear span of the null. +* `ProbabilityTheory.ae_limsup_lt_top_infinitePi_of_add_sum_eq_sum`: such a test martingale has an + almost surely finite `limsup` under that law, so it does not have power one against it. +* `ProbabilityTheory.exists_isTestMartingale_dirac_tendsto_top`: for the null of the two point + masses on `Bool`, some test martingale for the i.i.d. null with initial value `1` tends to `∞` + almost surely under i.i.d. fair coin flips. + +## Implementation notes + +An `ℱ n`-measurable set and the values `M n` and `M (n + 1)` are functions of the first `N + 1` +observations for some `N`, so their integrals under `Measure.infinitePi` are integrals under +`Measure.pi` over `Finset.Iic N`. The finite-dimensional step is a polarization argument. Write +`B = ∑ i, b i • P i`. The integral of a function of finitely many observations under the product +of copies of `Q₁ + t • B` is a polynomial in `t`. For `t ≥ 1`, the measure `Q₁ + t • B` is a +positive multiple of a convex combination of the `P i`, which lies in the null, so the identities +of the martingale hold for these `t`. By the identity theorem for analytic functions they hold at +`t = 0`, that is under `Q₁`. + +## References + +* [ZRW24] Z. Zhang, A. Ramdas and R. Wang, *On the existence of powerful p-values and e-values for + composite hypotheses*, Ann. Statist. 52 (2024), arXiv:2305.16539: §7. +-/ + +public section + +open MeasureTheory Filter +open scoped ENNReal NNReal Topology + +namespace ProbabilityTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} + +/-! ### Mixtures and their products -/ + +/-- A combination of measures with nonnegative weights of nonzero sum is that sum times a convex +combination of the same measures. -/ +private lemma sum_smul_eq_smul_sum_div_smul {ι : Type*} {T : Finset ι} {P : ι → Measure 𝓧} + {w : ι → ℝ≥0} (hw : ∑ i ∈ T, w i ≠ 0) : + ∑ i ∈ T, w i • P i = (∑ i ∈ T, w i) • ∑ i ∈ T, (w i / ∑ j ∈ T, w j) • P i := by + rw [Finset.smul_sum] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + rw [smul_smul, mul_div_cancel₀ _ hw] + +/-- A convex set of measures contains the convex combinations of finitely many of its members. -/ +private lemma sum_smul_mem_of_convex {S : Set (Measure 𝓧)} (hS : Convex ℝ≥0∞ S) {ι : Type*} + {P : ι → Measure 𝓧} {T : Finset ι} (hP : ∀ i ∈ T, P i ∈ S) {w : ι → ℝ≥0} + (hw : ∑ i ∈ T, w i = 1) : ∑ i ∈ T, w i • P i ∈ S := by + classical + induction T using Finset.induction_on generalizing w with + | empty => simp at hw + | insert a T ha ih => + rw [Finset.sum_insert ha] at hw ⊢ + have hPa := hP a (Finset.mem_insert_self a T) + have hPT : ∀ i ∈ T, P i ∈ S := fun i hi ↦ hP i (Finset.mem_insert_of_mem hi) + rcases eq_or_ne (∑ i ∈ T, w i) 0 with h0 | h0 + · rw [h0, add_zero] at hw + rw [Finset.sum_eq_zero fun i hi ↦ by rw [Finset.sum_eq_zero_iff.1 h0 i hi, zero_smul], + add_zero, hw, one_smul] + exact hPa + · rw [sum_smul_eq_smul_sum_div_smul h0] + have h := hS hPa (ih hPT (w := fun i ↦ w i / ∑ j ∈ T, w j) ?_) zero_le zero_le + (show (w a : ℝ≥0∞) + ((∑ i ∈ T, w i : ℝ≥0) : ℝ≥0∞) = 1 by exact_mod_cast hw) + · rwa [Measure.coe_nnreal_smul, Measure.coe_nnreal_smul] at h + · rw [← Finset.sum_div, div_self h0] + +/-- A combination of probability measures with weights of sum `1` is a probability measure. -/ +private lemma isProbabilityMeasure_sum_smul {ι : Type*} [Fintype ι] {P : ι → Measure 𝓧} + [∀ i, IsProbabilityMeasure (P i)] {w : ι → ℝ≥0} (hw : ∑ i, w i = 1) : + IsProbabilityMeasure (∑ i, w i • P i) := by + constructor + simp only [sum_apply, smul_apply, measure_univ, ENNReal.smul_one] + exact_mod_cast hw + +/-- The integral of a function of finitely many observations under the product of copies of a +mixture of finite measures is a polynomial in the weights, whose coefficients are its integrals +under the products of the components. -/ +private lemma lintegral_pi_sum_smul {J κ : Type*} [Fintype J] [DecidableEq J] [Fintype κ] + {R : κ → Measure 𝓧} [∀ k, IsFiniteMeasure (R k)] (w : κ → ℝ≥0) (F : (J → 𝓧) → ℝ≥0∞) : + ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ ∑ k, w k • R k) = + ∑ e : J → κ, (∏ j, (w (e j) : ℝ≥0∞)) * ∫⁻ x, F x ∂Measure.pi (fun j ↦ R (e j)) := by + have h : Measure.pi (fun _ : J ↦ ∑ k, w k • R k) = + ∑ e : J → κ, (∏ j, (w (e j) : ℝ≥0∞)) • Measure.pi (fun j ↦ R (e j)) := by + refine Measure.pi_eq fun A hA ↦ ?_ + simp only [sum_apply, smul_apply, Measure.pi_pi, smul_eq_mul, Measure.nnreal_smul_coe_apply, + Fintype.prod_sum, Finset.prod_mul_distrib] + rw [h] + simp only [lintegral_finsetSum_measure, lintegral_smul_measure, smul_eq_mul] + +/-- The product of copies of a multiple `s • ν` of a finite measure is `s ^ card J` times the +product of copies of `ν`. -/ +private lemma pi_const_smul {J : Type*} [Fintype J] (ν : Measure 𝓧) [IsFiniteMeasure ν] + (s : ℝ≥0) : + Measure.pi (fun _ : J ↦ s • ν) = s ^ Fintype.card J • Measure.pi (fun _ : J ↦ ν) := by + refine Measure.pi_eq fun A hA ↦ ?_ + simp only [smul_apply, Measure.pi_pi, Finset.prod_mul_distrib, Finset.prod_const, + Finset.card_univ, ENNReal.smul_def, smul_eq_mul, ENNReal.coe_pow] + +/-! ### Polarization -/ + +/-- **Polarization.** Let `Q` be a probability measure and `P i` finite measures with +`Q + ∑ i, b i • P i = ∑ i, c i • P i`. If two functions of the observations indexed by a finite +type `J` have equal integrals under the product of copies of every convex combination of the +`P i`, finite for the first function, then they have equal integrals under the product of copies +of `Q`. -/ +private lemma lintegral_pi_eq_of_add_sum_eq_sum {J ι : Type*} [Fintype J] [Fintype ι] + {P : ι → Measure 𝓧} [∀ i, IsFiniteMeasure (P i)] {b c : ι → ℝ≥0} {Q : Measure 𝓧} + [IsProbabilityMeasure Q] (hQ : Q + ∑ i, b i • P i = ∑ i, c i • P i) + {F G : (J → 𝓧) → ℝ≥0∞} + (hFG : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → + ∫⁻ x, F x ∂Measure.pi (fun _ ↦ ∑ i, w i • P i) = + ∫⁻ x, G x ∂Measure.pi (fun _ ↦ ∑ i, w i • P i)) + (hF : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → + ∫⁻ x, F x ∂Measure.pi (fun _ ↦ ∑ i, w i • P i) ≠ ∞) : + ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ Q) = ∫⁻ x, G x ∂Measure.pi (fun _ : J ↦ Q) := by + classical + set B := ∑ i, b i • P i with hB + -- `Q + t • B` as the mixture of `R true = B` and `R false = Q` with weights `w t` + set R : Bool → Measure 𝓧 := fun k ↦ bif k then B else Q with hR + have : IsFiniteMeasure B := by rw [hB]; infer_instance + have : ∀ k, IsFiniteMeasure (R k) := fun k ↦ by + cases k <;> simp only [hR, Bool.cond_false, Bool.cond_true] <;> infer_instance + set w : ℝ≥0 → Bool → ℝ≥0 := fun t k ↦ bif k then t else 1 with hw + set α : ((J → 𝓧) → ℝ≥0∞) → (J → Bool) → ℝ≥0∞ := + fun H e ↦ ∫⁻ x, H x ∂Measure.pi (fun j ↦ R (e j)) + have hpoly (H : (J → 𝓧) → ℝ≥0∞) (t : ℝ≥0) : + ∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + t • B) = + ∑ e : J → Bool, (∏ j, (w t (e j) : ℝ≥0∞)) * α H e := by + have hmix : Q + t • B = ∑ k, w t k • R k := by simp [hw, hR, add_comm] + rw [hmix, lintegral_pi_sum_smul] + -- for `t ≥ 1`, `Q + t • B` is a positive multiple of a convex combination of the `P i` + have hgood (t : ℝ≥0) (ht : 1 ≤ t) : + ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ Q + t • B) = + ∫⁻ x, G x ∂Measure.pi (fun _ : J ↦ Q + t • B) ∧ + ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ Q + t • B) ≠ ∞ := by + have hμ : Q + t • B = ∑ i, (c i + (t - 1) * b i) • P i := by + calc Q + t • B = (Q + B) + (t - 1) • B := by + conv_lhs => rw [← add_tsub_cancel_of_le ht, add_smul, one_smul] + rw [add_assoc] + _ = ∑ i, (c i + (t - 1) * b i) • P i := by + rw [hQ, hB, Finset.smul_sum, ← Finset.sum_add_distrib] + exact Finset.sum_congr rfl fun i _ ↦ by rw [smul_smul, ← add_smul] + have hs : ∑ i, (c i + (t - 1) * b i) ≠ 0 := by + intro h0 + have h : Q + t • B = 0 := by + rw [hμ] + exact Finset.sum_eq_zero fun i hi ↦ by rw [Finset.sum_eq_zero_iff.1 h0 i hi, zero_smul] + have h' := congrArg (· Set.univ) h + simp at h' + have hv : ∑ i, (c i + (t - 1) * b i) / ∑ j, (c j + (t - 1) * b j) = 1 := by + rw [← Finset.sum_div, div_self hs] + rw [hμ, sum_smul_eq_smul_sum_div_smul hs, pi_const_smul, lintegral_smul_measure, + lintegral_smul_measure, hFG _ hv] + refine ⟨rfl, ?_⟩ + rw [ENNReal.smul_def, smul_eq_mul, ← hFG _ hv] + exact ENNReal.mul_ne_top ENNReal.coe_ne_top (hF _ hv) + -- the coefficients of the polynomials are finite + have hα_ne (H : (J → 𝓧) → ℝ≥0∞) + (hH : ∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + (1 : ℝ≥0) • B) ≠ ∞) (e : J → Bool) : + α H e ≠ ∞ := by + have hw1 (k : Bool) : w 1 k = 1 := by cases k <;> rfl + rw [hpoly] at hH + simp only [hw1, ENNReal.coe_one, Finset.prod_const_one, one_mul] at hH + exact ENNReal.sum_ne_top.1 hH e (Finset.mem_univ e) + have hαF := hα_ne F (hgood 1 le_rfl).2 + have hαG := hα_ne G ((hgood 1 le_rfl).1 ▸ (hgood 1 le_rfl).2) + have hfin (H : (J → 𝓧) → ℝ≥0∞) (hH : ∀ e, α H e ≠ ∞) (t : ℝ≥0) : + ∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + t • B) ≠ ∞ := by + rw [hpoly] + exact ENNReal.sum_ne_top.2 fun e _ ↦ + ENNReal.mul_ne_top (ENNReal.prod_ne_top fun _ _ ↦ ENNReal.coe_ne_top) (hH e) + -- the real polynomials + set φ : ((J → 𝓧) → ℝ≥0∞) → ℝ → ℝ := + fun H x ↦ ∑ e : J → Bool, (∏ j, bif e j then x else 1) * (α H e).toReal + have hφ_eq (H : (J → 𝓧) → ℝ≥0∞) (hH : ∀ e, α H e ≠ ∞) (t : ℝ≥0) : + φ H t = (∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + t • B)).toReal := by + rw [hpoly, ENNReal.toReal_sum fun e _ ↦ + ENNReal.mul_ne_top (ENNReal.prod_ne_top fun _ _ ↦ ENNReal.coe_ne_top) (hH e)] + refine Finset.sum_congr rfl fun e _ ↦ ?_ + rw [ENNReal.toReal_mul, ENNReal.toReal_prod] + congr 1 + refine Finset.prod_congr rfl fun j _ ↦ ?_ + cases e j <;> simp [hw] + have han (H : (J → 𝓧) → ℝ≥0∞) : AnalyticOnNhd ℝ (φ H) Set.univ := fun x _ ↦ + Finset.analyticAt_fun_sum _ fun e _ ↦ (Finset.analyticAt_fun_prod _ fun j _ ↦ by + cases e j + · exact analyticAt_const + · exact analyticAt_id).mul analyticAt_const + -- they agree on `(1, ∞)`, hence everywhere + have hφFG : φ F = φ G := (han F).eq_of_eventuallyEq (han G) (z₀ := 2) <| by + filter_upwards [lt_mem_nhds (by norm_num : (1 : ℝ) < 2)] with x hx + have hx' : (x.toNNReal : ℝ) = x := Real.coe_toNNReal _ (by linarith) + have h1 : 1 ≤ x.toNNReal := by + rw [← NNReal.coe_le_coe, hx', NNReal.coe_one] + exact hx.le + rw [← hx', hφ_eq F hαF, hφ_eq G hαG, (hgood _ h1).1] + have h0 : φ F ((0 : ℝ≥0) : ℝ) = φ G ((0 : ℝ≥0) : ℝ) := by rw [hφFG] + rw [hφ_eq F hαF, hφ_eq G hαG] at h0 + have hF0 := hfin F hαF 0 + have hG0 := hfin G hαG 0 + simp only [zero_smul, add_zero] at h0 hF0 hG0 + exact (ENNReal.toReal_eq_toReal_iff' hF0 hG0).1 h0 + +/-- **Polarization for i.i.d. laws.** Let `Q` be a probability measure and `P i` probability +measures with `Q + ∑ i, b i • P i = ∑ i, c i • P i`. If two functions of the first `N + 1` +observations have equal integrals under the i.i.d. law of every convex combination of the `P i`, +finite for the first function, then they have equal integrals under the i.i.d. law of `Q`. -/ +private lemma lintegral_infinitePi_eq_of_add_sum_eq_sum {ι : Type*} [Fintype ι] + {P : ι → Measure 𝓧} [∀ i, IsProbabilityMeasure (P i)] {b c : ι → ℝ≥0} {Q : Measure 𝓧} + [IsProbabilityMeasure Q] (hQ : Q + ∑ i, b i • P i = ∑ i, c i • P i) {N : ℕ} + {f g : (ℕ → 𝓧) → ℝ≥0∞} (hf : Measurable[Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) N] f) + (hg : Measurable[Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) N] g) + (hfg : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → + ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i) = + ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i)) + (hf_ne : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → + ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i) ≠ ∞) : + ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ Q) = ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ ↦ Q) := by + rw [Filtration.piLE_eq_comap_frestrictLe] at hf hg + obtain ⟨f', hf', rfl⟩ := hf.exists_eq_measurable_comp + obtain ⟨g', hg', rfl⟩ := hg.exists_eq_measurable_comp + have h (μ : Measure 𝓧) [IsProbabilityMeasure μ] {H : (Finset.Iic N → 𝓧) → ℝ≥0∞} + (hH : Measurable H) : + ∫⁻ ω, (H ∘ Preorder.frestrictLe N) ω ∂Measure.infinitePi (fun _ ↦ μ) = + ∫⁻ x, H x ∂Measure.pi (fun _ : Finset.Iic N ↦ μ) := + lintegral_restrict_infinitePi _ hH + rw [h Q hf', h Q hg'] + refine lintegral_pi_eq_of_add_sum_eq_sum hQ (fun w hw ↦ ?_) fun w hw ↦ ?_ + · have := isProbabilityMeasure_sum_smul (P := P) hw + rw [← h _ hf', ← h _ hg'] + exact hfg w hw + · have := isProbabilityMeasure_sum_smul (P := P) hw + rw [← h _ hf'] + exact hf_ne w hw + +/-! ### Test martingales for convex i.i.d. nulls -/ + +/-- **Test martingales for a convex i.i.d. null have no power against its linear span.** Let `S₁` +be a convex set of measures and `Q₁` a probability measure in its linear span, written as +`Q₁ + ∑ i, b i • P i = ∑ i, c i • P i` with finitely many probability measures `P i ∈ S₁`. Let `ℱ` +be a filtration each of whose σ-algebras depends on finitely many observations. Then a test +martingale for the i.i.d. laws of the members of `S₁` whose initial value has expectation `1` +under each of them is a test martingale for the i.i.d. law of `Q₁`. This proves, for convex nulls, +the conjecture of [ZRW24, §7] that a test martingale with power one against `Q₁` forces `Q₁` out +of the linear span of the null. -/ +theorem isTestMartingale_infinitePi_of_add_sum_eq_sum {S₁ : Set (Measure 𝓧)} + (hS₁ : Convex ℝ≥0∞ S₁) {ι : Type*} [Fintype ι] {P : ι → Measure 𝓧} + [∀ i, IsProbabilityMeasure (P i)] (hP : ∀ i, P i ∈ S₁) {b c : ι → ℝ≥0} {Q₁ : Measure 𝓧} + [IsProbabilityMeasure Q₁] (hQ₁ : Q₁ + ∑ i, b i • P i = ∑ i, c i • P i) + {ℱ : Filtration ℕ (MeasurableSpace.pi : MeasurableSpace (ℕ → 𝓧))} + (hℱ : ∀ n, ∃ N, ℱ n ≤ Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) N) {M : ℕ → (ℕ → 𝓧) → ℝ≥0∞} + (hM : IsTestMartingale M ℱ ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁)) + (hM0 : ∀ P ∈ S₁, ∫⁻ ω, M 0 ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) = 1) : + IsTestMartingale M ℱ {Measure.infinitePi fun _ : ℕ ↦ Q₁} := by + have hmem (w : ι → ℝ≥0) (hw : ∑ i, w i = 1) : ∑ i, w i • P i ∈ S₁ := + sum_smul_mem_of_convex hS₁ (fun i _ ↦ hP i) hw + have hnull (w : ι → ℝ≥0) (hw : ∑ i, w i = 1) : Measure.infinitePi (fun _ : ℕ ↦ ∑ i, w i • P i) ∈ + (fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁ := + ⟨_, hmem w hw, rfl⟩ + refine ⟨hM.adapted, ?_, ?_⟩ + · rintro _ rfl + obtain ⟨N, hN⟩ := hℱ 0 + refine (lintegral_infinitePi_eq_of_add_sum_eq_sum hQ₁ ((hM.adapted 0).mono hN le_rfl) + (measurable_const (a := (1 : ℝ≥0∞))) (fun w hw ↦ ?_) fun w hw ↦ ?_).trans_le (by simp) + · have := isProbabilityMeasure_sum_smul (P := P) hw + rw [hM0 _ (hmem w hw)] + simp + · rw [hM0 _ (hmem w hw)] + exact ENNReal.one_ne_top + · rintro _ rfl n s hs + obtain ⟨N₁, hN₁⟩ := hℱ n + obtain ⟨N₂, hN₂⟩ := hℱ (n + 1) + have h₁ : ℱ n ≤ Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) (max N₁ N₂) := + hN₁.trans (Filtration.mono _ (le_max_left _ _)) + have h₂ : ℱ (n + 1) ≤ Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) (max N₁ N₂) := + hN₂.trans (Filtration.mono _ (le_max_right _ _)) + have hs' : MeasurableSet s := ℱ.le n s hs + rw [← lintegral_indicator hs', ← lintegral_indicator hs'] + refine lintegral_infinitePi_eq_of_add_sum_eq_sum hQ₁ + (((hM.adapted (n + 1)).mono h₂ le_rfl).indicator (h₁ s hs)) + (((hM.adapted n).mono h₁ le_rfl).indicator (h₁ s hs)) (fun w hw ↦ ?_) fun w hw ↦ ?_ + · rw [lintegral_indicator hs', lintegral_indicator hs'] + exact hM.setLIntegral_succ_eq _ (hnull w hw) n s hs + · have := isProbabilityMeasure_sum_smul (P := P) hw + rw [lintegral_indicator hs'] + exact ((setLIntegral_le_lintegral _ _).trans_lt + ((hM.isTestSupermartingale.lintegral_le_one (hnull w hw) (n + 1)).trans_lt + ENNReal.one_lt_top)).ne + +/-- **No power one against the linear span of a convex i.i.d. null.** Under the hypotheses of +`isTestMartingale_infinitePi_of_add_sum_eq_sum`, the test martingale has an almost surely finite +`limsup` under the i.i.d. law of `Q₁`: it does not have power one against `Q₁`. -/ +theorem ae_limsup_lt_top_infinitePi_of_add_sum_eq_sum {S₁ : Set (Measure 𝓧)} + (hS₁ : Convex ℝ≥0∞ S₁) {ι : Type*} [Fintype ι] {P : ι → Measure 𝓧} + [∀ i, IsProbabilityMeasure (P i)] (hP : ∀ i, P i ∈ S₁) {b c : ι → ℝ≥0} {Q₁ : Measure 𝓧} + [IsProbabilityMeasure Q₁] (hQ₁ : Q₁ + ∑ i, b i • P i = ∑ i, c i • P i) + {ℱ : Filtration ℕ (MeasurableSpace.pi : MeasurableSpace (ℕ → 𝓧))} + (hℱ : ∀ n, ∃ N, ℱ n ≤ Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) N) {M : ℕ → (ℕ → 𝓧) → ℝ≥0∞} + (hM : IsTestMartingale M ℱ ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁)) + (hM0 : ∀ P ∈ S₁, ∫⁻ ω, M 0 ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) = 1) : + ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ Q₁), limsup (fun n ↦ M n ω) atTop < ∞ := + (isTestMartingale_infinitePi_of_add_sum_eq_sum hS₁ hP hQ₁ hℱ hM + hM0).isTestSupermartingale.ae_limsup_lt_top (Set.mem_singleton _) + +/-! ### Convexity is needed -/ + +/-- The process of the counterexample: `1` while the observations up to time `n` all equal the +first one, and `2 ^ n` once two different values have been seen. -/ +private noncomputable def doublingProcess (n : ℕ) (ω : ℕ → Bool) : ℝ≥0∞ := + if ∀ i ≤ n, ω i = ω 0 then 1 else 2 ^ n + +/-- The doubling process equals `1` on constant sequences. -/ +private lemma doublingProcess_const (n : ℕ) (x : Bool) : doublingProcess n (fun _ ↦ x) = 1 := by + simp [doublingProcess] + +/-- The doubling process is a test martingale for the i.i.d. laws of the two point masses on +`Bool`: under each of them the observations are almost surely constant and the process stays at +`1`. -/ +private lemma isTestMartingale_doublingProcess : + IsTestMartingale doublingProcess (Filtration.piLE (X := fun _ : ℕ ↦ Bool)) + ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' + {Measure.dirac false, Measure.dirac true}) := by + have hmem : ∀ μ ∈ ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' + {Measure.dirac false, Measure.dirac true}), ∃ x : Bool, μ = Measure.dirac (fun _ ↦ x) := by + rintro μ ⟨P, hP, rfl⟩ + rcases hP with rfl | rfl + · exact ⟨false, Measure.infinitePi_dirac (fun _ ↦ false)⟩ + · exact ⟨true, Measure.infinitePi_dirac (fun _ ↦ true)⟩ + have hadapted : Adapted (Filtration.piLE (X := fun _ : ℕ ↦ Bool)) doublingProcess := by + intro n + rw [Filtration.piLE_eq_comap_frestrictLe] + have h : doublingProcess n = (fun y : (Finset.Iic n → Bool) ↦ + if ∀ i : Finset.Iic n, y i = y ⟨0, Finset.mem_Iic.2 n.zero_le⟩ then (1 : ℝ≥0∞) + else 2 ^ n) ∘ Preorder.frestrictLe n := by + ext ω + simp only [doublingProcess, Function.comp_apply, Preorder.frestrictLe, Finset.restrict, + Subtype.forall, Finset.mem_Iic] + exact if_congr Iff.rfl rfl rfl + rw [h] + exact (measurable_of_finite _).comp (comap_measurable _) + refine ⟨hadapted, fun μ hμ ↦ ?_, fun μ hμ n s hs ↦ ?_⟩ + · obtain ⟨x, rfl⟩ := hmem μ hμ + rw [lintegral_dirac, doublingProcess_const] + · obtain ⟨x, rfl⟩ := hmem μ hμ + classical + rw [restrict_dirac' (Filtration.le _ n s hs)] + split_ifs + · rw [lintegral_dirac, lintegral_dirac, doublingProcess_const, doublingProcess_const] + · simp + +/-- Under i.i.d. fair coin flips, two different values appear almost surely. -/ +private lemma ae_exists_ne_infinitePi_coin : ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ + (2⁻¹ : ℝ≥0∞) • (Measure.dirac false + Measure.dirac true)), ∃ i, ω i ≠ ω 0 := by + have : IsProbabilityMeasure ((2⁻¹ : ℝ≥0∞) • (Measure.dirac false + Measure.dirac true)) := + ⟨by simp [ENNReal.inv_two_add_inv_two]⟩ + -- a constant sequence has probability at most `2⁻¹ ^ n` for every `n`, hence `0` + have hconst (x : Bool) : Measure.infinitePi (fun _ : ℕ ↦ + (2⁻¹ : ℝ≥0∞) • (Measure.dirac false + Measure.dirac true)) {fun _ ↦ x} = 0 := by + have hx : ((2⁻¹ : ℝ≥0∞) • (Measure.dirac false + Measure.dirac true)) {x} = 2⁻¹ := by + cases x <;> simp + have hle (n : ℕ) : Measure.infinitePi (fun _ : ℕ ↦ + (2⁻¹ : ℝ≥0∞) • (Measure.dirac false + Measure.dirac true)) {fun _ ↦ x} ≤ 2⁻¹ ^ n := by + calc _ ≤ Measure.infinitePi (fun _ : ℕ ↦ + (2⁻¹ : ℝ≥0∞) • (Measure.dirac false + Measure.dirac true)) + (Set.pi (Finset.range n : Set ℕ) fun _ ↦ {x}) := measure_mono fun ω hω ↦ by simp_all + _ = 2⁻¹ ^ n := by + rw [Measure.infinitePi_pi _ fun _ _ ↦ measurableSet_singleton x, hx, Finset.prod_const, + Finset.card_range] + exact le_antisymm (ge_of_tendsto' (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one + (by norm_num)) hle) bot_le + refine measure_mono_null (fun ω hω ↦ ?_) (measure_union_null (hconst false) (hconst true)) + simp only [Set.mem_compl_iff, Set.mem_ofPred_eq, not_exists, not_not] at hω + have hω' : ω = fun _ ↦ ω 0 := funext hω + cases h : ω 0 + · exact Or.inl (hω'.trans (by rw [h])) + · exact Or.inr (hω'.trans (by rw [h])) + +/-- Once two different values have been seen, the doubling process tends to `∞`. -/ +private lemma tendsto_doublingProcess {ω : ℕ → Bool} (hω : ∃ i, ω i ≠ ω 0) : + Tendsto (fun n ↦ doublingProcess n ω) atTop (𝓝 ∞) := by + obtain ⟨i, hi⟩ := hω + refine (ENNReal.tendsto_pow_atTop_nhds_top_iff.2 (by norm_num : (1 : ℝ≥0∞) < 2)).congr' ?_ + filter_upwards [eventually_ge_atTop i] with n hn + rw [doublingProcess, ite_eq_right fun h ↦ hi (h i hn)] + +/-- **Convexity is needed.** For the null of the two point masses on `Bool`, whose midpoint is the +fair coin, some test martingale for the i.i.d. null with initial value `1`, for the filtration of +the observations, tends to `∞` almost surely under i.i.d. fair coin flips. -/ +theorem exists_isTestMartingale_dirac_tendsto_top : + ∃ M : ℕ → (ℕ → Bool) → ℝ≥0∞, M 0 = 1 ∧ + IsTestMartingale M (Filtration.piLE (X := fun _ : ℕ ↦ Bool)) + ((fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' + {Measure.dirac false, Measure.dirac true}) ∧ + ∀ᵐ ω ∂Measure.infinitePi (fun _ : ℕ ↦ + (2⁻¹ : ℝ≥0∞) • (Measure.dirac false + Measure.dirac true)), + Tendsto (fun n ↦ M n ω) atTop (𝓝 ∞) := + ⟨doublingProcess, funext fun ω ↦ by simp [doublingProcess], isTestMartingale_doublingProcess, + ae_exists_ne_infinitePi_coin.mono fun _ ↦ tendsto_doublingProcess⟩ + +end ProbabilityTheory From c2cfc5fef671f74308abaf6c44f81cce42aa12f2 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:13:02 +0100 Subject: [PATCH 2/4] refactor: expose the mixture and convexity helpers and credit [EVR26, Note 03] MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Move the generic product-of-mixtures lemmas to `MeasureTheory/Constructions/Pi.lean` (`Measure.pi_const_smul`, `Measure.pi_sum_smul`, `Measure.lintegral_pi_sum_smul`), the finite convex combinations over `ℝ≥0∞` to `Analysis/Convex/ENNReal.lean` (`Finset.sum_smul_eq_smul_sum_div_smul`, `Convex.sum_nnreal_smul_mem`) and `MeasureTheory.isProbabilityMeasure_sum_smul` to `MeasureTheory/Measure/ProbabilityMeasure/Convex.lean`, all public. Split the identity-theorem step of the polarization proof into its own lemma, and cite [EVR26, Note 03] and the adapted paper-project file. Co-Authored-By: Claude Code --- LMLExplore/Analysis/Convex/ENNReal.lean | 63 ++++++ .../EValues/PowerOne/TestMartingale.lean | 205 +++++++----------- .../MeasureTheory/Constructions/Pi.lean | 43 +++- .../Measure/ProbabilityMeasure/Convex.lean | 38 ++++ 4 files changed, 222 insertions(+), 127 deletions(-) create mode 100644 LMLExplore/Analysis/Convex/ENNReal.lean create mode 100644 LMLExplore/MeasureTheory/Measure/ProbabilityMeasure/Convex.lean diff --git a/LMLExplore/Analysis/Convex/ENNReal.lean b/LMLExplore/Analysis/Convex/ENNReal.lean new file mode 100644 index 00000000..1bec6876 --- /dev/null +++ b/LMLExplore/Analysis/Convex/ENNReal.lean @@ -0,0 +1,63 @@ +/- +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 Mathlib.Algebra.BigOperators.Field +public import Mathlib.Analysis.Convex.Basic +public import Mathlib.Basic.ENNReal.Action +public import Mathlib.Basic.ENNReal.Inv + +/-! +# Finite convex combinations for convexity over `ℝ≥0∞` + +Convex sets of measures are stated with Mathlib's `Convex ℝ≥0∞`, for which Mathlib's +`Convex.sum_mem` does not apply: it needs a field of scalars acting on an additive group. This file +proves that such a convex set contains the finite convex combinations of its members with weights +in `ℝ≥0`, acting through the coercion `ℝ≥0 → ℝ≥0∞` (Mathlib's `ENNReal.smul_def`). + +## Main statements + +* `Finset.sum_smul_eq_smul_sum_div_smul`: a combination with weights of nonzero sum is that sum + times the normalized combination. +* `Convex.sum_nnreal_smul_mem`: a set convex over `ℝ≥0∞` contains the finite combinations of its + members with weights in `ℝ≥0` of sum `1`. +-/ + +public section + +open scoped ENNReal NNReal + +/-- A combination with weights of nonzero sum is that sum times the convex combination of the same +points with the normalized weights. -/ +lemma Finset.sum_smul_eq_smul_sum_div_smul {𝕜 E ι : Type*} [Semifield 𝕜] [AddCommMonoid E] + [Module 𝕜 E] {T : Finset ι} {x : ι → E} {w : ι → 𝕜} (hw : ∑ i ∈ T, w i ≠ 0) : + ∑ i ∈ T, w i • x i = (∑ i ∈ T, w i) • ∑ i ∈ T, (w i / ∑ j ∈ T, w j) • x i := by + rw [Finset.smul_sum] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + rw [smul_smul, mul_div_cancel₀ _ hw] + +/-- A set convex over `ℝ≥0∞` contains the finite combinations of its members with weights in +`ℝ≥0` of sum `1`, the weights acting through the coercion `ℝ≥0 → ℝ≥0∞`. -/ +lemma Convex.sum_nnreal_smul_mem {E ι : Type*} [AddCommMonoid E] [Module ℝ≥0∞ E] {S : Set E} + (hS : Convex ℝ≥0∞ S) {T : Finset ι} {w : ι → ℝ≥0} (hw : ∑ i ∈ T, w i = 1) {x : ι → E} + (hx : ∀ i ∈ T, x i ∈ S) : ∑ i ∈ T, w i • x i ∈ S := by + classical + induction T using Finset.induction_on generalizing w with + | empty => simp at hw + | insert a T ha ih => + rw [Finset.sum_insert ha] at hw ⊢ + have hxa := hx a (Finset.mem_insert_self a T) + have hxT : ∀ i ∈ T, x i ∈ S := fun i hi ↦ hx i (Finset.mem_insert_of_mem hi) + rcases eq_or_ne (∑ i ∈ T, w i) 0 with h0 | h0 + · rw [h0, add_zero] at hw + rw [Finset.sum_eq_zero fun i hi ↦ by rw [Finset.sum_eq_zero_iff.1 h0 i hi, zero_smul], + add_zero, hw, one_smul] + exact hxa + · rw [Finset.sum_smul_eq_smul_sum_div_smul h0] + have h := hS hxa (ih (w := fun i ↦ w i / ∑ j ∈ T, w j) ?_ hxT) zero_le zero_le + (show (w a : ℝ≥0∞) + ((∑ i ∈ T, w i : ℝ≥0) : ℝ≥0∞) = 1 by exact_mod_cast hw) + · rwa [← ENNReal.smul_def, ← ENNReal.smul_def] at h + · rw [← Finset.sum_div, div_self h0] diff --git a/LMLExplore/EValues/PowerOne/TestMartingale.lean b/LMLExplore/EValues/PowerOne/TestMartingale.lean index 2744008e..0be7e3ca 100644 --- a/LMLExplore/EValues/PowerOne/TestMartingale.lean +++ b/LMLExplore/EValues/PowerOne/TestMartingale.lean @@ -8,6 +8,9 @@ module public import LMLExplore.EValues.TestSupermartingale public import Mathlib.Analysis.Convex.Basic public import Mathlib.Probability.ProductMeasure +import LMLExplore.Analysis.Convex.ENNReal +import LMLExplore.MeasureTheory.Constructions.Pi +import LMLExplore.MeasureTheory.Measure.ProbabilityMeasure.Convex import LMLExplore.Probability.Martingale.OptionalStopping import Mathlib.Analysis.Analytic.Constructions import Mathlib.Analysis.Analytic.Uniqueness @@ -22,17 +25,17 @@ and Wang conjecture that if a test martingale for the i.i.d. null has power one law of `Q₁`, then `Q₁` lies outside the linear span of `S₁`, perhaps under additional conditions [ZRW24, §7]. -For a convex `S₁` this holds, for every filtration each of whose σ-algebras depends on finitely -many observations. Let `Q₁` be a probability measure in the linear span of `S₁`, written as -`Q₁ + ∑ i, b i • P i = ∑ i, c i • P i` with finitely many `P i ∈ S₁` and `b i, c i ≥ 0`. Then every -test martingale for the i.i.d. null whose initial value has expectation `1` under the null is a -test martingale under the i.i.d. law of `Q₁`. In particular its `limsup` is almost surely finite -under that law: it does not have power one against `Q₁`. +For a convex `S₁` this holds [EVR26, Note 03, Theorem 1], for every filtration each of whose +σ-algebras depends on finitely many observations. Let `Q₁` be a probability measure in the linear +span of `S₁`, written as `Q₁ + ∑ i, b i • P i = ∑ i, c i • P i` with finitely many `P i ∈ S₁` and +`b i, c i ≥ 0`. Then every test martingale for the i.i.d. null whose initial value has expectation +`1` under the null is a test martingale under the i.i.d. law of `Q₁`. In particular its `limsup` +is almost surely finite under that law: it does not have power one against `Q₁`. Convexity is needed. For the null of the two point masses on `Bool`, the fair coin is the midpoint of the null, yet the process equal to `1` while all observations agree, and to `2 ^ n` at time `n` once two different ones have been seen, is a test martingale for the i.i.d. null that tends to `∞` -almost surely under i.i.d. fair coin flips. +almost surely under i.i.d. fair coin flips [EVR26, Note 03, Counterexample 1]. ## Main statements @@ -56,10 +59,18 @@ positive multiple of a convex combination of the `P i`, which lies in the null, of the martingale hold for these `t`. By the identity theorem for analytic functions they hold at `t = 0`, that is under `Q₁`. +The statements and proofs are adapted from `EValuesResearch/Results/TestMartingaleConverse.lean` +(commit `6f05c5f`) in the paper project `RemyDegenne/evalues_research`, which formalizes +[EVR26, Note 03] (`results/03-test-martingale-converse.md` there). + ## References * [ZRW24] Z. Zhang, A. Ramdas and R. Wang, *On the existence of powerful p-values and e-values for composite hypotheses*, Ann. Statist. 52 (2024), arXiv:2305.16539: §7. +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, notes 01 to 34 and + the Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026; written and + refereed by AI agents: Note 03, *Converse of the power-one theorem for test martingales*, + Theorem 1 and Counterexample 1. -/ public section @@ -71,73 +82,49 @@ namespace ProbabilityTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} -/-! ### Mixtures and their products -/ - -/-- A combination of measures with nonnegative weights of nonzero sum is that sum times a convex -combination of the same measures. -/ -private lemma sum_smul_eq_smul_sum_div_smul {ι : Type*} {T : Finset ι} {P : ι → Measure 𝓧} - {w : ι → ℝ≥0} (hw : ∑ i ∈ T, w i ≠ 0) : - ∑ i ∈ T, w i • P i = (∑ i ∈ T, w i) • ∑ i ∈ T, (w i / ∑ j ∈ T, w j) • P i := by - rw [Finset.smul_sum] - refine Finset.sum_congr rfl fun i _ ↦ ?_ - rw [smul_smul, mul_div_cancel₀ _ hw] - -/-- A convex set of measures contains the convex combinations of finitely many of its members. -/ -private lemma sum_smul_mem_of_convex {S : Set (Measure 𝓧)} (hS : Convex ℝ≥0∞ S) {ι : Type*} - {P : ι → Measure 𝓧} {T : Finset ι} (hP : ∀ i ∈ T, P i ∈ S) {w : ι → ℝ≥0} - (hw : ∑ i ∈ T, w i = 1) : ∑ i ∈ T, w i • P i ∈ S := by - classical - induction T using Finset.induction_on generalizing w with - | empty => simp at hw - | insert a T ha ih => - rw [Finset.sum_insert ha] at hw ⊢ - have hPa := hP a (Finset.mem_insert_self a T) - have hPT : ∀ i ∈ T, P i ∈ S := fun i hi ↦ hP i (Finset.mem_insert_of_mem hi) - rcases eq_or_ne (∑ i ∈ T, w i) 0 with h0 | h0 - · rw [h0, add_zero] at hw - rw [Finset.sum_eq_zero fun i hi ↦ by rw [Finset.sum_eq_zero_iff.1 h0 i hi, zero_smul], - add_zero, hw, one_smul] - exact hPa - · rw [sum_smul_eq_smul_sum_div_smul h0] - have h := hS hPa (ih hPT (w := fun i ↦ w i / ∑ j ∈ T, w j) ?_) zero_le zero_le - (show (w a : ℝ≥0∞) + ((∑ i ∈ T, w i : ℝ≥0) : ℝ≥0∞) = 1 by exact_mod_cast hw) - · rwa [Measure.coe_nnreal_smul, Measure.coe_nnreal_smul] at h - · rw [← Finset.sum_div, div_self h0] - -/-- A combination of probability measures with weights of sum `1` is a probability measure. -/ -private lemma isProbabilityMeasure_sum_smul {ι : Type*} [Fintype ι] {P : ι → Measure 𝓧} - [∀ i, IsProbabilityMeasure (P i)] {w : ι → ℝ≥0} (hw : ∑ i, w i = 1) : - IsProbabilityMeasure (∑ i, w i • P i) := by - constructor - simp only [sum_apply, smul_apply, measure_univ, ENNReal.smul_one] - exact_mod_cast hw - -/-- The integral of a function of finitely many observations under the product of copies of a -mixture of finite measures is a polynomial in the weights, whose coefficients are its integrals -under the products of the components. -/ -private lemma lintegral_pi_sum_smul {J κ : Type*} [Fintype J] [DecidableEq J] [Fintype κ] - {R : κ → Measure 𝓧} [∀ k, IsFiniteMeasure (R k)] (w : κ → ℝ≥0) (F : (J → 𝓧) → ℝ≥0∞) : - ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ ∑ k, w k • R k) = - ∑ e : J → κ, (∏ j, (w (e j) : ℝ≥0∞)) * ∫⁻ x, F x ∂Measure.pi (fun j ↦ R (e j)) := by - have h : Measure.pi (fun _ : J ↦ ∑ k, w k • R k) = - ∑ e : J → κ, (∏ j, (w (e j) : ℝ≥0∞)) • Measure.pi (fun j ↦ R (e j)) := by - refine Measure.pi_eq fun A hA ↦ ?_ - simp only [sum_apply, smul_apply, Measure.pi_pi, smul_eq_mul, Measure.nnreal_smul_coe_apply, - Fintype.prod_sum, Finset.prod_mul_distrib] - rw [h] - simp only [lintegral_finsetSum_measure, lintegral_smul_measure, smul_eq_mul] - -/-- The product of copies of a multiple `s • ν` of a finite measure is `s ^ card J` times the -product of copies of `ν`. -/ -private lemma pi_const_smul {J : Type*} [Fintype J] (ν : Measure 𝓧) [IsFiniteMeasure ν] - (s : ℝ≥0) : - Measure.pi (fun _ : J ↦ s • ν) = s ^ Fintype.card J • Measure.pi (fun _ : J ↦ ν) := by - refine Measure.pi_eq fun A hA ↦ ?_ - simp only [smul_apply, Measure.pi_pi, Finset.prod_mul_distrib, Finset.prod_const, - Finset.card_univ, ENNReal.smul_def, smul_eq_mul, ENNReal.coe_pow] - /-! ### Polarization -/ +/-- **Identity theorem for the polynomials of the polarization.** Two families `a` and `a'` of +finite coefficients indexed by `J → Bool` whose polynomials +`t ↦ ∑ e, (∏ j, bif e j then t else 1) * a e` agree for every `t > 1` agree for every `t ≥ 0`. -/ +private lemma sum_prod_bif_mul_eq_of_one_lt {J : Type*} [Fintype J] [DecidableEq J] + {a a' : (J → Bool) → ℝ≥0∞} (ha : ∀ e, a e ≠ ∞) (ha' : ∀ e, a' e ≠ ∞) + (h : ∀ t : ℝ≥0, 1 < t → ∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * a e = + ∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * a' e) (t : ℝ≥0) : + ∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * a e = + ∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * a' e := by + have hfin (c : (J → Bool) → ℝ≥0∞) (hc : ∀ e, c e ≠ ∞) (t : ℝ≥0) (e : J → Bool) : + (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * c e ≠ ∞ := + ENNReal.mul_ne_top (ENNReal.prod_ne_top fun _ _ ↦ ENNReal.coe_ne_top) (hc e) + -- the real polynomials + set φ : ((J → Bool) → ℝ≥0∞) → ℝ → ℝ := + fun c x ↦ ∑ e : J → Bool, (∏ j, bif e j then x else 1) * (c e).toReal + have hφ_eq (c : (J → Bool) → ℝ≥0∞) (hc : ∀ e, c e ≠ ∞) (t : ℝ≥0) : + φ c t = (∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * c e).toReal := by + rw [ENNReal.toReal_sum fun e _ ↦ hfin c hc t e] + refine Finset.sum_congr rfl fun e _ ↦ ?_ + rw [ENNReal.toReal_mul, ENNReal.toReal_prod] + congr 1 + refine Finset.prod_congr rfl fun j _ ↦ ?_ + cases e j <;> simp + have han (c : (J → Bool) → ℝ≥0∞) : AnalyticOnNhd ℝ (φ c) Set.univ := fun x _ ↦ + Finset.analyticAt_fun_sum _ fun e _ ↦ (Finset.analyticAt_fun_prod _ fun j _ ↦ by + cases e j + · exact analyticAt_const + · exact analyticAt_id).mul analyticAt_const + -- they agree on `(1, ∞)`, hence everywhere + have hφ : φ a = φ a' := (han a).eq_of_eventuallyEq (han a') (z₀ := 2) <| by + filter_upwards [lt_mem_nhds (by norm_num : (1 : ℝ) < 2)] with x hx + have hx' : (x.toNNReal : ℝ) = x := Real.coe_toNNReal _ (by linarith) + have h1 : 1 < x.toNNReal := by + rw [← NNReal.coe_lt_coe, hx', NNReal.coe_one] + exact hx + rw [← hx', hφ_eq a ha, hφ_eq a' ha', h _ h1] + have ht := congrFun hφ t + rw [hφ_eq a ha, hφ_eq a' ha'] at ht + exact (ENNReal.toReal_eq_toReal_iff' (ENNReal.sum_ne_top.2 fun e _ ↦ hfin a ha t e) + (ENNReal.sum_ne_top.2 fun e _ ↦ hfin a' ha' t e)).1 ht + /-- **Polarization.** Let `Q` be a probability measure and `P i` finite measures with `Q + ∑ i, b i • P i = ∑ i, c i • P i`. If two functions of the observations indexed by a finite type `J` have equal integrals under the product of copies of every convex combination of the @@ -155,19 +142,18 @@ private lemma lintegral_pi_eq_of_add_sum_eq_sum {J ι : Type*} [Fintype J] [Fint ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ Q) = ∫⁻ x, G x ∂Measure.pi (fun _ : J ↦ Q) := by classical set B := ∑ i, b i • P i with hB - -- `Q + t • B` as the mixture of `R true = B` and `R false = Q` with weights `w t` + -- `Q + t • B` as the mixture of `R true = B` and `R false = Q` with weights `t` and `1` set R : Bool → Measure 𝓧 := fun k ↦ bif k then B else Q with hR have : IsFiniteMeasure B := by rw [hB]; infer_instance have : ∀ k, IsFiniteMeasure (R k) := fun k ↦ by cases k <;> simp only [hR, Bool.cond_false, Bool.cond_true] <;> infer_instance - set w : ℝ≥0 → Bool → ℝ≥0 := fun t k ↦ bif k then t else 1 with hw set α : ((J → 𝓧) → ℝ≥0∞) → (J → Bool) → ℝ≥0∞ := fun H e ↦ ∫⁻ x, H x ∂Measure.pi (fun j ↦ R (e j)) have hpoly (H : (J → 𝓧) → ℝ≥0∞) (t : ℝ≥0) : ∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + t • B) = - ∑ e : J → Bool, (∏ j, (w t (e j) : ℝ≥0∞)) * α H e := by - have hmix : Q + t • B = ∑ k, w t k • R k := by simp [hw, hR, add_comm] - rw [hmix, lintegral_pi_sum_smul] + ∑ e : J → Bool, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * α H e := by + have hmix : Q + t • B = ∑ k, (bif k then t else 1 : ℝ≥0) • R k := by simp [hR, add_comm] + rw [hmix, Measure.lintegral_pi_sum_smul] -- for `t ≥ 1`, `Q + t • B` is a positive multiple of a convex combination of the `P i` have hgood (t : ℝ≥0) (ht : 1 ≤ t) : ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ Q + t • B) = @@ -189,57 +175,24 @@ private lemma lintegral_pi_eq_of_add_sum_eq_sum {J ι : Type*} [Fintype J] [Fint simp at h' have hv : ∑ i, (c i + (t - 1) * b i) / ∑ j, (c j + (t - 1) * b j) = 1 := by rw [← Finset.sum_div, div_self hs] - rw [hμ, sum_smul_eq_smul_sum_div_smul hs, pi_const_smul, lintegral_smul_measure, - lintegral_smul_measure, hFG _ hv] + rw [hμ, Finset.sum_smul_eq_smul_sum_div_smul hs, Measure.pi_const_smul, + lintegral_smul_measure, lintegral_smul_measure, hFG _ hv] refine ⟨rfl, ?_⟩ rw [ENNReal.smul_def, smul_eq_mul, ← hFG _ hv] exact ENNReal.mul_ne_top ENNReal.coe_ne_top (hF _ hv) - -- the coefficients of the polynomials are finite + -- the coefficients of the polynomials are finite, as the case `t = 1` shows have hα_ne (H : (J → 𝓧) → ℝ≥0∞) (hH : ∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + (1 : ℝ≥0) • B) ≠ ∞) (e : J → Bool) : α H e ≠ ∞ := by - have hw1 (k : Bool) : w 1 k = 1 := by cases k <;> rfl + have hw1 (k : Bool) : (bif k then (1 : ℝ≥0) else 1) = 1 := by cases k <;> rfl rw [hpoly] at hH simp only [hw1, ENNReal.coe_one, Finset.prod_const_one, one_mul] at hH exact ENNReal.sum_ne_top.1 hH e (Finset.mem_univ e) - have hαF := hα_ne F (hgood 1 le_rfl).2 - have hαG := hα_ne G ((hgood 1 le_rfl).1 ▸ (hgood 1 le_rfl).2) - have hfin (H : (J → 𝓧) → ℝ≥0∞) (hH : ∀ e, α H e ≠ ∞) (t : ℝ≥0) : - ∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + t • B) ≠ ∞ := by - rw [hpoly] - exact ENNReal.sum_ne_top.2 fun e _ ↦ - ENNReal.mul_ne_top (ENNReal.prod_ne_top fun _ _ ↦ ENNReal.coe_ne_top) (hH e) - -- the real polynomials - set φ : ((J → 𝓧) → ℝ≥0∞) → ℝ → ℝ := - fun H x ↦ ∑ e : J → Bool, (∏ j, bif e j then x else 1) * (α H e).toReal - have hφ_eq (H : (J → 𝓧) → ℝ≥0∞) (hH : ∀ e, α H e ≠ ∞) (t : ℝ≥0) : - φ H t = (∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + t • B)).toReal := by - rw [hpoly, ENNReal.toReal_sum fun e _ ↦ - ENNReal.mul_ne_top (ENNReal.prod_ne_top fun _ _ ↦ ENNReal.coe_ne_top) (hH e)] - refine Finset.sum_congr rfl fun e _ ↦ ?_ - rw [ENNReal.toReal_mul, ENNReal.toReal_prod] - congr 1 - refine Finset.prod_congr rfl fun j _ ↦ ?_ - cases e j <;> simp [hw] - have han (H : (J → 𝓧) → ℝ≥0∞) : AnalyticOnNhd ℝ (φ H) Set.univ := fun x _ ↦ - Finset.analyticAt_fun_sum _ fun e _ ↦ (Finset.analyticAt_fun_prod _ fun j _ ↦ by - cases e j - · exact analyticAt_const - · exact analyticAt_id).mul analyticAt_const - -- they agree on `(1, ∞)`, hence everywhere - have hφFG : φ F = φ G := (han F).eq_of_eventuallyEq (han G) (z₀ := 2) <| by - filter_upwards [lt_mem_nhds (by norm_num : (1 : ℝ) < 2)] with x hx - have hx' : (x.toNNReal : ℝ) = x := Real.coe_toNNReal _ (by linarith) - have h1 : 1 ≤ x.toNNReal := by - rw [← NNReal.coe_le_coe, hx', NNReal.coe_one] - exact hx.le - rw [← hx', hφ_eq F hαF, hφ_eq G hαG, (hgood _ h1).1] - have h0 : φ F ((0 : ℝ≥0) : ℝ) = φ G ((0 : ℝ≥0) : ℝ) := by rw [hφFG] - rw [hφ_eq F hαF, hφ_eq G hαG] at h0 - have hF0 := hfin F hαF 0 - have hG0 := hfin G hαG 0 - simp only [zero_smul, add_zero] at h0 hF0 hG0 - exact (ENNReal.toReal_eq_toReal_iff' hF0 hG0).1 h0 + obtain ⟨h1eq, h1ne⟩ := hgood 1 le_rfl + have h0 := sum_prod_bif_mul_eq_of_one_lt (hα_ne F h1ne) (hα_ne G (by rwa [← h1eq])) + (fun t ht ↦ by rw [← hpoly, ← hpoly]; exact (hgood t ht.le).1) 0 + rw [← hpoly, ← hpoly] at h0 + simpa only [zero_smul, add_zero] using h0 /-- **Polarization for i.i.d. laws.** Let `Q` be a probability measure and `P i` probability measures with `Q + ∑ i, b i • P i = ∑ i, c i • P i`. If two functions of the first `N + 1` @@ -280,9 +233,9 @@ be a convex set of measures and `Q₁` a probability measure in its linear span, `Q₁ + ∑ i, b i • P i = ∑ i, c i • P i` with finitely many probability measures `P i ∈ S₁`. Let `ℱ` be a filtration each of whose σ-algebras depends on finitely many observations. Then a test martingale for the i.i.d. laws of the members of `S₁` whose initial value has expectation `1` -under each of them is a test martingale for the i.i.d. law of `Q₁`. This proves, for convex nulls, -the conjecture of [ZRW24, §7] that a test martingale with power one against `Q₁` forces `Q₁` out -of the linear span of the null. -/ +under each of them is a test martingale for the i.i.d. law of `Q₁` [EVR26, Note 03, Theorem 1]. +This proves, for convex nulls, the conjecture of [ZRW24, §7] that a test martingale with power one +against `Q₁` forces `Q₁` out of the linear span of the null. -/ theorem isTestMartingale_infinitePi_of_add_sum_eq_sum {S₁ : Set (Measure 𝓧)} (hS₁ : Convex ℝ≥0∞ S₁) {ι : Type*} [Fintype ι] {P : ι → Measure 𝓧} [∀ i, IsProbabilityMeasure (P i)] (hP : ∀ i, P i ∈ S₁) {b c : ι → ℝ≥0} {Q₁ : Measure 𝓧} @@ -293,7 +246,7 @@ theorem isTestMartingale_infinitePi_of_add_sum_eq_sum {S₁ : Set (Measure 𝓧) (hM0 : ∀ P ∈ S₁, ∫⁻ ω, M 0 ω ∂Measure.infinitePi (fun _ : ℕ ↦ P) = 1) : IsTestMartingale M ℱ {Measure.infinitePi fun _ : ℕ ↦ Q₁} := by have hmem (w : ι → ℝ≥0) (hw : ∑ i, w i = 1) : ∑ i, w i • P i ∈ S₁ := - sum_smul_mem_of_convex hS₁ (fun i _ ↦ hP i) hw + hS₁.sum_nnreal_smul_mem hw fun i _ ↦ hP i have hnull (w : ι → ℝ≥0) (hw : ∑ i, w i = 1) : Measure.infinitePi (fun _ : ℕ ↦ ∑ i, w i • P i) ∈ (fun P ↦ Measure.infinitePi fun _ : ℕ ↦ P) '' S₁ := ⟨_, hmem w hw, rfl⟩ @@ -329,7 +282,8 @@ theorem isTestMartingale_infinitePi_of_add_sum_eq_sum {S₁ : Set (Measure 𝓧) /-- **No power one against the linear span of a convex i.i.d. null.** Under the hypotheses of `isTestMartingale_infinitePi_of_add_sum_eq_sum`, the test martingale has an almost surely finite -`limsup` under the i.i.d. law of `Q₁`: it does not have power one against `Q₁`. -/ +`limsup` under the i.i.d. law of `Q₁`: it does not have power one against `Q₁` +[EVR26, Note 03, Theorem 1]. -/ theorem ae_limsup_lt_top_infinitePi_of_add_sum_eq_sum {S₁ : Set (Measure 𝓧)} (hS₁ : Convex ℝ≥0∞ S₁) {ι : Type*} [Fintype ι] {P : ι → Measure 𝓧} [∀ i, IsProbabilityMeasure (P i)] (hP : ∀ i, P i ∈ S₁) {b c : ι → ℝ≥0} {Q₁ : Measure 𝓧} @@ -425,7 +379,8 @@ private lemma tendsto_doublingProcess {ω : ℕ → Bool} (hω : ∃ i, ω i ≠ /-- **Convexity is needed.** For the null of the two point masses on `Bool`, whose midpoint is the fair coin, some test martingale for the i.i.d. null with initial value `1`, for the filtration of -the observations, tends to `∞` almost surely under i.i.d. fair coin flips. -/ +the observations, tends to `∞` almost surely under i.i.d. fair coin flips +[EVR26, Note 03, Counterexample 1]. -/ theorem exists_isTestMartingale_dirac_tendsto_top : ∃ M : ℕ → (ℕ → Bool) → ℝ≥0∞, M 0 = 1 ∧ IsTestMartingale M (Filtration.piLE (X := fun _ : ℕ ↦ Bool)) diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean index cc275003..36a58ec7 100644 --- a/LMLExplore/MeasureTheory/Constructions/Pi.lean +++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean @@ -10,7 +10,7 @@ public import Mathlib.Probability.ConditionalProbability import TauCeti.MeasureTheory.Constructions.Pi /-! -# Product measures: laws of coordinatewise images, restricted factors and bounds by lines +# Product measures: laws of coordinatewise images, restricted factors, mixtures and bounds by lines Under the product measure `Measure.pi μ`, the law of a function `f` of the coordinatewise images `X i (y i)` is the law of `f` under the product of the laws of the `X i`. For example, the law of @@ -20,6 +20,10 @@ mean of independent samples of the law of `X`. Restricting every factor of a product of copies of `μ` to a set `B` of finite positive measure gives the product of the conditional measures `μ[|B]`, scaled by `μ(B)` to the number of factors. +The product of copies of a multiple `s • ν` is `s ^ card ι` times the product of copies of `ν`, and +the product of copies of a finite mixture `∑ k, w k • R k` is the mixture of the products +`Measure.pi (fun i ↦ R (e i))` over the assignments `e : ι → κ`, with weights `∏ i, w (e i)`. + Under a product of probability measures, a measurable set whose lines along one coordinate `i` all have `μ i`-measure at most `c` has product measure at most `c`, by resampling the coordinate `i` and integrating the measures of the lines. @@ -30,6 +34,11 @@ all have `μ i`-measure at most `c` has product measure at most `c`, by resampli `(Measure.pi μ).map (fun y ↦ f fun i ↦ X i (y i)) = (Measure.pi fun i ↦ (μ i).map (X i)).map f`. * `MeasureTheory.Measure.pi_restrict_eq_pow_smul_pi_cond`: `Measure.pi (fun _ ↦ μ.restrict B) = μ B ^ card ι • Measure.pi (fun _ ↦ μ[|B])`. +* `MeasureTheory.Measure.pi_const_smul`: + `Measure.pi (fun _ ↦ s • ν) = s ^ card ι • Measure.pi (fun _ ↦ ν)`. +* `MeasureTheory.Measure.pi_sum_smul`, `MeasureTheory.Measure.lintegral_pi_sum_smul`: + `Measure.pi (fun _ ↦ ∑ k, w k • R k) = ∑ e, (∏ i, w (e i)) • Measure.pi (fun i ↦ R (e i))`, and + the corresponding expansion of integrals. * `MeasureTheory.Measure.pi_eval_preimage_le`: for measures of mass at most `1`, the product measure of the cylinder `{y | y i ∈ s}` is at most `μ i s`, for every set `s`. * `MeasureTheory.Measure.pi_le_of_forall_measure_update_preimage_le`: under a product of @@ -39,7 +48,7 @@ all have `μ i`-measure at most `c` has product measure at most `c`, by resampli public section -open scoped ENNReal +open scoped ENNReal NNReal namespace MeasureTheory.Measure @@ -74,6 +83,36 @@ lemma pi_restrict_eq_pow_smul_pi_cond {α : Type*} {mα : MeasurableSpace α} { rw [cond_apply' (hs i), Measure.restrict_apply (hs i), ← mul_assoc, ENNReal.mul_inv_cancel hB0 hB, one_mul, Set.inter_comm] +/-- The product of copies of a multiple `s • ν` of a σ-finite measure is `s ^ card ι` times the +product of copies of `ν`. -/ +lemma pi_const_smul {α : Type*} {mα : MeasurableSpace α} (ν : Measure α) [SigmaFinite ν] + (s : ℝ≥0) : + Measure.pi (fun _ : ι ↦ s • ν) = s ^ Fintype.card ι • Measure.pi (fun _ : ι ↦ ν) := by + refine Measure.pi_eq fun A hA ↦ ?_ + simp only [smul_apply, Measure.pi_pi, Finset.prod_mul_distrib, Finset.prod_const, + Finset.card_univ, ENNReal.smul_def, smul_eq_mul, ENNReal.coe_pow] + +/-- **Product of copies of a mixture.** The product of copies of a finite mixture +`∑ k, w k • R k` of finite measures is the mixture of the products `Measure.pi (fun i ↦ R (e i))` +over the assignments `e : ι → κ`, with weights `∏ i, w (e i)`. -/ +lemma pi_sum_smul [DecidableEq ι] {α κ : Type*} {mα : MeasurableSpace α} [Fintype κ] + {R : κ → Measure α} [∀ k, IsFiniteMeasure (R k)] (w : κ → ℝ≥0) : + Measure.pi (fun _ : ι ↦ ∑ k, w k • R k) = + ∑ e : ι → κ, (∏ i, (w (e i) : ℝ≥0∞)) • Measure.pi (fun i ↦ R (e i)) := by + refine Measure.pi_eq fun A hA ↦ ?_ + simp only [sum_apply, smul_apply, Measure.pi_pi, smul_eq_mul, Measure.nnreal_smul_coe_apply, + Fintype.prod_sum, Finset.prod_mul_distrib] + +/-- The integral under the product of copies of a finite mixture `∑ k, w k • R k` of finite +measures is a polynomial in the weights: the sum over the assignments `e : ι → κ` of +`∏ i, w (e i)` times the integral under `Measure.pi (fun i ↦ R (e i))`. -/ +lemma lintegral_pi_sum_smul [DecidableEq ι] {α κ : Type*} {mα : MeasurableSpace α} [Fintype κ] + {R : κ → Measure α} [∀ k, IsFiniteMeasure (R k)] (w : κ → ℝ≥0) (F : (ι → α) → ℝ≥0∞) : + ∫⁻ x, F x ∂Measure.pi (fun _ : ι ↦ ∑ k, w k • R k) = + ∑ e : ι → κ, (∏ i, (w (e i) : ℝ≥0∞)) * ∫⁻ x, F x ∂Measure.pi (fun i ↦ R (e i)) := by + rw [pi_sum_smul] + simp only [lintegral_finsetSum_measure, lintegral_smul_measure, smul_eq_mul] + /-- For measures of mass at most `1`, the product measure of the cylinder `eval i ⁻¹' s` of a set `s`, measurable or not, is at most `μ i s`. -/ lemma pi_eval_preimage_le {μ : ∀ i, Measure (Ω i)} [∀ i, IsZeroOrProbabilityMeasure (μ i)] diff --git a/LMLExplore/MeasureTheory/Measure/ProbabilityMeasure/Convex.lean b/LMLExplore/MeasureTheory/Measure/ProbabilityMeasure/Convex.lean new file mode 100644 index 00000000..1886bc21 --- /dev/null +++ b/LMLExplore/MeasureTheory/Measure/ProbabilityMeasure/Convex.lean @@ -0,0 +1,38 @@ +/- +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 Mathlib.MeasureTheory.Measure.Typeclasses.Probability + +/-! +# Finite convex combinations of probability measures + +A combination `∑ i, w i • P i` of finitely many probability measures with weights `w i : ℝ≥0` of +sum `1` is a probability measure. This is the finite form of Tau Ceti's +`TauCeti.MeasureTheory.isProbabilityMeasure_smul_add_smul`, for two measures. + +## Main statements + +* `MeasureTheory.isProbabilityMeasure_sum_smul`: a finite convex combination of probability + measures is a probability measure. +-/ + +public section + +open scoped ENNReal NNReal + +namespace MeasureTheory + +/-- A combination of probability measures with weights in `ℝ≥0` of sum `1` is a probability +measure. -/ +lemma isProbabilityMeasure_sum_smul {α ι : Type*} {mα : MeasurableSpace α} [Fintype ι] + {P : ι → Measure α} [∀ i, IsProbabilityMeasure (P i)] {w : ι → ℝ≥0} (hw : ∑ i, w i = 1) : + IsProbabilityMeasure (∑ i, w i • P i) := by + constructor + simp only [sum_apply, smul_apply, measure_univ, ENNReal.smul_one] + exact_mod_cast hw + +end MeasureTheory From bdb9bffc7a4955433ffefc7228ffd4722b434581 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:45:01 +0100 Subject: [PATCH 3/4] refactor: expose the polarization lemmas and place the supporting lemmas by topic Make the polarization lemmas public as `MeasureTheory.Measure.lintegral_pi_eq_of_add_sum_eq_sum` (in `Constructions/Pi`) and `MeasureTheory.Measure.lintegral_infinitePi_eq_of_add_sum_eq_sum` (in `Probability/ProductMeasure`). Move `Finset.sum_smul_eq_smul_sum_div_smul` to `Algebra/BigOperators/Field` and `isProbabilityMeasure_sum_smul` to `MeasureTheory/Measure/Typeclasses/Probability`. Use `Preorder.frestrictLe_apply` instead of unfolding in the adaptedness of the counterexample. Co-Authored-By: Claude Code --- LMLExplore/Algebra/BigOperators/Field.lean | 33 ++++ LMLExplore/Analysis/Convex/ENNReal.lean | 13 +- .../EValues/PowerOne/TestMartingale.lean | 166 ++---------------- .../MeasureTheory/Constructions/Pi.lean | 120 +++++++++++++ .../Probability.lean} | 0 LMLExplore/Probability/ProductMeasure.lean | 44 +++++ 6 files changed, 209 insertions(+), 167 deletions(-) create mode 100644 LMLExplore/Algebra/BigOperators/Field.lean rename LMLExplore/MeasureTheory/Measure/{ProbabilityMeasure/Convex.lean => Typeclasses/Probability.lean} (100%) diff --git a/LMLExplore/Algebra/BigOperators/Field.lean b/LMLExplore/Algebra/BigOperators/Field.lean new file mode 100644 index 00000000..75bd6982 --- /dev/null +++ b/LMLExplore/Algebra/BigOperators/Field.lean @@ -0,0 +1,33 @@ +/- +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 Mathlib.Algebra.BigOperators.Field +public import Mathlib.Algebra.BigOperators.GroupWithZero.Action +public import Mathlib.Algebra.Module.Defs + +/-! +# Normalizing a finite combination over a semifield + +A finite combination `∑ i ∈ T, w i • x i` with weights in a semifield of nonzero sum is that sum +times the combination with the normalized weights `w i / ∑ j ∈ T, w j`, which sum to `1`. + +## Main statements + +* `Finset.sum_smul_eq_smul_sum_div_smul`: a combination with weights of nonzero sum is that sum + times the normalized combination. +-/ + +public section + +/-- A combination with weights of nonzero sum is that sum times the convex combination of the same +points with the normalized weights. -/ +lemma Finset.sum_smul_eq_smul_sum_div_smul {𝕜 E ι : Type*} [Semifield 𝕜] [AddCommMonoid E] + [Module 𝕜 E] {T : Finset ι} {x : ι → E} {w : ι → 𝕜} (hw : ∑ i ∈ T, w i ≠ 0) : + ∑ i ∈ T, w i • x i = (∑ i ∈ T, w i) • ∑ i ∈ T, (w i / ∑ j ∈ T, w j) • x i := by + rw [Finset.smul_sum] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + rw [smul_smul, mul_div_cancel₀ _ hw] diff --git a/LMLExplore/Analysis/Convex/ENNReal.lean b/LMLExplore/Analysis/Convex/ENNReal.lean index 1bec6876..c1efe2e8 100644 --- a/LMLExplore/Analysis/Convex/ENNReal.lean +++ b/LMLExplore/Analysis/Convex/ENNReal.lean @@ -5,10 +5,10 @@ Authors: LMLExplore contributors -/ module -public import Mathlib.Algebra.BigOperators.Field public import Mathlib.Analysis.Convex.Basic public import Mathlib.Basic.ENNReal.Action public import Mathlib.Basic.ENNReal.Inv +import LMLExplore.Algebra.BigOperators.Field /-! # Finite convex combinations for convexity over `ℝ≥0∞` @@ -20,8 +20,6 @@ in `ℝ≥0`, acting through the coercion `ℝ≥0 → ℝ≥0∞` (Mathlib's `E ## Main statements -* `Finset.sum_smul_eq_smul_sum_div_smul`: a combination with weights of nonzero sum is that sum - times the normalized combination. * `Convex.sum_nnreal_smul_mem`: a set convex over `ℝ≥0∞` contains the finite combinations of its members with weights in `ℝ≥0` of sum `1`. -/ @@ -30,15 +28,6 @@ public section open scoped ENNReal NNReal -/-- A combination with weights of nonzero sum is that sum times the convex combination of the same -points with the normalized weights. -/ -lemma Finset.sum_smul_eq_smul_sum_div_smul {𝕜 E ι : Type*} [Semifield 𝕜] [AddCommMonoid E] - [Module 𝕜 E] {T : Finset ι} {x : ι → E} {w : ι → 𝕜} (hw : ∑ i ∈ T, w i ≠ 0) : - ∑ i ∈ T, w i • x i = (∑ i ∈ T, w i) • ∑ i ∈ T, (w i / ∑ j ∈ T, w j) • x i := by - rw [Finset.smul_sum] - refine Finset.sum_congr rfl fun i _ ↦ ?_ - rw [smul_smul, mul_div_cancel₀ _ hw] - /-- A set convex over `ℝ≥0∞` contains the finite combinations of its members with weights in `ℝ≥0` of sum `1`, the weights acting through the coercion `ℝ≥0 → ℝ≥0∞`. -/ lemma Convex.sum_nnreal_smul_mem {E ι : Type*} [AddCommMonoid E] [Module ℝ≥0∞ E] {S : Set E} diff --git a/LMLExplore/EValues/PowerOne/TestMartingale.lean b/LMLExplore/EValues/PowerOne/TestMartingale.lean index 0be7e3ca..583d2009 100644 --- a/LMLExplore/EValues/PowerOne/TestMartingale.lean +++ b/LMLExplore/EValues/PowerOne/TestMartingale.lean @@ -9,12 +9,9 @@ public import LMLExplore.EValues.TestSupermartingale public import Mathlib.Analysis.Convex.Basic public import Mathlib.Probability.ProductMeasure import LMLExplore.Analysis.Convex.ENNReal -import LMLExplore.MeasureTheory.Constructions.Pi -import LMLExplore.MeasureTheory.Measure.ProbabilityMeasure.Convex +import LMLExplore.MeasureTheory.Measure.Typeclasses.Probability import LMLExplore.Probability.Martingale.OptionalStopping -import Mathlib.Analysis.Analytic.Constructions -import Mathlib.Analysis.Analytic.Uniqueness -import Mathlib.MeasureTheory.Function.FactorsThrough +import LMLExplore.Probability.ProductMeasure /-! # Test martingales for convex i.i.d. nulls have no power against the span of the null @@ -57,7 +54,9 @@ observations for some `N`, so their integrals under `Measure.infinitePi` are int of copies of `Q₁ + t • B` is a polynomial in `t`. For `t ≥ 1`, the measure `Q₁ + t • B` is a positive multiple of a convex combination of the `P i`, which lies in the null, so the identities of the martingale hold for these `t`. By the identity theorem for analytic functions they hold at -`t = 0`, that is under `Q₁`. +`t = 0`, that is under `Q₁`. These polarization steps are +`MeasureTheory.Measure.lintegral_pi_eq_of_add_sum_eq_sum` and its i.i.d. form +`MeasureTheory.Measure.lintegral_infinitePi_eq_of_add_sum_eq_sum`. The statements and proofs are adapted from `EValuesResearch/Results/TestMartingaleConverse.lean` (commit `6f05c5f`) in the paper project `RemyDegenne/evalues_research`, which formalizes @@ -82,150 +81,6 @@ namespace ProbabilityTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} -/-! ### Polarization -/ - -/-- **Identity theorem for the polynomials of the polarization.** Two families `a` and `a'` of -finite coefficients indexed by `J → Bool` whose polynomials -`t ↦ ∑ e, (∏ j, bif e j then t else 1) * a e` agree for every `t > 1` agree for every `t ≥ 0`. -/ -private lemma sum_prod_bif_mul_eq_of_one_lt {J : Type*} [Fintype J] [DecidableEq J] - {a a' : (J → Bool) → ℝ≥0∞} (ha : ∀ e, a e ≠ ∞) (ha' : ∀ e, a' e ≠ ∞) - (h : ∀ t : ℝ≥0, 1 < t → ∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * a e = - ∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * a' e) (t : ℝ≥0) : - ∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * a e = - ∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * a' e := by - have hfin (c : (J → Bool) → ℝ≥0∞) (hc : ∀ e, c e ≠ ∞) (t : ℝ≥0) (e : J → Bool) : - (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * c e ≠ ∞ := - ENNReal.mul_ne_top (ENNReal.prod_ne_top fun _ _ ↦ ENNReal.coe_ne_top) (hc e) - -- the real polynomials - set φ : ((J → Bool) → ℝ≥0∞) → ℝ → ℝ := - fun c x ↦ ∑ e : J → Bool, (∏ j, bif e j then x else 1) * (c e).toReal - have hφ_eq (c : (J → Bool) → ℝ≥0∞) (hc : ∀ e, c e ≠ ∞) (t : ℝ≥0) : - φ c t = (∑ e, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * c e).toReal := by - rw [ENNReal.toReal_sum fun e _ ↦ hfin c hc t e] - refine Finset.sum_congr rfl fun e _ ↦ ?_ - rw [ENNReal.toReal_mul, ENNReal.toReal_prod] - congr 1 - refine Finset.prod_congr rfl fun j _ ↦ ?_ - cases e j <;> simp - have han (c : (J → Bool) → ℝ≥0∞) : AnalyticOnNhd ℝ (φ c) Set.univ := fun x _ ↦ - Finset.analyticAt_fun_sum _ fun e _ ↦ (Finset.analyticAt_fun_prod _ fun j _ ↦ by - cases e j - · exact analyticAt_const - · exact analyticAt_id).mul analyticAt_const - -- they agree on `(1, ∞)`, hence everywhere - have hφ : φ a = φ a' := (han a).eq_of_eventuallyEq (han a') (z₀ := 2) <| by - filter_upwards [lt_mem_nhds (by norm_num : (1 : ℝ) < 2)] with x hx - have hx' : (x.toNNReal : ℝ) = x := Real.coe_toNNReal _ (by linarith) - have h1 : 1 < x.toNNReal := by - rw [← NNReal.coe_lt_coe, hx', NNReal.coe_one] - exact hx - rw [← hx', hφ_eq a ha, hφ_eq a' ha', h _ h1] - have ht := congrFun hφ t - rw [hφ_eq a ha, hφ_eq a' ha'] at ht - exact (ENNReal.toReal_eq_toReal_iff' (ENNReal.sum_ne_top.2 fun e _ ↦ hfin a ha t e) - (ENNReal.sum_ne_top.2 fun e _ ↦ hfin a' ha' t e)).1 ht - -/-- **Polarization.** Let `Q` be a probability measure and `P i` finite measures with -`Q + ∑ i, b i • P i = ∑ i, c i • P i`. If two functions of the observations indexed by a finite -type `J` have equal integrals under the product of copies of every convex combination of the -`P i`, finite for the first function, then they have equal integrals under the product of copies -of `Q`. -/ -private lemma lintegral_pi_eq_of_add_sum_eq_sum {J ι : Type*} [Fintype J] [Fintype ι] - {P : ι → Measure 𝓧} [∀ i, IsFiniteMeasure (P i)] {b c : ι → ℝ≥0} {Q : Measure 𝓧} - [IsProbabilityMeasure Q] (hQ : Q + ∑ i, b i • P i = ∑ i, c i • P i) - {F G : (J → 𝓧) → ℝ≥0∞} - (hFG : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → - ∫⁻ x, F x ∂Measure.pi (fun _ ↦ ∑ i, w i • P i) = - ∫⁻ x, G x ∂Measure.pi (fun _ ↦ ∑ i, w i • P i)) - (hF : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → - ∫⁻ x, F x ∂Measure.pi (fun _ ↦ ∑ i, w i • P i) ≠ ∞) : - ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ Q) = ∫⁻ x, G x ∂Measure.pi (fun _ : J ↦ Q) := by - classical - set B := ∑ i, b i • P i with hB - -- `Q + t • B` as the mixture of `R true = B` and `R false = Q` with weights `t` and `1` - set R : Bool → Measure 𝓧 := fun k ↦ bif k then B else Q with hR - have : IsFiniteMeasure B := by rw [hB]; infer_instance - have : ∀ k, IsFiniteMeasure (R k) := fun k ↦ by - cases k <;> simp only [hR, Bool.cond_false, Bool.cond_true] <;> infer_instance - set α : ((J → 𝓧) → ℝ≥0∞) → (J → Bool) → ℝ≥0∞ := - fun H e ↦ ∫⁻ x, H x ∂Measure.pi (fun j ↦ R (e j)) - have hpoly (H : (J → 𝓧) → ℝ≥0∞) (t : ℝ≥0) : - ∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + t • B) = - ∑ e : J → Bool, (∏ j, ((bif e j then t else 1 : ℝ≥0) : ℝ≥0∞)) * α H e := by - have hmix : Q + t • B = ∑ k, (bif k then t else 1 : ℝ≥0) • R k := by simp [hR, add_comm] - rw [hmix, Measure.lintegral_pi_sum_smul] - -- for `t ≥ 1`, `Q + t • B` is a positive multiple of a convex combination of the `P i` - have hgood (t : ℝ≥0) (ht : 1 ≤ t) : - ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ Q + t • B) = - ∫⁻ x, G x ∂Measure.pi (fun _ : J ↦ Q + t • B) ∧ - ∫⁻ x, F x ∂Measure.pi (fun _ : J ↦ Q + t • B) ≠ ∞ := by - have hμ : Q + t • B = ∑ i, (c i + (t - 1) * b i) • P i := by - calc Q + t • B = (Q + B) + (t - 1) • B := by - conv_lhs => rw [← add_tsub_cancel_of_le ht, add_smul, one_smul] - rw [add_assoc] - _ = ∑ i, (c i + (t - 1) * b i) • P i := by - rw [hQ, hB, Finset.smul_sum, ← Finset.sum_add_distrib] - exact Finset.sum_congr rfl fun i _ ↦ by rw [smul_smul, ← add_smul] - have hs : ∑ i, (c i + (t - 1) * b i) ≠ 0 := by - intro h0 - have h : Q + t • B = 0 := by - rw [hμ] - exact Finset.sum_eq_zero fun i hi ↦ by rw [Finset.sum_eq_zero_iff.1 h0 i hi, zero_smul] - have h' := congrArg (· Set.univ) h - simp at h' - have hv : ∑ i, (c i + (t - 1) * b i) / ∑ j, (c j + (t - 1) * b j) = 1 := by - rw [← Finset.sum_div, div_self hs] - rw [hμ, Finset.sum_smul_eq_smul_sum_div_smul hs, Measure.pi_const_smul, - lintegral_smul_measure, lintegral_smul_measure, hFG _ hv] - refine ⟨rfl, ?_⟩ - rw [ENNReal.smul_def, smul_eq_mul, ← hFG _ hv] - exact ENNReal.mul_ne_top ENNReal.coe_ne_top (hF _ hv) - -- the coefficients of the polynomials are finite, as the case `t = 1` shows - have hα_ne (H : (J → 𝓧) → ℝ≥0∞) - (hH : ∫⁻ x, H x ∂Measure.pi (fun _ : J ↦ Q + (1 : ℝ≥0) • B) ≠ ∞) (e : J → Bool) : - α H e ≠ ∞ := by - have hw1 (k : Bool) : (bif k then (1 : ℝ≥0) else 1) = 1 := by cases k <;> rfl - rw [hpoly] at hH - simp only [hw1, ENNReal.coe_one, Finset.prod_const_one, one_mul] at hH - exact ENNReal.sum_ne_top.1 hH e (Finset.mem_univ e) - obtain ⟨h1eq, h1ne⟩ := hgood 1 le_rfl - have h0 := sum_prod_bif_mul_eq_of_one_lt (hα_ne F h1ne) (hα_ne G (by rwa [← h1eq])) - (fun t ht ↦ by rw [← hpoly, ← hpoly]; exact (hgood t ht.le).1) 0 - rw [← hpoly, ← hpoly] at h0 - simpa only [zero_smul, add_zero] using h0 - -/-- **Polarization for i.i.d. laws.** Let `Q` be a probability measure and `P i` probability -measures with `Q + ∑ i, b i • P i = ∑ i, c i • P i`. If two functions of the first `N + 1` -observations have equal integrals under the i.i.d. law of every convex combination of the `P i`, -finite for the first function, then they have equal integrals under the i.i.d. law of `Q`. -/ -private lemma lintegral_infinitePi_eq_of_add_sum_eq_sum {ι : Type*} [Fintype ι] - {P : ι → Measure 𝓧} [∀ i, IsProbabilityMeasure (P i)] {b c : ι → ℝ≥0} {Q : Measure 𝓧} - [IsProbabilityMeasure Q] (hQ : Q + ∑ i, b i • P i = ∑ i, c i • P i) {N : ℕ} - {f g : (ℕ → 𝓧) → ℝ≥0∞} (hf : Measurable[Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) N] f) - (hg : Measurable[Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) N] g) - (hfg : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → - ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i) = - ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i)) - (hf_ne : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → - ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i) ≠ ∞) : - ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ Q) = ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ ↦ Q) := by - rw [Filtration.piLE_eq_comap_frestrictLe] at hf hg - obtain ⟨f', hf', rfl⟩ := hf.exists_eq_measurable_comp - obtain ⟨g', hg', rfl⟩ := hg.exists_eq_measurable_comp - have h (μ : Measure 𝓧) [IsProbabilityMeasure μ] {H : (Finset.Iic N → 𝓧) → ℝ≥0∞} - (hH : Measurable H) : - ∫⁻ ω, (H ∘ Preorder.frestrictLe N) ω ∂Measure.infinitePi (fun _ ↦ μ) = - ∫⁻ x, H x ∂Measure.pi (fun _ : Finset.Iic N ↦ μ) := - lintegral_restrict_infinitePi _ hH - rw [h Q hf', h Q hg'] - refine lintegral_pi_eq_of_add_sum_eq_sum hQ (fun w hw ↦ ?_) fun w hw ↦ ?_ - · have := isProbabilityMeasure_sum_smul (P := P) hw - rw [← h _ hf', ← h _ hg'] - exact hfg w hw - · have := isProbabilityMeasure_sum_smul (P := P) hw - rw [← h _ hf'] - exact hf_ne w hw - /-! ### Test martingales for convex i.i.d. nulls -/ /-- **Test martingales for a convex i.i.d. null have no power against its linear span.** Let `S₁` @@ -253,7 +108,7 @@ theorem isTestMartingale_infinitePi_of_add_sum_eq_sum {S₁ : Set (Measure 𝓧) refine ⟨hM.adapted, ?_, ?_⟩ · rintro _ rfl obtain ⟨N, hN⟩ := hℱ 0 - refine (lintegral_infinitePi_eq_of_add_sum_eq_sum hQ₁ ((hM.adapted 0).mono hN le_rfl) + refine (Measure.lintegral_infinitePi_eq_of_add_sum_eq_sum hQ₁ ((hM.adapted 0).mono hN le_rfl) (measurable_const (a := (1 : ℝ≥0∞))) (fun w hw ↦ ?_) fun w hw ↦ ?_).trans_le (by simp) · have := isProbabilityMeasure_sum_smul (P := P) hw rw [hM0 _ (hmem w hw)] @@ -269,7 +124,7 @@ theorem isTestMartingale_infinitePi_of_add_sum_eq_sum {S₁ : Set (Measure 𝓧) hN₂.trans (Filtration.mono _ (le_max_right _ _)) have hs' : MeasurableSet s := ℱ.le n s hs rw [← lintegral_indicator hs', ← lintegral_indicator hs'] - refine lintegral_infinitePi_eq_of_add_sum_eq_sum hQ₁ + refine Measure.lintegral_infinitePi_eq_of_add_sum_eq_sum hQ₁ (((hM.adapted (n + 1)).mono h₂ le_rfl).indicator (h₁ s hs)) (((hM.adapted n).mono h₁ le_rfl).indicator (h₁ s hs)) (fun w hw ↦ ?_) fun w hw ↦ ?_ · rw [lintegral_indicator hs', lintegral_indicator hs'] @@ -327,9 +182,10 @@ private lemma isTestMartingale_doublingProcess : if ∀ i : Finset.Iic n, y i = y ⟨0, Finset.mem_Iic.2 n.zero_le⟩ then (1 : ℝ≥0∞) else 2 ^ n) ∘ Preorder.frestrictLe n := by ext ω - simp only [doublingProcess, Function.comp_apply, Preorder.frestrictLe, Finset.restrict, - Subtype.forall, Finset.mem_Iic] - exact if_congr Iff.rfl rfl rfl + simp only [doublingProcess, Function.comp_apply, Preorder.frestrictLe_apply, Subtype.forall, + Finset.mem_Iic] + -- the two sides differ only in their `Decidable` instances + congr rw [h] exact (measurable_of_finite _).comp (comap_measurable _) refine ⟨hadapted, fun μ hμ ↦ ?_, fun μ hμ n s hs ↦ ?_⟩ diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean index 36a58ec7..2c1fd473 100644 --- a/LMLExplore/MeasureTheory/Constructions/Pi.lean +++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean @@ -7,6 +7,9 @@ module public import Mathlib.MeasureTheory.Constructions.Pi public import Mathlib.Probability.ConditionalProbability +import LMLExplore.Algebra.BigOperators.Field +import Mathlib.Analysis.Analytic.Constructions +import Mathlib.Analysis.Analytic.Uniqueness import TauCeti.MeasureTheory.Constructions.Pi /-! @@ -23,6 +26,10 @@ gives the product of the conditional measures `μ[|B]`, scaled by `μ(B)` to the The product of copies of a multiple `s • ν` is `s ^ card ι` times the product of copies of `ν`, and the product of copies of a finite mixture `∑ k, w k • R k` is the mixture of the products `Measure.pi (fun i ↦ R (e i))` over the assignments `e : ι → κ`, with weights `∏ i, w (e i)`. +Expanding the product of copies of `Q + t • B` this way makes its integrals polynomials in `t`, +which is how equal integrals under the products of copies of the convex combinations of finitely +many measures `P i` transfer to every probability measure `Q` with +`Q + ∑ i, b i • P i = ∑ i, c i • P i`. Under a product of probability measures, a measurable set whose lines along one coordinate `i` all have `μ i`-measure at most `c` has product measure at most `c`, by resampling the coordinate @@ -39,6 +46,10 @@ all have `μ i`-measure at most `c` has product measure at most `c`, by resampli * `MeasureTheory.Measure.pi_sum_smul`, `MeasureTheory.Measure.lintegral_pi_sum_smul`: `Measure.pi (fun _ ↦ ∑ k, w k • R k) = ∑ e, (∏ i, w (e i)) • Measure.pi (fun i ↦ R (e i))`, and the corresponding expansion of integrals. +* `MeasureTheory.Measure.lintegral_pi_eq_of_add_sum_eq_sum`: if `Q + ∑ i, b i • P i = + ∑ i, c i • P i`, two functions with equal integrals under the products of copies of every convex + combination of the `P i`, finite for the first one, have equal integrals under the product of + copies of `Q`. * `MeasureTheory.Measure.pi_eval_preimage_le`: for measures of mass at most `1`, the product measure of the cylinder `{y | y i ∈ s}` is at most `μ i s`, for every set `s`. * `MeasureTheory.Measure.pi_le_of_forall_measure_update_preimage_le`: under a product of @@ -113,6 +124,115 @@ lemma lintegral_pi_sum_smul [DecidableEq ι] {α κ : Type*} {mα : MeasurableSp rw [pi_sum_smul] simp only [lintegral_finsetSum_measure, lintegral_smul_measure, smul_eq_mul] +/-- **Identity theorem for the polynomials of the polarization.** Two families `a` and `a'` of +finite coefficients indexed by `ι → Bool` whose polynomials +`t ↦ ∑ e, (∏ i, bif e i then t else 1) * a e` agree for every `t > 1` agree for every `t ≥ 0`. -/ +private lemma sum_prod_bif_mul_eq_of_one_lt [DecidableEq ι] {a a' : (ι → Bool) → ℝ≥0∞} + (ha : ∀ e, a e ≠ ∞) (ha' : ∀ e, a' e ≠ ∞) + (h : ∀ t : ℝ≥0, 1 < t → ∑ e, (∏ i, ((bif e i then t else 1 : ℝ≥0) : ℝ≥0∞)) * a e = + ∑ e, (∏ i, ((bif e i then t else 1 : ℝ≥0) : ℝ≥0∞)) * a' e) (t : ℝ≥0) : + ∑ e, (∏ i, ((bif e i then t else 1 : ℝ≥0) : ℝ≥0∞)) * a e = + ∑ e, (∏ i, ((bif e i then t else 1 : ℝ≥0) : ℝ≥0∞)) * a' e := by + have hfin (c : (ι → Bool) → ℝ≥0∞) (hc : ∀ e, c e ≠ ∞) (t : ℝ≥0) (e : ι → Bool) : + (∏ i, ((bif e i then t else 1 : ℝ≥0) : ℝ≥0∞)) * c e ≠ ∞ := + ENNReal.mul_ne_top (ENNReal.prod_ne_top fun _ _ ↦ ENNReal.coe_ne_top) (hc e) + -- the real polynomials + set φ : ((ι → Bool) → ℝ≥0∞) → ℝ → ℝ := + fun c x ↦ ∑ e : ι → Bool, (∏ i, bif e i then x else 1) * (c e).toReal + have hφ_eq (c : (ι → Bool) → ℝ≥0∞) (hc : ∀ e, c e ≠ ∞) (t : ℝ≥0) : + φ c t = (∑ e, (∏ i, ((bif e i then t else 1 : ℝ≥0) : ℝ≥0∞)) * c e).toReal := by + rw [ENNReal.toReal_sum fun e _ ↦ hfin c hc t e] + refine Finset.sum_congr rfl fun e _ ↦ ?_ + rw [ENNReal.toReal_mul, ENNReal.toReal_prod] + congr 1 + refine Finset.prod_congr rfl fun i _ ↦ ?_ + cases e i <;> simp + have han (c : (ι → Bool) → ℝ≥0∞) : AnalyticOnNhd ℝ (φ c) Set.univ := fun x _ ↦ + Finset.analyticAt_fun_sum _ fun e _ ↦ (Finset.analyticAt_fun_prod _ fun i _ ↦ by + cases e i + · exact analyticAt_const + · exact analyticAt_id).mul analyticAt_const + -- they agree on `(1, ∞)`, hence everywhere + have hφ : φ a = φ a' := (han a).eq_of_eventuallyEq (han a') (z₀ := 2) <| by + filter_upwards [lt_mem_nhds (by norm_num : (1 : ℝ) < 2)] with x hx + have hx' : (x.toNNReal : ℝ) = x := Real.coe_toNNReal _ (by linarith) + have h1 : 1 < x.toNNReal := by + rw [← NNReal.coe_lt_coe, hx', NNReal.coe_one] + exact hx + rw [← hx', hφ_eq a ha, hφ_eq a' ha', h _ h1] + have ht := congrFun hφ t + rw [hφ_eq a ha, hφ_eq a' ha'] at ht + exact (ENNReal.toReal_eq_toReal_iff' (ENNReal.sum_ne_top.2 fun e _ ↦ hfin a ha t e) + (ENNReal.sum_ne_top.2 fun e _ ↦ hfin a' ha' t e)).1 ht + +/-- **Polarization.** Let `Q` be a probability measure and `P k` finite measures with +`Q + ∑ k, b k • P k = ∑ k, c k • P k`. If two functions on `ι → α` have equal integrals under the +product of copies of every convex combination of the `P k`, finite for the first function, then +they have equal integrals under the product of copies of `Q`. -/ +lemma lintegral_pi_eq_of_add_sum_eq_sum {α κ : Type*} {mα : MeasurableSpace α} [Fintype κ] + {P : κ → Measure α} [∀ k, IsFiniteMeasure (P k)] {b c : κ → ℝ≥0} {Q : Measure α} + [IsProbabilityMeasure Q] (hQ : Q + ∑ k, b k • P k = ∑ k, c k • P k) + {F G : (ι → α) → ℝ≥0∞} + (hFG : ∀ w : κ → ℝ≥0, ∑ k, w k = 1 → + ∫⁻ x, F x ∂Measure.pi (fun _ ↦ ∑ k, w k • P k) = + ∫⁻ x, G x ∂Measure.pi (fun _ ↦ ∑ k, w k • P k)) + (hF : ∀ w : κ → ℝ≥0, ∑ k, w k = 1 → + ∫⁻ x, F x ∂Measure.pi (fun _ ↦ ∑ k, w k • P k) ≠ ∞) : + ∫⁻ x, F x ∂Measure.pi (fun _ : ι ↦ Q) = ∫⁻ x, G x ∂Measure.pi (fun _ : ι ↦ Q) := by + classical + set B := ∑ k, b k • P k with hB + -- `Q + t • B` as the mixture of `R true = B` and `R false = Q` with weights `t` and `1` + set R : Bool → Measure α := fun k ↦ bif k then B else Q with hR + have : IsFiniteMeasure B := by rw [hB]; infer_instance + have : ∀ k, IsFiniteMeasure (R k) := fun k ↦ by + cases k <;> simp only [hR, Bool.cond_false, Bool.cond_true] <;> infer_instance + set A : ((ι → α) → ℝ≥0∞) → (ι → Bool) → ℝ≥0∞ := + fun H e ↦ ∫⁻ x, H x ∂Measure.pi (fun i ↦ R (e i)) + have hpoly (H : (ι → α) → ℝ≥0∞) (t : ℝ≥0) : + ∫⁻ x, H x ∂Measure.pi (fun _ : ι ↦ Q + t • B) = + ∑ e : ι → Bool, (∏ i, ((bif e i then t else 1 : ℝ≥0) : ℝ≥0∞)) * A H e := by + have hmix : Q + t • B = ∑ k, (bif k then t else 1 : ℝ≥0) • R k := by simp [hR, add_comm] + rw [hmix, lintegral_pi_sum_smul] + -- for `t ≥ 1`, `Q + t • B` is a positive multiple of a convex combination of the `P k` + have hgood (t : ℝ≥0) (ht : 1 ≤ t) : + ∫⁻ x, F x ∂Measure.pi (fun _ : ι ↦ Q + t • B) = + ∫⁻ x, G x ∂Measure.pi (fun _ : ι ↦ Q + t • B) ∧ + ∫⁻ x, F x ∂Measure.pi (fun _ : ι ↦ Q + t • B) ≠ ∞ := by + have hμ : Q + t • B = ∑ k, (c k + (t - 1) * b k) • P k := by + calc Q + t • B = (Q + B) + (t - 1) • B := by + conv_lhs => rw [← add_tsub_cancel_of_le ht, add_smul, one_smul] + rw [add_assoc] + _ = ∑ k, (c k + (t - 1) * b k) • P k := by + rw [hQ, hB, Finset.smul_sum, ← Finset.sum_add_distrib] + exact Finset.sum_congr rfl fun k _ ↦ by rw [smul_smul, ← add_smul] + have hs : ∑ k, (c k + (t - 1) * b k) ≠ 0 := by + intro h0 + have h : Q + t • B = 0 := by + rw [hμ] + exact Finset.sum_eq_zero fun k hk ↦ by rw [Finset.sum_eq_zero_iff.1 h0 k hk, zero_smul] + have h' := congrArg (· Set.univ) h + simp at h' + have hv : ∑ k, (c k + (t - 1) * b k) / ∑ j, (c j + (t - 1) * b j) = 1 := by + rw [← Finset.sum_div, div_self hs] + rw [hμ, Finset.sum_smul_eq_smul_sum_div_smul hs, pi_const_smul, lintegral_smul_measure, + lintegral_smul_measure, hFG _ hv] + refine ⟨rfl, ?_⟩ + rw [ENNReal.smul_def, smul_eq_mul, ← hFG _ hv] + exact ENNReal.mul_ne_top ENNReal.coe_ne_top (hF _ hv) + -- the coefficients of the polynomials are finite, as the case `t = 1` shows + have hA_ne (H : (ι → α) → ℝ≥0∞) + (hH : ∫⁻ x, H x ∂Measure.pi (fun _ : ι ↦ Q + (1 : ℝ≥0) • B) ≠ ∞) (e : ι → Bool) : + A H e ≠ ∞ := by + have hw1 (k : Bool) : (bif k then (1 : ℝ≥0) else 1) = 1 := by cases k <;> rfl + rw [hpoly] at hH + simp only [hw1, ENNReal.coe_one, Finset.prod_const_one, one_mul] at hH + exact ENNReal.sum_ne_top.1 hH e (Finset.mem_univ e) + obtain ⟨h1eq, h1ne⟩ := hgood 1 le_rfl + have h0 := sum_prod_bif_mul_eq_of_one_lt (hA_ne F h1ne) (hA_ne G (by rwa [← h1eq])) + (fun t ht ↦ by rw [← hpoly, ← hpoly]; exact (hgood t ht.le).1) 0 + rw [← hpoly, ← hpoly] at h0 + simpa only [zero_smul, add_zero] using h0 + /-- For measures of mass at most `1`, the product measure of the cylinder `eval i ⁻¹' s` of a set `s`, measurable or not, is at most `μ i s`. -/ lemma pi_eval_preimage_le {μ : ∀ i, Measure (Ω i)} [∀ i, IsZeroOrProbabilityMeasure (μ i)] diff --git a/LMLExplore/MeasureTheory/Measure/ProbabilityMeasure/Convex.lean b/LMLExplore/MeasureTheory/Measure/Typeclasses/Probability.lean similarity index 100% rename from LMLExplore/MeasureTheory/Measure/ProbabilityMeasure/Convex.lean rename to LMLExplore/MeasureTheory/Measure/Typeclasses/Probability.lean diff --git a/LMLExplore/Probability/ProductMeasure.lean b/LMLExplore/Probability/ProductMeasure.lean index c218f9e8..286ced1d 100644 --- a/LMLExplore/Probability/ProductMeasure.lean +++ b/LMLExplore/Probability/ProductMeasure.lean @@ -7,6 +7,10 @@ module public import LMLExplore.MeasureTheory.MeasurableSpace.Constructions public import Mathlib.Probability.Independence.InfinitePi +public import Mathlib.Probability.Process.Filtration +import LMLExplore.MeasureTheory.Constructions.Pi +import LMLExplore.MeasureTheory.Measure.Typeclasses.Probability +import Mathlib.MeasureTheory.Function.FactorsThrough /-! # Infinite products of probability measures: the first terms and the next terms @@ -15,12 +19,19 @@ Under the infinite product `Measure.infinitePi` of copies of a probability measu `n` coordinates have the product law `Measure.pi`, and they are independent of the next `m` coordinates. +If `Q + ∑ i, b i • P i = ∑ i, c i • P i` for a probability measure `Q` and probability measures +`P i`, two functions of the first `N + 1` observations with equal integrals under the i.i.d. law of +every convex combination of the `P i` have equal integrals under the i.i.d. law of `Q`. + ## Main statements * `MeasureTheory.measurePreserving_initSeg`: the first `n` terms `initSeg n` of an i.i.d. sequence have the product law. * `MeasureTheory.Measure.infinitePi_fin_mem_and_forall_add_mem`: for an i.i.d. sequence, the first `n` terms and the next `m` terms are independent. +* `MeasureTheory.Measure.lintegral_infinitePi_eq_of_add_sum_eq_sum`: polarization for i.i.d. laws, + from the convex combinations of finitely many probability measures to every probability measure + in their linear span. -/ public section @@ -82,4 +93,37 @@ theorem infinitePi_fin_mem_and_forall_add_mem {X : Type*} [MeasurableSpace X] ( rw [h_pi, Measure.infinitePi_pi _ fun _ _ ↦ hC, Finset.prod_const, Nat.card_Ico, Nat.add_sub_cancel_left] +open scoped NNReal ENNReal in +/-- **Polarization for i.i.d. laws.** Let `Q` be a probability measure and `P i` probability +measures with `Q + ∑ i, b i • P i = ∑ i, c i • P i`. If two functions of the first `N + 1` +observations have equal integrals under the i.i.d. law of every convex combination of the `P i`, +finite for the first function, then they have equal integrals under the i.i.d. law of `Q`. -/ +lemma lintegral_infinitePi_eq_of_add_sum_eq_sum {𝓧 ι : Type*} {m𝓧 : MeasurableSpace 𝓧} + [Fintype ι] {P : ι → Measure 𝓧} [∀ i, IsProbabilityMeasure (P i)] {b c : ι → ℝ≥0} + {Q : Measure 𝓧} [IsProbabilityMeasure Q] (hQ : Q + ∑ i, b i • P i = ∑ i, c i • P i) {N : ℕ} + {f g : (ℕ → 𝓧) → ℝ≥0∞} (hf : Measurable[Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) N] f) + (hg : Measurable[Filtration.piLE (X := fun _ : ℕ ↦ 𝓧) N] g) + (hfg : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → + ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i) = + ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i)) + (hf_ne : ∀ w : ι → ℝ≥0, ∑ i, w i = 1 → + ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ ∑ i, w i • P i) ≠ ∞) : + ∫⁻ ω, f ω ∂Measure.infinitePi (fun _ ↦ Q) = ∫⁻ ω, g ω ∂Measure.infinitePi (fun _ ↦ Q) := by + rw [Filtration.piLE_eq_comap_frestrictLe] at hf hg + obtain ⟨f', hf', rfl⟩ := hf.exists_eq_measurable_comp + obtain ⟨g', hg', rfl⟩ := hg.exists_eq_measurable_comp + have h (μ : Measure 𝓧) [IsProbabilityMeasure μ] {H : (Finset.Iic N → 𝓧) → ℝ≥0∞} + (hH : Measurable H) : + ∫⁻ ω, (H ∘ Preorder.frestrictLe N) ω ∂Measure.infinitePi (fun _ ↦ μ) = + ∫⁻ x, H x ∂Measure.pi (fun _ : Finset.Iic N ↦ μ) := + lintegral_restrict_infinitePi _ hH + rw [h Q hf', h Q hg'] + refine lintegral_pi_eq_of_add_sum_eq_sum hQ (fun w hw ↦ ?_) fun w hw ↦ ?_ + · have := isProbabilityMeasure_sum_smul (P := P) hw + rw [← h _ hf', ← h _ hg'] + exact hfg w hw + · have := isProbabilityMeasure_sum_smul (P := P) hw + rw [← h _ hf'] + exact hf_ne w hw + end MeasureTheory.Measure From 1ed2f7047e0d49422a2707fcc8cca5b88d0ca347 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 16:06:59 +0100 Subject: [PATCH 4/4] docs: credit [EVR26, Note 03, Theorem 1] for the polarization lemmas Co-Authored-By: Claude Code --- LMLExplore/MeasureTheory/Constructions/Pi.lean | 12 +++++++++++- LMLExplore/Probability/ProductMeasure.lean | 12 +++++++++++- 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean index 2c1fd473..4344d91e 100644 --- a/LMLExplore/MeasureTheory/Constructions/Pi.lean +++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean @@ -29,7 +29,10 @@ the product of copies of a finite mixture `∑ k, w k • R k` is the mixture of Expanding the product of copies of `Q + t • B` this way makes its integrals polynomials in `t`, which is how equal integrals under the products of copies of the convex combinations of finitely many measures `P i` transfer to every probability measure `Q` with -`Q + ∑ i, b i • P i = ∑ i, c i • P i`. +`Q + ∑ i, b i • P i = ∑ i, c i • P i`. This polarization argument is the proof of +[EVR26, Note 03, Theorem 1], and the lemmas are adapted from +`EValuesResearch/Results/TestMartingaleConverse.lean` (commit `6f05c5f`) in the paper project +`RemyDegenne/evalues_research`. Under a product of probability measures, a measurable set whose lines along one coordinate `i` all have `μ i`-measure at most `c` has product measure at most `c`, by resampling the coordinate @@ -55,6 +58,13 @@ all have `μ i`-measure at most `c` has product measure at most `c`, by resampli * `MeasureTheory.Measure.pi_le_of_forall_measure_update_preimage_le`: under a product of probability measures, a measurable set whose lines `{t | update x i t ∈ E}` along one coordinate `i` all have `μ i`-measure at most `c` has product measure at most `c`. + +## References + +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, notes 01 to 34 and + the Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026; written and + refereed by AI agents: Note 03, *Converse of the power-one theorem for test martingales*, + Theorem 1. -/ public section diff --git a/LMLExplore/Probability/ProductMeasure.lean b/LMLExplore/Probability/ProductMeasure.lean index 286ced1d..c491ec9d 100644 --- a/LMLExplore/Probability/ProductMeasure.lean +++ b/LMLExplore/Probability/ProductMeasure.lean @@ -21,7 +21,10 @@ coordinates. If `Q + ∑ i, b i • P i = ∑ i, c i • P i` for a probability measure `Q` and probability measures `P i`, two functions of the first `N + 1` observations with equal integrals under the i.i.d. law of -every convex combination of the `P i` have equal integrals under the i.i.d. law of `Q`. +every convex combination of the `P i` have equal integrals under the i.i.d. law of `Q`. This is +the polarization step of [EVR26, Note 03, Theorem 1], adapted from +`EValuesResearch/Results/TestMartingaleConverse.lean` (commit `6f05c5f`) in the paper project +`RemyDegenne/evalues_research`. ## Main statements @@ -32,6 +35,13 @@ every convex combination of the `P i` have equal integrals under the i.i.d. law * `MeasureTheory.Measure.lintegral_infinitePi_eq_of_add_sum_eq_sum`: polarization for i.i.d. laws, from the convex combinations of finitely many probability measures to every probability measure in their linear span. + +## References + +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, notes 01 to 34 and + the Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026; written and + refereed by AI agents: Note 03, *Converse of the power-one theorem for test martingales*, + Theorem 1. -/ public section