From 316fbdc945a56583311ededa84c96a91fbd2cb2a Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 20:33:22 +0100 Subject: [PATCH 1/5] feat: p-to-e calibrators, their admissibility, rescaling, mixtures and the power calibrators Co-Authored-By: Claude Code --- LMLExplore/EValues/Calibrator.lean | 521 ++++++++++++++++++ LMLExplore/Topology/Order/LeftRightLim.lean | 47 ++ .../Topology/Semicontinuity/ENNReal.lean | 14 +- 3 files changed, 579 insertions(+), 3 deletions(-) create mode 100644 LMLExplore/EValues/Calibrator.lean create mode 100644 LMLExplore/Topology/Order/LeftRightLim.lean diff --git a/LMLExplore/EValues/Calibrator.lean b/LMLExplore/EValues/Calibrator.lean new file mode 100644 index 00000000..409473dd --- /dev/null +++ b/LMLExplore/EValues/Calibrator.lean @@ -0,0 +1,521 @@ +/- +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.PVariable +public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal +public import Mathlib.Analysis.SpecialFunctions.Log.Basic +public import Mathlib.Topology.Semicontinuity.Defs +import Mathlib.Analysis.SpecialFunctions.Pow.Continuity +import Mathlib.Analysis.SpecialFunctions.Pow.Deriv +import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus +import LMLExplore.Topology.Order.LeftRightLim +import LMLExplore.Topology.Semicontinuity.ENNReal +import Mathlib.Topology.Order.Monotone +import TauCeti.Analysis.SpecialFunctions.Pow.Integral + +/-! +# P-to-e calibrators + +A p-to-e calibrator is a way of turning p-variables into e-variables: an antitone +`f : ℝ≥0∞ → ℝ≥0∞`, zero on `(1, ∞]`, such that `f ∘ p` is an e-variable for every p-variable `p` +of every null hypothesis on every measurable space. By [RW, Proposition 2.5], these are exactly the +antitone functions vanishing on `(1, ∞]` with `∫₀¹ f ≤ 1`, and this characterization is taken here +as the definition. The definition is justified by `IsPToECalibrator.isEVar_comp` and its converse +`isPToECalibrator_iff_isEVar`, whose proof rests on the fact that a p-variable is stochastically +larger than the uniform law on `[0, 1]` (`IsPVar.lintegral_comp_le`). + +A calibrator is admissible when no other calibrator dominates it. The admissible calibrators are +the upper semicontinuous calibrators with `f 0 = ∞` and `∫₀¹ f = 1` [RW, Proposition 2.5]. + +## Main definitions + +* `ProbabilityTheory.IsPToECalibrator f`: `f` is a p-to-e calibrator. +* `ProbabilityTheory.IsAdmissiblePToECalibrator f`: `f` is a calibrator that no other calibrator + strictly dominates. +* `ProbabilityTheory.powCalibrator κ`: the calibrator `x ↦ κ x ^ (κ - 1)` on `[0, 1]`. +* `ProbabilityTheory.powMixCalibrator`: the mixture of the calibrators `powCalibrator κ` over + `κ` uniform on `(0, 1)`. + +## Main statements + +* `ProbabilityTheory.IsPVar.lintegral_comp_le`: under a measure of mass at most `1`, the integral + of an antitone function of a p-variable is at most its integral against the uniform law. +* `ProbabilityTheory.IsPToECalibrator.isEVar_comp`: a calibrator turns every p-variable into an + e-variable [VW21, Proposition 2.1], and `ProbabilityTheory.isPToECalibrator_iff_isEVar`: an + antitone function vanishing on `(1, ∞]` is a calibrator as soon as it turns the identity of + `[0, 1]`, under Lebesgue measure, into an e-variable. +* `ProbabilityTheory.IsPToECalibrator.le_inv`: a calibrator is at most `x ↦ x⁻¹`. +* `ProbabilityTheory.isAdmissiblePToECalibrator_iff`: the characterization of admissible + calibrators [RW, Proposition 2.5]. +* `ProbabilityTheory.IsPToECalibrator.const_mul_comp_mul` and its admissible version: the + rescaling `x ↦ a f (a x)`, `a ≥ 1`, of a calibrator is a calibrator [RW, Proposition 2.6]. +* `ProbabilityTheory.isPToECalibrator_lintegral`: mixtures of calibrators are calibrators. +* `ProbabilityTheory.isAdmissiblePToECalibrator_powCalibrator` and + `ProbabilityTheory.powMixCalibrator_ofReal`: the power calibrators are admissible, and their + mixture is `(1 - x + x log x) / (x (log x) ^ 2)` on `(0, 1)` [RW, (2.1)–(2.2)]. + +## References + +* A. Ramdas and R. Wang, *Hypothesis Testing with E-values*, Foundations and Trends in + Statistics 1 (2025), arXiv:2410.23614v6 [RW]: Definition 2.3, Propositions 2.5 and 2.6, (2.1) + and (2.2). +* V. Vovk and R. Wang, *E-values: calibration, combination and applications*, Ann. Statist. 49 + (2021), arXiv:1912.06116v4 [VW21]: Proposition 2.1. +-/ + +public section + +open MeasureTheory Set Filter Topology +open scoped ENNReal NNReal + +namespace ProbabilityTheory + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S : Set (Measure Ω)} {p : Ω → ℝ≥0∞} + {P : Measure Ω} {f g : ℝ≥0∞ → ℝ≥0∞} + +/-! ### P-variables are stochastically larger than the uniform law -/ + +/-- The uniform law on `[0, 1]` gives mass `min a 1` to `{x | x < a}`. -/ +private lemma volume_restrict_Icc_ofReal_lt (a : ℝ≥0∞) : + volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x < a} = min a 1 := by + rw [Measure.restrict_apply (measurableSet_lt ENNReal.measurable_ofReal measurable_const)] + rcases le_or_gt a 1 with ha | ha + · have ha' : a ≠ ∞ := ne_top_of_le_ne_top ENNReal.one_ne_top ha + have h_set : {x : ℝ | ENNReal.ofReal x < a} ∩ Icc 0 1 = Ico 0 a.toReal := by + ext x + simp only [mem_inter_iff, mem_ofPred_eq, mem_Icc, mem_Ico] + constructor + · rintro ⟨h, h0, -⟩ + exact ⟨h0, (ENNReal.ofReal_lt_iff_lt_toReal h0 ha').1 h⟩ + · rintro ⟨h0, h⟩ + refine ⟨(ENNReal.ofReal_lt_iff_lt_toReal h0 ha').2 h, h0, h.le.trans ?_⟩ + exact ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using ha) + rw [h_set, Real.volume_Ico, sub_zero, ENNReal.ofReal_toReal ha', min_eq_left ha] + · have h_set : {x : ℝ | ENNReal.ofReal x < a} ∩ Icc 0 1 = Icc 0 1 := + inter_eq_right.2 fun x hx ↦ (ENNReal.ofReal_le_one.2 hx.2).trans_lt ha + simp [h_set, min_eq_right ha.le] + +/-- Under a measure of total mass at most `1`, a p-variable charges every lower set of `ℝ≥0∞` at +most as much as a uniform variable on `[0, 1]` does. -/ +theorem IsPVar.measure_preimage_le (hp : IsPVar p S) (hP : P ∈ S) (hP1 : P univ ≤ 1) + {L : Set ℝ≥0∞} (hL : IsLowerSet L) : + P (p ⁻¹' L) ≤ volume.restrict (Icc (0 : ℝ) 1) (ENNReal.ofReal ⁻¹' L) := by + have h_sub : Iio (sSup L) ⊆ L := fun x hx ↦ by + obtain ⟨y, hyL, hxy⟩ := lt_sSup_iff.1 (mem_Iio.1 hx) + exact hL hxy.le hyL + calc P (p ⁻¹' L) ≤ min (sSup L) 1 := by + refine le_min ?_ ((measure_mono (subset_univ _)).trans hP1) + have h_sub' : p ⁻¹' L ⊆ {ω | p ω ≤ sSup L} := fun ω (hω : p ω ∈ L) ↦ le_sSup hω + exact (measure_mono h_sub').trans (hp.measure_le_le P hP _) + _ = volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x < sSup L} := + (volume_restrict_Icc_ofReal_lt _).symm + _ ≤ _ := measure_mono fun _ hx ↦ h_sub hx + +/-- **A p-variable is stochastically larger than the uniform law**: under a measure of total mass +at most `1`, the integral of an antitone function of a p-variable is at most its integral against +the uniform law on `[0, 1]`. -/ +theorem IsPVar.lintegral_comp_le (hp : IsPVar p S) (hP : P ∈ S) (hP1 : P univ ≤ 1) + (hf : Antitone f) : + ∫⁻ ω, f (p ω) ∂P ≤ ∫⁻ x in Icc (0 : ℝ) 1, f (ENNReal.ofReal x) := by + -- the layer cake formula on both sides reduces the claim to the superlevel sets of `f`, which + -- are lower sets since `f` is antitone + have h_cake_P := TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul P + (hf.measurable.comp hp.measurable).aemeasurable one_pos + have h_cake_U := TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul + (volume.restrict (Icc (0 : ℝ) 1)) + (hf.measurable.comp ENNReal.measurable_ofReal).aemeasurable one_pos + simp only [ENNReal.rpow_one, ENNReal.ofReal_one, one_mul, sub_self, Real.rpow_zero, + mul_one, Function.comp_apply] at h_cake_P h_cake_U + rw [h_cake_P, h_cake_U] + exact lintegral_mono fun t ↦ hp.measure_preimage_le hP hP1 + (L := {y | ENNReal.ofReal t < f y}) fun _ _ hxy hy ↦ hy.trans_le (hf hxy) + +/-! ### Calibrators -/ + +/-- A **p-to-e calibrator** is an antitone `f : ℝ≥0∞ → ℝ≥0∞`, zero on `(1, ∞]`, with +`∫₀¹ f ≤ 1`. This is the characterization of [RW, Proposition 2.5], taken as the definition: +these are exactly the antitone functions, zero on `(1, ∞]`, that turn every p-variable into an +e-variable (`IsPToECalibrator.isEVar_comp`, `isPToECalibrator_iff_isEVar`). -/ +structure IsPToECalibrator (f : ℝ≥0∞ → ℝ≥0∞) : Prop where + antitone : Antitone f + eq_zero_of_one_lt : ∀ x, 1 < x → f x = 0 + lintegral_le_one : ∫⁻ x in Icc (0 : ℝ) 1, f (ENNReal.ofReal x) ≤ 1 + +theorem IsPToECalibrator.measurable (hf : IsPToECalibrator f) : Measurable f := + hf.antitone.measurable + +/-- **A calibrator turns p-variables into e-variables** [VW21, Proposition 2.1]: for a null of +probability measures, `f ∘ p` is an e-variable for every calibrator `f` and every +p-variable `p`. -/ +theorem IsPToECalibrator.isEVar_comp (hf : IsPToECalibrator f) + (hS : ∀ P ∈ S, IsProbabilityMeasure P) (hp : IsPVar p S) : IsEVar (f ∘ p) S := + IsEVar.of_lintegral_le_one hS (hf.measurable.comp hp.measurable) fun P hP ↦ + have := hS P hP + (hp.lintegral_comp_le hP prob_le_one hf.antitone).trans hf.lintegral_le_one + +/-- **The converse**: an antitone function vanishing on `(1, ∞]` is a calibrator exactly when it +turns the identity of `[0, 1]`, an exact p-variable under the Lebesgue measure on `[0, 1]`, into +an e-variable. -/ +theorem isPToECalibrator_iff_isEVar : + IsPToECalibrator f ↔ Antitone f ∧ (∀ x, 1 < x → f x = 0) ∧ + IsEVar (fun x : ℝ ↦ f (ENNReal.ofReal x)) {volume.restrict (Icc 0 1)} := by + have : IsProbabilityMeasure (volume.restrict (Icc (0 : ℝ) 1)) := ⟨by simp⟩ + refine ⟨fun hf ↦ ⟨hf.antitone, hf.eq_zero_of_one_lt, ?_⟩, fun ⟨h_anti, h_zero, hE⟩ ↦ + ⟨h_anti, h_zero, hE.lintegral_le_one (mem_singleton _)⟩⟩ + exact hf.isEVar_comp (by simp only [mem_singleton_iff, forall_eq]; infer_instance) + isExactPVar_ofReal_volume.toIsPVar + +/-- A calibrator is at most `x ↦ x⁻¹`: `x f x ≤ ∫₀ˣ f ≤ 1`. -/ +theorem IsPToECalibrator.le_inv (hf : IsPToECalibrator f) (x : ℝ≥0∞) : f x ≤ x⁻¹ := by + rcases lt_or_ge 1 x with hx | hx + · simp [hf.eq_zero_of_one_lt x hx] + have hx' : x ≠ ∞ := ne_top_of_le_ne_top ENNReal.one_ne_top hx + rw [ENNReal.le_inv_iff_mul_le] + calc f x * x = ∫⁻ _ in Icc (0 : ℝ) x.toReal, f x := by + rw [setLIntegral_const, Real.volume_Icc, sub_zero, ENNReal.ofReal_toReal hx'] + _ ≤ ∫⁻ u in Icc (0 : ℝ) x.toReal, f (ENNReal.ofReal u) := + setLIntegral_mono (hf.measurable.comp ENNReal.measurable_ofReal) fun u hu ↦ + hf.antitone (ENNReal.ofReal_le_of_le_toReal hu.2) + _ ≤ ∫⁻ u in Icc (0 : ℝ) 1, f (ENNReal.ofReal u) := + lintegral_mono_set (Icc_subset_Icc_right + (ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using hx))) + _ ≤ 1 := hf.lintegral_le_one + +/-! ### Rescaling and mixtures -/ + +/-- A function of `ℝ≥0∞` vanishing on `(1, ∞]` has the same integral on `[0, b]`, `b ≥ 1`, as +on `[0, 1]`. -/ +private lemma setLIntegral_Icc_ofReal_of_eq_zero (h_zero : ∀ x, 1 < x → f x = 0) {b : ℝ} + (hb : 1 ≤ b) : + ∫⁻ x in Icc (0 : ℝ) b, f (ENNReal.ofReal x) = ∫⁻ x in Icc (0 : ℝ) 1, f (ENNReal.ofReal x) := by + rw [← Icc_union_Ioc_eq_Icc zero_le_one hb, lintegral_union measurableSet_Ioc + ((Iic_disjoint_Ioc le_rfl).mono_left Icc_subset_Iic_self), + setLIntegral_congr_fun measurableSet_Ioc (g := 0) fun x hx ↦ + h_zero _ (ENNReal.one_lt_ofReal.2 hx.1)] + simp + +/-- The change of variables behind the rescaling of calibrators. -/ +private lemma setLIntegral_const_mul_comp_mul (h_meas : Measurable f) + (h_zero : ∀ x, 1 < x → f x = 0) {a : ℝ≥0} (ha : 1 ≤ a) : + ∫⁻ x in Icc (0 : ℝ) 1, (a : ℝ≥0∞) * f (a * ENNReal.ofReal x) = + ∫⁻ x in Icc (0 : ℝ) 1, f (ENNReal.ofReal x) := by + have ha0 : (0 : ℝ) < a := zero_lt_one.trans_le (by exact_mod_cast ha) + have h_cov := TauCeti.setLIntegral_comp_mul_left_mul_rpow (fun t ↦ f (ENNReal.ofReal t)) ha0 + (S := Icc 0 a) (T := Icc 0 1) measurableSet_Icc (fun s ↦ by + simp only [mem_Icc] + constructor + · rintro ⟨h0, h1⟩ + exact ⟨mul_nonneg ha0.le h0, by nlinarith⟩ + · rintro ⟨h0, h1⟩ + exact ⟨nonneg_of_mul_nonneg_right h0 ha0, by nlinarith⟩) Icc_subset_Ici_self 0 + simp only [Real.rpow_zero, ENNReal.ofReal_one, mul_one, zero_add] at h_cov + have h_eq (x : ℝ) : (a : ℝ≥0∞) * ENNReal.ofReal x = ENNReal.ofReal (a * x) := by + rw [ENNReal.ofReal_mul ha0.le, ENNReal.ofReal_coe_nnreal] + simp_rw [h_eq] + have h_inv : (a : ℝ≥0∞) * ENNReal.ofReal ((a : ℝ) ^ (-1 : ℝ)) = 1 := by + rw [Real.rpow_neg_one, ENNReal.ofReal_inv_of_pos ha0, ENNReal.ofReal_coe_nnreal, + ENNReal.mul_inv_cancel (by simpa using ha0.ne') ENNReal.coe_ne_top] + rw [lintegral_const_mul (f := fun x ↦ f (ENNReal.ofReal (a * x))) _ + (h_meas.comp (ENNReal.measurable_ofReal.comp (measurable_const_mul _))), h_cov, + setLIntegral_Icc_ofReal_of_eq_zero h_zero (by exact_mod_cast ha), ← mul_assoc, h_inv, one_mul] + +/-- **Rescaling** [RW, Proposition 2.6]: for `a ≥ 1`, `x ↦ a f (a x)` is a calibrator when `f` +is one. -/ +theorem IsPToECalibrator.const_mul_comp_mul (hf : IsPToECalibrator f) {a : ℝ≥0} (ha : 1 ≤ a) : + IsPToECalibrator fun x ↦ a * f (a * x) where + antitone _ _ hxy := by + dsimp only + gcongr + exact hf.antitone (by gcongr) + eq_zero_of_one_lt x hx := by + rw [hf.eq_zero_of_one_lt _ (hx.trans_le (le_mul_of_one_le_left' (by exact_mod_cast ha))), + mul_zero] + lintegral_le_one := by + rw [setLIntegral_const_mul_comp_mul hf.measurable hf.eq_zero_of_one_lt ha] + exact hf.lintegral_le_one + +/-- **Mixtures of calibrators** are calibrators: for a probability measure `π` on the indices and +a measurable family of functions `f i` that are calibrators for `π`-almost every `i`, +`x ↦ ∫⁻ i, f i x ∂π` is a calibrator. -/ +theorem isPToECalibrator_lintegral {ι : Type*} [MeasurableSpace ι] {π : Measure ι} + [IsProbabilityMeasure π] {f : ι → ℝ≥0∞ → ℝ≥0∞} (hf : ∀ᵐ i ∂π, IsPToECalibrator (f i)) + (h_meas : Measurable (Function.uncurry f)) : + IsPToECalibrator fun x ↦ ∫⁻ i, f i x ∂π where + antitone _ _ hxy := lintegral_mono_ae (hf.mono fun _ hi ↦ hi.antitone hxy) + eq_zero_of_one_lt x hx := by + rw [lintegral_congr_ae (g := 0) (hf.mono fun _ hi ↦ hi.eq_zero_of_one_lt x hx)] + simp + lintegral_le_one := by + rw [lintegral_lintegral_swap (f := fun x i ↦ f i (ENNReal.ofReal x)) + (h_meas.comp (measurable_snd.prodMk + (ENNReal.measurable_ofReal.comp measurable_fst))).aemeasurable] + calc ∫⁻ i, (∫⁻ x in Icc (0 : ℝ) 1, f i (ENNReal.ofReal x)) ∂π ≤ ∫⁻ _, 1 ∂π := + lintegral_mono_ae (hf.mono fun _ hi ↦ hi.lintegral_le_one) + _ = 1 := by simp + +/-! ### Admissible calibrators -/ + +/-- A calibrator is **admissible** when no other calibrator strictly dominates it: every +calibrator `g ≥ f` is `f` [RW, Definition 2.3]. They are characterized in +`isAdmissiblePToECalibrator_iff`. -/ +structure IsAdmissiblePToECalibrator (f : ℝ≥0∞ → ℝ≥0∞) : Prop extends IsPToECalibrator f where + eq_of_le : ∀ g, IsPToECalibrator g → f ≤ g → g = f + +/-- Adding the constant `1 - ∫₀¹ f` on `[0, 1]` to a calibrator gives a calibrator of integral +`1`. -/ +private lemma IsPToECalibrator.add_indicator (hf : IsPToECalibrator f) : + IsPToECalibrator (fun x ↦ f x + + (Iic 1).indicator (fun _ ↦ 1 - ∫⁻ u in Icc (0 : ℝ) 1, f (ENNReal.ofReal u)) x) ∧ + ∫⁻ x in Icc (0 : ℝ) 1, (f (ENNReal.ofReal x) + + (Iic 1).indicator (fun _ ↦ 1 - ∫⁻ u in Icc (0 : ℝ) 1, f (ENNReal.ofReal u)) + (ENNReal.ofReal x)) = 1 := by + set c := 1 - ∫⁻ u in Icc (0 : ℝ) 1, f (ENNReal.ofReal u) + have h_int : ∫⁻ x in Icc (0 : ℝ) 1, (f (ENNReal.ofReal x) + + (Iic 1).indicator (fun _ ↦ c) (ENNReal.ofReal x)) = 1 := by + rw [lintegral_add_left (f := fun x ↦ f (ENNReal.ofReal x)) + (hf.measurable.comp ENNReal.measurable_ofReal), + setLIntegral_congr_fun measurableSet_Icc + (f := fun x ↦ (Iic 1).indicator (fun _ ↦ c) (ENNReal.ofReal x)) (g := fun _ ↦ c) + fun x hx ↦ indicator_of_mem (ENNReal.ofReal_le_one.2 hx.2) _] + simp [c, add_tsub_cancel_of_le hf.lintegral_le_one] + refine ⟨⟨fun x y hxy ↦ add_le_add (hf.antitone hxy) ?_, fun x hx ↦ ?_, h_int.le⟩, h_int⟩ + · by_cases hy : y ≤ 1 + · simp [indicator_of_mem (mem_Iic.2 hy), + indicator_of_mem (mem_Iic.2 (hxy.trans hy))] + · simp [indicator_of_notMem (mt mem_Iic.1 hy)] + · simp [hf.eq_zero_of_one_lt x hx, indicator_of_notMem (mt mem_Iic.1 (not_le.2 hx))] + +/-- Setting a calibrator to `∞` at `0` gives a calibrator. -/ +private lemma IsPToECalibrator.ite_zero (hf : IsPToECalibrator f) : + IsPToECalibrator fun x ↦ if x = 0 then ∞ else f x where + antitone x y hxy := by + by_cases hx : x = 0 + · simp [hx] + · simp [hx, ((pos_iff_ne_zero.2 hx).trans_le hxy).ne', hf.antitone hxy] + eq_zero_of_one_lt x hx := by simp [(zero_le_one.trans_lt hx).ne', hf.eq_zero_of_one_lt x hx] + lintegral_le_one := by + rw [← setLIntegral_congr Ioc_ae_eq_Icc, setLIntegral_congr_fun measurableSet_Ioc + (g := fun x ↦ f (ENNReal.ofReal x)) fun x hx ↦ by simp [hx.1], + setLIntegral_congr Ioc_ae_eq_Icc] + exact hf.lintegral_le_one + +/-- The left limit `Function.leftLim f` of a calibrator, its upper semicontinuous +regularization, is a calibrator. -/ +private lemma IsPToECalibrator.leftLim (hf : IsPToECalibrator f) : + IsPToECalibrator (Function.leftLim f) where + antitone := hf.antitone.leftLim + eq_zero_of_one_lt x hx := by + obtain ⟨y, h1y, hyx⟩ := exists_between hx + exact nonpos_iff_eq_zero.1 + ((hf.antitone.leftLim_le hyx).trans_eq (hf.eq_zero_of_one_lt y h1y)) + lintegral_le_one := by + refine le_of_eq_of_le (lintegral_congr_ae ?_) hf.lintegral_le_one + -- the left limit differs from `f` only at its countably many discontinuities + have h_null : volume (ENNReal.toReal '' {x | ¬ContinuousAt f x}) = 0 := + (hf.antitone.countable_not_continuousAt.image _).measure_zero _ + filter_upwards [ae_restrict_mem measurableSet_Icc, + ae_restrict_of_ae (measure_eq_zero_iff_ae_notMem.1 h_null)] with u hu hu_null + refine ContinuousWithinAt.leftLim_eq (ContinuousAt.continuousWithinAt ?_) + by_contra h + exact hu_null ⟨_, h, ENNReal.toReal_ofReal hu.1⟩ + +/-- An upper semicontinuous function with `f 0 = ∞` and `∫₀¹ f = 1` is dominated by no calibrator +other than itself. -/ +private lemma eq_of_le_of_upperSemicontinuous + (h_usc : UpperSemicontinuous f) (h_top : f 0 = ∞) + (h_int : ∫⁻ x in Icc (0 : ℝ) 1, f (ENNReal.ofReal x) = 1) (hg : IsPToECalibrator g) + (hfg : f ≤ g) : g = f := by + -- `g` and `f` have the same integral, so they agree almost everywhere on `[0, 1]` + have h_ae : ∀ᵐ u ∂volume.restrict (Icc (0 : ℝ) 1), + f (ENNReal.ofReal u) = g (ENNReal.ofReal u) := + ae_eq_of_ae_le_of_lintegral_le (.of_forall fun _ ↦ hfg _) (by simp [h_int]) + (hg.measurable.comp ENNReal.measurable_ofReal).aemeasurable + (hg.lintegral_le_one.trans_eq h_int.symm) + refine funext fun x ↦ le_antisymm ?_ (hfg x) + rcases eq_or_ne x 0 with rfl | hx0 + · simp [h_top] + rcases lt_or_ge 1 x with hx1 | hx1 + · simp [hg.eq_zero_of_one_lt x hx1] + by_contra h_lt + rw [not_le] at h_lt + -- by upper semicontinuity, `f < g x ≤ g` on an interval to the left of `x` + obtain ⟨l, u, ⟨hlx, hxu⟩, h_sub⟩ := (mem_nhds_iff_exists_Ioo_subset' + ⟨0, pos_iff_ne_zero.2 hx0⟩ ⟨2, hx1.trans_lt ENNReal.one_lt_two⟩).1 (h_usc x _ h_lt) + have hx_top : x ≠ ∞ := ne_top_of_le_ne_top ENNReal.one_ne_top hx1 + have hl_top : l ≠ ∞ := (hlx.trans_le le_top).ne + have h_pos : 0 < volume.restrict (Icc (0 : ℝ) 1) (Ioo l.toReal x.toReal) := by + rw [Measure.restrict_apply measurableSet_Ioo, + inter_eq_left.2 fun v (hv : v ∈ Ioo l.toReal x.toReal) ↦ mem_Icc.2 + ⟨ENNReal.toReal_nonneg.trans hv.1.le, hv.2.le.trans + (ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using hx1))⟩, Real.volume_Ioo] + exact ENNReal.ofReal_pos.2 (sub_pos.2 ((ENNReal.toReal_lt_toReal hl_top hx_top).2 hlx)) + refine h_pos.ne' (measure_mono_null (fun v hv ↦ ?_) (ae_iff.1 h_ae)) + have hv0 : 0 ≤ v := ENNReal.toReal_nonneg.trans hv.1.le + have hv_mem : ENNReal.ofReal v ∈ Ioo l u := + ⟨(ENNReal.lt_ofReal_iff_toReal_lt hl_top).2 hv.1, + ((ENNReal.ofReal_lt_iff_lt_toReal hv0 hx_top).2 hv.2).trans hxu⟩ + exact (h_sub hv_mem).trans_le (hg.antitone ((ENNReal.ofReal_lt_iff_lt_toReal hv0 hx_top).2 + hv.2).le) |>.ne + +/-- **Admissible calibrators** [RW, Proposition 2.5]: a calibrator is admissible exactly when it +is upper semicontinuous, `f 0 = ∞` and `∫₀¹ f = 1`. -/ +theorem isAdmissiblePToECalibrator_iff : + IsAdmissiblePToECalibrator f ↔ IsPToECalibrator f ∧ UpperSemicontinuous f ∧ f 0 = ∞ ∧ + ∫⁻ x in Icc (0 : ℝ) 1, f (ENNReal.ofReal x) = 1 := by + refine ⟨fun hf ↦ ⟨hf.toIsPToECalibrator, ?_, ?_, ?_⟩, fun ⟨hf, h_usc, h_top, h_int⟩ ↦ + ⟨hf, fun g hg hfg ↦ eq_of_le_of_upperSemicontinuous h_usc h_top h_int hg hfg⟩⟩ + · rw [← hf.eq_of_le _ hf.leftLim fun x ↦ hf.antitone.le_leftLim le_rfl] + exact hf.antitone.upperSemicontinuous_leftLim + · rw [← hf.eq_of_le _ hf.ite_zero fun x ↦ by by_cases hx : x = 0 <;> simp [hx]] + simp + · have h := hf.toIsPToECalibrator.add_indicator + have h_eq := hf.eq_of_le _ h.1 fun x ↦ le_self_add + refine Eq.trans ?_ h.2 + exact setLIntegral_congr_fun measurableSet_Icc fun x _ ↦ + (congrFun h_eq (ENNReal.ofReal x)).symm + +/-- **Rescaling** of admissible calibrators [RW, Proposition 2.6]: for `a ≥ 1`, `x ↦ a f (a x)` +is admissible when `f` is. -/ +theorem IsAdmissiblePToECalibrator.const_mul_comp_mul (hf : IsAdmissiblePToECalibrator f) + {a : ℝ≥0} (ha : 1 ≤ a) : IsAdmissiblePToECalibrator fun x ↦ a * f (a * x) := by + obtain ⟨hf, h_usc, h_top, h_int⟩ := isAdmissiblePToECalibrator_iff.1 hf + have ha0 : (a : ℝ≥0∞) ≠ 0 := by + exact_mod_cast (zero_lt_one.trans_le ha).ne' + refine isAdmissiblePToECalibrator_iff.2 ⟨hf.const_mul_comp_mul ha, ?_, by simp [h_top, ha0], ?_⟩ + · exact (h_usc.comp (ENNReal.continuous_const_mul ENNReal.coe_ne_top)).ennreal_const_mul + ENNReal.coe_ne_top + · rw [setLIntegral_const_mul_comp_mul hf.measurable hf.eq_zero_of_one_lt ha, h_int] + +/-! ### Power calibrators -/ + +/-- The **power calibrator** `x ↦ κ x ^ (κ - 1)` on `[0, 1]`, zero on `(1, ∞]` [RW, (2.1)]. For +`κ < 1` its value at `0` is `0 ^ (κ - 1) = ∞`. -/ +noncomputable def powCalibrator (κ : ℝ) (x : ℝ≥0∞) : ℝ≥0∞ := + if x ≤ 1 then ENNReal.ofReal κ * x ^ (κ - 1) else 0 + +theorem powCalibrator_def (κ : ℝ) (x : ℝ≥0∞) : + powCalibrator κ x = if x ≤ 1 then ENNReal.ofReal κ * x ^ (κ - 1) else 0 := + (rfl) + +@[simp] +theorem powCalibrator_of_le_one (κ : ℝ) {x : ℝ≥0∞} (hx : x ≤ 1) : + powCalibrator κ x = ENNReal.ofReal κ * x ^ (κ - 1) := by + simp [powCalibrator_def, hx] + +@[simp] +theorem powCalibrator_of_one_lt (κ : ℝ) {x : ℝ≥0∞} (hx : 1 < x) : powCalibrator κ x = 0 := by + simp [powCalibrator_def, not_le.2 hx] + +theorem measurable_powCalibrator : Measurable (Function.uncurry powCalibrator) := by + simp only [Function.uncurry_def, powCalibrator_def] + refine Measurable.ite (measurableSet_le measurable_snd measurable_const) ?_ measurable_const + exact (ENNReal.measurable_ofReal.comp measurable_fst).mul + (measurable_snd.pow (measurable_fst.sub_const 1)) + +/-- The integral of `powCalibrator κ` on `[0, 1]` is `1` for `κ > 0`. -/ +theorem setLIntegral_powCalibrator {κ : ℝ} (hκ : 0 < κ) : + ∫⁻ x in Icc (0 : ℝ) 1, powCalibrator κ (ENNReal.ofReal x) = 1 := by + rw [← setLIntegral_congr Ioo_ae_eq_Icc, setLIntegral_congr_fun measurableSet_Ioo + (g := fun x ↦ ENNReal.ofReal κ * ENNReal.ofReal (x ^ (κ - 1))) fun x hx ↦ by + rw [powCalibrator_of_le_one _ (ENNReal.ofReal_le_one.2 hx.2.le), + ENNReal.ofReal_rpow_of_pos hx.1], + lintegral_const_mul _ (by fun_prop), + TauCeti.lintegral_ofReal_rpow_Ioo (by linarith) zero_le_one, sub_add_cancel, + Real.one_rpow, ← ENNReal.ofReal_mul hκ.le, mul_one_div_cancel hκ.ne', ENNReal.ofReal_one] + +/-- The power calibrators `x ↦ κ x ^ (κ - 1)`, `0 < κ ≤ 1`, are calibrators. -/ +theorem isPToECalibrator_powCalibrator {κ : ℝ} (hκ0 : 0 < κ) (hκ1 : κ ≤ 1) : + IsPToECalibrator (powCalibrator κ) where + antitone x y hxy := by + rcases le_or_gt y 1 with hy | hy + · rw [powCalibrator_of_le_one _ hy, powCalibrator_of_le_one _ (hxy.trans hy), + ← neg_sub, ENNReal.rpow_neg, ENNReal.rpow_neg] + gcongr + · simp [hy] + eq_zero_of_one_lt _ hx := powCalibrator_of_one_lt _ hx + lintegral_le_one := (setLIntegral_powCalibrator hκ0).le + +/-- The power calibrators `x ↦ κ x ^ (κ - 1)`, `0 < κ < 1`, are admissible [RW, (2.1)]. -/ +theorem isAdmissiblePToECalibrator_powCalibrator {κ : ℝ} (hκ0 : 0 < κ) (hκ1 : κ < 1) : + IsAdmissiblePToECalibrator (powCalibrator κ) := by + refine isAdmissiblePToECalibrator_iff.2 ⟨isPToECalibrator_powCalibrator hκ0 hκ1.le, ?_, ?_, + setLIntegral_powCalibrator hκ0⟩ + · -- below `1`, `powCalibrator κ` is dominated by a continuous function that it equals there + intro x + have h_cont : Continuous fun y : ℝ≥0∞ ↦ ENNReal.ofReal κ * y ^ (κ - 1) := + (ENNReal.continuous_const_mul ENNReal.ofReal_ne_top).comp ENNReal.continuous_rpow_const + rcases le_or_gt x 1 with hx | hx + · intro c hc + rw [powCalibrator_of_le_one _ hx] at hc + filter_upwards [h_cont.continuousAt.eventually (gt_mem_nhds hc)] with y hy + rcases le_or_gt y 1 with hy1 | hy1 + · rwa [powCalibrator_of_le_one _ hy1] + · rw [powCalibrator_of_one_lt _ hy1] + exact zero_le.trans_lt hy + · intro c hc + rw [powCalibrator_of_one_lt _ hx] at hc + filter_upwards [Ioi_mem_nhds hx] with y hy + rwa [powCalibrator_of_one_lt _ hy] + · rw [powCalibrator_of_le_one _ zero_le_one, ENNReal.zero_rpow_of_neg (by linarith), + ENNReal.mul_top (by simpa using hκ0)] + +/-! ### The mixture of the power calibrators -/ + +/-- The mixture `x ↦ ∫₀¹ κ x ^ (κ - 1) dκ` of the power calibrators over `κ` uniform on `(0, 1)` +[RW, (2.2)]; it is `(1 - x + x log x) / (x (log x) ^ 2)` on `(0, 1)` +(`powMixCalibrator_ofReal`). -/ +noncomputable def powMixCalibrator (x : ℝ≥0∞) : ℝ≥0∞ := + ∫⁻ κ in Ioo (0 : ℝ) 1, powCalibrator κ x + +theorem powMixCalibrator_def (x : ℝ≥0∞) : + powMixCalibrator x = ∫⁻ κ in Ioo (0 : ℝ) 1, powCalibrator κ x := + (rfl) + +/-- The mixture of the power calibrators is a calibrator. -/ +theorem isPToECalibrator_powMixCalibrator : IsPToECalibrator powMixCalibrator := by + have : IsProbabilityMeasure (volume.restrict (Ioo (0 : ℝ) 1)) := ⟨by simp⟩ + simp_rw [funext powMixCalibrator_def] + refine isPToECalibrator_lintegral ?_ measurable_powCalibrator + filter_upwards [ae_restrict_mem measurableSet_Ioo] with κ hκ + exact isPToECalibrator_powCalibrator hκ.1 hκ.2.le + +/-- An antiderivative of `κ ↦ κ x ^ (κ - 1)`, for `x > 0` with `log x ≠ 0`. -/ +private lemma hasDerivAt_rpow_sub_one_mul {x : ℝ} (hx : 0 < x) (hlog : Real.log x ≠ 0) (κ : ℝ) : + HasDerivAt (fun κ ↦ x ^ (κ - 1) * (κ * Real.log x - 1) / Real.log x ^ 2) + (κ * x ^ (κ - 1)) κ := by + have h_pow : HasDerivAt (fun κ ↦ x ^ (κ - 1)) (x ^ (κ - 1) * Real.log x) κ := by + exact HasDerivAt.comp_sub_const κ 1 (Real.hasStrictDerivAt_const_rpow hx (κ - 1)).hasDerivAt + refine ((h_pow.mul (((hasDerivAt_id κ).mul_const (Real.log x)).sub_const 1)).div_const + (Real.log x ^ 2)).congr_deriv ?_ + simp only [id] + field_simp + ring + +/-- **The closed form of the mixture of the power calibrators** [RW, (2.2)]: on `(0, 1)`, +`∫₀¹ κ x ^ (κ - 1) dκ = (1 - x + x log x) / (x (log x) ^ 2)`. -/ +theorem powMixCalibrator_ofReal {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : + powMixCalibrator (ENNReal.ofReal x) = + ENNReal.ofReal ((1 - x + x * Real.log x) / (x * Real.log x ^ 2)) := by + have hlog : Real.log x ≠ 0 := (Real.log_neg hx0 hx1).ne + have h_cont : Continuous fun κ : ℝ ↦ κ * x ^ (κ - 1) := + continuous_id.mul ((Real.continuous_const_rpow hx0.ne').comp (continuous_sub_right 1)) + have h_int : ∫ κ in (0 : ℝ)..1, κ * x ^ (κ - 1) = + (1 - x + x * Real.log x) / (x * Real.log x ^ 2) := by + rw [intervalIntegral.integral_eq_sub_of_hasDerivAt + (fun κ _ ↦ hasDerivAt_rpow_sub_one_mul hx0 hlog κ) (h_cont.intervalIntegrable _ _)] + simp only [sub_self, Real.rpow_zero, one_mul, zero_sub, zero_mul, Real.rpow_neg_one] + field_simp + ring + rw [powMixCalibrator_def, ← h_int, intervalIntegral.integral_of_le zero_le_one, + ofReal_integral_eq_lintegral_ofReal (h_cont.integrableOn_Icc.mono_set Ioc_subset_Icc_self) + (ae_restrict_of_forall_mem measurableSet_Ioc fun κ hκ ↦ + mul_nonneg hκ.1.le (Real.rpow_nonneg hx0.le _)), ← setLIntegral_congr Ioo_ae_eq_Ioc] + refine setLIntegral_congr_fun measurableSet_Ioo fun κ hκ ↦ ?_ + rw [powCalibrator_of_le_one _ (ENNReal.ofReal_le_one.2 hx1.le), ENNReal.ofReal_rpow_of_pos hx0, + ← ENNReal.ofReal_mul hκ.1.le] + +end ProbabilityTheory diff --git a/LMLExplore/Topology/Order/LeftRightLim.lean b/LMLExplore/Topology/Order/LeftRightLim.lean new file mode 100644 index 00000000..203d0062 --- /dev/null +++ b/LMLExplore/Topology/Order/LeftRightLim.lean @@ -0,0 +1,47 @@ +/- +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.Topology.Order.LeftRightLim +public import Mathlib.Topology.Semicontinuity.Defs + +/-! +# Semicontinuity of one-sided limits of antitone functions + +The left limit `Function.leftLim f` of an antitone function `f` is upper semicontinuous: it is +the upper semicontinuous regularization of `f`, from which it differs only at the (countably +many) discontinuities of `f`. Replacing a p-to-e calibrator by its left limit is how one shows that +admissible calibrators are upper semicontinuous. + +## Main statements + +* `Antitone.upperSemicontinuous_leftLim`: the left limit of an antitone function is upper + semicontinuous. +-/ + +public section + +open Filter Function Set +open scoped Topology + +variable {α β : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] + [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} + +/-- The left limit `leftLim f` of an antitone function `f` is upper semicontinuous. -/ +theorem Antitone.upperSemicontinuous_leftLim (hf : Antitone f) : + UpperSemicontinuous (leftLim f) := by + intro x c hc + rcases eq_or_neBot (𝓝[<] x) with h | h + · -- no point to the left of `x` is close to `x`, and to its right `leftLim f ≤ f x` + filter_upwards [inf_principal_eq_bot.1 h] with z hz + rcases (not_lt.1 hz).eq_or_lt with rfl | hxz + · exact hc + · exact (hf.leftLim_le hxz).trans_lt (leftLim_eq_of_eq_bot f h ▸ hc) + · -- some `y < x` has `f y < c`, and `leftLim f ≤ f y` to the right of `y` + obtain ⟨y, hyc, hyx⟩ := + ((hf.tendsto_leftLim x).eventually (gt_mem_nhds hc)).and self_mem_nhdsWithin |>.exists + filter_upwards [Ioi_mem_nhds hyx] with z hz + exact (hf.leftLim_le hz).trans_lt hyc diff --git a/LMLExplore/Topology/Semicontinuity/ENNReal.lean b/LMLExplore/Topology/Semicontinuity/ENNReal.lean index d8b0e4d2..689e513e 100644 --- a/LMLExplore/Topology/Semicontinuity/ENNReal.lean +++ b/LMLExplore/Topology/Semicontinuity/ENNReal.lean @@ -9,16 +9,18 @@ public import Mathlib.Topology.Instances.ENNReal.Lemmas public import Mathlib.Topology.Semicontinuity.Basic /-! -# Lower semicontinuity of functions to `ℝ≥0∞` +# Semicontinuity of functions to `ℝ≥0∞` Multiplication by a finite constant `c : ℝ≥0∞` is continuous and monotone, so it preserves lower -semicontinuity of functions to `ℝ≥0∞`. Rescaling a rate function of a large deviation principle -by a positive weight uses this. +and upper semicontinuity of functions to `ℝ≥0∞`. Rescaling a rate function of a large deviation +principle by a positive weight uses the first, and rescaling a p-to-e calibrator the second. ## Main statements * `LowerSemicontinuous.ennreal_const_mul`: if `f` is lower semicontinuous and `c ≠ ∞`, then `y ↦ c * f y` is lower semicontinuous. +* `UpperSemicontinuous.ennreal_const_mul`: if `f` is upper semicontinuous and `c ≠ ∞`, then + `y ↦ c * f y` is upper semicontinuous. -/ public section @@ -32,3 +34,9 @@ semicontinuous. -/ theorem LowerSemicontinuous.ennreal_const_mul (hf : LowerSemicontinuous f) {c : ℝ≥0∞} (hc : c ≠ ∞) : LowerSemicontinuous fun y ↦ c * f y := (ENNReal.continuous_const_mul hc).comp_lowerSemicontinuous hf fun _ _ h ↦ by dsimp only; gcongr + +/-- A finite multiple `y ↦ c * f y` of an upper semicontinuous function `f` to `ℝ≥0∞` is upper +semicontinuous. -/ +theorem UpperSemicontinuous.ennreal_const_mul (hf : UpperSemicontinuous f) {c : ℝ≥0∞} + (hc : c ≠ ∞) : UpperSemicontinuous fun y ↦ c * f y := + (ENNReal.continuous_const_mul hc).comp_upperSemicontinuous hf fun _ _ h ↦ by dsimp only; gcongr From 277f988112b5a910f180100b921972c56c56fe7e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 21:43:26 +0100 Subject: [PATCH 2/5] refactor: move p-variable dominance lemmas to PVariable, extract powCalibrator semicontinuity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Move `IsPVar.measure_preimage_le`, `IsPVar.lintegral_comp_le` and the uniform-law distribution lemma `volume_restrict_Icc_ofReal_lt` (now public) to `PVariable.lean`, and extract its `≤` twin `volume_restrict_Icc_ofReal_le` from `isExactPVar_ofReal_volume`. - Rename `measurable_powCalibrator` to `measurable_uncurry_powCalibrator`. - Extract `upperSemicontinuous_powCalibrator` and a private `toReal_le_one_of_le_one`. - Fix overclaiming docstrings (κ ranges, probability-measure nulls, leftLim module doc). Co-Authored-By: Claude Code --- LMLExplore/EValues/Calibrator.lean | 140 +++++++------------- LMLExplore/EValues/PVariable.lean | 100 +++++++++++--- LMLExplore/Topology/Order/LeftRightLim.lean | 7 +- 3 files changed, 134 insertions(+), 113 deletions(-) diff --git a/LMLExplore/EValues/Calibrator.lean b/LMLExplore/EValues/Calibrator.lean index 409473dd..f52dcf93 100644 --- a/LMLExplore/EValues/Calibrator.lean +++ b/LMLExplore/EValues/Calibrator.lean @@ -22,11 +22,12 @@ import TauCeti.Analysis.SpecialFunctions.Pow.Integral A p-to-e calibrator is a way of turning p-variables into e-variables: an antitone `f : ℝ≥0∞ → ℝ≥0∞`, zero on `(1, ∞]`, such that `f ∘ p` is an e-variable for every p-variable `p` -of every null hypothesis on every measurable space. By [RW, Proposition 2.5], these are exactly the -antitone functions vanishing on `(1, ∞]` with `∫₀¹ f ≤ 1`, and this characterization is taken here -as the definition. The definition is justified by `IsPToECalibrator.isEVar_comp` and its converse -`isPToECalibrator_iff_isEVar`, whose proof rests on the fact that a p-variable is stochastically -larger than the uniform law on `[0, 1]` (`IsPVar.lintegral_comp_le`). +of every null hypothesis of probability measures on every measurable space. By +[RW, Proposition 2.5], these are exactly the antitone functions vanishing on `(1, ∞]` with +`∫₀¹ f ≤ 1`, and this characterization is taken here as the definition. The definition is +justified by `IsPToECalibrator.isEVar_comp` and its converse `isPToECalibrator_iff_isEVar`, whose +proof rests on the fact that a p-variable is stochastically larger than the uniform law on +`[0, 1]` (`IsPVar.lintegral_comp_le`). A calibrator is admissible when no other calibrator dominates it. The admissible calibrators are the upper semicontinuous calibrators with `f 0 = ∞` and `∫₀¹ f = 1` [RW, Proposition 2.5]. @@ -36,14 +37,13 @@ the upper semicontinuous calibrators with `f 0 = ∞` and `∫₀¹ f = 1` [RW, * `ProbabilityTheory.IsPToECalibrator f`: `f` is a p-to-e calibrator. * `ProbabilityTheory.IsAdmissiblePToECalibrator f`: `f` is a calibrator that no other calibrator strictly dominates. -* `ProbabilityTheory.powCalibrator κ`: the calibrator `x ↦ κ x ^ (κ - 1)` on `[0, 1]`. +* `ProbabilityTheory.powCalibrator κ`: the function `x ↦ κ x ^ (κ - 1)` on `[0, 1]`, zero on + `(1, ∞]`; it is a calibrator for `0 < κ ≤ 1`. * `ProbabilityTheory.powMixCalibrator`: the mixture of the calibrators `powCalibrator κ` over `κ` uniform on `(0, 1)`. ## Main statements -* `ProbabilityTheory.IsPVar.lintegral_comp_le`: under a measure of mass at most `1`, the integral - of an antitone function of a p-variable is at most its integral against the uniform law. * `ProbabilityTheory.IsPToECalibrator.isEVar_comp`: a calibrator turns every p-variable into an e-variable [VW21, Proposition 2.1], and `ProbabilityTheory.isPToECalibrator_iff_isEVar`: an antitone function vanishing on `(1, ∞]` is a calibrator as soon as it turns the identity of @@ -55,8 +55,9 @@ the upper semicontinuous calibrators with `f 0 = ∞` and `∫₀¹ f = 1` [RW, rescaling `x ↦ a f (a x)`, `a ≥ 1`, of a calibrator is a calibrator [RW, Proposition 2.6]. * `ProbabilityTheory.isPToECalibrator_lintegral`: mixtures of calibrators are calibrators. * `ProbabilityTheory.isAdmissiblePToECalibrator_powCalibrator` and - `ProbabilityTheory.powMixCalibrator_ofReal`: the power calibrators are admissible, and their - mixture is `(1 - x + x log x) / (x (log x) ^ 2)` on `(0, 1)` [RW, (2.1)–(2.2)]. + `ProbabilityTheory.powMixCalibrator_ofReal`: the power calibrators `powCalibrator κ` are + admissible for `0 < κ < 1`, and their mixture is `(1 - x + x log x) / (x (log x) ^ 2)` on + `(0, 1)` [RW, (2.1)–(2.2)]. ## References @@ -77,63 +78,6 @@ namespace ProbabilityTheory variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S : Set (Measure Ω)} {p : Ω → ℝ≥0∞} {P : Measure Ω} {f g : ℝ≥0∞ → ℝ≥0∞} -/-! ### P-variables are stochastically larger than the uniform law -/ - -/-- The uniform law on `[0, 1]` gives mass `min a 1` to `{x | x < a}`. -/ -private lemma volume_restrict_Icc_ofReal_lt (a : ℝ≥0∞) : - volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x < a} = min a 1 := by - rw [Measure.restrict_apply (measurableSet_lt ENNReal.measurable_ofReal measurable_const)] - rcases le_or_gt a 1 with ha | ha - · have ha' : a ≠ ∞ := ne_top_of_le_ne_top ENNReal.one_ne_top ha - have h_set : {x : ℝ | ENNReal.ofReal x < a} ∩ Icc 0 1 = Ico 0 a.toReal := by - ext x - simp only [mem_inter_iff, mem_ofPred_eq, mem_Icc, mem_Ico] - constructor - · rintro ⟨h, h0, -⟩ - exact ⟨h0, (ENNReal.ofReal_lt_iff_lt_toReal h0 ha').1 h⟩ - · rintro ⟨h0, h⟩ - refine ⟨(ENNReal.ofReal_lt_iff_lt_toReal h0 ha').2 h, h0, h.le.trans ?_⟩ - exact ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using ha) - rw [h_set, Real.volume_Ico, sub_zero, ENNReal.ofReal_toReal ha', min_eq_left ha] - · have h_set : {x : ℝ | ENNReal.ofReal x < a} ∩ Icc 0 1 = Icc 0 1 := - inter_eq_right.2 fun x hx ↦ (ENNReal.ofReal_le_one.2 hx.2).trans_lt ha - simp [h_set, min_eq_right ha.le] - -/-- Under a measure of total mass at most `1`, a p-variable charges every lower set of `ℝ≥0∞` at -most as much as a uniform variable on `[0, 1]` does. -/ -theorem IsPVar.measure_preimage_le (hp : IsPVar p S) (hP : P ∈ S) (hP1 : P univ ≤ 1) - {L : Set ℝ≥0∞} (hL : IsLowerSet L) : - P (p ⁻¹' L) ≤ volume.restrict (Icc (0 : ℝ) 1) (ENNReal.ofReal ⁻¹' L) := by - have h_sub : Iio (sSup L) ⊆ L := fun x hx ↦ by - obtain ⟨y, hyL, hxy⟩ := lt_sSup_iff.1 (mem_Iio.1 hx) - exact hL hxy.le hyL - calc P (p ⁻¹' L) ≤ min (sSup L) 1 := by - refine le_min ?_ ((measure_mono (subset_univ _)).trans hP1) - have h_sub' : p ⁻¹' L ⊆ {ω | p ω ≤ sSup L} := fun ω (hω : p ω ∈ L) ↦ le_sSup hω - exact (measure_mono h_sub').trans (hp.measure_le_le P hP _) - _ = volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x < sSup L} := - (volume_restrict_Icc_ofReal_lt _).symm - _ ≤ _ := measure_mono fun _ hx ↦ h_sub hx - -/-- **A p-variable is stochastically larger than the uniform law**: under a measure of total mass -at most `1`, the integral of an antitone function of a p-variable is at most its integral against -the uniform law on `[0, 1]`. -/ -theorem IsPVar.lintegral_comp_le (hp : IsPVar p S) (hP : P ∈ S) (hP1 : P univ ≤ 1) - (hf : Antitone f) : - ∫⁻ ω, f (p ω) ∂P ≤ ∫⁻ x in Icc (0 : ℝ) 1, f (ENNReal.ofReal x) := by - -- the layer cake formula on both sides reduces the claim to the superlevel sets of `f`, which - -- are lower sets since `f` is antitone - have h_cake_P := TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul P - (hf.measurable.comp hp.measurable).aemeasurable one_pos - have h_cake_U := TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul - (volume.restrict (Icc (0 : ℝ) 1)) - (hf.measurable.comp ENNReal.measurable_ofReal).aemeasurable one_pos - simp only [ENNReal.rpow_one, ENNReal.ofReal_one, one_mul, sub_self, Real.rpow_zero, - mul_one, Function.comp_apply] at h_cake_P h_cake_U - rw [h_cake_P, h_cake_U] - exact lintegral_mono fun t ↦ hp.measure_preimage_le hP hP1 - (L := {y | ENNReal.ofReal t < f y}) fun _ _ hxy hy ↦ hy.trans_le (hf hxy) - /-! ### Calibrators -/ /-- A **p-to-e calibrator** is an antitone `f : ℝ≥0∞ → ℝ≥0∞`, zero on `(1, ∞]`, with @@ -169,6 +113,10 @@ theorem isPToECalibrator_iff_isEVar : exact hf.isEVar_comp (by simp only [mem_singleton_iff, forall_eq]; infer_instance) isExactPVar_ofReal_volume.toIsPVar +/-- An element of `ℝ≥0∞` at most `1` has real part at most `1`. -/ +private lemma toReal_le_one_of_le_one {x : ℝ≥0∞} (hx : x ≤ 1) : x.toReal ≤ 1 := + ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using hx) + /-- A calibrator is at most `x ↦ x⁻¹`: `x f x ≤ ∫₀ˣ f ≤ 1`. -/ theorem IsPToECalibrator.le_inv (hf : IsPToECalibrator f) (x : ℝ≥0∞) : f x ≤ x⁻¹ := by rcases lt_or_ge 1 x with hx | hx @@ -181,8 +129,7 @@ theorem IsPToECalibrator.le_inv (hf : IsPToECalibrator f) (x : ℝ≥0∞) : f x setLIntegral_mono (hf.measurable.comp ENNReal.measurable_ofReal) fun u hu ↦ hf.antitone (ENNReal.ofReal_le_of_le_toReal hu.2) _ ≤ ∫⁻ u in Icc (0 : ℝ) 1, f (ENNReal.ofReal u) := - lintegral_mono_set (Icc_subset_Icc_right - (ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using hx))) + lintegral_mono_set (Icc_subset_Icc_right (toReal_le_one_of_le_one hx)) _ ≤ 1 := hf.lintegral_le_one /-! ### Rescaling and mixtures -/ @@ -351,7 +298,7 @@ private lemma eq_of_le_of_upperSemicontinuous rw [Measure.restrict_apply measurableSet_Ioo, inter_eq_left.2 fun v (hv : v ∈ Ioo l.toReal x.toReal) ↦ mem_Icc.2 ⟨ENNReal.toReal_nonneg.trans hv.1.le, hv.2.le.trans - (ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using hx1))⟩, Real.volume_Ioo] + (toReal_le_one_of_le_one hx1)⟩, Real.volume_Ioo] exact ENNReal.ofReal_pos.2 (sub_pos.2 ((ENNReal.toReal_lt_toReal hl_top hx_top).2 hlx)) refine h_pos.ne' (measure_mono_null (fun v hv ↦ ?_) (ae_iff.1 h_ae)) have hv0 : 0 ≤ v := ENNReal.toReal_nonneg.trans hv.1.le @@ -392,8 +339,10 @@ theorem IsAdmissiblePToECalibrator.const_mul_comp_mul (hf : IsAdmissiblePToECali /-! ### Power calibrators -/ -/-- The **power calibrator** `x ↦ κ x ^ (κ - 1)` on `[0, 1]`, zero on `(1, ∞]` [RW, (2.1)]. For -`κ < 1` its value at `0` is `0 ^ (κ - 1) = ∞`. -/ +/-- The **power calibrator** `x ↦ κ x ^ (κ - 1)` on `[0, 1]`, zero on `(1, ∞]` [RW, (2.1)]. It is +defined for every real `κ` and is a calibrator for `0 < κ ≤ 1` (`isPToECalibrator_powCalibrator`); +for `κ ≤ 0` it is identically `0`, since `ENNReal.ofReal κ = 0`. For `0 < κ < 1` its value at `0` +is `κ 0 ^ (κ - 1) = ∞`. -/ noncomputable def powCalibrator (κ : ℝ) (x : ℝ≥0∞) : ℝ≥0∞ := if x ≤ 1 then ENNReal.ofReal κ * x ^ (κ - 1) else 0 @@ -410,7 +359,7 @@ theorem powCalibrator_of_le_one (κ : ℝ) {x : ℝ≥0∞} (hx : x ≤ 1) : theorem powCalibrator_of_one_lt (κ : ℝ) {x : ℝ≥0∞} (hx : 1 < x) : powCalibrator κ x = 0 := by simp [powCalibrator_def, not_le.2 hx] -theorem measurable_powCalibrator : Measurable (Function.uncurry powCalibrator) := by +theorem measurable_uncurry_powCalibrator : Measurable (Function.uncurry powCalibrator) := by simp only [Function.uncurry_def, powCalibrator_def] refine Measurable.ite (measurableSet_le measurable_snd measurable_const) ?_ measurable_const exact (ENNReal.measurable_ofReal.comp measurable_fst).mul @@ -439,29 +388,32 @@ theorem isPToECalibrator_powCalibrator {κ : ℝ} (hκ0 : 0 < κ) (hκ1 : κ ≤ eq_zero_of_one_lt _ hx := powCalibrator_of_one_lt _ hx lintegral_le_one := (setLIntegral_powCalibrator hκ0).le +/-- The power calibrator `powCalibrator κ` is upper semicontinuous, for every real `κ`. -/ +theorem upperSemicontinuous_powCalibrator (κ : ℝ) : UpperSemicontinuous (powCalibrator κ) := by + -- below `1`, `powCalibrator κ` is dominated by a continuous function that it equals there + intro x + have h_cont : Continuous fun y : ℝ≥0∞ ↦ ENNReal.ofReal κ * y ^ (κ - 1) := + (ENNReal.continuous_const_mul ENNReal.ofReal_ne_top).comp ENNReal.continuous_rpow_const + rcases le_or_gt x 1 with hx | hx + · intro c hc + rw [powCalibrator_of_le_one _ hx] at hc + filter_upwards [h_cont.continuousAt.eventually (gt_mem_nhds hc)] with y hy + rcases le_or_gt y 1 with hy1 | hy1 + · rwa [powCalibrator_of_le_one _ hy1] + · rw [powCalibrator_of_one_lt _ hy1] + exact zero_le.trans_lt hy + · intro c hc + rw [powCalibrator_of_one_lt _ hx] at hc + filter_upwards [Ioi_mem_nhds hx] with y hy + rwa [powCalibrator_of_one_lt _ hy] + /-- The power calibrators `x ↦ κ x ^ (κ - 1)`, `0 < κ < 1`, are admissible [RW, (2.1)]. -/ theorem isAdmissiblePToECalibrator_powCalibrator {κ : ℝ} (hκ0 : 0 < κ) (hκ1 : κ < 1) : IsAdmissiblePToECalibrator (powCalibrator κ) := by - refine isAdmissiblePToECalibrator_iff.2 ⟨isPToECalibrator_powCalibrator hκ0 hκ1.le, ?_, ?_, - setLIntegral_powCalibrator hκ0⟩ - · -- below `1`, `powCalibrator κ` is dominated by a continuous function that it equals there - intro x - have h_cont : Continuous fun y : ℝ≥0∞ ↦ ENNReal.ofReal κ * y ^ (κ - 1) := - (ENNReal.continuous_const_mul ENNReal.ofReal_ne_top).comp ENNReal.continuous_rpow_const - rcases le_or_gt x 1 with hx | hx - · intro c hc - rw [powCalibrator_of_le_one _ hx] at hc - filter_upwards [h_cont.continuousAt.eventually (gt_mem_nhds hc)] with y hy - rcases le_or_gt y 1 with hy1 | hy1 - · rwa [powCalibrator_of_le_one _ hy1] - · rw [powCalibrator_of_one_lt _ hy1] - exact zero_le.trans_lt hy - · intro c hc - rw [powCalibrator_of_one_lt _ hx] at hc - filter_upwards [Ioi_mem_nhds hx] with y hy - rwa [powCalibrator_of_one_lt _ hy] - · rw [powCalibrator_of_le_one _ zero_le_one, ENNReal.zero_rpow_of_neg (by linarith), - ENNReal.mul_top (by simpa using hκ0)] + refine isAdmissiblePToECalibrator_iff.2 ⟨isPToECalibrator_powCalibrator hκ0 hκ1.le, + upperSemicontinuous_powCalibrator κ, ?_, setLIntegral_powCalibrator hκ0⟩ + rw [powCalibrator_of_le_one _ zero_le_one, ENNReal.zero_rpow_of_neg (by linarith), + ENNReal.mul_top (by simpa using hκ0)] /-! ### The mixture of the power calibrators -/ @@ -479,7 +431,7 @@ theorem powMixCalibrator_def (x : ℝ≥0∞) : theorem isPToECalibrator_powMixCalibrator : IsPToECalibrator powMixCalibrator := by have : IsProbabilityMeasure (volume.restrict (Ioo (0 : ℝ) 1)) := ⟨by simp⟩ simp_rw [funext powMixCalibrator_def] - refine isPToECalibrator_lintegral ?_ measurable_powCalibrator + refine isPToECalibrator_lintegral ?_ measurable_uncurry_powCalibrator filter_upwards [ae_restrict_mem measurableSet_Ioo] with κ hκ exact isPToECalibrator_powCalibrator hκ.1 hκ.2.le diff --git a/LMLExplore/EValues/PVariable.lean b/LMLExplore/EValues/PVariable.lean index 2f3b8059..52d06efd 100644 --- a/LMLExplore/EValues/PVariable.lean +++ b/LMLExplore/EValues/PVariable.lean @@ -7,6 +7,7 @@ module public import LMLExplore.EValues.EVariable public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic +import TauCeti.Analysis.SpecialFunctions.Pow.Integral /-! # P-variables @@ -17,7 +18,8 @@ A p-variable for a null hypothesis `S : Set (Measure Ω)` is a measurable `p : arbitrary set of measures and p-variables are `ℝ≥0∞`-valued; values above `1` carry no evidence. This file defines p-variables and exact p-variables, and proves that, for a null of probability measures, the inverse `E⁻¹` of an e-variable is a p-variable (the e-to-p calibration, with -`0⁻¹ = ∞` and no truncation at `1`). +`0⁻¹ = ∞` and no truncation at `1`), and that a p-variable is stochastically larger than the +uniform law on `[0, 1]`. ## Main definitions @@ -32,8 +34,14 @@ measures, the inverse `E⁻¹` of an e-variable is a p-variable (the e-to-p cali * `ProbabilityTheory.isExactPVar_ofReal_volume`: the identity of `[0, 1]` under Lebesgue measure is an exact p-variable, and `ProbabilityTheory.isExactPVar_ofReal_of_map_eq`: so is every random variable uniformly distributed on `[0, 1]` under every member of the null. +* `ProbabilityTheory.volume_restrict_Icc_ofReal_le` and + `ProbabilityTheory.volume_restrict_Icc_ofReal_lt`: the distribution function of the uniform law + on `[0, 1]`. * `ProbabilityTheory.IsExactPVar.ae_le_one`: an exact p-variable is almost surely at most `1` under every probability measure of the null. +* `ProbabilityTheory.IsPVar.lintegral_comp_le`: under a measure of mass at most `1`, the integral + of an antitone function of a p-variable is at most its integral against the uniform law on + `[0, 1]`: a p-variable is stochastically larger than the uniform law. ## References @@ -50,6 +58,7 @@ namespace ProbabilityTheory variable {Ω 𝓨 : Type*} {mΩ : MeasurableSpace Ω} {m𝓨 : MeasurableSpace 𝓨} {S T : Set (Measure Ω)} {p q : Ω → ℝ≥0∞} {E : Ω → ℝ≥0∞} {P : Measure Ω} + {f : ℝ≥0∞ → ℝ≥0∞} /-- A measurable `p : Ω → ℝ≥0∞` is a **p-variable** for the null `S` when `P {ω | p ω ≤ α} ≤ α` for every `P ∈ S` and every level `α`. -/ @@ -145,25 +154,49 @@ theorem IsExactPVar.ae_le_one (hp : IsExactPVar p S) (hP : P ∈ S) [IsProbabili rw [ae_iff_measure_eq (measurableSet_le hp.measurable measurable_const).nullMeasurableSet, hp.measure_le_eq P hP 1 le_rfl, measure_univ] +/-! ### The uniform law on `[0, 1]` -/ + +/-- The distribution function of the uniform law on `[0, 1]`: it gives mass `min α 1` to +`{x | x ≤ α}`. -/ +theorem volume_restrict_Icc_ofReal_le (α : ℝ≥0∞) : + volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x ≤ α} = min α 1 := by + rcases eq_or_ne α ∞ with rfl | hα + · simp + have h_set : {x : ℝ | ENNReal.ofReal x ≤ α} ∩ Icc 0 1 = Icc 0 (min α.toReal 1) := by + ext x + simp only [mem_inter_iff, mem_ofPred_eq, mem_Icc, le_min_iff, + ENNReal.ofReal_le_iff_le_toReal hα] + tauto + rw [Measure.restrict_apply (measurableSet_le ENNReal.measurable_ofReal measurable_const), h_set] + simp [ENNReal.ofReal_min, hα] + +/-- The uniform law on `[0, 1]` gives mass `min a 1` to `{x | x < a}`. -/ +theorem volume_restrict_Icc_ofReal_lt (a : ℝ≥0∞) : + volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x < a} = min a 1 := by + rw [Measure.restrict_apply (measurableSet_lt ENNReal.measurable_ofReal measurable_const)] + rcases le_or_gt a 1 with ha | ha + · have ha' : a ≠ ∞ := ne_top_of_le_ne_top ENNReal.one_ne_top ha + have h_set : {x : ℝ | ENNReal.ofReal x < a} ∩ Icc 0 1 = Ico 0 a.toReal := by + ext x + simp only [mem_inter_iff, mem_ofPred_eq, mem_Icc, mem_Ico] + constructor + · rintro ⟨h, h0, -⟩ + exact ⟨h0, (ENNReal.ofReal_lt_iff_lt_toReal h0 ha').1 h⟩ + · rintro ⟨h0, h⟩ + have h_lt := (ENNReal.ofReal_lt_iff_lt_toReal h0 ha').2 h + exact ⟨h_lt, h0, ENNReal.ofReal_le_one.1 (h_lt.le.trans ha)⟩ + rw [h_set, Real.volume_Ico, sub_zero, ENNReal.ofReal_toReal ha', min_eq_left ha] + · have h_set : {x : ℝ | ENNReal.ofReal x < a} ∩ Icc 0 1 = Icc 0 1 := + inter_eq_right.2 fun x hx ↦ (ENNReal.ofReal_le_one.2 hx.2).trans_lt ha + simp [h_set, min_eq_right ha.le] + /-- The identity of `[0, 1]`, under the Lebesgue measure on `[0, 1]`, is an exact p-variable. -/ theorem isExactPVar_ofReal_volume : IsExactPVar (fun x : ℝ ↦ ENNReal.ofReal x) {volume.restrict (Icc 0 1)} := by - -- the distribution function of the uniform law: `{x ∈ [0, 1] | x ≤ α}` has measure `min α 1` - have h_eq (α : ℝ≥0∞) : - volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x ≤ α} = min α 1 := by - rcases eq_or_ne α ∞ with rfl | hα - · simp - have h_set : {x : ℝ | ENNReal.ofReal x ≤ α} ∩ Icc 0 1 = Icc 0 (min α.toReal 1) := by - ext x - simp only [mem_inter_iff, mem_ofPred_eq, mem_Icc, le_min_iff, - ENNReal.ofReal_le_iff_le_toReal hα] - tauto - rw [Measure.restrict_apply (measurableSet_le ENNReal.measurable_ofReal measurable_const), h_set] - simp [ENNReal.ofReal_min, hα] refine ⟨⟨ENNReal.measurable_ofReal, fun P hP α ↦ ?_⟩, fun P hP α hα ↦ ?_⟩ - · rw [mem_singleton_iff.1 hP, h_eq] + · rw [mem_singleton_iff.1 hP, volume_restrict_Icc_ofReal_le] exact min_le_left α 1 - · rw [mem_singleton_iff.1 hP, h_eq, min_eq_left hα] + · rw [mem_singleton_iff.1 hP, volume_restrict_Icc_ofReal_le, min_eq_left hα] /-- A real random variable `U` uniformly distributed on `[0, 1]` under every member of the null `S` is an exact p-variable for `S`. -/ @@ -175,4 +208,41 @@ theorem isExactPVar_ofReal_of_map_eq {U : Ω → ℝ} (hU : Measurable U) rintro _ ⟨P, hP, rfl⟩ exact hU_law P hP +/-! ### P-variables are stochastically larger than the uniform law -/ + +/-- Under a measure of total mass at most `1`, a p-variable charges every lower set of `ℝ≥0∞` at +most as much as a uniform variable on `[0, 1]` does. -/ +theorem IsPVar.measure_preimage_le (hp : IsPVar p S) (hP : P ∈ S) (hP1 : P univ ≤ 1) + {L : Set ℝ≥0∞} (hL : IsLowerSet L) : + P (p ⁻¹' L) ≤ volume.restrict (Icc (0 : ℝ) 1) (ENNReal.ofReal ⁻¹' L) := by + have h_sub : Iio (sSup L) ⊆ L := fun x hx ↦ by + obtain ⟨y, hyL, hxy⟩ := lt_sSup_iff.1 (mem_Iio.1 hx) + exact hL hxy.le hyL + calc P (p ⁻¹' L) ≤ min (sSup L) 1 := by + refine le_min ?_ ((measure_mono (subset_univ _)).trans hP1) + have h_sub' : p ⁻¹' L ⊆ {ω | p ω ≤ sSup L} := fun ω (hω : p ω ∈ L) ↦ le_sSup hω + exact (measure_mono h_sub').trans (hp.measure_le_le P hP _) + _ = volume.restrict (Icc (0 : ℝ) 1) {x | ENNReal.ofReal x < sSup L} := + (volume_restrict_Icc_ofReal_lt _).symm + _ ≤ _ := measure_mono fun _ hx ↦ h_sub hx + +/-- **A p-variable is stochastically larger than the uniform law**: under a measure of total mass +at most `1`, the integral of an antitone function of a p-variable is at most its integral against +the uniform law on `[0, 1]`. -/ +theorem IsPVar.lintegral_comp_le (hp : IsPVar p S) (hP : P ∈ S) (hP1 : P univ ≤ 1) + (hf : Antitone f) : + ∫⁻ ω, f (p ω) ∂P ≤ ∫⁻ x in Icc (0 : ℝ) 1, f (ENNReal.ofReal x) := by + -- the layer cake formula on both sides reduces the claim to the superlevel sets of `f`, which + -- are lower sets since `f` is antitone + have h_cake_P := TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul P + (hf.measurable.comp hp.measurable).aemeasurable one_pos + have h_cake_U := TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul + (volume.restrict (Icc (0 : ℝ) 1)) + (hf.measurable.comp ENNReal.measurable_ofReal).aemeasurable one_pos + simp only [ENNReal.rpow_one, ENNReal.ofReal_one, one_mul, sub_self, Real.rpow_zero, + mul_one, Function.comp_apply] at h_cake_P h_cake_U + rw [h_cake_P, h_cake_U] + exact lintegral_mono fun t ↦ hp.measure_preimage_le hP hP1 + (L := {y | ENNReal.ofReal t < f y}) fun _ _ hxy hy ↦ hy.trans_le (hf hxy) + end ProbabilityTheory diff --git a/LMLExplore/Topology/Order/LeftRightLim.lean b/LMLExplore/Topology/Order/LeftRightLim.lean index 203d0062..a6c8d5b0 100644 --- a/LMLExplore/Topology/Order/LeftRightLim.lean +++ b/LMLExplore/Topology/Order/LeftRightLim.lean @@ -11,10 +11,9 @@ public import Mathlib.Topology.Semicontinuity.Defs /-! # Semicontinuity of one-sided limits of antitone functions -The left limit `Function.leftLim f` of an antitone function `f` is upper semicontinuous: it is -the upper semicontinuous regularization of `f`, from which it differs only at the (countably -many) discontinuities of `f`. Replacing a p-to-e calibrator by its left limit is how one shows that -admissible calibrators are upper semicontinuous. +The left limit `Function.leftLim f` of an antitone function `f` is upper semicontinuous, and +it agrees with `f` wherever `f` is continuous. Replacing a p-to-e calibrator by its left limit is +how one shows that admissible calibrators are upper semicontinuous. ## Main statements From 4843124f6335999fa2f7ec7a02bf6a261e124f7d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 22:07:26 +0100 Subject: [PATCH 3/5] docs: state the probability-measure hypothesis in the calibrator docstrings Co-Authored-By: Claude Code --- LMLExplore/EValues/Calibrator.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/LMLExplore/EValues/Calibrator.lean b/LMLExplore/EValues/Calibrator.lean index f52dcf93..e4caf65b 100644 --- a/LMLExplore/EValues/Calibrator.lean +++ b/LMLExplore/EValues/Calibrator.lean @@ -44,10 +44,11 @@ the upper semicontinuous calibrators with `f 0 = ∞` and `∫₀¹ f = 1` [RW, ## Main statements -* `ProbabilityTheory.IsPToECalibrator.isEVar_comp`: a calibrator turns every p-variable into an - e-variable [VW21, Proposition 2.1], and `ProbabilityTheory.isPToECalibrator_iff_isEVar`: an - antitone function vanishing on `(1, ∞]` is a calibrator as soon as it turns the identity of - `[0, 1]`, under Lebesgue measure, into an e-variable. +* `ProbabilityTheory.IsPToECalibrator.isEVar_comp`: for a null of probability measures, a + calibrator turns every p-variable into an e-variable [VW21, Proposition 2.1], and + `ProbabilityTheory.isPToECalibrator_iff_isEVar`: an antitone function vanishing on `(1, ∞]` is + a calibrator as soon as it turns the identity of `[0, 1]`, under Lebesgue measure, into an + e-variable. * `ProbabilityTheory.IsPToECalibrator.le_inv`: a calibrator is at most `x ↦ x⁻¹`. * `ProbabilityTheory.isAdmissiblePToECalibrator_iff`: the characterization of admissible calibrators [RW, Proposition 2.5]. @@ -82,8 +83,9 @@ variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {S : Set (Measure Ω)} {p : Ω /-- A **p-to-e calibrator** is an antitone `f : ℝ≥0∞ → ℝ≥0∞`, zero on `(1, ∞]`, with `∫₀¹ f ≤ 1`. This is the characterization of [RW, Proposition 2.5], taken as the definition: -these are exactly the antitone functions, zero on `(1, ∞]`, that turn every p-variable into an -e-variable (`IsPToECalibrator.isEVar_comp`, `isPToECalibrator_iff_isEVar`). -/ +these are exactly the antitone functions, zero on `(1, ∞]`, that turn every p-variable of every +null of probability measures into an e-variable (`IsPToECalibrator.isEVar_comp`, +`isPToECalibrator_iff_isEVar`). -/ structure IsPToECalibrator (f : ℝ≥0∞ → ℝ≥0∞) : Prop where antitone : Antitone f eq_zero_of_one_lt : ∀ x, 1 < x → f x = 0 From ae76cfb21b818a507e28cd88d378d9fb80310eae Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 22:31:37 +0100 Subject: [PATCH 4/5] refactor: export the rpow antiderivative, inline the toReal bound, simplify arithmetic closes Move `hasDerivAt_rpow_sub_one_mul` to a public `Real.hasDerivAt_rpow_sub_one_mul` in `LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean`, replace the private `toReal_le_one_of_le_one` by the Mathlib lemma `ENNReal.toReal_le_of_le_ofReal`, and close the arithmetic in `setLIntegral_powCalibrator` and `h_inv` with `simp`. Co-Authored-By: Claude Code --- .../Analysis/SpecialFunctions/Pow/Deriv.lean | 38 +++++++++++++++++++ LMLExplore/EValues/Calibrator.lean | 33 +++++----------- 2 files changed, 47 insertions(+), 24 deletions(-) create mode 100644 LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean diff --git a/LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean b/LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean new file mode 100644 index 00000000..c9dafbee --- /dev/null +++ b/LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean @@ -0,0 +1,38 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.Analysis.Calculus.Deriv.Basic +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Analysis.SpecialFunctions.Pow.Deriv + +/-! +# Derivatives of exponentials in the exponent + +A complement to `Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean`. + +## Main statements + +* `Real.hasDerivAt_rpow_sub_one_mul`: for `x > 0` with `log x ≠ 0`, the function + `κ ↦ x ^ (κ - 1) (κ log x - 1) / (log x) ^ 2` is an antiderivative of `κ ↦ κ x ^ (κ - 1)`. +-/ + +public section + +namespace Real + +/-- An antiderivative of `κ ↦ κ x ^ (κ - 1)`, for `x > 0` with `log x ≠ 0`. -/ +theorem hasDerivAt_rpow_sub_one_mul {x : ℝ} (hx : 0 < x) (hlog : log x ≠ 0) (κ : ℝ) : + HasDerivAt (fun κ ↦ x ^ (κ - 1) * (κ * log x - 1) / log x ^ 2) (κ * x ^ (κ - 1)) κ := by + have h_pow : HasDerivAt (fun κ ↦ x ^ (κ - 1)) (x ^ (κ - 1) * log x) κ := + HasDerivAt.comp_sub_const κ 1 (hasStrictDerivAt_const_rpow hx (κ - 1)).hasDerivAt + refine ((h_pow.mul (((hasDerivAt_id κ).mul_const (log x)).sub_const 1)).div_const + (log x ^ 2)).congr_deriv ?_ + simp only [id] + field_simp + ring + +end Real diff --git a/LMLExplore/EValues/Calibrator.lean b/LMLExplore/EValues/Calibrator.lean index e4caf65b..c8e245ea 100644 --- a/LMLExplore/EValues/Calibrator.lean +++ b/LMLExplore/EValues/Calibrator.lean @@ -10,7 +10,7 @@ public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal public import Mathlib.Analysis.SpecialFunctions.Log.Basic public import Mathlib.Topology.Semicontinuity.Defs import Mathlib.Analysis.SpecialFunctions.Pow.Continuity -import Mathlib.Analysis.SpecialFunctions.Pow.Deriv +import LMLExplore.Analysis.SpecialFunctions.Pow.Deriv import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus import LMLExplore.Topology.Order.LeftRightLim import LMLExplore.Topology.Semicontinuity.ENNReal @@ -115,10 +115,6 @@ theorem isPToECalibrator_iff_isEVar : exact hf.isEVar_comp (by simp only [mem_singleton_iff, forall_eq]; infer_instance) isExactPVar_ofReal_volume.toIsPVar -/-- An element of `ℝ≥0∞` at most `1` has real part at most `1`. -/ -private lemma toReal_le_one_of_le_one {x : ℝ≥0∞} (hx : x ≤ 1) : x.toReal ≤ 1 := - ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using hx) - /-- A calibrator is at most `x ↦ x⁻¹`: `x f x ≤ ∫₀ˣ f ≤ 1`. -/ theorem IsPToECalibrator.le_inv (hf : IsPToECalibrator f) (x : ℝ≥0∞) : f x ≤ x⁻¹ := by rcases lt_or_ge 1 x with hx | hx @@ -131,7 +127,8 @@ theorem IsPToECalibrator.le_inv (hf : IsPToECalibrator f) (x : ℝ≥0∞) : f x setLIntegral_mono (hf.measurable.comp ENNReal.measurable_ofReal) fun u hu ↦ hf.antitone (ENNReal.ofReal_le_of_le_toReal hu.2) _ ≤ ∫⁻ u in Icc (0 : ℝ) 1, f (ENNReal.ofReal u) := - lintegral_mono_set (Icc_subset_Icc_right (toReal_le_one_of_le_one hx)) + lintegral_mono_set (Icc_subset_Icc_right + (ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using hx))) _ ≤ 1 := hf.lintegral_le_one /-! ### Rescaling and mixtures -/ @@ -166,8 +163,8 @@ private lemma setLIntegral_const_mul_comp_mul (h_meas : Measurable f) rw [ENNReal.ofReal_mul ha0.le, ENNReal.ofReal_coe_nnreal] simp_rw [h_eq] have h_inv : (a : ℝ≥0∞) * ENNReal.ofReal ((a : ℝ) ^ (-1 : ℝ)) = 1 := by - rw [Real.rpow_neg_one, ENNReal.ofReal_inv_of_pos ha0, ENNReal.ofReal_coe_nnreal, - ENNReal.mul_inv_cancel (by simpa using ha0.ne') ENNReal.coe_ne_top] + simp [Real.rpow_neg_one, ENNReal.ofReal_inv_of_pos ha0, ENNReal.mul_inv_cancel, + (zero_lt_one.trans_le ha).ne'] rw [lintegral_const_mul (f := fun x ↦ f (ENNReal.ofReal (a * x))) _ (h_meas.comp (ENNReal.measurable_ofReal.comp (measurable_const_mul _))), h_cov, setLIntegral_Icc_ofReal_of_eq_zero h_zero (by exact_mod_cast ha), ← mul_assoc, h_inv, one_mul] @@ -300,7 +297,7 @@ private lemma eq_of_le_of_upperSemicontinuous rw [Measure.restrict_apply measurableSet_Ioo, inter_eq_left.2 fun v (hv : v ∈ Ioo l.toReal x.toReal) ↦ mem_Icc.2 ⟨ENNReal.toReal_nonneg.trans hv.1.le, hv.2.le.trans - (toReal_le_one_of_le_one hx1)⟩, Real.volume_Ioo] + (ENNReal.toReal_le_of_le_ofReal zero_le_one (by simpa using hx1))⟩, Real.volume_Ioo] exact ENNReal.ofReal_pos.2 (sub_pos.2 ((ENNReal.toReal_lt_toReal hl_top hx_top).2 hlx)) refine h_pos.ne' (measure_mono_null (fun v hv ↦ ?_) (ae_iff.1 h_ae)) have hv0 : 0 ≤ v := ENNReal.toReal_nonneg.trans hv.1.le @@ -375,8 +372,8 @@ theorem setLIntegral_powCalibrator {κ : ℝ} (hκ : 0 < κ) : rw [powCalibrator_of_le_one _ (ENNReal.ofReal_le_one.2 hx.2.le), ENNReal.ofReal_rpow_of_pos hx.1], lintegral_const_mul _ (by fun_prop), - TauCeti.lintegral_ofReal_rpow_Ioo (by linarith) zero_le_one, sub_add_cancel, - Real.one_rpow, ← ENNReal.ofReal_mul hκ.le, mul_one_div_cancel hκ.ne', ENNReal.ofReal_one] + TauCeti.lintegral_ofReal_rpow_Ioo (by linarith) zero_le_one, ← ENNReal.ofReal_mul hκ.le] + simp [hκ.ne'] /-- The power calibrators `x ↦ κ x ^ (κ - 1)`, `0 < κ ≤ 1`, are calibrators. -/ theorem isPToECalibrator_powCalibrator {κ : ℝ} (hκ0 : 0 < κ) (hκ1 : κ ≤ 1) : @@ -437,18 +434,6 @@ theorem isPToECalibrator_powMixCalibrator : IsPToECalibrator powMixCalibrator := filter_upwards [ae_restrict_mem measurableSet_Ioo] with κ hκ exact isPToECalibrator_powCalibrator hκ.1 hκ.2.le -/-- An antiderivative of `κ ↦ κ x ^ (κ - 1)`, for `x > 0` with `log x ≠ 0`. -/ -private lemma hasDerivAt_rpow_sub_one_mul {x : ℝ} (hx : 0 < x) (hlog : Real.log x ≠ 0) (κ : ℝ) : - HasDerivAt (fun κ ↦ x ^ (κ - 1) * (κ * Real.log x - 1) / Real.log x ^ 2) - (κ * x ^ (κ - 1)) κ := by - have h_pow : HasDerivAt (fun κ ↦ x ^ (κ - 1)) (x ^ (κ - 1) * Real.log x) κ := by - exact HasDerivAt.comp_sub_const κ 1 (Real.hasStrictDerivAt_const_rpow hx (κ - 1)).hasDerivAt - refine ((h_pow.mul (((hasDerivAt_id κ).mul_const (Real.log x)).sub_const 1)).div_const - (Real.log x ^ 2)).congr_deriv ?_ - simp only [id] - field_simp - ring - /-- **The closed form of the mixture of the power calibrators** [RW, (2.2)]: on `(0, 1)`, `∫₀¹ κ x ^ (κ - 1) dκ = (1 - x + x log x) / (x (log x) ^ 2)`. -/ theorem powMixCalibrator_ofReal {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : @@ -460,7 +445,7 @@ theorem powMixCalibrator_ofReal {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : have h_int : ∫ κ in (0 : ℝ)..1, κ * x ^ (κ - 1) = (1 - x + x * Real.log x) / (x * Real.log x ^ 2) := by rw [intervalIntegral.integral_eq_sub_of_hasDerivAt - (fun κ _ ↦ hasDerivAt_rpow_sub_one_mul hx0 hlog κ) (h_cont.intervalIntegrable _ _)] + (fun κ _ ↦ Real.hasDerivAt_rpow_sub_one_mul hx0 hlog κ) (h_cont.intervalIntegrable _ _)] simp only [sub_self, Real.rpow_zero, one_mul, zero_sub, zero_mul, Real.rpow_neg_one] field_simp ring From 842529b5ad36983d29cf50f8fa411c8a62e10359 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 22:55:28 +0100 Subject: [PATCH 5/5] refactor: rename the rpow antiderivative lemma to hasDerivAt_const_rpow_sub_one_mul_div The lemma differentiates in the exponent, so it follows Mathlib's `const_rpow` convention, and the name now records the `/ log x ^ 2` factor. Co-Authored-By: Claude Code --- LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean | 4 ++-- LMLExplore/EValues/Calibrator.lean | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean b/LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean index c9dafbee..1bfc9296 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Pow/Deriv.lean @@ -16,7 +16,7 @@ A complement to `Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean`. ## Main statements -* `Real.hasDerivAt_rpow_sub_one_mul`: for `x > 0` with `log x ≠ 0`, the function +* `Real.hasDerivAt_const_rpow_sub_one_mul_div`: for `x > 0` with `log x ≠ 0`, the function `κ ↦ x ^ (κ - 1) (κ log x - 1) / (log x) ^ 2` is an antiderivative of `κ ↦ κ x ^ (κ - 1)`. -/ @@ -25,7 +25,7 @@ public section namespace Real /-- An antiderivative of `κ ↦ κ x ^ (κ - 1)`, for `x > 0` with `log x ≠ 0`. -/ -theorem hasDerivAt_rpow_sub_one_mul {x : ℝ} (hx : 0 < x) (hlog : log x ≠ 0) (κ : ℝ) : +theorem hasDerivAt_const_rpow_sub_one_mul_div {x : ℝ} (hx : 0 < x) (hlog : log x ≠ 0) (κ : ℝ) : HasDerivAt (fun κ ↦ x ^ (κ - 1) * (κ * log x - 1) / log x ^ 2) (κ * x ^ (κ - 1)) κ := by have h_pow : HasDerivAt (fun κ ↦ x ^ (κ - 1)) (x ^ (κ - 1) * log x) κ := HasDerivAt.comp_sub_const κ 1 (hasStrictDerivAt_const_rpow hx (κ - 1)).hasDerivAt diff --git a/LMLExplore/EValues/Calibrator.lean b/LMLExplore/EValues/Calibrator.lean index c8e245ea..5d762eb9 100644 --- a/LMLExplore/EValues/Calibrator.lean +++ b/LMLExplore/EValues/Calibrator.lean @@ -445,7 +445,8 @@ theorem powMixCalibrator_ofReal {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : have h_int : ∫ κ in (0 : ℝ)..1, κ * x ^ (κ - 1) = (1 - x + x * Real.log x) / (x * Real.log x ^ 2) := by rw [intervalIntegral.integral_eq_sub_of_hasDerivAt - (fun κ _ ↦ Real.hasDerivAt_rpow_sub_one_mul hx0 hlog κ) (h_cont.intervalIntegrable _ _)] + (fun κ _ ↦ Real.hasDerivAt_const_rpow_sub_one_mul_div hx0 hlog κ) + (h_cont.intervalIntegrable _ _)] simp only [sub_self, Real.rpow_zero, one_mul, zero_sub, zero_mul, Real.rpow_neg_one] field_simp ring