From a16fa46264923c674b41fe40fe4883796e311c62 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:32:42 +0100 Subject: [PATCH 1/5] feat: nulls dense in total variation have the e-variables of all laws, and the mean-zero null has no power MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The effective null is closed in total variation, so a null whose closure in total variation contains every probability measure has, for every finite number of i.i.d. observations, the e-variables of the null of all laws (total variation is subadditive over products). Instance: the laws on ℝ with mean 0 and a finite, positive variance; their one-observation e-variables are the measurable functions bounded by 1, maxLogGrowth and bipolarRate vanish against every law, tests have no power against i.i.d. alternatives, and e-processes for independent sequences with marginals in the null are at most 1. EValues roadmap, Layer 1 item 1 and Layer 6 item 2. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- .../EValues/EffectiveSet/TotalVariation.lean | 305 ++++++++++++++++++ LMLExplore/EValues/MeanZeroNull.lean | 258 +++++++++++++++ .../Measure/TotalVariation/Basic.lean | 15 + .../Measure/TotalVariation/Pi.lean | 133 ++++++++ 4 files changed, 711 insertions(+) create mode 100644 LMLExplore/EValues/EffectiveSet/TotalVariation.lean create mode 100644 LMLExplore/EValues/MeanZeroNull.lean create mode 100644 LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean diff --git a/LMLExplore/EValues/EffectiveSet/TotalVariation.lean b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean new file mode 100644 index 00000000..701e48f4 --- /dev/null +++ b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean @@ -0,0 +1,305 @@ +/- +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.BipolarRate +public import LMLExplore.EValues.EffectiveSet +public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs +public import Mathlib.Probability.ProductMeasure + +import LMLExplore.MeasureTheory.Measure.TotalVariation.Basic +import LMLExplore.MeasureTheory.Measure.TotalVariation.Pi +import TauCeti.MeasureTheory.Measure.TotalVariation.Basic + +/-! +# Nulls dense in total variation + +The effective null `effectiveSet S` of a null `S` is closed under setwise convergence +(`ProbabilityTheory.mem_effectiveSet_of_measure_le_liminf`), hence in total variation. So every +limit in total variation of members of a null of probability measures belongs to its effective +null, and no e-variable for `S` has expectation above `1` under it. A null that is dense in +total variation among the probability measures therefore has the e-variables of the null of all +laws: e-variables cannot tell it apart from the null of all laws, and they have no power. + +* **One observation.** If every point mass `Measure.dirac x` is a limit in total variation of + members of `S`, the e-variables for `S` are the measurable functions bounded by `1` + everywhere. This applies to the laws of independent sequences, indexed by a countable type, + with marginals in such a null, on a space with measurable singletons: on a given sequence, the + marginals can be chosen to miss masses of arbitrarily small sum. +* **Finitely many i.i.d. observations.** Total variation is subadditive over products + (`MeasureTheory.etvDist_pi_le_sum`), so if a probability measure `Q` is a limit in total + variation of members of `S`, then `Q ^ ι` is a limit of members of `S ^ ι` for every finite + `ι`, and lies in the effective null of the i.i.d. null `{P ^ ι | P ∈ S}`. If this holds for + every `Q`, an `ι`-sample function is an e-variable for the i.i.d. laws of `S` exactly when it is + one for the i.i.d. laws of all probability measures. Under the i.i.d. law of such a `Q`, the + maximal expected logarithm `maxLogGrowth Q S n` of an `n`-sample e-variable and the bipolar rate + `bipolarRate Q S` vanish, and a test of level `α` for the i.i.d. laws of `S` has power at most + `α`. + +The mean-zero null on `ℝ` (`ProbabilityTheory.meanZeroNull`) is the motivating instance; this is +the form for e-variables of the theorem of Bahadur and Savage [BS56]. + +## Main statements + +* `ProbabilityTheory.mem_effectiveSet_of_forall_exists_etvDist_lt`: the effective null is closed + in total variation. +* `ProbabilityTheory.isEVar_iff_of_forall_exists_etvDist_dirac_lt`: if every point mass is a limit + in total variation of members of `S`, the e-variables for `S` are the measurable functions + bounded by `1`. +* `ProbabilityTheory.isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt`: the same for the + laws of independent sequences with marginals in `S`. +* `ProbabilityTheory.pi_mem_effectiveSet_of_forall_exists_etvDist_lt`: a limit `Q` in total + variation of members of `S` has `Q ^ ι` in the effective null of the i.i.d. null. +* `ProbabilityTheory.isEVar_pi_iff_of_forall_exists_etvDist_lt`: a null dense in total variation + has, for every finite number of i.i.d. observations, the e-variables of the null of all laws. +* `ProbabilityTheory.measure_pi_le_of_forall_exists_etvDist_lt`, + `ProbabilityTheory.maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt`, + `ProbabilityTheory.bipolarRate_eq_zero_of_forall_exists_etvDist_lt`: against such a `Q`, tests + have no power and evidence does not grow. + +## Implementation notes + +Membership in the effective null is derived from its closure under setwise convergence, in the +form `ProbabilityTheory.mem_effectiveSet_of_measure_le_liminf`, which handles unbounded +e-variables by monotone convergence. Total variation enters only through the eventwise bound +`μ s ≤ ν s + etvDist μ ν` (`MeasureTheory.measure_le_add_etvDist`) and its subadditivity over +products. + +## References + +* [BS56] R. R. Bahadur and L. J. Savage, *The nonexistence of certain statistical procedures in + nonparametric problems*, Ann. Math. Statist. 27 (1956). +-/ + +public section + +open MeasureTheory Filter Set InformationTheory + +open scoped ENNReal Topology + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S : Set (Measure Ω)} {μ : Measure Ω} + +/-! ### Closure in total variation -/ + +/-- **The effective null is closed in total variation**: a measure that is a limit in total +variation of members of the effective null of `S` belongs to it. -/ +theorem mem_effectiveSet_of_forall_exists_etvDist_lt + (h : ∀ ε > 0, ∃ ν ∈ effectiveSet S, etvDist ν μ < ε) : μ ∈ effectiveSet S := by + -- The members of the effective null, along the filter of their distance to `μ` tending to `0`. + set f : effectiveSet S → ℝ≥0∞ := fun ν ↦ etvDist (ν : Measure Ω) μ + have : (Filter.comap f (𝓝 0)).NeBot := + (ENNReal.nhds_zero_basis.comap f).neBot_iff.2 fun {ε} hε ↦ + let ⟨ν, hν, hνμ⟩ := h ε hε + ⟨⟨ν, hν⟩, hνμ⟩ + refine mem_effectiveSet_of_measure_le_liminf (l := Filter.comap f (𝓝 0)) (μs := Subtype.val) + (.of_forall fun ν ↦ ν.2) fun s hs ↦ ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ ?_ + have hev : ∀ᶠ ν : effectiveSet S in Filter.comap f (𝓝 0), μ s - ε ≤ (ν : Measure Ω) s := by + filter_upwards [tendsto_comap.eventually (gt_mem_nhds (ENNReal.coe_pos.2 hε))] with ν hν + refine tsub_le_iff_right.2 ((measure_le_add_etvDist μ ν hs).trans ?_) + rw [etvDist_comm] + exact add_le_add le_rfl hν.le + exact tsub_le_iff_right.1 (le_liminf_of_le (by isBoundedDefault) hev) + +/-- A limit in total variation of members of a null `S` of measures of mass at most `1` belongs +to the effective null of `S`. -/ +private lemma mem_effectiveSet_of_forall_exists_mem_etvDist_lt (hS : ∀ P ∈ S, P univ ≤ 1) + (h : ∀ ε > 0, ∃ P ∈ S, etvDist P μ < ε) : μ ∈ effectiveSet S := + mem_effectiveSet_of_forall_exists_etvDist_lt fun ε hε ↦ + let ⟨P, hP, hPμ⟩ := h ε hε + ⟨P, subset_effectiveSet hS hP, hPμ⟩ + +/-! ### One observation and independent sequences -/ + +/-- **One observation.** If every point mass is a limit in total variation of members of a null +`S` of measures of mass at most `1` (for instance probability measures), the e-variables for `S` +are the measurable functions bounded by `1` everywhere. -/ +theorem isEVar_iff_of_forall_exists_etvDist_dirac_lt (hS : ∀ P ∈ S, P univ ≤ 1) + (hS_dirac : ∀ x : Ω, ∀ ε > 0, ∃ P ∈ S, etvDist P (Measure.dirac x) < ε) + {X : Ω → ℝ≥0∞} : + IsEVar X S ↔ Measurable X ∧ ∀ x, X x ≤ 1 := by + refine ⟨fun hX ↦ ⟨hX.measurable, fun x ↦ ?_⟩, fun h ↦ .of_lintegral_le_measure_univ + (fun P hP ↦ ⟨(hS P hP).trans_lt ENNReal.one_lt_top⟩) h.1 fun P _ ↦ ?_⟩ + · have hx : Measure.dirac x ∈ effectiveSet S := + mem_effectiveSet_of_forall_exists_mem_etvDist_lt hS (hS_dirac x) + simpa [lintegral_dirac' x hX.measurable] using hx X hX + · calc ∫⁻ ω, X ω ∂P ≤ ∫⁻ _, 1 ∂P := lintegral_mono h.2 + _ = P univ := lintegral_one + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {S : Set (Measure 𝓧)} + +/-- If every point mass is a limit in total variation of members of a null `S` of probability +measures, so is every point mass on `ι → 𝓧`, for a countable `ι`, of laws of independent +sequences with marginals in `S`: on the given sequence `x`, the marginals can be chosen so that +the masses they miss have a small sum. -/ +private lemma exists_infinitePi_etvDist_dirac_lt {ι : Type*} [Countable ι] + [MeasurableSingletonClass 𝓧] (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hS_dirac : ∀ x : 𝓧, ∀ ε > 0, ∃ P ∈ S, etvDist P (Measure.dirac x) < ε) (x : ι → 𝓧) + {ε : ℝ≥0∞} (hε : 0 < ε) : + ∃ P ∈ Measure.infinitePi '' {P : ι → Measure 𝓧 | ∀ i, P i ∈ S}, + etvDist P (Measure.dirac x) < ε := by + obtain ⟨δ, hδ0, hδ⟩ := ENNReal.exists_pos_sum_of_countable (ENNReal.half_pos hε.ne').ne' ι + -- For each `i`, a member of `S` that misses a mass at most `δ i` of the point `x i`. + have hchoose (i : ι) : ∃ P ∈ S, P {x i}ᶜ < δ i := by + obtain ⟨P, hP, hPx⟩ := hS_dirac (x i) (2 * δ i) (by simpa using hδ0 i) + have := hS P hP + refine ⟨P, hP, ?_⟩ + rw [etvDist_comm, etvDist_dirac_left] at hPx + rw [prob_compl_eq_one_sub (measurableSet_singleton _)] + exact (ENNReal.mul_lt_mul_iff_right two_ne_zero ENNReal.ofNat_ne_top).1 hPx + choose P hPS hPx using hchoose + have := fun i ↦ hS _ (hPS i) + refine ⟨Measure.infinitePi P, ⟨P, hPS, rfl⟩, ?_⟩ + have hcompl : Measure.infinitePi P {x}ᶜ < ε / 2 := by + calc Measure.infinitePi P {x}ᶜ + _ ≤ Measure.infinitePi P (⋃ i, Function.eval i ⁻¹' {x i}ᶜ) := by + refine measure_mono fun y hy ↦ ?_ + obtain ⟨i, hi⟩ := Function.ne_iff.1 hy + exact mem_iUnion.2 ⟨i, hi⟩ + _ ≤ ∑' i, Measure.infinitePi P (Function.eval i ⁻¹' {x i}ᶜ) := measure_iUnion_le _ + _ = ∑' i, P i {x i}ᶜ := by + congr 1 with i + exact (measurePreserving_eval_infinitePi P i).measure_preimage + (measurableSet_singleton _).compl.nullMeasurableSet + _ ≤ ∑' i, (δ i : ℝ≥0∞) := by gcongr with i; exact (hPx i).le + _ < ε / 2 := hδ + rw [etvDist_comm, etvDist_dirac_left, mul_comm] + refine (ENNReal.lt_div_iff_mul_lt (.inl two_ne_zero) (.inl ENNReal.ofNat_ne_top)).1 + (lt_of_le_of_lt ?_ hcompl) + rw [tsub_le_iff_left, ← measure_univ (μ := Measure.infinitePi P)] + exact measure_univ_le_add_compl _ + +/-- **Independent sequences.** If every point mass is a limit in total variation of members of a +null `S` of probability measures, on a space with measurable singletons, the e-variables for the +laws of the independent sequences indexed by a countable `ι` with marginals in `S` are the +measurable functions bounded by `1` everywhere. -/ +theorem isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt {ι : Type*} [Countable ι] + [MeasurableSingletonClass 𝓧] (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hS_dirac : ∀ x : 𝓧, ∀ ε > 0, ∃ P ∈ S, etvDist P (Measure.dirac x) < ε) + {X : (ι → 𝓧) → ℝ≥0∞} : + IsEVar X (Measure.infinitePi '' {P : ι → Measure 𝓧 | ∀ i, P i ∈ S}) ↔ + Measurable X ∧ ∀ x, X x ≤ 1 := by + refine isEVar_iff_of_forall_exists_etvDist_dirac_lt ?_ + fun x _ hε ↦ exists_infinitePi_etvDist_dirac_lt hS hS_dirac x hε + rintro _ ⟨P, hP, rfl⟩ + have := fun i ↦ hS _ (hP i) + exact prob_le_one + +/-! ### Finitely many i.i.d. observations -/ + +variable {ι : Type*} [Fintype ι] {Q : Measure 𝓧} + +/-- A limit in total variation of probability measures is a probability measure. -/ +private lemma isProbabilityMeasure_of_forall_exists_etvDist_lt + (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) : + IsProbabilityMeasure Q := by + have h (ε : NNReal) (hε : 0 < ε) : Q univ ≤ 1 + ε ∧ 1 ≤ Q univ + ε := by + obtain ⟨P, hP, hPQ⟩ := hQ ε (ENNReal.coe_pos.2 hε) + have := hS P hP + constructor + · calc Q univ ≤ P univ + etvDist Q P := measure_le_add_etvDist Q P .univ + _ ≤ 1 + ε := by + rw [measure_univ, etvDist_comm] + exact add_le_add le_rfl hPQ.le + · calc 1 = P univ := measure_univ.symm + _ ≤ Q univ + etvDist P Q := measure_le_add_etvDist P Q .univ + _ ≤ Q univ + ε := add_le_add le_rfl hPQ.le + exact ⟨le_antisymm (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).1) + (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).2)⟩ + +/-- If `Q` is a limit in total variation of members of a null `S` of probability measures, then +`Q ^ ι` is a limit in total variation of the products `P ^ ι` of members of `S`. -/ +private lemma exists_etvDist_pi_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P) + [IsProbabilityMeasure Q] (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) {ε : ℝ≥0∞} (hε : 0 < ε) : + ∃ P ∈ S, etvDist (Measure.pi fun _ : ι ↦ P) (Measure.pi fun _ : ι ↦ Q) < ε := by + obtain ⟨P, hP, hPQ⟩ := hQ (ε / Fintype.card ι) + (ENNReal.div_pos hε.ne' (ENNReal.natCast_ne_top _)) + have := hS P hP + refine ⟨P, hP, (etvDist_pi_le_sum _ _).trans_lt ?_⟩ + rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_comm] + exact (ENNReal.lt_div_iff_mul_lt (.inr (etvDist_ne_top _ _)) + (.inl (ENNReal.natCast_ne_top _))).1 hPQ + +/-- **I.i.d. observations of a limit in total variation.** If a probability measure `Q` is a limit +in total variation of members of a null `S` of probability measures, then for every finite `ι` the +product `Q ^ ι` belongs to the effective null of the i.i.d. null `{P ^ ι | P ∈ S}`: no e-variable +for the i.i.d. laws of `S` has expectation above `1` under the i.i.d. law of `Q`. -/ +theorem pi_mem_effectiveSet_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) : + Measure.pi (fun _ : ι ↦ Q) ∈ effectiveSet ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' S) := by + have := isProbabilityMeasure_of_forall_exists_etvDist_lt hS hQ + refine mem_effectiveSet_of_forall_exists_mem_etvDist_lt ?_ fun ε hε ↦ ?_ + · rintro _ ⟨P, hP, rfl⟩ + have := hS P hP + simp + · obtain ⟨P, hP, hPQ⟩ := exists_etvDist_pi_lt (ι := ι) hS hQ hε + exact ⟨_, ⟨P, hP, rfl⟩, hPQ⟩ + +/-- **A null dense in total variation has the e-variables of all laws.** If every probability +measure is a limit in total variation of members of a null `S` of probability measures, then for +every finite set `ι` of i.i.d. observations, a function is an e-variable for the products `P ^ ι` +of the members of `S` exactly when it is one for the products of all probability measures. -/ +theorem isEVar_pi_iff_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hdense : ∀ Q : Measure 𝓧, IsProbabilityMeasure Q → ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) + {X : (ι → 𝓧) → ℝ≥0∞} : + IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' S) ↔ + IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' {P | IsProbabilityMeasure P}) := by + refine ⟨fun hX ↦ .of_lintegral_le_one ?_ hX.measurable ?_, + fun hX ↦ hX.anti_set (image_mono fun P hP ↦ hS P hP)⟩ + · rintro _ ⟨Q, hQ, rfl⟩ + have : IsProbabilityMeasure Q := hQ + infer_instance + · rintro _ ⟨Q, hQ, rfl⟩ + have : IsProbabilityMeasure Q := hQ + exact pi_mem_effectiveSet_of_forall_exists_etvDist_lt hS (hdense Q hQ) X hX + +/-- **No power against a limit in total variation.** If a probability measure `Q` is a limit in +total variation of members of a null `S` of probability measures, a measurable set of `ι` +observations with probability at most `α` under the i.i.d. law of every member of `S` has +probability at most `α` under the i.i.d. law of `Q`. -/ +theorem measure_pi_le_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) {R : Set (ι → 𝓧)} (hR : MeasurableSet R) + {α : ℝ≥0∞} (hα : ∀ P ∈ S, Measure.pi (fun _ : ι ↦ P) R ≤ α) : + Measure.pi (fun _ : ι ↦ Q) R ≤ α := by + have := isProbabilityMeasure_of_forall_exists_etvDist_lt hS hQ + refine ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ ?_ + obtain ⟨P, hP, hPQ⟩ := exists_etvDist_pi_lt (ι := ι) hS hQ (ENNReal.coe_pos.2 hε) + calc Measure.pi (fun _ : ι ↦ Q) R + _ ≤ Measure.pi (fun _ : ι ↦ P) R + + etvDist (Measure.pi fun _ : ι ↦ Q) (Measure.pi fun _ : ι ↦ P) := + measure_le_add_etvDist _ _ hR + _ ≤ α + ε := by + rw [etvDist_comm] + exact add_le_add (hα P hP) hPQ.le + +/-- **No growth against a limit in total variation.** If a probability measure `Q` is a limit in +total variation of members of a null `S` of probability measures, the maximal expected logarithm +under `Q ^ n` of an `n`-sample e-variable for the i.i.d. laws of `S` is `0`. -/ +theorem maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) (n : ℕ) : + maxLogGrowth Q S n = 0 := by + have := isProbabilityMeasure_of_forall_exists_etvDist_lt hS hQ + refine le_antisymm ?_ (maxLogGrowth_nonneg _ _ _) + rw [maxLogGrowth_def] + refine (maxUtility_le_klIntegral_of_mem_effectiveSet ?_ + (pi_mem_effectiveSet_of_forall_exists_etvDist_lt hS hQ)).trans_eq ?_ + · rintro _ ⟨P, hP, rfl⟩ + have := hS P hP + infer_instance + · rw [klIntegral_eq_klDiv rfl, klDiv_self] + rfl + +/-- **The bipolar rate against a limit in total variation is zero.** If a probability measure `Q` +is a limit in total variation of members of a null `S` of probability measures, the optimal growth +rate `bipolarRate Q S` of the evidence against the i.i.d. laws of `S` under the i.i.d. law of `Q` +is `0`. -/ +theorem bipolarRate_eq_zero_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P) + (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) : + bipolarRate Q S = 0 := by + simp [bipolarRate_def, maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt hS hQ] + +end ProbabilityTheory diff --git a/LMLExplore/EValues/MeanZeroNull.lean b/LMLExplore/EValues/MeanZeroNull.lean new file mode 100644 index 00000000..ffbde47d --- /dev/null +++ b/LMLExplore/EValues/MeanZeroNull.lean @@ -0,0 +1,258 @@ +/- +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.EffectiveSet.TotalVariation +public import LMLExplore.EValues.EProcess +public import Mathlib.Probability.Moments.Variance + +import Mathlib.MeasureTheory.Measure.TotalVariation.Basic + +/-! +# The mean-zero null: e-variables without power + +The null `meanZeroNull` of the laws on `ℝ` with mean `0` and a finite, positive variance is dense +in total variation among the probability measures on `ℝ`: a law `Q` is approximated by `Q` +restricted to a large interval and scaled by a factor below `1`, completed by two atoms that +restore the mean `0` and make the variance positive. So the results of +`LMLExplore.EValues.EffectiveSet.TotalVariation` apply, and the null cannot be tested with +e-variables against i.i.d. alternatives, the form for e-variables of the theorem of Bahadur and +Savage [BS56]: + +* for every finite number of i.i.d. observations, its e-variables are those of the null of all + laws on `ℝ`; for one observation, they are the measurable functions bounded by `1` + everywhere; +* against the i.i.d. law of every `Q`, the maximal expected logarithm of an `n`-sample e-variable + and the bipolar rate vanish, and a test of level `α` has power at most `α`; +* every e-process, for any filtration, for the laws of the independent sequences with marginals in + the null is at most `1` at every time and on every sequence. + +## Main definitions + +* `ProbabilityTheory.meanZeroNull`: the laws on `ℝ` with mean `0` and finite, positive variance. + +## Main statements + +* `ProbabilityTheory.exists_mem_meanZeroNull_etvDist_lt`: the null is dense in total variation. +* `ProbabilityTheory.isEVar_pi_meanZeroNull_iff`: its `ι`-sample e-variables are those of the + i.i.d. laws of all probability measures. +* `ProbabilityTheory.isEVar_meanZeroNull_iff`: its one-observation e-variables are the measurable + functions bounded by `1`. +* `ProbabilityTheory.maxLogGrowth_meanZeroNull`, `ProbabilityTheory.bipolarRate_meanZeroNull`, + `ProbabilityTheory.measure_pi_le_of_forall_meanZeroNull`: no growth and no power against i.i.d. + alternatives. +* `ProbabilityTheory.le_one_of_isEProcess_infinitePi_meanZeroNull`: e-processes for the laws of + independent sequences with marginals in the null are at most `1`. + +## References + +* [BS56] R. R. Bahadur and L. J. Savage, *The nonexistence of certain statistical procedures in + nonparametric problems*, Ann. Math. Statist. 27 (1956). +-/ + +public section + +open MeasureTheory Filter Set + +open scoped ENNReal Topology + +namespace ProbabilityTheory + +/-- The laws on `ℝ` with mean `0` and a finite, positive variance: the probability measures `μ` +under which the identity is square integrable, with `∫ x ∂μ = 0` and `0 < variance id μ`. -/ +def meanZeroNull : Set (Measure ℝ) := + {μ | IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧ ∫ x, x ∂μ = 0 ∧ 0 < variance id μ} + +/-- Membership in the mean-zero null. -/ +lemma mem_meanZeroNull_iff {μ : Measure ℝ} : + μ ∈ meanZeroNull ↔ + IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧ ∫ x, x ∂μ = 0 ∧ 0 < variance id μ := + Iff.rfl + +/-- The members of the mean-zero null are probability measures. -/ +lemma isProbabilityMeasure_of_mem_meanZeroNull {μ : Measure ℝ} (hμ : μ ∈ meanZeroNull) : + IsProbabilityMeasure μ := + hμ.1 + +/-! ### Density in total variation -/ + +/-- **Completion to a law with mean zero.** A finite measure on `ℝ` of mass less than `1` carried +by a bounded interval is below a member of the mean-zero null: add two atoms of mass +`(1 - ν univ) / 2` at `z - 1` and `z + 1`, for the `z` that makes the mean `0`. -/ +private lemma exists_mem_meanZeroNull_le (ν : Measure ℝ) [IsFiniteMeasure ν] (hν : ν univ < 1) + {M : ℝ} (hM : ∀ᵐ x ∂ν, |x| ≤ M) : ∃ P ∈ meanZeroNull, ν ≤ P := by + set b := ν.real univ with hb_def + have hb0 : 0 ≤ b := measureReal_nonneg + have hb1 : b < 1 := ENNReal.toReal_lt_of_lt_ofReal (by simpa using hν) + have h1b : 1 - b ≠ 0 := by linarith + set z := -(∫ x, x ∂ν) / (1 - b) with hz + set c := ENNReal.ofReal ((1 - b) / 2) with hc + have hc0 : c ≠ 0 := by rw [hc, ne_eq, ENNReal.ofReal_eq_zero, not_le]; linarith + have hct : c ≠ ∞ := ENNReal.ofReal_ne_top + set D := Measure.dirac (z - 1) + Measure.dirac (z + 1) with hD + have : IsFiniteMeasure (c • D) := Measure.smul_finite D hct + set P := ν + c • D with hP + have hDb : ∀ᵐ x ∂D, |x| ≤ |z| + 1 := by + rw [hD, ae_add_measure_iff, ae_dirac_eq, ae_dirac_eq, eventually_pure, eventually_pure] + exact ⟨abs_le.2 ⟨by linarith [neg_abs_le z], by linarith [le_abs_self z]⟩, + abs_le.2 ⟨by linarith [neg_abs_le z], by linarith [le_abs_self z]⟩⟩ + have hPb : ∀ᵐ x ∂P, |x| ≤ max M (|z| + 1) := by + rw [hP, ae_add_measure_iff] + exact ⟨hM.mono fun x hx ↦ hx.trans (le_max_left _ _), + Measure.ae_smul_measure (hDb.mono fun x hx ↦ hx.trans (le_max_right _ _)) c⟩ + have hint {μ : Measure ℝ} [IsFiniteMeasure μ] {K : ℝ} (hK : ∀ᵐ x ∂μ, |x| ≤ K) : + Integrable (fun x : ℝ ↦ x) μ := + Integrable.of_bound measurable_id.aestronglyMeasurable K (by simpa using hK) + have hDu : D univ = 2 := by simp [hD, one_add_one_eq_two] + have hPprob : IsProbabilityMeasure P := by + constructor + rw [hP, add_apply, smul_apply, hDu, smul_eq_mul, + ← ofReal_measureReal (measure_ne_top ν univ), ← hb_def, hc, + ← ENNReal.ofReal_ofNat 2, ← ENNReal.ofReal_mul (by linarith), + ← ENNReal.ofReal_add hb0 (by linarith), ← ENNReal.ofReal_one] + congr 1 + ring + have hmean : ∫ x, x ∂P = 0 := by + rw [hP, integral_add_measure (hint hM) ((hint hDb).smul_measure hct), integral_smul_measure, + hD, integral_add_measure (integrable_dirac (by simp)) (integrable_dirac (by simp)), + integral_dirac, integral_dirac, hc, ENNReal.toReal_ofReal (by linarith), hz, smul_eq_mul] + field_simp + ring + have hmem : MemLp id 2 P := MemLp.of_bound measurable_id.aestronglyMeasurable (max M (|z| + 1)) + (hPb.mono fun x hx ↦ by simpa [Real.norm_eq_abs] using hx) + have hvar : 0 < variance id P := by + refine ENNReal.toReal_pos ?_ hmem.evariance_lt_top.ne + have hz2 : ‖z - 1‖ₑ ^ 2 + ‖z + 1‖ₑ ^ 2 ≠ 0 := by + simp only [ne_eq, add_eq_zero, pow_eq_zero_iff two_ne_zero, eNorm_eq_zero, not_and] + intro h1 + linarith + have hge : c * (‖z - 1‖ₑ ^ 2 + ‖z + 1‖ₑ ^ 2) ≤ evariance id P := by + calc c * (‖z - 1‖ₑ ^ 2 + ‖z + 1‖ₑ ^ 2) = ∫⁻ x, ‖x - 0‖ₑ ^ 2 ∂(c • D) := by + rw [lintegral_smul_measure, hD, lintegral_add_measure, lintegral_dirac, + lintegral_dirac, smul_eq_mul, sub_zero, sub_zero] + _ ≤ ∫⁻ x, ‖x - 0‖ₑ ^ 2 ∂P := lintegral_mono' (Measure.le_add_left le_rfl) le_rfl + _ = evariance id P := by rw [evariance, ← hmean]; rfl + exact (lt_of_lt_of_le (ENNReal.mul_pos hc0 hz2) hge).ne' + exact ⟨P, ⟨hPprob, hmem, hmean, hvar⟩, Measure.le_add_right le_rfl⟩ + +/-- **The mean-zero null is dense in total variation**: every probability measure on `ℝ` is a +limit in total variation of laws with mean `0` and a finite, positive variance. -/ +theorem exists_mem_meanZeroNull_etvDist_lt (Q : Measure ℝ) [IsProbabilityMeasure Q] + {ε : ℝ≥0∞} (hε : 0 < ε) : ∃ P ∈ meanZeroNull, etvDist P Q < ε := by + -- `Q` restricted to `[-M, M]` and scaled by `1 - η` misses a mass at most `2 δ` of `Q`, and + -- the completion `P` of it is at distance at most twice that mass. + obtain ⟨δ', hδ'0, hδ'⟩ := ENNReal.exists_nnreal_pos_mul_lt (b := ε) (a := 4) (by norm_num) + hε.ne' + set δ : ℝ≥0∞ := (δ' : ℝ≥0∞) + have hδ0 : δ ≠ 0 := ENNReal.coe_ne_zero.2 hδ'0.ne' + have hδ2 : 2 * (2 * δ) < ε := by + calc 2 * (2 * δ) = δ * 4 := by ring + _ < ε := hδ' + have hU : (⋃ M : ℕ, Icc (-(M : ℝ)) M) = univ := + eq_univ_of_forall fun x ↦ mem_iUnion.2 ⟨⌈|x|⌉₊, abs_le.1 (Nat.le_ceil _)⟩ + have htend : Tendsto (fun M : ℕ ↦ Q (Icc (-(M : ℝ)) (M : ℝ))) atTop (𝓝 1) := by + have := tendsto_measure_iUnion_atTop (μ := Q) (s := fun M : ℕ ↦ Icc (-(M : ℝ)) (M : ℝ)) + fun m n hmn ↦ Icc_subset_Icc (by simpa using hmn) (by simpa using hmn) + rwa [hU, measure_univ] at this + obtain ⟨M, hM⟩ := (htend.eventually (lt_mem_nhds + (ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero hδ0))).exists + set I := Icc (-(M : ℝ)) M + set η := min δ 2⁻¹ + have hη0 : η ≠ 0 := by simp [η, hδ0] + have hη1 : η ≤ 1 := ((min_le_right _ _).trans_lt ENNReal.one_half_lt_one).le + set ν := (1 - η) • Q.restrict I + have hνQ : ν ≤ Q := fun s ↦ by + calc ν s = (1 - η) * Q.restrict I s := rfl + _ ≤ Q.restrict I s := mul_le_of_le_one_left' tsub_le_self + _ ≤ Q s := Measure.restrict_le_self s + have hνuniv : ν univ = (1 - η) * Q I := by simp [ν] + have : IsFiniteMeasure ν := isFiniteMeasure_of_le Q hνQ + have hν1 : ν univ < 1 := by + rw [hνuniv] + calc (1 - η) * Q I ≤ 1 - η := mul_le_of_le_one_right' prob_le_one + _ < 1 := ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero hη0 + have hνM : ∀ᵐ x ∂ν, |x| ≤ (M : ℝ) := + Measure.ae_smul_measure + (ae_restrict_of_forall_mem measurableSet_Icc fun x hx ↦ abs_le.2 (mem_Icc.1 hx)) _ + obtain ⟨P, hP, hνP⟩ := exists_mem_meanZeroNull_le ν hν1 hνM + have := hP.1 + -- `ν` misses a mass less than `2 δ` of `Q`. + have hmiss : 1 - ν univ ≤ 2 * δ := by + refine tsub_le_iff_left.2 ?_ + calc (1 : ℝ≥0∞) ≤ Q I + δ := tsub_le_iff_right.1 hM.le + _ = (1 - η) * Q I + η * Q I + δ := by rw [← add_mul, tsub_add_cancel_of_le hη1, one_mul] + _ ≤ ν univ + 2 * δ := by + rw [hνuniv, two_mul, add_assoc] + gcongr + exact (mul_le_of_le_one_right' prob_le_one).trans (min_le_left _ _) + refine ⟨P, hP, lt_of_le_of_lt ?_ hδ2⟩ + calc etvDist P Q ≤ etvDist P ν + etvDist ν Q := etvDist_triangle _ _ _ + _ = (1 - ν univ) + (1 - ν univ) := by + rw [etvDist_of_ge hνP, etvDist_of_le hνQ, measure_univ (μ := P), measure_univ (μ := Q)] + _ ≤ 2 * (2 * δ) := by rw [← two_mul]; gcongr + +/-! ### E-variables -/ + +/-- **Same e-variables as for all laws.** For every finite set `ι` of i.i.d. real observations, a +function is an e-variable for the i.i.d. laws of the mean-zero null exactly when it is one for the +i.i.d. laws of all probability measures on `ℝ`. -/ +theorem isEVar_pi_meanZeroNull_iff {ι : Type*} [Fintype ι] {X : (ι → ℝ) → ℝ≥0∞} : + IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' meanZeroNull) ↔ + IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' {P | IsProbabilityMeasure P}) := + isEVar_pi_iff_of_forall_exists_etvDist_lt (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) + fun Q _ _ hε ↦ exists_mem_meanZeroNull_etvDist_lt Q hε + +/-- **One observation.** The e-variables for the laws on `ℝ` with mean `0` and a finite, positive +variance are the measurable functions bounded by `1` everywhere. -/ +theorem isEVar_meanZeroNull_iff {X : ℝ → ℝ≥0∞} : + IsEVar X meanZeroNull ↔ Measurable X ∧ ∀ x, X x ≤ 1 := + isEVar_iff_of_forall_exists_etvDist_dirac_lt + (fun _ hP ↦ (isProbabilityMeasure_of_mem_meanZeroNull hP).measure_univ.le) + fun x _ hε ↦ exists_mem_meanZeroNull_etvDist_lt (Measure.dirac x) hε + +/-! ### No power against i.i.d. alternatives -/ + +/-- **No growth.** For every law `Q` on `ℝ` and every number `n` of observations, the maximal +expected logarithm under `Q ^ n` of an `n`-sample e-variable for the i.i.d. laws of the mean-zero +null is `0`. -/ +theorem maxLogGrowth_meanZeroNull (Q : Measure ℝ) [IsProbabilityMeasure Q] (n : ℕ) : + maxLogGrowth Q meanZeroNull n = 0 := + maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt + (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) + (fun _ hε ↦ exists_mem_meanZeroNull_etvDist_lt Q hε) n + +/-- **The bipolar rate is zero.** For every law `Q` on `ℝ`, the optimal growth rate of the +evidence against the i.i.d. laws of the mean-zero null under the i.i.d. law of `Q` is `0`. -/ +theorem bipolarRate_meanZeroNull (Q : Measure ℝ) [IsProbabilityMeasure Q] : + bipolarRate Q meanZeroNull = 0 := + bipolarRate_eq_zero_of_forall_exists_etvDist_lt + (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) + fun _ hε ↦ exists_mem_meanZeroNull_etvDist_lt Q hε + +/-- **No power.** A measurable set of `ι` real observations with probability at most `α` under +the i.i.d. law of every member of the mean-zero null has probability at most `α` under the +i.i.d. law of every probability measure on `ℝ`. -/ +theorem measure_pi_le_of_forall_meanZeroNull {ι : Type*} [Fintype ι] {R : Set (ι → ℝ)} + (hR : MeasurableSet R) {α : ℝ≥0∞} + (hα : ∀ P ∈ meanZeroNull, Measure.pi (fun _ : ι ↦ P) R ≤ α) (Q : Measure ℝ) + [IsProbabilityMeasure Q] : + Measure.pi (fun _ : ι ↦ Q) R ≤ α := + measure_pi_le_of_forall_exists_etvDist_lt (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) + (fun _ hε ↦ exists_mem_meanZeroNull_etvDist_lt Q hε) hR hα + +/-- **Independent sequences.** Every e-process, for any filtration, for the laws of the +independent sequences of real observations whose marginals have mean `0` and a finite, positive +variance is at most `1` at every time and on every sequence. -/ +theorem le_one_of_isEProcess_infinitePi_meanZeroNull + {ℱ : Filtration ℕ (MeasurableSpace.pi : MeasurableSpace (ℕ → ℝ))} {E : ℕ → (ℕ → ℝ) → ℝ≥0∞} + (hE : IsEProcess E ℱ (Measure.infinitePi '' {P : ℕ → Measure ℝ | ∀ n, P n ∈ meanZeroNull})) + (n : ℕ) (x : ℕ → ℝ) : + E n x ≤ 1 := + ((isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt + (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) + (fun y _ hε ↦ exists_mem_meanZeroNull_etvDist_lt (Measure.dirac y) hε)).1 (hE.isEVar n)).2 x + +end ProbabilityTheory diff --git a/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean b/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean index c0baff2c..9b19d282 100644 --- a/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean +++ b/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean @@ -48,6 +48,7 @@ contraction of the oscillation of functions by a Markov kernel (Dobrushin's coef `|∫ f dμ - ∫ f dν| ≤ (b - a) / 2 * tvDist μ ν`, and `MeasureTheory.abs_integral_sub_integral_le_mul_tvDist_of_forall_sub_le` its form for `f` whose values differ by at most `c`. +* `MeasureTheory.measure_le_add_etvDist`: `μ s ≤ ν s + etvDist μ ν` for every measurable `s`. * `MeasureTheory.abs_measureReal_sub_measureReal_le_tvDist_div_two`, `MeasureTheory.tvDist_le_two_mul_of_forall_measureReal_le_add`: for measures of the same mass, the total variation distance bounds the difference of the masses of every event, and eventwise @@ -160,6 +161,20 @@ theorem abs_integral_sub_integral_le_mul_tvDist_of_forall_sub_le [IsFiniteMeasur /-! ### Eventwise bounds -/ +/-- **Events of measures close in total variation**, in `ℝ≥0∞`: every measurable event `s` +satisfies `μ s ≤ ν s + etvDist μ ν`. No finiteness is assumed: the distance is `∞` unless both +measures are finite. -/ +theorem measure_le_add_etvDist (μ ν : Measure 𝓧) {s : Set 𝓧} (hs : MeasurableSet s) : + μ s ≤ ν s + etvDist μ ν := by + by_cases h : IsFiniteMeasure μ ∧ IsFiniteMeasure ν + · obtain ⟨_, _⟩ := h + rw [etvDist_eq_iSup_sub_add_iSup_sub] + calc μ s ≤ ν s + (μ s - ν s) := le_add_tsub + _ ≤ _ := by + gcongr + exact le_add_right (le_iSup₂ (f := fun A (_ : MeasurableSet A) ↦ μ A - ν A) s hs) + · simp [etvDist_of_not_isFiniteMeasure h] + /-- **Events of measures of the same mass close in total variation**: for finite measures `μ` and `ν` of the same mass, every measurable event `s` satisfies `|μ s - ν s| ≤ tvDist μ ν / 2`. -/ diff --git a/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean b/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean new file mode 100644 index 00000000..a9ae716e --- /dev/null +++ b/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean @@ -0,0 +1,133 @@ +/- +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.Constructions.Pi +public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs + +import Mathlib.MeasureTheory.Measure.TotalVariation.Basic +import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RNDerivProd + +/-! +# Total variation distance between product measures + +The total variation distance between two finite products of probability measures is at most the +sum of the distances between the factors: + +```text +etvDist (Measure.pi μ) (Measure.pi ν) ≤ ∑ i, etvDist (μ i) (ν i). +``` + +In particular `n` independent observations of `μ` and of `ν` are at distance at most +`n * etvDist μ ν`, so that the `n`-fold products of a sequence of laws that converges to `ν` in +total variation converge to the `n`-fold product of `ν`. + +## Main statements + +* `MeasureTheory.etvDist_pi_le_sum`: the total variation distance between products of + probability measures is at most the sum of the distances between the factors. + +## Implementation notes + +The proof goes through a common minorant of two finite measures: on a Hahn decomposition `s` of +`(μ, ν)`, the measure `ρ = μ.restrict s + ν.restrict sᶜ` is below `μ` and `ν`, with +`μ univ + ν univ = 2 * ρ univ + etvDist μ ν`. For probability measures the product of +the minorants is below both products and has mass `∏ i, ρ i univ`, so the distance between the +products is at most `2 * (1 - ∏ i, ρ i univ) ≤ ∑ i, 2 * (1 - ρ i univ)`. +-/ + +public section + +open Set +open scoped ENNReal + +namespace MeasureTheory + +variable {ι : Type*} [Fintype ι] {X : ι → Type*} {mX : ∀ i, MeasurableSpace (X i)} + +/-- The product of finite measures is monotone in each factor. -/ +private lemma pi_mono {μ ν : ∀ i, Measure (X i)} [∀ i, IsFiniteMeasure (ν i)] + (h : ∀ i, μ i ≤ ν i) : + Measure.pi μ ≤ Measure.pi ν := by + have (i : ι) : IsFiniteMeasure (μ i) := isFiniteMeasure_of_le (ν i) (h i) + rw [Measure.pi_eq_withDensity_prod_rnDeriv fun i ↦ Measure.absolutelyContinuous_of_le (h i)] + calc (Measure.pi ν).withDensity (fun x ↦ ∏ i, (μ i).rnDeriv (ν i) (x i)) + _ ≤ (Measure.pi ν).withDensity 1 := by + refine withDensity_mono ?_ + filter_upwards [Measure.ae_le_pi fun i ↦ Measure.rnDeriv_le_one_of_le (h i)] with x hx + exact Finset.prod_le_one fun i _ ↦ hx i + _ = Measure.pi ν := withDensity_one + +/-- A common minorant of two finite measures: on a Hahn decomposition `s`, the measure +`μ.restrict s + ν.restrict sᶜ` is below `μ` and `ν`, and its mass is the mean of the masses of `μ` +and `ν` minus half their total variation distance. -/ +private lemma exists_le_le_add_etvDist {α : Type*} {mα : MeasurableSpace α} (μ ν : Measure α) + [IsFiniteMeasure μ] [IsFiniteMeasure ν] : + ∃ ρ : Measure α, ρ ≤ μ ∧ ρ ≤ ν ∧ μ univ + ν univ = 2 * ρ univ + etvDist μ ν := by + obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν + refine ⟨μ.restrict s + ν.restrict sᶜ, ?_, ?_, ?_⟩ + · calc μ.restrict s + ν.restrict sᶜ ≤ μ.restrict s + μ.restrict sᶜ := + add_le_add le_rfl hs.ge_on_compl + _ = μ := Measure.restrict_add_restrict_compl hs.measurableSet + · calc μ.restrict s + ν.restrict sᶜ ≤ ν.restrict s + ν.restrict sᶜ := + add_le_add hs.le_on le_rfl + _ = ν := Measure.restrict_add_restrict_compl hs.measurableSet + · obtain ⟨a, ha⟩ := le_iff_exists_add.1 (by simpa using hs.le_on univ : μ s ≤ ν s) + obtain ⟨b, hb⟩ := le_iff_exists_add.1 (by simpa using hs.ge_on_compl univ : ν sᶜ ≤ μ sᶜ) + rw [hs.etvDist_eq, add_apply, Measure.restrict_apply_univ, Measure.restrict_apply_univ, + ← measure_add_measure_compl hs.measurableSet (μ := μ), + ← measure_add_measure_compl hs.measurableSet (μ := ν), ha, hb, + ENNReal.add_sub_cancel_left (measure_ne_top μ s), + ENNReal.add_sub_cancel_left (measure_ne_top ν sᶜ)] + ring + +/-- For numbers in `[0, 1]`, one minus their product is at most the sum of the numbers `1 - m i`: +the union bound for independent events of probabilities `1 - m i`. -/ +private lemma one_sub_prod_le_sum_one_sub {κ : Type*} (s : Finset κ) {m : κ → ℝ≥0∞} + (hm : ∀ i ∈ s, m i ≤ 1) : + 1 - ∏ i ∈ s, m i ≤ ∑ i ∈ s, (1 - m i) := by + classical + induction s using Finset.induction with + | empty => simp + | insert j s hj ih => + have hmj : m j ≤ 1 := hm j (Finset.mem_insert_self j s) + have hms : ∀ i ∈ s, m i ≤ 1 := fun i hi ↦ hm i (Finset.mem_insert_of_mem hi) + have hprod : ∏ i ∈ s, m i ≤ 1 := Finset.prod_le_one hms + rw [Finset.prod_insert hj, Finset.sum_insert hj] + calc 1 - m j * ∏ i ∈ s, m i ≤ (1 - m j) + (1 - ∏ i ∈ s, m i) := by + refine tsub_le_iff_right.2 ?_ + calc (1 : ℝ≥0∞) = (1 - m j) + m j * ((1 - ∏ i ∈ s, m i) + ∏ i ∈ s, m i) := by + rw [tsub_add_cancel_of_le hprod, mul_one, tsub_add_cancel_of_le hmj] + _ = (1 - m j) + (m j * (1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i) := by rw [mul_add] + _ ≤ (1 - m j) + ((1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i) := by + gcongr; exact mul_le_of_le_one_left' hmj + _ = (1 - m j) + (1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i := (add_assoc _ _ _).symm + _ ≤ (1 - m j) + ∑ i ∈ s, (1 - m i) := by gcongr; exact ih hms + +/-- **Total variation distance between product measures.** The total variation distance between +two finite products of probability measures is at most the sum of the distances between the +factors. -/ +theorem etvDist_pi_le_sum (μ ν : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] + [∀ i, IsProbabilityMeasure (ν i)] : + etvDist (Measure.pi μ) (Measure.pi ν) ≤ ∑ i, etvDist (μ i) (ν i) := by + choose ρ hρμ hρν hρ using fun i ↦ exists_le_le_add_etvDist (μ i) (ν i) + have (i : ι) : IsFiniteMeasure (ρ i) := isFiniteMeasure_of_le (μ i) (hρμ i) + have hm (i : ι) : ρ i univ ≤ 1 := (hρμ i univ).trans prob_le_one + calc etvDist (Measure.pi μ) (Measure.pi ν) + _ ≤ etvDist (Measure.pi μ) (Measure.pi ρ) + etvDist (Measure.pi ρ) (Measure.pi ν) := + etvDist_triangle _ _ _ + _ = 2 * (1 - ∏ i, ρ i univ) := by + rw [etvDist_of_ge (pi_mono hρμ), etvDist_of_le (pi_mono hρν)] + simp [Measure.pi_univ, two_mul] + _ ≤ 2 * ∑ i, (1 - ρ i univ) := by + gcongr; exact one_sub_prod_le_sum_one_sub _ fun i _ ↦ hm i + _ = ∑ i, 2 * (1 - ρ i univ) := Finset.mul_sum _ _ _ + _ ≤ ∑ i, etvDist (μ i) (ν i) := by + gcongr with i + rw [ENNReal.mul_sub fun _ _ ↦ ENNReal.ofNat_ne_top, mul_one, tsub_le_iff_left] + simpa [one_add_one_eq_two] using (hρ i).le + +end MeasureTheory From 94149e2d31e30661d9e6a9dd229df7efea85d995 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:17:32 +0100 Subject: [PATCH 2/5] refactor: address review of the total-variation nulls - Make the general helpers public in their own files: `Measure.pi_mono` (`@[gcongr]`) in `Constructions/Pi.lean`, `exists_le_le_add_etvDist` and `isProbabilityMeasure_of_forall_exists_etvDist_lt` in `TotalVariation/Basic.lean`, and `ENNReal.one_sub_prod_le_sum_one_sub` in `Basic/ENNReal/BigOperators.lean`. - Rename `meanZeroNull` to `meanZeroPosVarNull`, with its lemmas. - Credit [EVR26, Note 22] and the EValuesResearch formalization in the three files. - Replace definitional `rfl` steps by named lemmas, prove the mass, mean and variance of the completion without long rewrite chains, factor out the choice of the interval and the positivity of the variance, and drop an unused import. Co-Authored-By: Claude Code --- LMLExplore/Basic/ENNReal/BigOperators.lean | 28 ++- .../EValues/EffectiveSet/TotalVariation.lean | 35 ++- LMLExplore/EValues/MeanZeroNull.lean | 211 ++++++++++-------- .../MeasureTheory/Constructions/Pi.lean | 21 +- .../Measure/TotalVariation/Basic.lean | 46 ++++ .../Measure/TotalVariation/Pi.lean | 86 ++----- 6 files changed, 239 insertions(+), 188 deletions(-) diff --git a/LMLExplore/Basic/ENNReal/BigOperators.lean b/LMLExplore/Basic/ENNReal/BigOperators.lean index f02db8ce..d40e451f 100644 --- a/LMLExplore/Basic/ENNReal/BigOperators.lean +++ b/LMLExplore/Basic/ENNReal/BigOperators.lean @@ -8,7 +8,7 @@ module public import Mathlib.Basic.ENNReal.BigOperators /-! -# Weighted sums of finite extended nonnegative reals +# Weighted sums and products of extended nonnegative reals ## Main statements @@ -16,6 +16,9 @@ public import Mathlib.Basic.ENNReal.BigOperators extended nonnegative reals `g x` with nonnegative real weights `f x`, mapped back to `ℝ≥0∞`, is `∑ x ∈ s, ENNReal.ofReal (f x) * g x`. It moves a real convex combination of finite divergences, such as a mixture of the divergence vectors of finitely many models, to `ℝ≥0∞`. +* `ENNReal.one_sub_prod_le_sum_one_sub`: for numbers `m i ≤ 1`, + `1 - ∏ i ∈ s, m i ≤ ∑ i ∈ s, (1 - m i)`, the union bound for independent events of + probabilities `1 - m i`. -/ public section @@ -33,4 +36,27 @@ lemma ofReal_sum_mul_toReal {ι : Type*} {s : Finset ι} {f : ι → ℝ} {g : refine Finset.sum_congr rfl fun x hx ↦ ?_ rw [ofReal_mul (hf x hx), ofReal_toReal (hg x hx)] +/-- For numbers `m i ≤ 1`, one minus their product is at most the sum of the numbers `1 - m i`: +the union bound for independent events of probabilities `1 - m i`. -/ +lemma one_sub_prod_le_sum_one_sub {ι : Type*} (s : Finset ι) {m : ι → ℝ≥0∞} + (hm : ∀ i ∈ s, m i ≤ 1) : + 1 - ∏ i ∈ s, m i ≤ ∑ i ∈ s, (1 - m i) := by + classical + induction s using Finset.induction with + | empty => simp + | insert j s hj ih => + have hmj : m j ≤ 1 := hm j (Finset.mem_insert_self j s) + have hms : ∀ i ∈ s, m i ≤ 1 := fun i hi ↦ hm i (Finset.mem_insert_of_mem hi) + have hprod : ∏ i ∈ s, m i ≤ 1 := Finset.prod_le_one hms + rw [Finset.prod_insert hj, Finset.sum_insert hj] + calc 1 - m j * ∏ i ∈ s, m i ≤ (1 - m j) + (1 - ∏ i ∈ s, m i) := by + refine tsub_le_iff_right.2 ?_ + calc (1 : ℝ≥0∞) = (1 - m j) + m j * ((1 - ∏ i ∈ s, m i) + ∏ i ∈ s, m i) := by + rw [tsub_add_cancel_of_le hprod, mul_one, tsub_add_cancel_of_le hmj] + _ = (1 - m j) + (m j * (1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i) := by rw [mul_add] + _ ≤ (1 - m j) + ((1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i) := by + gcongr; exact mul_le_of_le_one_left' hmj + _ = (1 - m j) + (1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i := (add_assoc _ _ _).symm + _ ≤ (1 - m j) + ∑ i ∈ s, (1 - m i) := by gcongr; exact ih hms + end ENNReal diff --git a/LMLExplore/EValues/EffectiveSet/TotalVariation.lean b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean index 701e48f4..d6087a15 100644 --- a/LMLExplore/EValues/EffectiveSet/TotalVariation.lean +++ b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean @@ -39,8 +39,9 @@ laws: e-variables cannot tell it apart from the null of all laws, and they have `bipolarRate Q S` vanish, and a test of level `α` for the i.i.d. laws of `S` has power at most `α`. -The mean-zero null on `ℝ` (`ProbabilityTheory.meanZeroNull`) is the motivating instance; this is -the form for e-variables of the theorem of Bahadur and Savage [BS56]. +The null on `ℝ` of the laws with mean `0` and a finite, positive variance +(`ProbabilityTheory.meanZeroPosVarNull`) is the motivating instance; this is the form for +e-variables of the theorem of Bahadur and Savage [BS56]. ## Main statements @@ -68,10 +69,19 @@ e-variables by monotone convergence. Total variation enters only through the eve `μ s ≤ ν s + etvDist μ ν` (`MeasureTheory.measure_le_add_etvDist`) and its subadditivity over products. +The results are those of [EVR26, Note 22]. The proofs are rewritten from the Lean proofs in +`EValuesResearch/Results/PowerlessNulls.lean` (commit `dd4072f`) of the paper project +`RemyDegenne/evalues_research`, which proves the corollary directly, by common minorants and +truncation, and the statements for one observation and for sequences through the masses +`⨆ P ∈ S, P {x}`; here all of them go through the closure of the effective null. [BS56] is cited +for the theorem of which this is the form for e-variables; its proofs are not used. + ## References * [BS56] R. R. Bahadur and L. J. Savage, *The nonexistence of certain statistical procedures in nonparametric problems*, Ann. Math. Statist. 27 (1956). +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, Note 22, and the + Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026. -/ public section @@ -193,24 +203,6 @@ theorem isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt {ι : Type*} [Co variable {ι : Type*} [Fintype ι] {Q : Measure 𝓧} -/-- A limit in total variation of probability measures is a probability measure. -/ -private lemma isProbabilityMeasure_of_forall_exists_etvDist_lt - (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) : - IsProbabilityMeasure Q := by - have h (ε : NNReal) (hε : 0 < ε) : Q univ ≤ 1 + ε ∧ 1 ≤ Q univ + ε := by - obtain ⟨P, hP, hPQ⟩ := hQ ε (ENNReal.coe_pos.2 hε) - have := hS P hP - constructor - · calc Q univ ≤ P univ + etvDist Q P := measure_le_add_etvDist Q P .univ - _ ≤ 1 + ε := by - rw [measure_univ, etvDist_comm] - exact add_le_add le_rfl hPQ.le - · calc 1 = P univ := measure_univ.symm - _ ≤ Q univ + etvDist P Q := measure_le_add_etvDist P Q .univ - _ ≤ Q univ + ε := add_le_add le_rfl hPQ.le - exact ⟨le_antisymm (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).1) - (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).2)⟩ - /-- If `Q` is a limit in total variation of members of a null `S` of probability measures, then `Q ^ ι` is a limit in total variation of the products `P ^ ι` of members of `S`. -/ private lemma exists_etvDist_pi_lt (hS : ∀ P ∈ S, IsProbabilityMeasure P) @@ -290,8 +282,7 @@ theorem maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsPr · rintro _ ⟨P, hP, rfl⟩ have := hS P hP infer_instance - · rw [klIntegral_eq_klDiv rfl, klDiv_self] - rfl + · rw [klIntegral_eq_klDiv rfl, klDiv_self, EReal.coe_ennreal_zero] /-- **The bipolar rate against a limit in total variation is zero.** If a probability measure `Q` is a limit in total variation of members of a null `S` of probability measures, the optimal growth diff --git a/LMLExplore/EValues/MeanZeroNull.lean b/LMLExplore/EValues/MeanZeroNull.lean index ffbde47d..e4d592ed 100644 --- a/LMLExplore/EValues/MeanZeroNull.lean +++ b/LMLExplore/EValues/MeanZeroNull.lean @@ -9,14 +9,12 @@ public import LMLExplore.EValues.EffectiveSet.TotalVariation public import LMLExplore.EValues.EProcess public import Mathlib.Probability.Moments.Variance -import Mathlib.MeasureTheory.Measure.TotalVariation.Basic - /-! # The mean-zero null: e-variables without power -The null `meanZeroNull` of the laws on `ℝ` with mean `0` and a finite, positive variance is dense -in total variation among the probability measures on `ℝ`: a law `Q` is approximated by `Q` -restricted to a large interval and scaled by a factor below `1`, completed by two atoms that +The null `meanZeroPosVarNull` of the laws on `ℝ` with mean `0` and a finite, positive variance +is dense in total variation among the probability measures on `ℝ`: a law `Q` is approximated by +`Q` restricted to a large interval and scaled by a factor below `1`, completed by two atoms that restore the mean `0` and make the variance positive. So the results of `LMLExplore.EValues.EffectiveSet.TotalVariation` apply, and the null cannot be tested with e-variables against i.i.d. alternatives, the form for e-variables of the theorem of Bahadur and @@ -32,25 +30,38 @@ Savage [BS56]: ## Main definitions -* `ProbabilityTheory.meanZeroNull`: the laws on `ℝ` with mean `0` and finite, positive variance. +* `ProbabilityTheory.meanZeroPosVarNull`: the laws on `ℝ` with mean `0` and finite, positive + variance. ## Main statements -* `ProbabilityTheory.exists_mem_meanZeroNull_etvDist_lt`: the null is dense in total variation. -* `ProbabilityTheory.isEVar_pi_meanZeroNull_iff`: its `ι`-sample e-variables are those of the - i.i.d. laws of all probability measures. -* `ProbabilityTheory.isEVar_meanZeroNull_iff`: its one-observation e-variables are the measurable - functions bounded by `1`. -* `ProbabilityTheory.maxLogGrowth_meanZeroNull`, `ProbabilityTheory.bipolarRate_meanZeroNull`, - `ProbabilityTheory.measure_pi_le_of_forall_meanZeroNull`: no growth and no power against i.i.d. - alternatives. -* `ProbabilityTheory.le_one_of_isEProcess_infinitePi_meanZeroNull`: e-processes for the laws of - independent sequences with marginals in the null are at most `1`. +* `ProbabilityTheory.exists_mem_meanZeroPosVarNull_etvDist_lt`: the null is dense in total + variation. +* `ProbabilityTheory.isEVar_pi_meanZeroPosVarNull_iff`: its `ι`-sample e-variables are those of + the i.i.d. laws of all probability measures. +* `ProbabilityTheory.isEVar_meanZeroPosVarNull_iff`: its one-observation e-variables are the + measurable functions bounded by `1`. +* `ProbabilityTheory.maxLogGrowth_meanZeroPosVarNull`, + `ProbabilityTheory.bipolarRate_meanZeroPosVarNull`, + `ProbabilityTheory.measure_pi_le_of_forall_meanZeroPosVarNull`: no growth and no power against + i.i.d. alternatives. +* `ProbabilityTheory.le_one_of_isEProcess_infinitePi_meanZeroPosVarNull`: e-processes for the laws + of independent sequences with marginals in the null are at most `1`. + +## Implementation notes + +The density of the null, and its consequences, are the results of [EVR26, Note 22]. The +construction of the approximating laws is adapted from the Lean proof in +`EValuesResearch/Results/PowerlessNulls.lean` (commit `dd4072f`) of the paper project +`RemyDegenne/evalues_research`. [BS56] is cited for the theorem of which this is the form for +e-variables; its proofs are not used. ## References * [BS56] R. R. Bahadur and L. J. Savage, *The nonexistence of certain statistical procedures in nonparametric problems*, Ann. Math. Statist. 27 (1956). +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, Note 22, and the + Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026. -/ public section @@ -63,85 +74,95 @@ namespace ProbabilityTheory /-- The laws on `ℝ` with mean `0` and a finite, positive variance: the probability measures `μ` under which the identity is square integrable, with `∫ x ∂μ = 0` and `0 < variance id μ`. -/ -def meanZeroNull : Set (Measure ℝ) := +def meanZeroPosVarNull : Set (Measure ℝ) := {μ | IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧ ∫ x, x ∂μ = 0 ∧ 0 < variance id μ} -/-- Membership in the mean-zero null. -/ -lemma mem_meanZeroNull_iff {μ : Measure ℝ} : - μ ∈ meanZeroNull ↔ +/-- Membership in `meanZeroPosVarNull`. -/ +lemma mem_meanZeroPosVarNull_iff {μ : Measure ℝ} : + μ ∈ meanZeroPosVarNull ↔ IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧ ∫ x, x ∂μ = 0 ∧ 0 < variance id μ := Iff.rfl -/-- The members of the mean-zero null are probability measures. -/ -lemma isProbabilityMeasure_of_mem_meanZeroNull {μ : Measure ℝ} (hμ : μ ∈ meanZeroNull) : +/-- The members of `meanZeroPosVarNull` are probability measures. -/ +lemma isProbabilityMeasure_of_mem_meanZeroPosVarNull {μ : Measure ℝ} (hμ : μ ∈ meanZeroPosVarNull) : IsProbabilityMeasure μ := hμ.1 /-! ### Density in total variation -/ +/-- Adding two atoms of the same mass `c ≠ 0` at `z - 1` and `z + 1` to a measure `ν` gives a +measure under which the identity is not almost everywhere `0`. -/ +private lemma not_ae_eq_zero_add_smul_dirac (ν : Measure ℝ) {c : ℝ≥0∞} (hc : c ≠ 0) (z : ℝ) : + ¬ ∀ᵐ x ∂(ν + c • (Measure.dirac (z - 1) + Measure.dirac (z + 1))), x = 0 := by + intro h + have h₁ := (Measure.ae_ennreal_smul_measure_iff hc).1 (ae_add_measure_iff.1 h).2 + rw [ae_add_measure_iff, ae_dirac_iff (measurableSet_singleton 0), + ae_dirac_iff (measurableSet_singleton 0)] at h₁ + have h₂ : z - 1 = 0 := h₁.1 + have h₃ : z + 1 = 0 := h₁.2 + linarith + /-- **Completion to a law with mean zero.** A finite measure on `ℝ` of mass less than `1` carried -by a bounded interval is below a member of the mean-zero null: add two atoms of mass +by a bounded interval is below a member of `meanZeroPosVarNull`: add two atoms of mass `(1 - ν univ) / 2` at `z - 1` and `z + 1`, for the `z` that makes the mean `0`. -/ -private lemma exists_mem_meanZeroNull_le (ν : Measure ℝ) [IsFiniteMeasure ν] (hν : ν univ < 1) - {M : ℝ} (hM : ∀ᵐ x ∂ν, |x| ≤ M) : ∃ P ∈ meanZeroNull, ν ≤ P := by +private lemma exists_mem_meanZeroPosVarNull_le (ν : Measure ℝ) [IsFiniteMeasure ν] + (hν : ν univ < 1) {M : ℝ} (hM : ∀ᵐ x ∂ν, |x| ≤ M) : ∃ P ∈ meanZeroPosVarNull, ν ≤ P := by set b := ν.real univ with hb_def - have hb0 : 0 ≤ b := measureReal_nonneg have hb1 : b < 1 := ENNReal.toReal_lt_of_lt_ofReal (by simpa using hν) - have h1b : 1 - b ≠ 0 := by linarith set z := -(∫ x, x ∂ν) / (1 - b) with hz set c := ENNReal.ofReal ((1 - b) / 2) with hc have hc0 : c ≠ 0 := by rw [hc, ne_eq, ENNReal.ofReal_eq_zero, not_le]; linarith - have hct : c ≠ ∞ := ENNReal.ofReal_ne_top + have hct : c.toReal = (1 - b) / 2 := ENNReal.toReal_ofReal (by linarith) set D := Measure.dirac (z - 1) + Measure.dirac (z + 1) with hD - have : IsFiniteMeasure (c • D) := Measure.smul_finite D hct + have : IsFiniteMeasure (c • D) := Measure.smul_finite D ENNReal.ofReal_ne_top set P := ν + c • D with hP - have hDb : ∀ᵐ x ∂D, |x| ≤ |z| + 1 := by - rw [hD, ae_add_measure_iff, ae_dirac_eq, ae_dirac_eq, eventually_pure, eventually_pure] - exact ⟨abs_le.2 ⟨by linarith [neg_abs_le z], by linarith [le_abs_self z]⟩, - abs_le.2 ⟨by linarith [neg_abs_le z], by linarith [le_abs_self z]⟩⟩ have hPb : ∀ᵐ x ∂P, |x| ≤ max M (|z| + 1) := by - rw [hP, ae_add_measure_iff] - exact ⟨hM.mono fun x hx ↦ hx.trans (le_max_left _ _), - Measure.ae_smul_measure (hDb.mono fun x hx ↦ hx.trans (le_max_right _ _)) c⟩ + rw [hP, ae_add_measure_iff, hD] + refine ⟨hM.mono fun x hx ↦ hx.trans (le_max_left _ _), Measure.ae_smul_measure ?_ c⟩ + rw [ae_add_measure_iff, ae_dirac_eq, ae_dirac_eq, eventually_pure, eventually_pure] + constructor <;> exact (abs_le.2 ⟨by linarith [neg_abs_le z], by linarith [le_abs_self z]⟩).trans + (le_max_right _ _) have hint {μ : Measure ℝ} [IsFiniteMeasure μ] {K : ℝ} (hK : ∀ᵐ x ∂μ, |x| ≤ K) : Integrable (fun x : ℝ ↦ x) μ := Integrable.of_bound measurable_id.aestronglyMeasurable K (by simpa using hK) - have hDu : D univ = 2 := by simp [hD, one_add_one_eq_two] have hPprob : IsProbabilityMeasure P := by - constructor - rw [hP, add_apply, smul_apply, hDu, smul_eq_mul, - ← ofReal_measureReal (measure_ne_top ν univ), ← hb_def, hc, - ← ENNReal.ofReal_ofNat 2, ← ENNReal.ofReal_mul (by linarith), - ← ENNReal.ofReal_add hb0 (by linarith), ← ENNReal.ofReal_one] - congr 1 + rw [isProbabilityMeasure_iff_real, hP, measureReal_add_apply, measureReal_ennreal_smul_apply, + hD, measureReal_add_apply, hct, ← hb_def] + simp ring have hmean : ∫ x, x ∂P = 0 := by - rw [hP, integral_add_measure (hint hM) ((hint hDb).smul_measure hct), integral_smul_measure, - hD, integral_add_measure (integrable_dirac (by simp)) (integrable_dirac (by simp)), - integral_dirac, integral_dirac, hc, ENNReal.toReal_ofReal (by linarith), hz, smul_eq_mul] + have hDint : Integrable (fun x : ℝ ↦ x) D := + (integrable_dirac (by simp)).add_measure (integrable_dirac (by simp)) + rw [hP, integral_add_measure (hint hM) (hDint.smul_measure ENNReal.ofReal_ne_top), + integral_smul_measure, hD, integral_add_measure (integrable_dirac (by simp)) + (integrable_dirac (by simp)), integral_dirac, integral_dirac, hct, hz, smul_eq_mul] field_simp ring have hmem : MemLp id 2 P := MemLp.of_bound measurable_id.aestronglyMeasurable (max M (|z| + 1)) (hPb.mono fun x hx ↦ by simpa [Real.norm_eq_abs] using hx) have hvar : 0 < variance id P := by - refine ENNReal.toReal_pos ?_ hmem.evariance_lt_top.ne - have hz2 : ‖z - 1‖ₑ ^ 2 + ‖z + 1‖ₑ ^ 2 ≠ 0 := by - simp only [ne_eq, add_eq_zero, pow_eq_zero_iff two_ne_zero, eNorm_eq_zero, not_and] - intro h1 - linarith - have hge : c * (‖z - 1‖ₑ ^ 2 + ‖z + 1‖ₑ ^ 2) ≤ evariance id P := by - calc c * (‖z - 1‖ₑ ^ 2 + ‖z + 1‖ₑ ^ 2) = ∫⁻ x, ‖x - 0‖ₑ ^ 2 ∂(c • D) := by - rw [lintegral_smul_measure, hD, lintegral_add_measure, lintegral_dirac, - lintegral_dirac, smul_eq_mul, sub_zero, sub_zero] - _ ≤ ∫⁻ x, ‖x - 0‖ₑ ^ 2 ∂P := lintegral_mono' (Measure.le_add_left le_rfl) le_rfl - _ = evariance id P := by rw [evariance, ← hmean]; rfl - exact (lt_of_lt_of_le (ENNReal.mul_pos hc0 hz2) hge).ne' + refine ENNReal.toReal_pos (fun h0 ↦ not_ae_eq_zero_add_smul_dirac ν hc0 z ?_) + hmem.evariance_lt_top.ne + have h := (evariance_eq_zero_iff measurable_id.aemeasurable).1 h0 + simp only [id_eq, hmean] at h + exact h exact ⟨P, ⟨hPprob, hmem, hmean, hvar⟩, Measure.le_add_right le_rfl⟩ -/-- **The mean-zero null is dense in total variation**: every probability measure on `ℝ` is a -limit in total variation of laws with mean `0` and a finite, positive variance. -/ -theorem exists_mem_meanZeroNull_etvDist_lt (Q : Measure ℝ) [IsProbabilityMeasure Q] - {ε : ℝ≥0∞} (hε : 0 < ε) : ∃ P ∈ meanZeroNull, etvDist P Q < ε := by +/-- A probability measure on `ℝ` gives a mass more than `1 - δ` to some interval `[-M, M]`. -/ +private lemma exists_one_sub_lt_measure_Icc (Q : Measure ℝ) [IsProbabilityMeasure Q] {δ : ℝ≥0∞} + (hδ : δ ≠ 0) : ∃ M : ℕ, 1 - δ < Q (Icc (-(M : ℝ)) M) := by + have hU : (⋃ M : ℕ, Icc (-(M : ℝ)) M) = univ := + eq_univ_of_forall fun x ↦ mem_iUnion.2 ⟨⌈|x|⌉₊, abs_le.1 (Nat.le_ceil _)⟩ + have htend := tendsto_measure_iUnion_atTop (μ := Q) (s := fun M : ℕ ↦ Icc (-(M : ℝ)) M) + fun m n hmn ↦ Icc_subset_Icc (by simpa using hmn) (by simpa using hmn) + rw [hU, measure_univ] at htend + exact (htend.eventually (lt_mem_nhds + (ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero hδ))).exists + +/-- **The null `meanZeroPosVarNull` is dense in total variation**: every probability measure on +`ℝ` is a limit in total variation of laws with mean `0` and a finite, positive variance. -/ +theorem exists_mem_meanZeroPosVarNull_etvDist_lt (Q : Measure ℝ) [IsProbabilityMeasure Q] + {ε : ℝ≥0∞} (hε : 0 < ε) : ∃ P ∈ meanZeroPosVarNull, etvDist P Q < ε := by -- `Q` restricted to `[-M, M]` and scaled by `1 - η` misses a mass at most `2 δ` of `Q`, and -- the completion `P` of it is at distance at most twice that mass. obtain ⟨δ', hδ'0, hδ'⟩ := ENNReal.exists_nnreal_pos_mul_lt (b := ε) (a := 4) (by norm_num) @@ -151,23 +172,15 @@ theorem exists_mem_meanZeroNull_etvDist_lt (Q : Measure ℝ) [IsProbabilityMeasu have hδ2 : 2 * (2 * δ) < ε := by calc 2 * (2 * δ) = δ * 4 := by ring _ < ε := hδ' - have hU : (⋃ M : ℕ, Icc (-(M : ℝ)) M) = univ := - eq_univ_of_forall fun x ↦ mem_iUnion.2 ⟨⌈|x|⌉₊, abs_le.1 (Nat.le_ceil _)⟩ - have htend : Tendsto (fun M : ℕ ↦ Q (Icc (-(M : ℝ)) (M : ℝ))) atTop (𝓝 1) := by - have := tendsto_measure_iUnion_atTop (μ := Q) (s := fun M : ℕ ↦ Icc (-(M : ℝ)) (M : ℝ)) - fun m n hmn ↦ Icc_subset_Icc (by simpa using hmn) (by simpa using hmn) - rwa [hU, measure_univ] at this - obtain ⟨M, hM⟩ := (htend.eventually (lt_mem_nhds - (ENNReal.sub_lt_self ENNReal.one_ne_top one_ne_zero hδ0))).exists + obtain ⟨M, hM⟩ := exists_one_sub_lt_measure_Icc Q hδ0 set I := Icc (-(M : ℝ)) M set η := min δ 2⁻¹ have hη0 : η ≠ 0 := by simp [η, hδ0] have hη1 : η ≤ 1 := ((min_le_right _ _).trans_lt ENNReal.one_half_lt_one).le set ν := (1 - η) • Q.restrict I have hνQ : ν ≤ Q := fun s ↦ by - calc ν s = (1 - η) * Q.restrict I s := rfl - _ ≤ Q.restrict I s := mul_le_of_le_one_left' tsub_le_self - _ ≤ Q s := Measure.restrict_le_self s + rw [smul_apply, smul_eq_mul] + exact (mul_le_of_le_one_left' tsub_le_self).trans (Measure.restrict_le_self s) have hνuniv : ν univ = (1 - η) * Q I := by simp [ν] have : IsFiniteMeasure ν := isFiniteMeasure_of_le Q hνQ have hν1 : ν univ < 1 := by @@ -177,7 +190,7 @@ theorem exists_mem_meanZeroNull_etvDist_lt (Q : Measure ℝ) [IsProbabilityMeasu have hνM : ∀ᵐ x ∂ν, |x| ≤ (M : ℝ) := Measure.ae_smul_measure (ae_restrict_of_forall_mem measurableSet_Icc fun x hx ↦ abs_le.2 (mem_Icc.1 hx)) _ - obtain ⟨P, hP, hνP⟩ := exists_mem_meanZeroNull_le ν hν1 hνM + obtain ⟨P, hP, hνP⟩ := exists_mem_meanZeroPosVarNull_le ν hν1 hνM have := hP.1 -- `ν` misses a mass less than `2 δ` of `Q`. have hmiss : 1 - ν univ ≤ 2 * δ := by @@ -199,60 +212,62 @@ theorem exists_mem_meanZeroNull_etvDist_lt (Q : Measure ℝ) [IsProbabilityMeasu /-- **Same e-variables as for all laws.** For every finite set `ι` of i.i.d. real observations, a function is an e-variable for the i.i.d. laws of the mean-zero null exactly when it is one for the i.i.d. laws of all probability measures on `ℝ`. -/ -theorem isEVar_pi_meanZeroNull_iff {ι : Type*} [Fintype ι] {X : (ι → ℝ) → ℝ≥0∞} : - IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' meanZeroNull) ↔ +theorem isEVar_pi_meanZeroPosVarNull_iff {ι : Type*} [Fintype ι] {X : (ι → ℝ) → ℝ≥0∞} : + IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' meanZeroPosVarNull) ↔ IsEVar X ((fun P ↦ Measure.pi fun _ : ι ↦ P) '' {P | IsProbabilityMeasure P}) := - isEVar_pi_iff_of_forall_exists_etvDist_lt (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) - fun Q _ _ hε ↦ exists_mem_meanZeroNull_etvDist_lt Q hε + isEVar_pi_iff_of_forall_exists_etvDist_lt (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull) + fun Q _ _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt Q hε /-- **One observation.** The e-variables for the laws on `ℝ` with mean `0` and a finite, positive variance are the measurable functions bounded by `1` everywhere. -/ -theorem isEVar_meanZeroNull_iff {X : ℝ → ℝ≥0∞} : - IsEVar X meanZeroNull ↔ Measurable X ∧ ∀ x, X x ≤ 1 := +theorem isEVar_meanZeroPosVarNull_iff {X : ℝ → ℝ≥0∞} : + IsEVar X meanZeroPosVarNull ↔ Measurable X ∧ ∀ x, X x ≤ 1 := isEVar_iff_of_forall_exists_etvDist_dirac_lt - (fun _ hP ↦ (isProbabilityMeasure_of_mem_meanZeroNull hP).measure_univ.le) - fun x _ hε ↦ exists_mem_meanZeroNull_etvDist_lt (Measure.dirac x) hε + (fun _ hP ↦ (isProbabilityMeasure_of_mem_meanZeroPosVarNull hP).measure_univ.le) + fun x _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt (Measure.dirac x) hε /-! ### No power against i.i.d. alternatives -/ /-- **No growth.** For every law `Q` on `ℝ` and every number `n` of observations, the maximal expected logarithm under `Q ^ n` of an `n`-sample e-variable for the i.i.d. laws of the mean-zero null is `0`. -/ -theorem maxLogGrowth_meanZeroNull (Q : Measure ℝ) [IsProbabilityMeasure Q] (n : ℕ) : - maxLogGrowth Q meanZeroNull n = 0 := +theorem maxLogGrowth_meanZeroPosVarNull (Q : Measure ℝ) [IsProbabilityMeasure Q] (n : ℕ) : + maxLogGrowth Q meanZeroPosVarNull n = 0 := maxLogGrowth_eq_zero_of_forall_exists_etvDist_lt - (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) - (fun _ hε ↦ exists_mem_meanZeroNull_etvDist_lt Q hε) n + (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull) + (fun _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt Q hε) n /-- **The bipolar rate is zero.** For every law `Q` on `ℝ`, the optimal growth rate of the evidence against the i.i.d. laws of the mean-zero null under the i.i.d. law of `Q` is `0`. -/ -theorem bipolarRate_meanZeroNull (Q : Measure ℝ) [IsProbabilityMeasure Q] : - bipolarRate Q meanZeroNull = 0 := +theorem bipolarRate_meanZeroPosVarNull (Q : Measure ℝ) [IsProbabilityMeasure Q] : + bipolarRate Q meanZeroPosVarNull = 0 := bipolarRate_eq_zero_of_forall_exists_etvDist_lt - (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) - fun _ hε ↦ exists_mem_meanZeroNull_etvDist_lt Q hε + (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull) + fun _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt Q hε /-- **No power.** A measurable set of `ι` real observations with probability at most `α` under the i.i.d. law of every member of the mean-zero null has probability at most `α` under the i.i.d. law of every probability measure on `ℝ`. -/ -theorem measure_pi_le_of_forall_meanZeroNull {ι : Type*} [Fintype ι] {R : Set (ι → ℝ)} +theorem measure_pi_le_of_forall_meanZeroPosVarNull {ι : Type*} [Fintype ι] {R : Set (ι → ℝ)} (hR : MeasurableSet R) {α : ℝ≥0∞} - (hα : ∀ P ∈ meanZeroNull, Measure.pi (fun _ : ι ↦ P) R ≤ α) (Q : Measure ℝ) + (hα : ∀ P ∈ meanZeroPosVarNull, Measure.pi (fun _ : ι ↦ P) R ≤ α) (Q : Measure ℝ) [IsProbabilityMeasure Q] : Measure.pi (fun _ : ι ↦ Q) R ≤ α := - measure_pi_le_of_forall_exists_etvDist_lt (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) - (fun _ hε ↦ exists_mem_meanZeroNull_etvDist_lt Q hε) hR hα + measure_pi_le_of_forall_exists_etvDist_lt (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull) + (fun _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt Q hε) hR hα /-- **Independent sequences.** Every e-process, for any filtration, for the laws of the independent sequences of real observations whose marginals have mean `0` and a finite, positive variance is at most `1` at every time and on every sequence. -/ -theorem le_one_of_isEProcess_infinitePi_meanZeroNull +theorem le_one_of_isEProcess_infinitePi_meanZeroPosVarNull {ℱ : Filtration ℕ (MeasurableSpace.pi : MeasurableSpace (ℕ → ℝ))} {E : ℕ → (ℕ → ℝ) → ℝ≥0∞} - (hE : IsEProcess E ℱ (Measure.infinitePi '' {P : ℕ → Measure ℝ | ∀ n, P n ∈ meanZeroNull})) + (hE : IsEProcess E ℱ + (Measure.infinitePi '' {P : ℕ → Measure ℝ | ∀ n, P n ∈ meanZeroPosVarNull})) (n : ℕ) (x : ℕ → ℝ) : E n x ≤ 1 := ((isEVar_infinitePi_iff_of_forall_exists_etvDist_dirac_lt - (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroNull) - (fun y _ hε ↦ exists_mem_meanZeroNull_etvDist_lt (Measure.dirac y) hε)).1 (hE.isEVar n)).2 x + (fun _ ↦ isProbabilityMeasure_of_mem_meanZeroPosVarNull) + (fun y _ hε ↦ exists_mem_meanZeroPosVarNull_etvDist_lt (Measure.dirac y) hε)).1 + (hE.isEVar n)).2 x end ProbabilityTheory diff --git a/LMLExplore/MeasureTheory/Constructions/Pi.lean b/LMLExplore/MeasureTheory/Constructions/Pi.lean index cc275003..9fb0c739 100644 --- a/LMLExplore/MeasureTheory/Constructions/Pi.lean +++ b/LMLExplore/MeasureTheory/Constructions/Pi.lean @@ -7,10 +7,13 @@ module public import Mathlib.MeasureTheory.Constructions.Pi public import Mathlib.Probability.ConditionalProbability +import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RNDerivProd import TauCeti.MeasureTheory.Constructions.Pi /-! -# Product measures: laws of coordinatewise images, restricted factors and bounds by lines +# Product measures: monotonicity, coordinatewise images, restricted factors, bounds by lines + +The product of finite measures is monotone in its factors. 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 @@ -26,6 +29,8 @@ all have `μ i`-measure at most `c` has product measure at most `c`, by resampli ## Main statements +* `MeasureTheory.Measure.pi_mono`: if `μ i ≤ ν i` for every `i`, with every `ν i` finite, then + `Measure.pi μ ≤ Measure.pi ν`. * `MeasureTheory.Measure.map_pi_comp_eq_map_pi_map`: `(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`: @@ -46,6 +51,20 @@ namespace MeasureTheory.Measure variable {ι : Type*} [Fintype ι] {Ω 𝓨 : ι → Type*} {mΩ : ∀ i, MeasurableSpace (Ω i)} [∀ i, MeasurableSpace (𝓨 i)] {β : Type*} {mβ : MeasurableSpace β} +/-- **Monotonicity of the product measure.** The product of finite measures is monotone in its +factors: if `μ i ≤ ν i` for every `i`, then `Measure.pi μ ≤ Measure.pi ν`. -/ +@[gcongr] +lemma pi_mono {μ ν : ∀ i, Measure (Ω i)} [∀ i, IsFiniteMeasure (ν i)] (h : ∀ i, μ i ≤ ν i) : + Measure.pi μ ≤ Measure.pi ν := by + have (i : ι) : IsFiniteMeasure (μ i) := isFiniteMeasure_of_le (ν i) (h i) + rw [pi_eq_withDensity_prod_rnDeriv fun i ↦ absolutelyContinuous_of_le (h i)] + calc (Measure.pi ν).withDensity (fun x ↦ ∏ i, (μ i).rnDeriv (ν i) (x i)) + _ ≤ (Measure.pi ν).withDensity 1 := by + refine withDensity_mono ?_ + filter_upwards [ae_le_pi fun i ↦ rnDeriv_le_one_of_le (h i)] with x hx + exact Finset.prod_le_one fun i _ ↦ hx i + _ = Measure.pi ν := withDensity_one + /-- The law under a product measure 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`. -/ lemma map_pi_comp_eq_map_pi_map {μ : ∀ i, Measure (Ω i)} {X : ∀ i, Ω i → 𝓨 i} diff --git a/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean b/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean index 9b19d282..3d94b281 100644 --- a/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean +++ b/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean @@ -10,6 +10,7 @@ public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs import Mathlib.MeasureTheory.Integral.Bochner.Set import Mathlib.MeasureTheory.Integral.IntegrableOn +import Mathlib.MeasureTheory.Measure.TotalVariation.Basic import Mathlib.MeasureTheory.VectorMeasure.Integral import LMLExplore.Order.ConditionallyCompleteLattice.Group import TauCeti.MeasureTheory.Measure.TotalVariation.Basic @@ -49,6 +50,10 @@ contraction of the oscillation of functions by a Markov kernel (Dobrushin's coef `MeasureTheory.abs_integral_sub_integral_le_mul_tvDist_of_forall_sub_le` its form for `f` whose values differ by at most `c`. * `MeasureTheory.measure_le_add_etvDist`: `μ s ≤ ν s + etvDist μ ν` for every measurable `s`. +* `MeasureTheory.isProbabilityMeasure_of_forall_exists_etvDist_lt`: a limit in total variation of + probability measures is a probability measure. +* `MeasureTheory.exists_le_le_add_etvDist`: two finite measures have a common minorant `ρ` with + `μ univ + ν univ = 2 * ρ univ + etvDist μ ν`. * `MeasureTheory.abs_measureReal_sub_measureReal_le_tvDist_div_two`, `MeasureTheory.tvDist_le_two_mul_of_forall_measureReal_le_add`: for measures of the same mass, the total variation distance bounds the difference of the masses of every event, and eventwise @@ -175,6 +180,47 @@ theorem measure_le_add_etvDist (μ ν : Measure 𝓧) {s : Set 𝓧} (hs : Measu exact le_add_right (le_iSup₂ (f := fun A (_ : MeasurableSet A) ↦ μ A - ν A) s hs) · simp [etvDist_of_not_isFiniteMeasure h] +/-- A limit in total variation of probability measures is a probability measure. -/ +theorem isProbabilityMeasure_of_forall_exists_etvDist_lt {S : Set (Measure 𝓧)} {Q : Measure 𝓧} + (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) : + IsProbabilityMeasure Q := by + have h (ε : ℝ≥0) (hε : 0 < ε) : Q univ ≤ 1 + ε ∧ 1 ≤ Q univ + ε := by + obtain ⟨P, hP, hPQ⟩ := hQ ε (ENNReal.coe_pos.2 hε) + have := hS P hP + constructor + · calc Q univ ≤ P univ + etvDist Q P := measure_le_add_etvDist Q P .univ + _ ≤ 1 + ε := by + rw [measure_univ, etvDist_comm] + exact add_le_add le_rfl hPQ.le + · calc 1 = P univ := measure_univ.symm + _ ≤ Q univ + etvDist P Q := measure_le_add_etvDist P Q .univ + _ ≤ Q univ + ε := add_le_add le_rfl hPQ.le + exact ⟨le_antisymm (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).1) + (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).2)⟩ + +/-- **A common minorant of two finite measures.** On a Hahn decomposition `s`, the measure +`μ.restrict s + ν.restrict sᶜ` is below `μ` and `ν`, and its mass is the mean of the masses of `μ` +and `ν` minus half their total variation distance. -/ +theorem exists_le_le_add_etvDist (μ ν : Measure 𝓧) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : + ∃ ρ : Measure 𝓧, ρ ≤ μ ∧ ρ ≤ ν ∧ μ univ + ν univ = 2 * ρ univ + etvDist μ ν := by + obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν + refine ⟨μ.restrict s + ν.restrict sᶜ, ?_, ?_, ?_⟩ + · calc μ.restrict s + ν.restrict sᶜ ≤ μ.restrict s + μ.restrict sᶜ := + add_le_add le_rfl hs.ge_on_compl + _ = μ := Measure.restrict_add_restrict_compl hs.measurableSet + · calc μ.restrict s + ν.restrict sᶜ ≤ ν.restrict s + ν.restrict sᶜ := + add_le_add hs.le_on le_rfl + _ = ν := Measure.restrict_add_restrict_compl hs.measurableSet + · have h₁ : μ s ≤ ν s := by simpa using hs.le_on univ + have h₂ : ν sᶜ ≤ μ sᶜ := by simpa using hs.ge_on_compl univ + calc μ univ + ν univ = (μ s + μ sᶜ) + (ν s + ν sᶜ) := by + rw [measure_add_measure_compl hs.measurableSet, + measure_add_measure_compl hs.measurableSet] + _ = (μ s + (ν sᶜ + (μ sᶜ - ν sᶜ))) + ((μ s + (ν s - μ s)) + ν sᶜ) := by + rw [add_tsub_cancel_of_le h₁, add_tsub_cancel_of_le h₂] + _ = 2 * (μ s + ν sᶜ) + ((ν s - μ s) + (μ sᶜ - ν sᶜ)) := by ring + _ = 2 * (μ.restrict s + ν.restrict sᶜ) univ + etvDist μ ν := by simp [hs.etvDist_eq] + /-- **Events of measures of the same mass close in total variation**: for finite measures `μ` and `ν` of the same mass, every measurable event `s` satisfies `|μ s - ν s| ≤ tvDist μ ν / 2`. -/ diff --git a/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean b/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean index a9ae716e..3d6f4da5 100644 --- a/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean +++ b/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean @@ -9,7 +9,9 @@ public import Mathlib.MeasureTheory.Constructions.Pi public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs import Mathlib.MeasureTheory.Measure.TotalVariation.Basic -import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RNDerivProd +import LMLExplore.Basic.ENNReal.BigOperators +import LMLExplore.MeasureTheory.Constructions.Pi +import LMLExplore.MeasureTheory.Measure.TotalVariation.Basic /-! # Total variation distance between product measures @@ -32,11 +34,22 @@ total variation converge to the `n`-fold product of `ν`. ## Implementation notes -The proof goes through a common minorant of two finite measures: on a Hahn decomposition `s` of -`(μ, ν)`, the measure `ρ = μ.restrict s + ν.restrict sᶜ` is below `μ` and `ν`, with +The proof goes through a common minorant of two finite measures +(`MeasureTheory.exists_le_le_add_etvDist`): on a Hahn decomposition `s` of `(μ, ν)`, the measure +`ρ = μ.restrict s + ν.restrict sᶜ` is below `μ` and `ν`, with `μ univ + ν univ = 2 * ρ univ + etvDist μ ν`. For probability measures the product of -the minorants is below both products and has mass `∏ i, ρ i univ`, so the distance between the -products is at most `2 * (1 - ∏ i, ρ i univ) ≤ ∑ i, 2 * (1 - ρ i univ)`. +the minorants is below both products (`MeasureTheory.Measure.pi_mono`) and has mass +`∏ i, ρ i univ`, so the distance between the products is at most +`2 * (1 - ∏ i, ρ i univ) ≤ ∑ i, 2 * (1 - ρ i univ)` (`ENNReal.one_sub_prod_le_sum_one_sub`). + +The argument, common minorants and the bound `1 - ∏ i, m i ≤ ∑ i, (1 - m i)`, is adapted from +the Lean proof of [EVR26, Note 22] in `EValuesResearch/Results/PowerlessNulls.lean` +(commit `dd4072f`) of the paper project `RemyDegenne/evalues_research`. + +## References + +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, Note 22, and the + Lean library `EValuesResearch` of github.com/RemyDegenne/evalues_research, 2026. -/ public section @@ -48,65 +61,6 @@ namespace MeasureTheory variable {ι : Type*} [Fintype ι] {X : ι → Type*} {mX : ∀ i, MeasurableSpace (X i)} -/-- The product of finite measures is monotone in each factor. -/ -private lemma pi_mono {μ ν : ∀ i, Measure (X i)} [∀ i, IsFiniteMeasure (ν i)] - (h : ∀ i, μ i ≤ ν i) : - Measure.pi μ ≤ Measure.pi ν := by - have (i : ι) : IsFiniteMeasure (μ i) := isFiniteMeasure_of_le (ν i) (h i) - rw [Measure.pi_eq_withDensity_prod_rnDeriv fun i ↦ Measure.absolutelyContinuous_of_le (h i)] - calc (Measure.pi ν).withDensity (fun x ↦ ∏ i, (μ i).rnDeriv (ν i) (x i)) - _ ≤ (Measure.pi ν).withDensity 1 := by - refine withDensity_mono ?_ - filter_upwards [Measure.ae_le_pi fun i ↦ Measure.rnDeriv_le_one_of_le (h i)] with x hx - exact Finset.prod_le_one fun i _ ↦ hx i - _ = Measure.pi ν := withDensity_one - -/-- A common minorant of two finite measures: on a Hahn decomposition `s`, the measure -`μ.restrict s + ν.restrict sᶜ` is below `μ` and `ν`, and its mass is the mean of the masses of `μ` -and `ν` minus half their total variation distance. -/ -private lemma exists_le_le_add_etvDist {α : Type*} {mα : MeasurableSpace α} (μ ν : Measure α) - [IsFiniteMeasure μ] [IsFiniteMeasure ν] : - ∃ ρ : Measure α, ρ ≤ μ ∧ ρ ≤ ν ∧ μ univ + ν univ = 2 * ρ univ + etvDist μ ν := by - obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν - refine ⟨μ.restrict s + ν.restrict sᶜ, ?_, ?_, ?_⟩ - · calc μ.restrict s + ν.restrict sᶜ ≤ μ.restrict s + μ.restrict sᶜ := - add_le_add le_rfl hs.ge_on_compl - _ = μ := Measure.restrict_add_restrict_compl hs.measurableSet - · calc μ.restrict s + ν.restrict sᶜ ≤ ν.restrict s + ν.restrict sᶜ := - add_le_add hs.le_on le_rfl - _ = ν := Measure.restrict_add_restrict_compl hs.measurableSet - · obtain ⟨a, ha⟩ := le_iff_exists_add.1 (by simpa using hs.le_on univ : μ s ≤ ν s) - obtain ⟨b, hb⟩ := le_iff_exists_add.1 (by simpa using hs.ge_on_compl univ : ν sᶜ ≤ μ sᶜ) - rw [hs.etvDist_eq, add_apply, Measure.restrict_apply_univ, Measure.restrict_apply_univ, - ← measure_add_measure_compl hs.measurableSet (μ := μ), - ← measure_add_measure_compl hs.measurableSet (μ := ν), ha, hb, - ENNReal.add_sub_cancel_left (measure_ne_top μ s), - ENNReal.add_sub_cancel_left (measure_ne_top ν sᶜ)] - ring - -/-- For numbers in `[0, 1]`, one minus their product is at most the sum of the numbers `1 - m i`: -the union bound for independent events of probabilities `1 - m i`. -/ -private lemma one_sub_prod_le_sum_one_sub {κ : Type*} (s : Finset κ) {m : κ → ℝ≥0∞} - (hm : ∀ i ∈ s, m i ≤ 1) : - 1 - ∏ i ∈ s, m i ≤ ∑ i ∈ s, (1 - m i) := by - classical - induction s using Finset.induction with - | empty => simp - | insert j s hj ih => - have hmj : m j ≤ 1 := hm j (Finset.mem_insert_self j s) - have hms : ∀ i ∈ s, m i ≤ 1 := fun i hi ↦ hm i (Finset.mem_insert_of_mem hi) - have hprod : ∏ i ∈ s, m i ≤ 1 := Finset.prod_le_one hms - rw [Finset.prod_insert hj, Finset.sum_insert hj] - calc 1 - m j * ∏ i ∈ s, m i ≤ (1 - m j) + (1 - ∏ i ∈ s, m i) := by - refine tsub_le_iff_right.2 ?_ - calc (1 : ℝ≥0∞) = (1 - m j) + m j * ((1 - ∏ i ∈ s, m i) + ∏ i ∈ s, m i) := by - rw [tsub_add_cancel_of_le hprod, mul_one, tsub_add_cancel_of_le hmj] - _ = (1 - m j) + (m j * (1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i) := by rw [mul_add] - _ ≤ (1 - m j) + ((1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i) := by - gcongr; exact mul_le_of_le_one_left' hmj - _ = (1 - m j) + (1 - ∏ i ∈ s, m i) + m j * ∏ i ∈ s, m i := (add_assoc _ _ _).symm - _ ≤ (1 - m j) + ∑ i ∈ s, (1 - m i) := by gcongr; exact ih hms - /-- **Total variation distance between product measures.** The total variation distance between two finite products of probability measures is at most the sum of the distances between the factors. -/ @@ -120,10 +74,10 @@ theorem etvDist_pi_le_sum (μ ν : ∀ i, Measure (X i)) [∀ i, IsProbabilityMe _ ≤ etvDist (Measure.pi μ) (Measure.pi ρ) + etvDist (Measure.pi ρ) (Measure.pi ν) := etvDist_triangle _ _ _ _ = 2 * (1 - ∏ i, ρ i univ) := by - rw [etvDist_of_ge (pi_mono hρμ), etvDist_of_le (pi_mono hρν)] + rw [etvDist_of_ge (Measure.pi_mono hρμ), etvDist_of_le (Measure.pi_mono hρν)] simp [Measure.pi_univ, two_mul] _ ≤ 2 * ∑ i, (1 - ρ i univ) := by - gcongr; exact one_sub_prod_le_sum_one_sub _ fun i _ ↦ hm i + gcongr; exact ENNReal.one_sub_prod_le_sum_one_sub _ fun i _ ↦ hm i _ = ∑ i, 2 * (1 - ρ i univ) := Finset.mul_sum _ _ _ _ ≤ ∑ i, etvDist (μ i) (ν i) := by gcongr with i From ff490178360746252384e1cfc5f9314f48628eb0 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:20:46 +0100 Subject: [PATCH 3/5] fix: import the bipolar rate from its new module after rebasing onto main Co-Authored-By: Claude Code --- LMLExplore/EValues/EffectiveSet/TotalVariation.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LMLExplore/EValues/EffectiveSet/TotalVariation.lean b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean index d6087a15..eb97d344 100644 --- a/LMLExplore/EValues/EffectiveSet/TotalVariation.lean +++ b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean @@ -5,7 +5,7 @@ Authors: LMLExplore contributors -/ module -public import LMLExplore.EValues.BipolarRate +public import LMLExplore.EValues.BipolarRate.Basic public import LMLExplore.EValues.EffectiveSet public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs public import Mathlib.Probability.ProductMeasure From 6ff512288d1e4d34eb77c4f21ee83805032a763c Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:57:16 +0100 Subject: [PATCH 4/5] refactor: move the effective-null base module to EffectiveSet/Basic and factor the eventwise total-variation bound Move LMLExplore/EValues/EffectiveSet.lean to LMLExplore/EValues/EffectiveSet/Basic.lean. Add MeasureTheory.measure_le_add_of_etvDist_le and use it at the four sites that re-derived it. In the mean-zero completion, factor the integral of the two-atom measure and drop the non-terminal simp. Co-Authored-By: Claude Code --- .../Basic.lean} | 0 .../EValues/EffectiveSet/TotalVariation.lean | 14 +++-------- LMLExplore/EValues/MeanZeroNull.lean | 24 +++++++++++++------ LMLExplore/EValues/Numeraire.lean | 2 +- .../Measure/TotalVariation/Basic.lean | 20 +++++++++------- 5 files changed, 32 insertions(+), 28 deletions(-) rename LMLExplore/EValues/{EffectiveSet.lean => EffectiveSet/Basic.lean} (100%) diff --git a/LMLExplore/EValues/EffectiveSet.lean b/LMLExplore/EValues/EffectiveSet/Basic.lean similarity index 100% rename from LMLExplore/EValues/EffectiveSet.lean rename to LMLExplore/EValues/EffectiveSet/Basic.lean diff --git a/LMLExplore/EValues/EffectiveSet/TotalVariation.lean b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean index eb97d344..1a6b49d8 100644 --- a/LMLExplore/EValues/EffectiveSet/TotalVariation.lean +++ b/LMLExplore/EValues/EffectiveSet/TotalVariation.lean @@ -6,7 +6,7 @@ Authors: LMLExplore contributors module public import LMLExplore.EValues.BipolarRate.Basic -public import LMLExplore.EValues.EffectiveSet +public import LMLExplore.EValues.EffectiveSet.Basic public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs public import Mathlib.Probability.ProductMeasure @@ -110,9 +110,7 @@ theorem mem_effectiveSet_of_forall_exists_etvDist_lt (.of_forall fun ν ↦ ν.2) fun s hs ↦ ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ ?_ have hev : ∀ᶠ ν : effectiveSet S in Filter.comap f (𝓝 0), μ s - ε ≤ (ν : Measure Ω) s := by filter_upwards [tendsto_comap.eventually (gt_mem_nhds (ENNReal.coe_pos.2 hε))] with ν hν - refine tsub_le_iff_right.2 ((measure_le_add_etvDist μ ν hs).trans ?_) - rw [etvDist_comm] - exact add_le_add le_rfl hν.le + exact tsub_le_iff_right.2 (measure_le_add_of_etvDist_le hs hν.le) exact tsub_le_iff_right.1 (le_liminf_of_le (by isBoundedDefault) hev) /-- A limit in total variation of members of a null `S` of measures of mass at most `1` belongs @@ -260,13 +258,7 @@ theorem measure_pi_le_of_forall_exists_etvDist_lt (hS : ∀ P ∈ S, IsProbabili have := isProbabilityMeasure_of_forall_exists_etvDist_lt hS hQ refine ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ ?_ obtain ⟨P, hP, hPQ⟩ := exists_etvDist_pi_lt (ι := ι) hS hQ (ENNReal.coe_pos.2 hε) - calc Measure.pi (fun _ : ι ↦ Q) R - _ ≤ Measure.pi (fun _ : ι ↦ P) R + - etvDist (Measure.pi fun _ : ι ↦ Q) (Measure.pi fun _ : ι ↦ P) := - measure_le_add_etvDist _ _ hR - _ ≤ α + ε := by - rw [etvDist_comm] - exact add_le_add (hα P hP) hPQ.le + exact (measure_le_add_of_etvDist_le hR hPQ.le).trans (add_le_add (hα P hP) le_rfl) /-- **No growth against a limit in total variation.** If a probability measure `Q` is a limit in total variation of members of a null `S` of probability measures, the maximal expected logarithm diff --git a/LMLExplore/EValues/MeanZeroNull.lean b/LMLExplore/EValues/MeanZeroNull.lean index e4d592ed..8b28561c 100644 --- a/LMLExplore/EValues/MeanZeroNull.lean +++ b/LMLExplore/EValues/MeanZeroNull.lean @@ -102,6 +102,18 @@ private lemma not_ae_eq_zero_add_smul_dirac (ν : Measure ℝ) {c : ℝ≥0∞} have h₃ : z + 1 = 0 := h₁.2 linarith +/-- The identity is integrable under two atoms at `z - 1` and `z + 1`. -/ +private lemma integrable_id_dirac_add_dirac (z : ℝ) : + Integrable (fun x : ℝ ↦ x) (Measure.dirac (z - 1) + Measure.dirac (z + 1)) := + (integrable_dirac (by simp)).add_measure (integrable_dirac (by simp)) + +/-- The mean of two atoms at `z - 1` and `z + 1` is `2 * z`. -/ +private lemma integral_id_dirac_add_dirac (z : ℝ) : + ∫ x, x ∂(Measure.dirac (z - 1) + Measure.dirac (z + 1)) = 2 * z := by + rw [integral_add_measure (integrable_dirac (by simp)) (integrable_dirac (by simp)), + integral_dirac, integral_dirac] + ring + /-- **Completion to a law with mean zero.** A finite measure on `ℝ` of mass less than `1` carried by a bounded interval is below a member of `meanZeroPosVarNull`: add two atoms of mass `(1 - ν univ) / 2` at `z - 1` and `z + 1`, for the `z` that makes the mean `0`. -/ @@ -127,15 +139,13 @@ private lemma exists_mem_meanZeroPosVarNull_le (ν : Measure ℝ) [IsFiniteMeasu Integrable.of_bound measurable_id.aestronglyMeasurable K (by simpa using hK) have hPprob : IsProbabilityMeasure P := by rw [isProbabilityMeasure_iff_real, hP, measureReal_add_apply, measureReal_ennreal_smul_apply, - hD, measureReal_add_apply, hct, ← hb_def] - simp + hD, measureReal_add_apply, hct, ← hb_def, probReal_univ, probReal_univ] ring have hmean : ∫ x, x ∂P = 0 := by - have hDint : Integrable (fun x : ℝ ↦ x) D := - (integrable_dirac (by simp)).add_measure (integrable_dirac (by simp)) - rw [hP, integral_add_measure (hint hM) (hDint.smul_measure ENNReal.ofReal_ne_top), - integral_smul_measure, hD, integral_add_measure (integrable_dirac (by simp)) - (integrable_dirac (by simp)), integral_dirac, integral_dirac, hct, hz, smul_eq_mul] + have hDint : Integrable (fun x : ℝ ↦ x) (c • D) := + (integrable_id_dirac_add_dirac z).smul_measure ENNReal.ofReal_ne_top + rw [hP, integral_add_measure (hint hM) hDint, + integral_smul_measure, hD, integral_id_dirac_add_dirac, hct, hz, smul_eq_mul] field_simp ring have hmem : MemLp id 2 P := MemLp.of_bound measurable_id.aestronglyMeasurable (max M (|z| + 1)) diff --git a/LMLExplore/EValues/Numeraire.lean b/LMLExplore/EValues/Numeraire.lean index 3d4ee92b..a3982e7b 100644 --- a/LMLExplore/EValues/Numeraire.lean +++ b/LMLExplore/EValues/Numeraire.lean @@ -6,7 +6,7 @@ Authors: LMLExplore contributors module public import Statlib.EValues.RIPr -public import LMLExplore.EValues.EffectiveSet +public import LMLExplore.EValues.EffectiveSet.Basic public import LMLExplore.EValues.EVariable public import LMLExplore.MeasureTheory.Measure.AbsolutelyContinuousSet public import LMLExplore.MeasureTheory.Measure.WithDensity diff --git a/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean b/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean index 3d94b281..6a197ce9 100644 --- a/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean +++ b/LMLExplore/MeasureTheory/Measure/TotalVariation/Basic.lean @@ -49,7 +49,8 @@ contraction of the oscillation of functions by a Markov kernel (Dobrushin's coef `|∫ f dμ - ∫ f dν| ≤ (b - a) / 2 * tvDist μ ν`, and `MeasureTheory.abs_integral_sub_integral_le_mul_tvDist_of_forall_sub_le` its form for `f` whose values differ by at most `c`. -* `MeasureTheory.measure_le_add_etvDist`: `μ s ≤ ν s + etvDist μ ν` for every measurable `s`. +* `MeasureTheory.measure_le_add_etvDist`: `μ s ≤ ν s + etvDist μ ν` for every measurable `s`, and + `MeasureTheory.measure_le_add_of_etvDist_le` its form `μ s ≤ ν s + ε` when `etvDist ν μ ≤ ε`. * `MeasureTheory.isProbabilityMeasure_of_forall_exists_etvDist_lt`: a limit in total variation of probability measures is a probability measure. * `MeasureTheory.exists_le_le_add_etvDist`: two finite measures have a common minorant `ρ` with @@ -81,7 +82,7 @@ on the masses. public section open Set -open scoped NNReal +open scoped ENNReal NNReal namespace MeasureTheory @@ -180,6 +181,12 @@ theorem measure_le_add_etvDist (μ ν : Measure 𝓧) {s : Set 𝓧} (hs : Measu exact le_add_right (le_iSup₂ (f := fun A (_ : MeasurableSet A) ↦ μ A - ν A) s hs) · simp [etvDist_of_not_isFiniteMeasure h] +/-- **Events of measures within `ε` in total variation**: if `etvDist ν μ ≤ ε`, every measurable +event `s` satisfies `μ s ≤ ν s + ε`. -/ +theorem measure_le_add_of_etvDist_le {μ ν : Measure 𝓧} {s : Set 𝓧} {ε : ℝ≥0∞} + (hs : MeasurableSet s) (h : etvDist ν μ ≤ ε) : μ s ≤ ν s + ε := + (measure_le_add_etvDist μ ν hs).trans (add_le_add le_rfl ((etvDist_comm μ ν).trans_le h)) + /-- A limit in total variation of probability measures is a probability measure. -/ theorem isProbabilityMeasure_of_forall_exists_etvDist_lt {S : Set (Measure 𝓧)} {Q : Measure 𝓧} (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hQ : ∀ ε > 0, ∃ P ∈ S, etvDist P Q < ε) : @@ -188,13 +195,8 @@ theorem isProbabilityMeasure_of_forall_exists_etvDist_lt {S : Set (Measure 𝓧) obtain ⟨P, hP, hPQ⟩ := hQ ε (ENNReal.coe_pos.2 hε) have := hS P hP constructor - · calc Q univ ≤ P univ + etvDist Q P := measure_le_add_etvDist Q P .univ - _ ≤ 1 + ε := by - rw [measure_univ, etvDist_comm] - exact add_le_add le_rfl hPQ.le - · calc 1 = P univ := measure_univ.symm - _ ≤ Q univ + etvDist P Q := measure_le_add_etvDist P Q .univ - _ ≤ Q univ + ε := add_le_add le_rfl hPQ.le + · simpa using measure_le_add_of_etvDist_le .univ hPQ.le + · simpa using measure_le_add_of_etvDist_le (μ := P) .univ ((etvDist_comm Q P).trans_le hPQ.le) exact ⟨le_antisymm (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).1) (ENNReal.le_of_forall_pos_le_add fun ε hε _ ↦ (h ε hε).2)⟩ From a98e860b44579401af3f127c442c1936e499c5c3 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 16:27:28 +0100 Subject: [PATCH 5/5] refactor: drop an unused import and split the rewrite chains of the completion lemma into calcs Co-Authored-By: Claude Code --- LMLExplore/EValues/MeanZeroNull.lean | 22 +++++++++++++------ .../Measure/TotalVariation/Pi.lean | 1 - 2 files changed, 15 insertions(+), 8 deletions(-) diff --git a/LMLExplore/EValues/MeanZeroNull.lean b/LMLExplore/EValues/MeanZeroNull.lean index 8b28561c..bb830708 100644 --- a/LMLExplore/EValues/MeanZeroNull.lean +++ b/LMLExplore/EValues/MeanZeroNull.lean @@ -138,16 +138,24 @@ private lemma exists_mem_meanZeroPosVarNull_le (ν : Measure ℝ) [IsFiniteMeasu Integrable (fun x : ℝ ↦ x) μ := Integrable.of_bound measurable_id.aestronglyMeasurable K (by simpa using hK) have hPprob : IsProbabilityMeasure P := by - rw [isProbabilityMeasure_iff_real, hP, measureReal_add_apply, measureReal_ennreal_smul_apply, - hD, measureReal_add_apply, hct, ← hb_def, probReal_univ, probReal_univ] - ring + have hDuniv : D.real univ = 2 := by + rw [measureReal_add_apply] + norm_num + rw [isProbabilityMeasure_iff_real] + calc P.real univ = b + c.toReal * D.real univ := by + rw [measureReal_add_apply] + simp [b] + _ = 1 := by rw [hct, hDuniv]; ring have hmean : ∫ x, x ∂P = 0 := by have hDint : Integrable (fun x : ℝ ↦ x) (c • D) := (integrable_id_dirac_add_dirac z).smul_measure ENNReal.ofReal_ne_top - rw [hP, integral_add_measure (hint hM) hDint, - integral_smul_measure, hD, integral_id_dirac_add_dirac, hct, hz, smul_eq_mul] - field_simp - ring + calc ∫ x, x ∂P = ∫ x, x ∂ν + c.toReal * ∫ x, x ∂D := by + rw [integral_add_measure (hint hM) hDint, integral_smul_measure, smul_eq_mul] + _ = ∫ x, x ∂ν + (1 - b) / 2 * (2 * z) := by rw [hct, integral_id_dirac_add_dirac] + _ = 0 := by + rw [hz] + field_simp + ring have hmem : MemLp id 2 P := MemLp.of_bound measurable_id.aestronglyMeasurable (max M (|z| + 1)) (hPb.mono fun x hx ↦ by simpa [Real.norm_eq_abs] using hx) have hvar : 0 < variance id P := by diff --git a/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean b/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean index 3d6f4da5..fec0bf60 100644 --- a/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean +++ b/LMLExplore/MeasureTheory/Measure/TotalVariation/Pi.lean @@ -8,7 +8,6 @@ module public import Mathlib.MeasureTheory.Constructions.Pi public import Mathlib.MeasureTheory.Measure.TotalVariation.Defs -import Mathlib.MeasureTheory.Measure.TotalVariation.Basic import LMLExplore.Basic.ENNReal.BigOperators import LMLExplore.MeasureTheory.Constructions.Pi import LMLExplore.MeasureTheory.Measure.TotalVariation.Basic