From af10b457c19cf3c638cbab186d48130e4eacb5d4 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 12:47:18 +0100 Subject: [PATCH 1/6] feat: the dual formula for the smallest relative entropy to a null generated by finitely many constraints, with no constraint qualification MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For measurable constraints `g i` and a probability measure `Q` under which every `log⁺ |g i|` is integrable, `⨅ P ∈ constraintNull (range g), klDiv Q P` is the largest expected logarithm of an e-variable for the null, and of a bet `1 + ∑ i, π i * g i` (EValues roadmap, Layer 1.4). The equality between e-variables and bets holds for every finite measure. No Slater condition is assumed: the proof completes the damped and scaled reverse information projection into a member of the null by a finitely supported measure, through the complete class theorem. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- LMLExplore/EValues/ConstraintNull/KLInf.lean | 574 +++++++++++++++++++ 1 file changed, 574 insertions(+) create mode 100644 LMLExplore/EValues/ConstraintNull/KLInf.lean diff --git a/LMLExplore/EValues/ConstraintNull/KLInf.lean b/LMLExplore/EValues/ConstraintNull/KLInf.lean new file mode 100644 index 00000000..ae33b6b0 --- /dev/null +++ b/LMLExplore/EValues/ConstraintNull/KLInf.lean @@ -0,0 +1,574 @@ +/- +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.ConstraintNull.CompleteClass +public import Mathlib.Analysis.SpecialFunctions.Log.PosLog +public import Statlib.EValues.RIPr + +/-! +# The dual formula for the smallest relative entropy to a null generated by constraints + +Let `g i`, for `i` in a finite type, be measurable real constraints on a measurable space `𝓧`, and +`Q` a probability measure on `𝓧`. The smallest relative entropy from `Q` to the null +`constraintNull (range g)`, written $\mathrm{KL}_{\inf}$ in the bandit literature, is the largest +expected logarithm under `Q` of an e-variable for the null, and of a bet `1 + ∑ i, π i * g i`: +$$\inf_{P}\mathrm{KL}(Q,P)=\sup_{\pi}\mathbb E_Q\log\Big(1+\sum_i\pi_ig_i\Big) +=\texttt{maxUtility Q (constraintNull (range g)) logUtility}.$$ +The second equality holds for every finite measure `Q`. The first holds as soon as every +`log⁺ |g i|` is `Q`-integrable, with no constraint qualification: no member of the null is asked +to satisfy the constraints strictly, the null may be empty, and both sides may be infinite. + +The formulas of Honda and Takemura for one mean constraint on the laws on `[0, 1]` and on +`(-∞, 1]` [HT15] are cases of it, which this file does not derive. The proof does not go through +Lagrange duality, which needs Slater's condition. It compares both sides with the largest expected +logarithm of an e-variable, which Statlib's numeraire attains, and splits along +`exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos`. + +* If a nonnegative combination of the constraints is nonnegative almost surely under the null and + under `Q`, and positive on a set of positive `Q`-measure, its multiples are bets with unbounded + expected logarithms, and the three quantities are infinite. +* Otherwise a measurable set `Y` carries the null and `Q`, and the constraints admit no arbitrage + on `Y`. On `Y` every e-variable is at most a bet, which gives the second equality. For the + first, let `E` be the numeraire. The measure with density `1 / E` with respect to `Q`, the + reverse information projection, is damped by `1 + δ ∑ i, |g i|`, so that it integrates the + constraints, and scaled by `1 - ε`. It is then completed into a member of the null by a finitely + supported measure on `Y`: the complete class theorem, applied to the constraints shifted by + their means under the damped projection, gives the points and the weights. The relative entropy + from `Q` to that member of the null is at most the largest expected logarithm plus + `E_Q[log (1 + δ ∑ i, |g i|)] - log (1 - ε)`, which tends to `0` with `δ` and `ε`. + +## Main statements + +* `ProbabilityTheory.maxUtility_constraintNull_eq_iSup_eintegral_log`: the largest expected + logarithm of an e-variable for the null is that of a bet. +* `ProbabilityTheory.iInf_klDiv_constraintNull_eq_maxUtility`: the smallest relative entropy to + the null is the largest expected logarithm of an e-variable. +* `ProbabilityTheory.iInf_klDiv_constraintNull_eq_iSup_eintegral_log`: **the dual formula**. +* `ProbabilityTheory.exists_add_sum_smul_dirac_mem_constraintNull`: on a set without arbitrage + that carries the null, a finite measure under which every e-variable has mean at most `c < 1` + is completed into a member of the null by a finitely supported measure. + +## References + +* [HT15] J. Honda and A. Takemura, *Non-asymptotic analysis of a new bandit algorithm for + semi-bounded rewards*, J. Mach. Learn. Res. 16 (2015). +* [LRR26] M. Larsson, A. Ramdas and J. Ruf, *Testing hypotheses generated by constraints*, Math. + Oper. Res. (2026), arXiv:2504.02974v5. +-/ + +public section + +open MeasureTheory Set InformationTheory LMLExplore +open scoped ENNReal NNReal + +namespace ProbabilityTheory + +variable {𝓧 ι : Type*} [Fintype ι] [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {Y : Set 𝓧} + {Q : Measure 𝓧} + +/-! ### Completion into a member of the null -/ + +/-- **Completion by a finitely supported measure**: on a set `Y` without arbitrage that carries +the null, a finite measure carried by `Y` that integrates the constraints and under which every +e-variable has mean at most `c`, for some `c < 1`, becomes a member of the null once a finitely +supported measure is added. The proof applies the complete class theorem to the constraints +shifted by multiples of their means under the measure. -/ +theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) + (hYne : Y.Nonempty) {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) + (hgμ : ∀ i, Integrable (g i) μ) {c : ℝ≥0∞} (hc : c < 1) + (hμE : ∀ E, IsEVar E (constraintNull (range g)) → ∫⁻ x, E x ∂μ ≤ c) : + ∃ (α : Type) (_ : Fintype α) (x : α → 𝓧) (w : α → ℝ), (∀ k, 0 ≤ w k) ∧ + μ + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) ∈ constraintNull (range g) := by + classical + set r := μ.real univ with hr_def + set m := 1 - r with hm_def + have hm0 : 0 < m := by + have h1 := hμE 1 (isEVar_one _) + simp only [Pi.one_apply, lintegral_one] at h1 + have h2 : r < 1 := by + rw [hr_def, measureReal_def] + exact ENNReal.toReal_lt_of_lt_ofReal (by simpa using h1.trans_lt hc) + linarith + set z : ι → ℝ := fun i ↦ -(∫ x, g i x ∂μ) / m with hz_def + -- the shifted constraints admit no arbitrage on `Y` + have hz : NoArbitrageOn (fun i x ↦ g i x - z i) Y := by + refine noArbitrageOn_iff.2 fun π hπ hπY ↦ ?_ + set σ := (∑ i, π i * ∫ x, g i x ∂μ) / m with hσ_def + have hσz : ∑ i, π i * z i = -σ := by + rw [hσ_def, Finset.sum_div, ← Finset.sum_neg_distrib] + exact Finset.sum_congr rfl fun i _ ↦ by simp only [hz_def]; ring + have hπg : ∀ x ∈ Y, -σ ≤ ∑ i, π i * g i x := by + intro x hx + have := hπY x hx + simp only [mul_sub, Finset.sum_sub_distrib, hσz] at this + linarith + rcases lt_or_ge 0 σ with hσ | hσ + · -- a positive deficit would be paid by the mass that `μ` lacks: the bet with weights `π / σ` + -- would have mean `1` under `μ` + exfalso + have hsum : ∀ x, ∑ i, π i / σ * g i x = (∑ i, π i * g i x) / σ := fun x ↦ by + rw [Finset.sum_div] + exact Finset.sum_congr rfl fun i _ ↦ by ring + have hEY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i / σ * g i x := by + intro x hx + rw [hsum] + have : -1 ≤ (∑ i, π i * g i x) / σ := by + rw [le_div_iff₀ hσ] + linarith [hπg x hx] + linarith + have hcoe : ∀ i, ((π i / σ).toNNReal : ℝ) = π i / σ := fun i ↦ + Real.coe_toNNReal _ (div_nonneg (hπ i) hσ.le) + have hbet : (fun i ↦ (π i / σ).toNNReal) ∈ constraintBets g := + mem_constraintBets_iff.2 fun ν hν ↦ + Filter.eventually_of_mem (mem_ae_iff.2 (hYμ ν hν)) fun x hx ↦ by + simpa only [hcoe] using hEY x hx + have h1 := hμE _ (isEVar_ofReal_one_add_of_mem_constraintBets hg hbet) + simp only [hcoe] at h1 + rw [lintegral_ofReal_one_add_sum_mul hgμ _ + (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hEY)] at h1 + have h2 : ∑ i, π i / σ * ∫ x, g i x ∂μ = m := by + have : ∑ i, π i / σ * ∫ x, g i x ∂μ = (∑ i, π i * ∫ x, g i x ∂μ) / σ := by + rw [Finset.sum_div] + exact Finset.sum_congr rfl fun i _ ↦ by ring + rw [this, hσ_def, div_div_cancel₀ (by + intro h0 + rw [h0, zero_div] at hσ_def + exact hσ.ne' hσ_def)] + rw [h2, ← hr_def, hm_def, add_sub_cancel, ENNReal.ofReal_one] at h1 + exact lt_irrefl _ (h1.trans_lt hc) + · -- no deficit: the combination is nonnegative, hence zero, on `Y` + have h0 : ∀ x ∈ Y, 0 ≤ ∑ i, π i * g i x := fun x hx ↦ by linarith [hπg x hx] + have hzero := noArbitrageOn_iff.1 hY π hπ h0 + have hb : ∑ i, π i * ∫ x, g i x ∂μ = 0 := by + have hgi : ∀ i, Integrable (fun x ↦ π i * g i x) μ := fun i ↦ (hgμ i).const_mul (π i) + simp_rw [← integral_const_mul] + rw [← integral_finsetSum _ fun i _ ↦ hgi i] + exact integral_eq_zero_of_ae (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hzero) + have hσ0 : σ = 0 := by rw [hσ_def, hb, zero_div] + intro x hx + simp only [mul_sub, Finset.sum_sub_distrib, hσz, hσ0, neg_zero, sub_zero] + exact hzero x hx + -- a finitely supported law under which the shifted constraints have nonpositive means + obtain ⟨x₀, hx₀⟩ := hYne + obtain ⟨α, _, x, w, -, hw, hwz, -⟩ := exists_charging_family_of_noArbitrageOn hz hx₀ + obtain ⟨hw0, hw1⟩ := mem_simplex_iff.1 hw + refine ⟨α, inferInstance, x, fun k ↦ m * w k, fun k ↦ mul_nonneg hm0.le (hw0 k), ?_⟩ + have hdirac : ∀ (f : 𝓧 → ℝ), Measurable f → ∀ k ∈ Finset.univ, + Integrable f (ENNReal.ofReal (m * w k) • Measure.dirac (x k)) := fun f hf k _ ↦ + (integrable_dirac' hf.stronglyMeasurable (by simp)).smul_measure ENNReal.ofReal_ne_top + refine mem_constraintNull_range_iff.2 ⟨⟨?_⟩, fun i ↦ ?_⟩ + · simp only [add_apply, sum_apply, smul_apply, measure_univ, smul_eq_mul, mul_one] + rw [← ENNReal.ofReal_sum_of_nonneg fun k _ ↦ mul_nonneg hm0.le (hw0 k), ← Finset.mul_sum, + hw1, mul_one, ← ENNReal.ofReal_toReal (measure_ne_top μ univ), + ← ENNReal.ofReal_add ENNReal.toReal_nonneg hm0.le] + rw [← measureReal_def, ← hr_def, hm_def] + simp + · refine ⟨(hgμ i).add_measure (integrable_finsetSum_measure.2 (hdirac _ (hg i))), ?_⟩ + rw [integral_add_measure (hgμ i) (integrable_finsetSum_measure.2 (hdirac _ (hg i))), + integral_finsetSum_measure (hdirac _ (hg i))] + simp_rw [integral_smul_measure, integral_dirac' _ _ (hg i).stronglyMeasurable, + ENNReal.toReal_ofReal (mul_nonneg hm0.le (hw0 _)), smul_eq_mul] + have h1 := hwz i + simp only [mul_sub, Finset.sum_sub_distrib, ← Finset.sum_mul, hw1, one_mul, + sub_nonpos] at h1 + have h2 : ∑ k, m * w k * g i (x k) = m * ∑ k, w k * g i (x k) := by + rw [Finset.mul_sum] + exact Finset.sum_congr rfl fun k _ ↦ by ring + have h3 : m * z i = -∫ x, g i x ∂μ := by + simp only [hz_def] + field_simp + rw [h2] + nlinarith + +/-! ### Strong duality on a set without arbitrage -/ + +/-- If every `log⁺ |g i|` is integrable under a finite measure, so is +`log (1 + ∑ i, |g i|)`. -/ +private lemma integrable_log_one_add_sum_abs (hg : ∀ i, Measurable (g i)) [IsFiniteMeasure Q] + (hQ : ∀ i, Integrable (fun x ↦ Real.posLog (g i x)) Q) : + Integrable (fun x ↦ Real.log (1 + ∑ i, |g i x|)) Q := by + have hint : Integrable + (fun x ↦ Real.log (Fintype.card ι) + ∑ i, Real.posLog (g i x) + Real.log 2) Q := + ((integrable_const _).add (integrable_finsetSum _ fun i _ ↦ hQ i)).add (integrable_const _) + refine hint.mono' + (by fun_prop : Measurable fun x ↦ Real.log (1 + ∑ i, |g i x|)).aestronglyMeasurable + (ae_of_all _ fun x ↦ ?_) + have hsum : 0 ≤ ∑ i, |g i x| := Finset.sum_nonneg fun i _ ↦ abs_nonneg _ + rw [Real.norm_of_nonneg (Real.log_nonneg (by linarith))] + refine Real.log_one_add_le_posLog.trans ?_ + gcongr + simpa using Real.posLog_sum Finset.univ fun i ↦ |g i x| + +/-- The bound of strong duality for a damping `δ` and a slack `ε`: when `Q` is carried by a set +`Y` without arbitrage that carries the null, and the largest expected logarithm `s` of an +e-variable is finite, the reverse information projection `Q / E`, for the numeraire `E`, damped by +`1 + δ ∑ i, |g i|` so that it integrates the constraints, and scaled by `1 - ε`, is completed into +a member of the null by a finitely supported measure, at a relative entropy at most +`s + E_Q[log (1 + δ ∑ i, |g i|)] - log (1 - ε)`. -/ +private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) + [IsProbabilityMeasure Q] (hQY : Q Yᶜ = 0) + (hQ : Integrable (fun x ↦ Real.log (1 + ∑ i, |g i x|)) Q) + (hs : maxUtility Q (constraintNull (range g)) logUtility ≠ ⊤) {δ ε : ℝ} (hδ : 0 < δ) + (hδ1 : δ ≤ 1) (hε : 0 < ε) (hε1 : ε < 1) : + ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) ≤ + maxUtility Q (constraintNull (range g)) logUtility + + ((∫ x, Real.log (1 + δ * ∑ i, |g i x|) ∂Q - Real.log (1 - ε) : ℝ) : EReal) := by + have hS : ∀ μ ∈ constraintNull (range g), IsFiniteMeasure μ := fun μ hμ ↦ by + have := isProbabilityMeasure_of_mem_constraintNull hμ + infer_instance + set s := maxUtility Q (constraintNull (range g)) logUtility with hs_def + set E := numeraire Q (constraintNull (range g)) with hE_def + have hEnum := isNumeraire_numeraire Q hS + have hsE : s = ∫ᵉ x, ENNReal.log (E x) ∂Q := maxUtility_eq_eintegral_numeraire Q hS + have hE_top : ∀ᵐ x ∂Q, E x ≠ ∞ := by + have := ae_ne_top_of_eintegral_ne_top (by fun_prop) hEnum.eintegrable_log (hsE ▸ hs) + filter_upwards [this] with x hx + simpa using hx + have hYne : Y.Nonempty := by + by_contra h + rw [not_nonempty_iff_eq_empty] at h + simp [h] at hQY + have hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≤ 1 := by + simpa using hEnum.lintegral_div_le_one (isEVar_one _) + set h : 𝓧 → ℝ := fun x ↦ 1 + δ * ∑ i, |g i x| with hh_def + have hsum : ∀ x, 0 ≤ ∑ i, |g i x| := fun x ↦ Finset.sum_nonneg fun i _ ↦ abs_nonneg _ + have hh1 : ∀ x, 1 ≤ h x := fun x ↦ by + simp only [h] + nlinarith [hsum x] + have hh0 : ∀ x, 0 < h x := fun x ↦ zero_lt_one.trans_le (hh1 x) + -- the damped and scaled reverse information projection + set d : 𝓧 → ℝ≥0∞ := fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / h x) with hd_def + have hd : Measurable d := by fun_prop + set μ := Q.withDensity d with hμ_def + have hμ_le : ∀ F : 𝓧 → ℝ≥0∞, Measurable F → + ∫⁻ x, F x ∂μ ≤ ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q := by + intro F hF + rw [lintegral_withDensity_eq_lintegral_mul _ hd hF, ← lintegral_const_mul' _ _ + ENNReal.ofReal_ne_top] + refine lintegral_mono fun x ↦ ?_ + have : ENNReal.ofReal ((1 - ε) / h x) ≤ ENNReal.ofReal (1 - ε) := + ENNReal.ofReal_le_ofReal (div_le_self (by linarith) (hh1 x)) + calc (d * F) x = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / h x) * F x := rfl + _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 - ε) * F x := by gcongr + _ = ENNReal.ofReal (1 - ε) * (F x / E x) := by rw [div_eq_mul_inv]; ring + have hμE : ∀ F, IsEVar F (constraintNull (range g)) → + ∫⁻ x, F x ∂μ ≤ ENNReal.ofReal (1 - ε) := fun F hF ↦ + (hμ_le F hF.measurable).trans (by + calc ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q ≤ ENNReal.ofReal (1 - ε) * 1 := by + gcongr + exact hEnum.lintegral_div_le_one hF + _ = _ := mul_one _) + have hμfin : IsFiniteMeasure μ := ⟨by + have := hμE 1 (isEVar_one _) + simp only [Pi.one_apply, lintegral_one] at this + exact this.trans_lt ENNReal.ofReal_lt_top⟩ + have hμY : μ Yᶜ = 0 := withDensity_absolutelyContinuous Q d hQY + have hgμ : ∀ i, Integrable (g i) μ := by + intro i + refine ⟨(hg i).aestronglyMeasurable, ?_⟩ + rw [HasFiniteIntegral, lintegral_withDensity_eq_lintegral_mul _ hd (by fun_prop)] + calc ∫⁻ x, (d * fun x ↦ ‖g i x‖ₑ) x ∂Q ≤ ∫⁻ x, ENNReal.ofReal (1 / δ) * (E x)⁻¹ ∂Q := by + refine lintegral_mono fun x ↦ ?_ + have hgi : |g i x| ≤ ∑ j, |g j x| := + Finset.single_le_sum (f := fun j ↦ |g j x|) (fun j _ ↦ abs_nonneg _) + (Finset.mem_univ i) + have h1 : (1 - ε) / h x * |g i x| ≤ 1 / δ := by + rw [div_mul_eq_mul_div, div_le_div_iff₀ (hh0 x) hδ, one_mul] + have h2 : (1 - ε) * |g i x| * δ ≤ δ * |g i x| := by + nlinarith [mul_nonneg (mul_nonneg hε.le hδ.le) (abs_nonneg (g i x))] + have h3 : δ * |g i x| ≤ δ * ∑ j, |g j x| := mul_le_mul_of_nonneg_left hgi hδ.le + simp only [h] + linarith + calc (d * fun x ↦ ‖g i x‖ₑ) x + = (E x)⁻¹ * (ENNReal.ofReal ((1 - ε) / h x) * ‖g i x‖ₑ) := by + simp only [Pi.mul_apply, d, mul_assoc] + _ = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / h x * |g i x|) := by + rw [Real.eNorm_eq_ofReal_abs, ← ENNReal.ofReal_mul + (div_nonneg (by linarith) (hh0 x).le)] + _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 / δ) := by gcongr + _ = ENNReal.ofReal (1 / δ) * (E x)⁻¹ := mul_comm _ _ + _ = ENNReal.ofReal (1 / δ) * ∫⁻ x, (E x)⁻¹ ∂Q := + lintegral_const_mul' _ _ ENNReal.ofReal_ne_top + _ < ⊤ := ENNReal.mul_lt_top ENNReal.ofReal_lt_top (hEinv.trans_lt ENNReal.one_lt_top) + -- its completion into a member `P` of the null + obtain ⟨α, _, x, w, -, hP⟩ := exists_add_sum_smul_dirac_mem_constraintNull hg hY hYμ hYne hμY + hgμ (ENNReal.ofReal_lt_one.2 (by linarith)) hμE + set P := μ + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) with hP_def + have := isProbabilityMeasure_of_mem_constraintNull hP + refine (iInf₂_le P hP).trans ?_ + rw [← maxUtility_singleton_eq_klDiv Q P] + have hμeff : μ ∈ effectiveSet {P} := fun X hX ↦ + calc ∫⁻ x, X x ∂μ ≤ ∫⁻ x, X x ∂P := lintegral_mono' (Measure.le_add_right le_rfl) le_rfl + _ ≤ P univ := hX.lintegral_le_measure_univ P rfl + _ = 1 := measure_univ + have hdpos : ∀ x, E x ≠ ∞ → d x ≠ 0 := fun x hx ↦ by + simp only [d, ne_eq, mul_eq_zero, ENNReal.inv_eq_zero, hx, ENNReal.ofReal_eq_zero, + not_le, false_or] + exact div_pos (by linarith) (hh0 x) + have hac : Q ≪ μ := withDensity_absolutelyContinuous' hd.aemeasurable + (by filter_upwards [hE_top] with x hx using hdpos x hx) + have hlogh0 : Integrable (fun x ↦ Real.log (h x)) Q := by + refine Integrable.mono' hQ + (by fun_prop : Measurable fun x ↦ Real.log (h x)).aestronglyMeasurable + (ae_of_all _ fun x ↦ ?_) + rw [Real.norm_of_nonneg (Real.log_nonneg (hh1 x))] + refine Real.log_le_log (hh0 x) ?_ + simp only [h] + nlinarith [hsum x] + have hlogh : Integrable (fun x ↦ Real.log (h x) - Real.log (1 - ε)) Q := + hlogh0.sub (integrable_const _) + have hrn : ∀ᵐ x ∂Q, ENNReal.log ((μ.rnDeriv Q)⁻¹ x) = + ENNReal.log (E x) + ((Real.log (h x) - Real.log (1 - ε) : ℝ) : EReal) := by + filter_upwards [Measure.rnDeriv_withDensity Q hd, hE_top] with x hx hxt + have hpos : 0 < (1 - ε) / h x := div_pos (by linarith) (hh0 x) + rw [Pi.inv_apply, hx] + simp only [d] + rw [ENNReal.mul_inv (Or.inr ENNReal.ofReal_ne_top) (Or.inr (ENNReal.ofReal_pos.2 hpos).ne'), + inv_inv, ENNReal.log_mul_add, ← ENNReal.ofReal_inv_of_pos hpos, + ENNReal.log_ofReal_of_pos (inv_pos.2 hpos), inv_div, + Real.log_div (hh0 x).ne' (by linarith)] + -- the relative entropy from `Q` to `P` is at most that of the likelihood ratio of `Q` to `μ` + refine iSup₂_le fun X hX ↦ (eintegral_log_isEVar_le_eintegral_rnDeriv hμeff hac hX).trans ?_ + have hI := eintegral_eq_integral hlogh + have hI_bot : ∫ᵉ x, ((Real.log (h x) - Real.log (1 - ε) : ℝ) : EReal) ∂Q ≠ ⊥ := by + rw [hI] + exact EReal.coe_ne_bot _ + have hI_top : ∫ᵉ x, ((Real.log (h x) - Real.log (1 - ε) : ℝ) : EReal) ∂Q ≠ ⊤ := by + rw [hI] + exact EReal.coe_ne_top _ + rw [eintegral_congr_ae hrn, eintegral_add (by fun_prop) (by fun_prop) + (eintegrable_of_eintegral_ne_bot hI_bot) (.inr hI_top) (.inr hI_bot), hI, ← hsE, + integral_sub hlogh0 (integrable_const _)] + simp [h] + +/-- **Strong duality on a set without arbitrage**: when `Q` is carried by a set `Y` without +arbitrage that carries the null, and `log (1 + ∑ i, |g i|)` is `Q`-integrable, the smallest +relative entropy from `Q` to the null is at most the largest expected logarithm of an +e-variable. -/ +theorem iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) + [IsProbabilityMeasure Q] (hQY : Q Yᶜ = 0) + (hQ : Integrable (fun x ↦ Real.log (1 + ∑ i, |g i x|)) Q) : + ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) ≤ + maxUtility Q (constraintNull (range g)) logUtility := by + have hS : ∀ μ ∈ constraintNull (range g), IsFiniteMeasure μ := fun μ hμ ↦ by + have := isProbabilityMeasure_of_mem_constraintNull hμ + infer_instance + set s := maxUtility Q (constraintNull (range g)) logUtility with hs_def + rcases eq_or_ne s ⊤ with hs | hs + · rw [hs] + exact le_top + have hsE : s = ∫ᵉ x, ENNReal.log (numeraire Q (constraintNull (range g)) x) ∂Q := + maxUtility_eq_eintegral_numeraire Q hS + have hs_bot : s ≠ ⊥ := ne_bot_of_le_ne_bot (by simp) + (show (0 : EReal) ≤ s from hsE ▸ (isNumeraire_numeraire Q hS).eintegral_log_nonneg) + -- the damping tends to zero, by dominated convergence + have hlim : Filter.Tendsto (fun n : ℕ ↦ ∫ x, Real.log (1 + (1 / ((n : ℝ) + 1)) * + ∑ i, |g i x|) ∂Q) Filter.atTop (nhds 0) := by + have hsum : ∀ x, 0 ≤ ∑ i, |g i x| := fun x ↦ Finset.sum_nonneg fun i _ ↦ abs_nonneg _ + rw [← integral_zero 𝓧 ℝ (μ := Q)] + refine tendsto_integral_of_dominated_convergence _ (fun n ↦ (by fun_prop : + Measurable fun x ↦ Real.log (1 + (1 / ((n : ℝ) + 1)) * ∑ i, |g i x|)).aestronglyMeasurable) + hQ (fun n ↦ ae_of_all _ fun x ↦ ?_) (ae_of_all _ fun x ↦ ?_) + · have h1 : 1 / ((n : ℝ) + 1) ≤ 1 := by + rw [div_le_one (by positivity)] + linarith [n.cast_nonneg (α := ℝ)] + have h2 : (1 / ((n : ℝ) + 1)) * ∑ i, |g i x| ≤ ∑ i, |g i x| := by + nlinarith [hsum x] + have h3 : 0 ≤ (1 / ((n : ℝ) + 1)) * ∑ i, |g i x| := by + have := hsum x + positivity + rw [Real.norm_of_nonneg (Real.log_nonneg (by linarith))] + exact Real.log_le_log (by linarith) (by linarith) + · have : Filter.Tendsto (fun n : ℕ ↦ 1 + (1 / ((n : ℝ) + 1)) * ∑ i, |g i x|) Filter.atTop + (nhds 1) := by + simpa using (tendsto_one_div_add_atTop_nhds_zero_nat.mul_const (∑ i, |g i x|)).const_add 1 + have h := (Real.continuousAt_log one_ne_zero).tendsto.comp this + rwa [Real.log_one] at h + -- choose the damping and the slack for a given margin + rw [← EReal.le_of_forall_lt_iff_le] + intro z hz + have hs_eq : s = ((s.toReal : ℝ) : EReal) := (EReal.coe_toReal hs hs_bot).symm + rw [hs_eq, EReal.coe_lt_coe_iff] at hz + set η := z - s.toReal with hη_def + have hη : 0 < η := by linarith + obtain ⟨n, hn⟩ := (hlim.eventually (gt_mem_nhds (half_pos hη))).exists + set ε := 1 - Real.exp (-(η / 2)) with hε_def + have hε : 0 < ε := by + have : Real.exp (-(η / 2)) < 1 := Real.exp_lt_one_iff.2 (by linarith) + linarith + have hε1 : ε < 1 := by + have := Real.exp_pos (-(η / 2)) + linarith + have hlogε : Real.log (1 - ε) = -(η / 2) := by + rw [hε_def, sub_sub_cancel, Real.log_exp] + refine (iInf_klDiv_constraintNull_le_maxUtility_add hg hY hYμ hQY hQ hs + (δ := 1 / ((n : ℝ) + 1)) (by positivity) (by + rw [div_le_one (by positivity)] + linarith [n.cast_nonneg (α := ℝ)]) hε hε1).trans ?_ + rw [← hs_def, hs_eq, ← EReal.coe_add, EReal.coe_le_coe_iff, hlogε] + linarith + +/-! ### E-variables and bets -/ + +/-- On a set `Y` without arbitrage that carries the null and `Q`, the largest expected logarithm +of an e-variable is at most that of a bet: every e-variable is at most a bet on `Y`. -/ +theorem maxUtility_constraintNull_le_iSup_eintegral_log_of_noArbitrageOn + (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) + (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) (hQY : Q Yᶜ = 0) : + maxUtility Q (constraintNull (range g)) logUtility ≤ + ⨆ π ∈ constraintBets g, + ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q := by + refine iSup₂_le fun X hX ↦ ?_ + obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_toReal_le_of_isEVar hg hY hX + have hcoe : ∀ i, ((π i).toNNReal : ℝ) = π i := fun i ↦ + Real.coe_toNNReal _ ((mem_nonredundantWeights_iff.1 hπK).1 i) + have hbet : (fun i ↦ (π i).toNNReal) ∈ constraintBets g := + mem_constraintBets_iff.2 fun ν hν ↦ + Filter.eventually_of_mem (mem_ae_iff.2 (hYμ ν hν)) fun x hx ↦ by + simpa only [hcoe] using ENNReal.toReal_nonneg.trans (hπ x hx) + refine le_trans ?_ (le_iSup₂ (f := fun π (_ : π ∈ constraintBets g) ↦ + ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q) _ hbet) + refine eintegral_mono_ae (Filter.eventually_of_mem (mem_ae_iff.2 hQY) fun x hx ↦ ?_) + simp only [Function.comp_apply, logUtility_apply, hcoe] + refine ENNReal.log_le_log ?_ + rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hX hx).ne] + exact ENNReal.ofReal_le_ofReal (hπ x hx) + +/-- If a nonnegative combination of the constraints is nonnegative almost surely under every +member of the null and under a finite measure `Q`, and positive on a set of positive `Q`-measure, +then the bets have arbitrarily large expected logarithms under `Q`. -/ +theorem iSup_eintegral_log_ofReal_one_add_eq_top (hg : ∀ i, Measurable (g i)) + [IsFiniteMeasure Q] {ρ : ι → ℝ} (hρ : ∀ i, 0 ≤ ρ i) + (hρμ : ∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ ∑ i, ρ i * g i x) + (hρQ : ∀ᵐ x ∂Q, 0 ≤ ∑ i, ρ i * g i x) (hQρ : Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0) : + ⨆ π ∈ constraintBets g, + ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q = ⊤ := by + obtain ⟨c, hc, hQc⟩ : ∃ c : ℝ, 0 < c ∧ Q {x | c ≤ ∑ i, ρ i * g i x} ≠ 0 := by + by_contra! h + refine hQρ ?_ + have : {x | 0 < ∑ i, ρ i * g i x} = ⋃ n : ℕ, {x | 1 / ((n : ℝ) + 1) ≤ ∑ i, ρ i * g i x} := by + ext x + simp only [mem_ofPred_eq, mem_iUnion] + constructor + · intro hx + obtain ⟨n, hn⟩ := exists_nat_one_div_lt hx + exact ⟨n, hn.le⟩ + · rintro ⟨n, hn⟩ + exact lt_of_lt_of_le (by positivity) hn + rw [this] + exact measure_iUnion_null fun n ↦ h _ (by positivity) + set A := {x | c ≤ ∑ i, ρ i * g i x} with hA_def + have hA : MeasurableSet A := measurableSet_le measurable_const (by fun_prop) + set q := (Q A).toReal with hq_def + have hq : 0 < q := ENNReal.toReal_pos hQc (measure_ne_top Q A) + rw [EReal.eq_top_iff_forall_lt] + intro y + -- the bet with weights `t ρ` is at least `1`, and at least `1 + t c` on `A` + set t := (Real.exp (|y| / q + 1) - 1) / c with ht_def + have ht : 0 ≤ t := div_nonneg (by linarith [Real.one_le_exp (by positivity : 0 ≤ |y| / q + 1)]) + hc.le + have hsum : ∀ x, ∑ i, ((t * ρ i).toNNReal : ℝ) * g i x = t * ∑ i, ρ i * g i x := fun x ↦ by + simp only [Real.coe_toNNReal _ (mul_nonneg ht (hρ _)), mul_assoc, ← Finset.mul_sum] + have hbet : (fun i ↦ (t * ρ i).toNNReal) ∈ constraintBets g := by + refine mem_constraintBets_iff.2 fun μ hμ ↦ ?_ + filter_upwards [hρμ μ hμ] with x hx + rw [hsum] + have := mul_nonneg ht hx + linarith + have hlog : Real.log (1 + t * c) = |y| / q + 1 := by + rw [ht_def, div_mul_cancel₀ _ hc.ne', add_sub_cancel, Real.log_exp] + have hlow : ((Real.log (1 + t * c) * q : ℝ) : EReal) ≤ + ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, ((t * ρ i).toNNReal : ℝ) * g i x)) ∂Q := by + have hlc : 0 ≤ Real.log (1 + t * c) := Real.log_nonneg (by nlinarith) + calc ((Real.log (1 + t * c) * q : ℝ) : EReal) + = ∫ᵉ x, ((A.indicator (fun _ ↦ ENNReal.ofReal (Real.log (1 + t * c))) x : ℝ≥0∞) : + EReal) ∂Q := by + have : ENNReal.ofReal (Real.log (1 + t * c)) * Q A = + ENNReal.ofReal (Real.log (1 + t * c) * q) := by + rw [ENNReal.ofReal_mul hlc, hq_def, ENNReal.ofReal_toReal (measure_ne_top Q A)] + rw [eintegral_coe_ennreal, lintegral_indicator_const hA, this, + EReal.coe_ennreal_ofReal, max_eq_left (mul_nonneg hlc hq.le)] + _ ≤ _ := by + refine eintegral_mono_ae ?_ + filter_upwards [hρQ] with x hx + rw [hsum] + have h1 : 0 < 1 + t * ∑ i, ρ i * g i x := by nlinarith + rw [ENNReal.log_ofReal_of_pos h1] + by_cases hxA : x ∈ A + · rw [indicator_of_mem hxA, EReal.coe_ennreal_ofReal, max_eq_left hlc, + EReal.coe_le_coe_iff] + exact Real.log_le_log (by nlinarith) (by nlinarith [show c ≤ _ from hxA]) + · rw [indicator_of_notMem hxA, EReal.coe_ennreal_zero, ← EReal.coe_zero, + EReal.coe_le_coe_iff] + exact Real.log_nonneg (by nlinarith) + calc (y : EReal) < ((Real.log (1 + t * c) * q : ℝ) : EReal) := by + rw [hlog, EReal.coe_lt_coe_iff] + nlinarith [le_abs_self y, abs_nonneg y, div_mul_cancel₀ |y| hq.ne'] + _ ≤ _ := hlow + _ ≤ _ := le_iSup₂ (f := fun π (_ : π ∈ constraintBets g) ↦ + ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q) _ hbet + +/-- **The largest expected logarithm of an e-variable is that of a bet**: for finitely many +measurable constraints `g i` and a finite measure `Q`, the largest expected logarithm under `Q` +of an e-variable for the null is the supremum of the expected logarithms of the bets +`1 + ∑ i, π i * g i`. The expected logarithm of a bet is `⊥` when the bet vanishes or is negative +on a set of positive `Q`-measure. -/ +theorem maxUtility_constraintNull_eq_iSup_eintegral_log (hg : ∀ i, Measurable (g i)) + (Q : Measure 𝓧) [IsFiniteMeasure Q] : + maxUtility Q (constraintNull (range g)) logUtility = + ⨆ π ∈ constraintBets g, + ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q := by + refine le_antisymm ?_ (iSup₂_le fun π hπ ↦ + (isEVar_ofReal_one_add_of_mem_constraintBets hg hπ).eintegral_le_maxUtility Q logUtility) + obtain ⟨Y, -, hYμ, hQY, hY⟩ | ⟨ρ, hρ, hρμ, hρQ, hQρ⟩ := + exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos hg Q + · exact maxUtility_constraintNull_le_iSup_eintegral_log_of_noArbitrageOn hg hY hYμ hQY + · rw [iSup_eintegral_log_ofReal_one_add_eq_top hg hρ hρμ hρQ hQρ] + exact le_top + +/-! ### The dual formula -/ + +/-- **The smallest relative entropy to the null is the largest expected logarithm of an +e-variable**: for finitely many measurable constraints `g i` and a probability measure `Q` under +which every `log⁺ |g i|` is integrable, with no constraint qualification. The null may be empty: +both sides are then `⊤`. -/ +theorem iInf_klDiv_constraintNull_eq_maxUtility {κ : Type*} [Finite κ] {g : κ → 𝓧 → ℝ} + (hg : ∀ i, Measurable (g i)) (Q : Measure 𝓧) [IsProbabilityMeasure Q] + (hQ : ∀ i, Integrable (fun x ↦ Real.posLog (g i x)) Q) : + ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) = + maxUtility Q (constraintNull (range g)) logUtility := by + have := Fintype.ofFinite κ + refine le_antisymm ?_ (le_iInf₂ fun P hP ↦ ?_) + · obtain ⟨Y, -, hYμ, hQY, hY⟩ | ⟨ρ, hρ, hρμ, hρQ, hQρ⟩ := + exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos hg Q + · exact iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn hg hY hYμ hQY + (integrable_log_one_add_sum_abs hg hQ) + · rw [maxUtility_constraintNull_eq_iSup_eintegral_log hg Q, + iSup_eintegral_log_ofReal_one_add_eq_top hg hρ hρμ hρQ hQρ] + exact le_top + · have := isProbabilityMeasure_of_mem_constraintNull hP + rw [← maxUtility_singleton_eq_klDiv Q P] + exact maxUtility_anti (singleton_subset_iff.2 hP) + +/-- **The dual formula for the smallest relative entropy to a null generated by finitely many +constraints**: for measurable constraints `g i` and a probability measure `Q` under which every +`log⁺ |g i|` is integrable, the smallest relative entropy from `Q` to the null is the supremum of +the expected logarithms of the bets `1 + ∑ i, π i * g i`, with no constraint qualification. The +formulas of [HT15] for one mean constraint are cases of it. -/ +theorem iInf_klDiv_constraintNull_eq_iSup_eintegral_log (hg : ∀ i, Measurable (g i)) + (Q : Measure 𝓧) [IsProbabilityMeasure Q] + (hQ : ∀ i, Integrable (fun x ↦ Real.posLog (g i x)) Q) : + ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) = + ⨆ π ∈ constraintBets g, + ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q := by + rw [iInf_klDiv_constraintNull_eq_maxUtility hg Q hQ, + maxUtility_constraintNull_eq_iSup_eintegral_log hg Q] + +end ProbabilityTheory From 51948b13867f234cd10ef438144fee004cae1852 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:49:03 +0100 Subject: [PATCH 2/6] refactor: factor the dual-formula proofs into lemmas and cite their sources MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Add `IsEVar.exists_mem_constraintBets_le_of_noArbitrageOn` (CompleteClass) and derive `IsEVar.exists_mem_constraintBets_ae_le` and the bet bound of KLInf from it. - Add `toNNReal_mem_constraintBets` and `isFiniteMeasure_of_mem_constraintNull` (Basic). - Move the integrability of `log (1 + ∑ i, |f i|)` to the new general file `Analysis/SpecialFunctions/Integrability/PosLog.lean`, public, with the damped version. - Extract the no-arbitrage step of the completion lemma as `noArbitrageOn_add_integral_div_of_lintegral_le`, and the facts about the damped reverse information projection as private lemmas. - Cite [EVR26, Note 20] and [LRR26, Theorem 3.1]; fix the docstrings flagged by review. Co-Authored-By: Claude Code --- .../Integrability/PosLog.lean | 74 ++++ LMLExplore/EValues/ConstraintNull/Basic.lean | 14 + .../EValues/ConstraintNull/CompleteClass.lean | 30 +- LMLExplore/EValues/ConstraintNull/KLInf.lean | 412 +++++++++--------- 4 files changed, 316 insertions(+), 214 deletions(-) create mode 100644 LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean diff --git a/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean b/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean new file mode 100644 index 00000000..f7c842c3 --- /dev/null +++ b/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean @@ -0,0 +1,74 @@ +/- +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.SpecialFunctions.Log.PosLog +public import Mathlib.MeasureTheory.Function.L1Space.Integrable +import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic + +/-! +# Integrability of `log (1 + ∑ i, |f i|)` + +Finitely many real functions whose positive logarithms `log⁺ (f i)` are integrable under a finite +measure have an integrable `log (1 + ∑ i, |f i|)`, and damping the sum by a factor in `[0, 1]` +keeps the integrability. + +## Main statements + +* `Real.abs_log_one_add_mul_le`: `|log (1 + δ t)| ≤ log (1 + t)` for `t ≥ 0` and `δ ∈ [0, 1]`. +* `MeasureTheory.integrable_log_one_add_sum_abs`: if every `log⁺ (f i)` is integrable under a + finite measure, so is `log (1 + ∑ i, |f i|)`. +* `MeasureTheory.Integrable.log_one_add_const_mul`: if `log (1 + f)` is integrable for a + nonnegative `f`, so is `log (1 + δ f)` for `δ ∈ [0, 1]`. +-/ + +public section + +open MeasureTheory + +namespace Real + +/-- Damping by a factor `δ ∈ [0, 1]` decreases `log (1 + t)`, for `t ≥ 0`, and keeps it +nonnegative. -/ +theorem abs_log_one_add_mul_le {δ t : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (ht : 0 ≤ t) : + |log (1 + δ * t)| ≤ log (1 + t) := by + have h0 : 0 ≤ δ * t := mul_nonneg hδ ht + rw [abs_of_nonneg (log_nonneg (by linarith))] + exact log_le_log (by linarith) (by nlinarith) + +end Real + +namespace MeasureTheory + +variable {α ι : Type*} [MeasurableSpace α] {μ : Measure α} + +/-- If every `log⁺ (f i)` is integrable under a finite measure, so is `log (1 + ∑ i, |f i|)`. -/ +theorem integrable_log_one_add_sum_abs [Fintype ι] [IsFiniteMeasure μ] {f : ι → α → ℝ} + (hf : ∀ i, AEMeasurable (f i) μ) (h : ∀ i, Integrable (fun x ↦ Real.posLog (f i x)) μ) : + Integrable (fun x ↦ Real.log (1 + ∑ i, |f i x|)) μ := by + have hint : Integrable + (fun x ↦ Real.log (Fintype.card ι) + ∑ i, Real.posLog (f i x) + Real.log 2) μ := + ((integrable_const _).add (integrable_finsetSum _ fun i _ ↦ h i)).add (integrable_const _) + have hm : AEMeasurable (fun x ↦ Real.log (1 + ∑ i, |f i x|)) μ := by fun_prop + refine hint.mono' hm.aestronglyMeasurable (ae_of_all _ fun x ↦ ?_) + have hsum : 0 ≤ ∑ i, |f i x| := Finset.sum_nonneg fun i _ ↦ abs_nonneg _ + rw [Real.norm_of_nonneg (Real.log_nonneg (by linarith))] + refine Real.log_one_add_le_posLog.trans ?_ + gcongr + simpa using Real.posLog_sum Finset.univ fun i ↦ |f i x| + +/-- If `log (1 + f)` is integrable for a nonnegative `f`, so is `log (1 + δ f)` for +`δ ∈ [0, 1]`. -/ +theorem Integrable.log_one_add_const_mul {f : α → ℝ} + (h : Integrable (fun x ↦ Real.log (1 + f x)) μ) (hfm : AEMeasurable f μ) (hf : ∀ x, 0 ≤ f x) + {δ : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) : + Integrable (fun x ↦ Real.log (1 + δ * f x)) μ := by + have hm : AEMeasurable (fun x ↦ Real.log (1 + δ * f x)) μ := by fun_prop + refine h.mono' hm.aestronglyMeasurable (ae_of_all _ fun x ↦ ?_) + rw [Real.norm_eq_abs] + exact Real.abs_log_one_add_mul_le hδ hδ1 (hf x) + +end MeasureTheory diff --git a/LMLExplore/EValues/ConstraintNull/Basic.lean b/LMLExplore/EValues/ConstraintNull/Basic.lean index c60f0231..e52146bf 100644 --- a/LMLExplore/EValues/ConstraintNull/Basic.lean +++ b/LMLExplore/EValues/ConstraintNull/Basic.lean @@ -90,6 +90,11 @@ theorem isProbabilityMeasure_of_mem_constraintNull (hμ : μ ∈ constraintNull IsProbabilityMeasure μ := hμ.1 +/-- The members of the null generated by constraints are finite measures. -/ +theorem isFiniteMeasure_of_mem_constraintNull (hμ : μ ∈ constraintNull Φ) : IsFiniteMeasure μ := + have := isProbabilityMeasure_of_mem_constraintNull hμ + inferInstance + /-- The members of the null generated by constraints integrate the constraints. -/ theorem integrable_of_mem_constraintNull (hμ : μ ∈ constraintNull Φ) (hf : f ∈ Φ) : Integrable f μ := @@ -219,6 +224,15 @@ theorem mem_constraintBets_iff : ∀ μ ∈ constraintNull (range g), ∀ᵐ x ∂μ, 0 ≤ 1 + ∑ i, (π i : ℝ) * g i x := Iff.rfl +/-- Nonnegative real weights `ρ` give a bet as soon as `1 + ∑ i, ρ i * g i` is nonnegative on a +set `Y` that carries every member of the null. -/ +theorem toNNReal_mem_constraintBets {Y : Set 𝓧} (hYμ : ∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) + {ρ : ι → ℝ} (hρ : ∀ i, 0 ≤ ρ i) (hρY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, ρ i * g i x) : + (fun i ↦ (ρ i).toNNReal) ∈ constraintBets g := + mem_constraintBets_iff.2 fun μ hμ ↦ + Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ by + simpa only [Real.coe_toNNReal _ (hρ _)] using hρY x hx + /-- The zero bet, which keeps the wealth at `1`. -/ @[simp] theorem zero_mem_constraintBets : 0 ∈ constraintBets g := diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean index 9d9125de..8ee1cbb8 100644 --- a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean +++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean @@ -74,9 +74,11 @@ supported member of the null, so that e-variables are finite on `Y`. arbitrage. * `ProbabilityTheory.forall_integral_nonpos_iff_exists_ae_le`: **the complete class theorem** [LRR26, Theorem 3.1]. -* `ProbabilityTheory.IsEVar.exists_mem_constraintBets_ae_le`, +* `ProbabilityTheory.IsEVar.exists_mem_constraintBets_le_of_noArbitrageOn`, + `ProbabilityTheory.IsEVar.exists_mem_constraintBets_ae_le`, `ProbabilityTheory.isEVar_constraintNull_iff`: the complete class theorem for e-variables - [LRR26, Theorem 3.1]: every e-variable is dominated by a bet. + [LRR26, Theorem 3.1]: every e-variable is dominated by a bet, on a set without arbitrage that + carries the null, and almost surely under every member of the null. ## References @@ -599,6 +601,19 @@ theorem forall_integral_nonpos_iff_exists_ae_le (hg : ∀ i, Measurable (g i)) (integral_sum_mul_nonpos_of_mem_constraintNull hμ fun i ↦ (π i).coe_nonneg) · rw [integral_undef hfi] +/-- **The complete class theorem for e-variables on a set without arbitrage** [LRR26, +Theorem 3.1]: on a set `Y` without arbitrage that carries the null, every e-variable for the null +is at most a bet `1 + ∑ i, π i * g i`. -/ +theorem IsEVar.exists_mem_constraintBets_le_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hYμ : ∀ μ ∈ constraintNull (range g), μ Yᶜ = 0) + (hE : IsEVar E (constraintNull (range g))) : + ∃ π ∈ constraintBets g, ∀ x ∈ Y, E x ≤ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) := by + obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_toReal_le_of_isEVar hg hY hE + refine ⟨fun i ↦ (π i).toNNReal, toNNReal_mem_constraintBets hYμ hπK.1 fun x hx ↦ + ENNReal.toReal_nonneg.trans (hπ x hx), fun x hx ↦ ?_⟩ + rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hE hx).ne] + simpa only [Real.coe_toNNReal _ (hπK.1 _)] using ENNReal.ofReal_le_ofReal (hπ x hx) + /-- **The complete class theorem for e-variables** [LRR26, Theorem 3.1]: every e-variable for the null generated by finitely many measurable constraints `g i` is dominated by a bet `1 + ∑ i, π i * g i`, almost surely under every member of the null. -/ @@ -607,15 +622,8 @@ theorem IsEVar.exists_mem_constraintBets_ae_le (hg : ∀ i, Measurable (g i)) ∃ π ∈ constraintBets g, ∀ μ ∈ constraintNull (range g), E ≤ᵐ[μ] fun x ↦ ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x) := by obtain ⟨Y, -, hYμ, hY⟩ := exists_measurableSet_noArbitrageOn hg - obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_toReal_le_of_isEVar hg hY hE - have hπY : ∀ x ∈ Y, (E x).toReal ≤ 1 + ∑ i, ((π i).toNNReal : ℝ) * g i x := fun x hx ↦ by - simpa only [Real.coe_toNNReal _ (hπK.1 _)] using hπ x hx - refine ⟨fun i ↦ (π i).toNNReal, mem_constraintBets_iff.2 fun μ hμ ↦ - Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ - ENNReal.toReal_nonneg.trans (hπY x hx), fun μ hμ ↦ - Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) fun x hx ↦ ?_⟩ - rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hE hx).ne] - exact ENNReal.ofReal_le_ofReal (hπY x hx) + obtain ⟨π, hπ, hπY⟩ := hE.exists_mem_constraintBets_le_of_noArbitrageOn hg hY hYμ + exact ⟨π, hπ, fun μ hμ ↦ Filter.eventually_of_mem (mem_ae_iff.2 (hYμ μ hμ)) hπY⟩ /-- **The e-variables for a null generated by finitely many constraints** [LRR26, Theorem 3.1]: for measurable constraints `g i`, the e-variables for the null are the measurable functions that diff --git a/LMLExplore/EValues/ConstraintNull/KLInf.lean b/LMLExplore/EValues/ConstraintNull/KLInf.lean index ae33b6b0..23ff951f 100644 --- a/LMLExplore/EValues/ConstraintNull/KLInf.lean +++ b/LMLExplore/EValues/ConstraintNull/KLInf.lean @@ -8,6 +8,7 @@ module public import LMLExplore.EValues.ConstraintNull.CompleteClass public import Mathlib.Analysis.SpecialFunctions.Log.PosLog public import Statlib.EValues.RIPr +import LMLExplore.Analysis.SpecialFunctions.Integrability.PosLog /-! # The dual formula for the smallest relative entropy to a null generated by constraints @@ -23,7 +24,9 @@ The second equality holds for every finite measure `Q`. The first holds as soon to satisfy the constraints strictly, the null may be empty, and both sides may be infinite. The formulas of Honda and Takemura for one mean constraint on the laws on `[0, 1]` and on -`(-∞, 1]` [HT15] are cases of it, which this file does not derive. The proof does not go through +`(-∞, 1]` [HT15] are cases of it, which this file does not derive. The statements and the proof +follow [EVR26, Note 20], whose Lean library EValuesResearch proves them; the proofs here are +adapted from it. The proof does not go through Lagrange duality, which needs Slater's condition. It compares both sides with the largest expected logarithm of an e-variable, which Statlib's numeraire attains, and splits along `exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos`. @@ -32,12 +35,14 @@ logarithm of an e-variable, which Statlib's numeraire attains, and splits along under `Q`, and positive on a set of positive `Q`-measure, its multiples are bets with unbounded expected logarithms, and the three quantities are infinite. * Otherwise a measurable set `Y` carries the null and `Q`, and the constraints admit no arbitrage - on `Y`. On `Y` every e-variable is at most a bet, which gives the second equality. For the + on `Y`. On `Y` every e-variable is at most a bet, by the complete class theorem + [LRR26, Theorem 3.1], which gives the second equality. For the first, let `E` be the numeraire. The measure with density `1 / E` with respect to `Q`, the reverse information projection, is damped by `1 + δ ∑ i, |g i|`, so that it integrates the constraints, and scaled by `1 - ε`. It is then completed into a member of the null by a finitely - supported measure on `Y`: the complete class theorem, applied to the constraints shifted by - their means under the damped projection, gives the points and the weights. The relative entropy + supported measure on `Y`: the complete class theorem [LRR26, Theorem 3.1], applied to the + constraints shifted by their means under the damped projection, gives the points and the + weights. The relative entropy from `Q` to that member of the null is at most the largest expected logarithm plus `E_Q[log (1 + δ ∑ i, |g i|)] - log (1 - ε)`, which tends to `0` with `δ` and `ε`. @@ -49,11 +54,14 @@ logarithm of an e-variable, which Statlib's numeraire attains, and splits along the null is the largest expected logarithm of an e-variable. * `ProbabilityTheory.iInf_klDiv_constraintNull_eq_iSup_eintegral_log`: **the dual formula**. * `ProbabilityTheory.exists_add_sum_smul_dirac_mem_constraintNull`: on a set without arbitrage - that carries the null, a finite measure under which every e-variable has mean at most `c < 1` - is completed into a member of the null by a finitely supported measure. + that carries the null, a finite measure carried by that set that integrates the constraints and + under which every e-variable has mean at most `c < 1` is completed into a member of the null by + a finitely supported measure. ## References +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, notes 01–34 and the + Lean library EValuesResearch, github.com/RemyDegenne/evalues_research (2026). * [HT15] J. Honda and A. Takemura, *Non-asymptotic analysis of a new bandit algorithm for semi-bounded rewards*, J. Mach. Learn. Res. 16 (2015). * [LRR26] M. Larsson, A. Ramdas and J. Ruf, *Testing hypotheses generated by constraints*, Math. @@ -72,11 +80,77 @@ variable {𝓧 ι : Type*} [Fintype ι] [MeasurableSpace 𝓧] {g : ι → 𝓧 /-! ### Completion into a member of the null -/ +/-- **The shifted constraints admit no arbitrage**: on a set `Y` without arbitrage that carries +the null, let `μ` be a finite measure carried by `Y` that integrates the constraints and under +which every e-variable has mean at most `c`, for some `c < 1`. Then the constraints shifted by +their means under `μ` divided by the mass `1 - μ 𝓧` that `μ` lacks, +`g i + (∫ g i ∂μ) / (1 - μ 𝓧)`, admit no arbitrage on `Y`. -/ +theorem noArbitrageOn_add_integral_div_of_lintegral_le (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) + {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) (hgμ : ∀ i, Integrable (g i) μ) + {c : ℝ≥0∞} (hc : c < 1) + (hμE : ∀ E, IsEVar E (constraintNull (range g)) → ∫⁻ x, E x ∂μ ≤ c) : + NoArbitrageOn (fun i x ↦ g i x + (∫ y, g i y ∂μ) / (1 - μ.real univ)) Y := by + set m := 1 - μ.real univ with hm_def + refine noArbitrageOn_iff.2 fun π hπ hπY ↦ ?_ + set σ := (∑ i, π i * ∫ x, g i x ∂μ) / m with hσ_def + have hσa : ∑ i, π i * ((∫ x, g i x ∂μ) / m) = σ := by + rw [hσ_def, Finset.sum_div] + exact Finset.sum_congr rfl fun i _ ↦ by ring + have hπg : ∀ x ∈ Y, -σ ≤ ∑ i, π i * g i x := by + intro x hx + have := hπY x hx + simp only [mul_add, Finset.sum_add_distrib, hσa] at this + linarith + rcases lt_or_ge 0 σ with hσ | hσ + · -- a positive deficit would be paid by the mass that `μ` lacks: the bet with weights `π / σ` + -- would have mean `1` under `μ` + exfalso + have hsum : ∀ x, ∑ i, π i / σ * g i x = (∑ i, π i * g i x) / σ := fun x ↦ by + rw [Finset.sum_div] + exact Finset.sum_congr rfl fun i _ ↦ by ring + have hEY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i / σ * g i x := by + intro x hx + rw [hsum] + have : -1 ≤ (∑ i, π i * g i x) / σ := by + rw [le_div_iff₀ hσ] + linarith [hπg x hx] + linarith + have hcoe : ∀ i, ((π i / σ).toNNReal : ℝ) = π i / σ := fun i ↦ + Real.coe_toNNReal _ (div_nonneg (hπ i) hσ.le) + have h1 := hμE _ (isEVar_ofReal_one_add_of_mem_constraintBets hg + (toNNReal_mem_constraintBets hYμ (fun i ↦ div_nonneg (hπ i) hσ.le) hEY)) + simp only [hcoe] at h1 + rw [lintegral_ofReal_one_add_sum_mul hgμ _ + (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hEY)] at h1 + have h2 : ∑ i, π i / σ * ∫ x, g i x ∂μ = m := by + have : ∑ i, π i / σ * ∫ x, g i x ∂μ = (∑ i, π i * ∫ x, g i x ∂μ) / σ := by + rw [Finset.sum_div] + exact Finset.sum_congr rfl fun i _ ↦ by ring + rw [this, hσ_def, div_div_cancel₀ (by + intro h0 + rw [h0, zero_div] at hσ_def + exact hσ.ne' hσ_def)] + rw [h2, hm_def, add_sub_cancel, ENNReal.ofReal_one] at h1 + exact lt_irrefl _ (h1.trans_lt hc) + · -- no deficit: the combination is nonnegative, hence zero, on `Y` + have h0 : ∀ x ∈ Y, 0 ≤ ∑ i, π i * g i x := fun x hx ↦ by linarith [hπg x hx] + have hzero := noArbitrageOn_iff.1 hY π hπ h0 + have hb : ∑ i, π i * ∫ x, g i x ∂μ = 0 := by + have hgi : ∀ i, Integrable (fun x ↦ π i * g i x) μ := fun i ↦ (hgμ i).const_mul (π i) + simp_rw [← integral_const_mul] + rw [← integral_finsetSum _ fun i _ ↦ hgi i] + exact integral_eq_zero_of_ae (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hzero) + have hσ0 : σ = 0 := by rw [hσ_def, hb, zero_div] + intro x hx + simp only [mul_add, Finset.sum_add_distrib, hσa, hσ0, add_zero] + exact hzero x hx + /-- **Completion by a finitely supported measure**: on a set `Y` without arbitrage that carries the null, a finite measure carried by `Y` that integrates the constraints and under which every e-variable has mean at most `c`, for some `c < 1`, becomes a member of the null once a finitely -supported measure is added. The proof applies the complete class theorem to the constraints -shifted by multiples of their means under the measure. -/ +supported measure is added. It rests on the complete class theorem [LRR26, Theorem 3.1], and +follows [EVR26, Note 20]. -/ theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) (hYne : Y.Nonempty) {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) @@ -94,68 +168,12 @@ theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g rw [hr_def, measureReal_def] exact ENNReal.toReal_lt_of_lt_ofReal (by simpa using h1.trans_lt hc) linarith - set z : ι → ℝ := fun i ↦ -(∫ x, g i x ∂μ) / m with hz_def - -- the shifted constraints admit no arbitrage on `Y` - have hz : NoArbitrageOn (fun i x ↦ g i x - z i) Y := by - refine noArbitrageOn_iff.2 fun π hπ hπY ↦ ?_ - set σ := (∑ i, π i * ∫ x, g i x ∂μ) / m with hσ_def - have hσz : ∑ i, π i * z i = -σ := by - rw [hσ_def, Finset.sum_div, ← Finset.sum_neg_distrib] - exact Finset.sum_congr rfl fun i _ ↦ by simp only [hz_def]; ring - have hπg : ∀ x ∈ Y, -σ ≤ ∑ i, π i * g i x := by - intro x hx - have := hπY x hx - simp only [mul_sub, Finset.sum_sub_distrib, hσz] at this - linarith - rcases lt_or_ge 0 σ with hσ | hσ - · -- a positive deficit would be paid by the mass that `μ` lacks: the bet with weights `π / σ` - -- would have mean `1` under `μ` - exfalso - have hsum : ∀ x, ∑ i, π i / σ * g i x = (∑ i, π i * g i x) / σ := fun x ↦ by - rw [Finset.sum_div] - exact Finset.sum_congr rfl fun i _ ↦ by ring - have hEY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i / σ * g i x := by - intro x hx - rw [hsum] - have : -1 ≤ (∑ i, π i * g i x) / σ := by - rw [le_div_iff₀ hσ] - linarith [hπg x hx] - linarith - have hcoe : ∀ i, ((π i / σ).toNNReal : ℝ) = π i / σ := fun i ↦ - Real.coe_toNNReal _ (div_nonneg (hπ i) hσ.le) - have hbet : (fun i ↦ (π i / σ).toNNReal) ∈ constraintBets g := - mem_constraintBets_iff.2 fun ν hν ↦ - Filter.eventually_of_mem (mem_ae_iff.2 (hYμ ν hν)) fun x hx ↦ by - simpa only [hcoe] using hEY x hx - have h1 := hμE _ (isEVar_ofReal_one_add_of_mem_constraintBets hg hbet) - simp only [hcoe] at h1 - rw [lintegral_ofReal_one_add_sum_mul hgμ _ - (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hEY)] at h1 - have h2 : ∑ i, π i / σ * ∫ x, g i x ∂μ = m := by - have : ∑ i, π i / σ * ∫ x, g i x ∂μ = (∑ i, π i * ∫ x, g i x ∂μ) / σ := by - rw [Finset.sum_div] - exact Finset.sum_congr rfl fun i _ ↦ by ring - rw [this, hσ_def, div_div_cancel₀ (by - intro h0 - rw [h0, zero_div] at hσ_def - exact hσ.ne' hσ_def)] - rw [h2, ← hr_def, hm_def, add_sub_cancel, ENNReal.ofReal_one] at h1 - exact lt_irrefl _ (h1.trans_lt hc) - · -- no deficit: the combination is nonnegative, hence zero, on `Y` - have h0 : ∀ x ∈ Y, 0 ≤ ∑ i, π i * g i x := fun x hx ↦ by linarith [hπg x hx] - have hzero := noArbitrageOn_iff.1 hY π hπ h0 - have hb : ∑ i, π i * ∫ x, g i x ∂μ = 0 := by - have hgi : ∀ i, Integrable (fun x ↦ π i * g i x) μ := fun i ↦ (hgμ i).const_mul (π i) - simp_rw [← integral_const_mul] - rw [← integral_finsetSum _ fun i _ ↦ hgi i] - exact integral_eq_zero_of_ae (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hzero) - have hσ0 : σ = 0 := by rw [hσ_def, hb, zero_div] - intro x hx - simp only [mul_sub, Finset.sum_sub_distrib, hσz, hσ0, neg_zero, sub_zero] - exact hzero x hx - -- a finitely supported law under which the shifted constraints have nonpositive means + -- the complete class theorem, applied to the constraints shifted by multiples of their means + -- under `μ`, gives a finitely supported law under which the shifted constraints have + -- nonpositive means obtain ⟨x₀, hx₀⟩ := hYne - obtain ⟨α, _, x, w, -, hw, hwz, -⟩ := exists_charging_family_of_noArbitrageOn hz hx₀ + obtain ⟨α, _, x, w, -, hw, hwz, -⟩ := exists_charging_family_of_noArbitrageOn + (noArbitrageOn_add_integral_div_of_lintegral_le hg hY hYμ hμY hgμ hc hμE) hx₀ obtain ⟨hw0, hw1⟩ := mem_simplex_iff.1 hw refine ⟨α, inferInstance, x, fun k ↦ m * w k, fun k ↦ mul_nonneg hm0.le (hw0 k), ?_⟩ have hdirac : ∀ (f : 𝓧 → ℝ), Measurable f → ∀ k ∈ Finset.univ, @@ -174,35 +192,91 @@ theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g simp_rw [integral_smul_measure, integral_dirac' _ _ (hg i).stronglyMeasurable, ENNReal.toReal_ofReal (mul_nonneg hm0.le (hw0 _)), smul_eq_mul] have h1 := hwz i - simp only [mul_sub, Finset.sum_sub_distrib, ← Finset.sum_mul, hw1, one_mul, - sub_nonpos] at h1 + simp only [mul_add, Finset.sum_add_distrib, ← Finset.sum_mul, hw1, one_mul] at h1 have h2 : ∑ k, m * w k * g i (x k) = m * ∑ k, w k * g i (x k) := by rw [Finset.mul_sum] exact Finset.sum_congr rfl fun k _ ↦ by ring - have h3 : m * z i = -∫ x, g i x ∂μ := by - simp only [hz_def] + have h3 : m * ((∫ x, g i x ∂μ) / m) = ∫ x, g i x ∂μ := by field_simp rw [h2] nlinarith -/-! ### Strong duality on a set without arbitrage -/ +/-! ### The damped reverse information projection -/ -/-- If every `log⁺ |g i|` is integrable under a finite measure, so is -`log (1 + ∑ i, |g i|)`. -/ -private lemma integrable_log_one_add_sum_abs (hg : ∀ i, Measurable (g i)) [IsFiniteMeasure Q] - (hQ : ∀ i, Integrable (fun x ↦ Real.posLog (g i x)) Q) : - Integrable (fun x ↦ Real.log (1 + ∑ i, |g i x|)) Q := by - have hint : Integrable - (fun x ↦ Real.log (Fintype.card ι) + ∑ i, Real.posLog (g i x) + Real.log 2) Q := - ((integrable_const _).add (integrable_finsetSum _ fun i _ ↦ hQ i)).add (integrable_const _) - refine hint.mono' - (by fun_prop : Measurable fun x ↦ Real.log (1 + ∑ i, |g i x|)).aestronglyMeasurable - (ae_of_all _ fun x ↦ ?_) - have hsum : 0 ≤ ∑ i, |g i x| := Finset.sum_nonneg fun i _ ↦ abs_nonneg _ - rw [Real.norm_of_nonneg (Real.log_nonneg (by linarith))] - refine Real.log_one_add_le_posLog.trans ?_ - gcongr - simpa using Real.posLog_sum Finset.univ fun i ↦ |g i x| +/-- The reverse information projection `Q / E` damped by `1 + δ ∑ i, |g i|` and scaled by `1 - ε` +integrates the constraints, as soon as `∫ 1 / E ∂Q` is finite. -/ +private lemma integrable_withDensity_inv_mul_ofReal_div {E : 𝓧 → ℝ≥0∞} (hE : Measurable E) + (hg : ∀ i, Measurable (g i)) (hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≠ ∞) {δ ε : ℝ} (hδ : 0 < δ) + (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (i : ι) : + Integrable (g i) + (Q.withDensity fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) := by + refine ⟨(hg i).aestronglyMeasurable, ?_⟩ + rw [HasFiniteIntegral, lintegral_withDensity_eq_lintegral_mul _ (by fun_prop) (by fun_prop)] + calc ∫⁻ x, ((fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) * + fun x ↦ ‖g i x‖ₑ) x ∂Q + ≤ ∫⁻ x, ENNReal.ofReal (1 / δ) * (E x)⁻¹ ∂Q := by + refine lintegral_mono fun x ↦ ?_ + have hsum : 0 ≤ ∑ j, |g j x| := Finset.sum_nonneg fun j _ ↦ abs_nonneg _ + have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by nlinarith + have hgi : |g i x| ≤ ∑ j, |g j x| := + Finset.single_le_sum (f := fun j ↦ |g j x|) (fun j _ ↦ abs_nonneg _) + (Finset.mem_univ i) + have h1 : (1 - ε) / (1 + δ * ∑ j, |g j x|) * |g i x| ≤ 1 / δ := by + rw [div_mul_eq_mul_div, div_le_div_iff₀ hh0 hδ, one_mul] + have h2 : (1 - ε) * |g i x| * δ ≤ δ * |g i x| := by + nlinarith [mul_nonneg (mul_nonneg hε hδ.le) (abs_nonneg (g i x))] + have h3 : δ * |g i x| ≤ δ * ∑ j, |g j x| := mul_le_mul_of_nonneg_left hgi hδ.le + linarith + calc ((fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) * + fun x ↦ ‖g i x‖ₑ) x + = (E x)⁻¹ * (ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) * ‖g i x‖ₑ) := by + simp only [Pi.mul_apply, mul_assoc] + _ = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|) * |g i x|) := by + rw [Real.eNorm_eq_ofReal_abs, ← ENNReal.ofReal_mul + (div_nonneg (by linarith) hh0.le)] + _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 / δ) := by gcongr + _ = ENNReal.ofReal (1 / δ) * (E x)⁻¹ := mul_comm _ _ + _ = ENNReal.ofReal (1 / δ) * ∫⁻ x, (E x)⁻¹ ∂Q := + lintegral_const_mul' _ _ ENNReal.ofReal_ne_top + _ < ⊤ := ENNReal.mul_lt_top ENNReal.ofReal_lt_top hEinv.lt_top + +/-- The mean of a function under the damped and scaled reverse information projection is at most +`1 - ε` times its mean divided by `E` under `Q`. -/ +private lemma lintegral_withDensity_inv_mul_ofReal_div_le {E F : 𝓧 → ℝ≥0∞} (hE : Measurable E) + (hF : Measurable F) (hg : ∀ i, Measurable (g i)) {δ ε : ℝ} (hδ : 0 ≤ δ) (hε1 : ε ≤ 1) : + ∫⁻ x, F x ∂(Q.withDensity fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) + ≤ ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q := by + rw [lintegral_withDensity_eq_lintegral_mul _ (by fun_prop) hF, + ← lintegral_const_mul' _ _ ENNReal.ofReal_ne_top] + refine lintegral_mono fun x ↦ ?_ + have hsum : 0 ≤ ∑ j, |g j x| := Finset.sum_nonneg fun j _ ↦ abs_nonneg _ + have : ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) ≤ ENNReal.ofReal (1 - ε) := + ENNReal.ofReal_le_ofReal (div_le_self (by linarith) (by nlinarith)) + calc ((fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) * F) x + = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) * F x := rfl + _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 - ε) * F x := by gcongr + _ = ENNReal.ofReal (1 - ε) * (F x / E x) := by rw [div_eq_mul_inv]; ring + +/-- The logarithm of the likelihood ratio of `Q` to the damped and scaled reverse information +projection is `log E + log (1 + δ ∑ i, |g i|) - log (1 - ε)`, `Q`-almost everywhere. -/ +private lemma log_inv_rnDeriv_withDensity_inv_mul_ofReal_div [SigmaFinite Q] {E : 𝓧 → ℝ≥0∞} + (hE : Measurable E) (hg : ∀ i, Measurable (g i)) {δ ε : ℝ} + (hδ : 0 ≤ δ) (hε1 : ε < 1) : + ∀ᵐ x ∂Q, ENNReal.log (((Q.withDensity fun x ↦ + (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))).rnDeriv Q)⁻¹ x) = + ENNReal.log (E x) + + ((Real.log (1 + δ * ∑ j, |g j x|) - Real.log (1 - ε) : ℝ) : EReal) := by + filter_upwards [Measure.rnDeriv_withDensity Q (by fun_prop : Measurable fun x ↦ + (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)))] with x hx + have hsum : 0 ≤ ∑ j, |g j x| := Finset.sum_nonneg fun j _ ↦ abs_nonneg _ + have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by nlinarith + have hpos : 0 < (1 - ε) / (1 + δ * ∑ j, |g j x|) := div_pos (by linarith) hh0 + rw [Pi.inv_apply, hx] + rw [ENNReal.mul_inv (Or.inr ENNReal.ofReal_ne_top) (Or.inr (ENNReal.ofReal_pos.2 hpos).ne'), + inv_inv, ENNReal.log_mul_add, ← ENNReal.ofReal_inv_of_pos hpos, + ENNReal.log_ofReal_of_pos (inv_pos.2 hpos), inv_div, Real.log_div hh0.ne' (by linarith)] + +/-! ### Strong duality on a set without arbitrage -/ /-- The bound of strong duality for a damping `δ` and a slack `ε`: when `Q` is carried by a set `Y` without arbitrage that carries the null, and the largest expected logarithm `s` of an @@ -219,12 +293,12 @@ private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurabl ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) ≤ maxUtility Q (constraintNull (range g)) logUtility + ((∫ x, Real.log (1 + δ * ∑ i, |g i x|) ∂Q - Real.log (1 - ε) : ℝ) : EReal) := by - have hS : ∀ μ ∈ constraintNull (range g), IsFiniteMeasure μ := fun μ hμ ↦ by - have := isProbabilityMeasure_of_mem_constraintNull hμ - infer_instance + have hS : ∀ μ ∈ constraintNull (range g), IsFiniteMeasure μ := + fun _ ↦ isFiniteMeasure_of_mem_constraintNull set s := maxUtility Q (constraintNull (range g)) logUtility with hs_def set E := numeraire Q (constraintNull (range g)) with hE_def have hEnum := isNumeraire_numeraire Q hS + have hEm : Measurable E := hEnum.isEVar.measurable have hsE : s = ∫ᵉ x, ENNReal.log (E x) ∂Q := maxUtility_eq_eintegral_numeraire Q hS have hE_top : ∀ᵐ x ∂Q, E x ≠ ∞ := by have := ae_ne_top_of_eintegral_ne_top (by fun_prop) hEnum.eintegrable_log (hsE ▸ hs) @@ -236,66 +310,26 @@ private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurabl simp [h] at hQY have hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≤ 1 := by simpa using hEnum.lintegral_div_le_one (isEVar_one _) - set h : 𝓧 → ℝ := fun x ↦ 1 + δ * ∑ i, |g i x| with hh_def - have hsum : ∀ x, 0 ≤ ∑ i, |g i x| := fun x ↦ Finset.sum_nonneg fun i _ ↦ abs_nonneg _ - have hh1 : ∀ x, 1 ≤ h x := fun x ↦ by - simp only [h] - nlinarith [hsum x] - have hh0 : ∀ x, 0 < h x := fun x ↦ zero_lt_one.trans_le (hh1 x) -- the damped and scaled reverse information projection - set d : 𝓧 → ℝ≥0∞ := fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / h x) with hd_def + set d : 𝓧 → ℝ≥0∞ := fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ i, |g i x|)) + with hd_def have hd : Measurable d := by fun_prop set μ := Q.withDensity d with hμ_def - have hμ_le : ∀ F : 𝓧 → ℝ≥0∞, Measurable F → - ∫⁻ x, F x ∂μ ≤ ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q := by - intro F hF - rw [lintegral_withDensity_eq_lintegral_mul _ hd hF, ← lintegral_const_mul' _ _ - ENNReal.ofReal_ne_top] - refine lintegral_mono fun x ↦ ?_ - have : ENNReal.ofReal ((1 - ε) / h x) ≤ ENNReal.ofReal (1 - ε) := - ENNReal.ofReal_le_ofReal (div_le_self (by linarith) (hh1 x)) - calc (d * F) x = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / h x) * F x := rfl - _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 - ε) * F x := by gcongr - _ = ENNReal.ofReal (1 - ε) * (F x / E x) := by rw [div_eq_mul_inv]; ring have hμE : ∀ F, IsEVar F (constraintNull (range g)) → ∫⁻ x, F x ∂μ ≤ ENNReal.ofReal (1 - ε) := fun F hF ↦ - (hμ_le F hF.measurable).trans (by - calc ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q ≤ ENNReal.ofReal (1 - ε) * 1 := by - gcongr - exact hEnum.lintegral_div_le_one hF - _ = _ := mul_one _) + (lintegral_withDensity_inv_mul_ofReal_div_le hEm hF.measurable hg hδ.le hε1.le).trans + (by + calc ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q ≤ ENNReal.ofReal (1 - ε) * 1 := by + gcongr + exact hEnum.lintegral_div_le_one hF + _ = _ := mul_one _) have hμfin : IsFiniteMeasure μ := ⟨by have := hμE 1 (isEVar_one _) simp only [Pi.one_apply, lintegral_one] at this exact this.trans_lt ENNReal.ofReal_lt_top⟩ have hμY : μ Yᶜ = 0 := withDensity_absolutelyContinuous Q d hQY - have hgμ : ∀ i, Integrable (g i) μ := by - intro i - refine ⟨(hg i).aestronglyMeasurable, ?_⟩ - rw [HasFiniteIntegral, lintegral_withDensity_eq_lintegral_mul _ hd (by fun_prop)] - calc ∫⁻ x, (d * fun x ↦ ‖g i x‖ₑ) x ∂Q ≤ ∫⁻ x, ENNReal.ofReal (1 / δ) * (E x)⁻¹ ∂Q := by - refine lintegral_mono fun x ↦ ?_ - have hgi : |g i x| ≤ ∑ j, |g j x| := - Finset.single_le_sum (f := fun j ↦ |g j x|) (fun j _ ↦ abs_nonneg _) - (Finset.mem_univ i) - have h1 : (1 - ε) / h x * |g i x| ≤ 1 / δ := by - rw [div_mul_eq_mul_div, div_le_div_iff₀ (hh0 x) hδ, one_mul] - have h2 : (1 - ε) * |g i x| * δ ≤ δ * |g i x| := by - nlinarith [mul_nonneg (mul_nonneg hε.le hδ.le) (abs_nonneg (g i x))] - have h3 : δ * |g i x| ≤ δ * ∑ j, |g j x| := mul_le_mul_of_nonneg_left hgi hδ.le - simp only [h] - linarith - calc (d * fun x ↦ ‖g i x‖ₑ) x - = (E x)⁻¹ * (ENNReal.ofReal ((1 - ε) / h x) * ‖g i x‖ₑ) := by - simp only [Pi.mul_apply, d, mul_assoc] - _ = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / h x * |g i x|) := by - rw [Real.eNorm_eq_ofReal_abs, ← ENNReal.ofReal_mul - (div_nonneg (by linarith) (hh0 x).le)] - _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 / δ) := by gcongr - _ = ENNReal.ofReal (1 / δ) * (E x)⁻¹ := mul_comm _ _ - _ = ENNReal.ofReal (1 / δ) * ∫⁻ x, (E x)⁻¹ ∂Q := - lintegral_const_mul' _ _ ENNReal.ofReal_ne_top - _ < ⊤ := ENNReal.mul_lt_top ENNReal.ofReal_lt_top (hEinv.trans_lt ENNReal.one_lt_top) + have hgμ : ∀ i, Integrable (g i) μ := integrable_withDensity_inv_mul_ofReal_div hEm hg + (hEinv.trans_lt ENNReal.one_lt_top).ne hδ hε.le hε1.le -- its completion into a member `P` of the null obtain ⟨α, _, x, w, -, hP⟩ := exists_add_sum_smul_dirac_mem_constraintNull hg hY hYμ hYne hμY hgμ (ENNReal.ofReal_lt_one.2 (by linarith)) hμE @@ -308,44 +342,33 @@ private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurabl _ ≤ P univ := hX.lintegral_le_measure_univ P rfl _ = 1 := measure_univ have hdpos : ∀ x, E x ≠ ∞ → d x ≠ 0 := fun x hx ↦ by + have hsum : 0 ≤ ∑ i, |g i x| := Finset.sum_nonneg fun i _ ↦ abs_nonneg _ simp only [d, ne_eq, mul_eq_zero, ENNReal.inv_eq_zero, hx, ENNReal.ofReal_eq_zero, not_le, false_or] - exact div_pos (by linarith) (hh0 x) + exact div_pos (by linarith) (by nlinarith) have hac : Q ≪ μ := withDensity_absolutelyContinuous' hd.aemeasurable (by filter_upwards [hE_top] with x hx using hdpos x hx) - have hlogh0 : Integrable (fun x ↦ Real.log (h x)) Q := by - refine Integrable.mono' hQ - (by fun_prop : Measurable fun x ↦ Real.log (h x)).aestronglyMeasurable - (ae_of_all _ fun x ↦ ?_) - rw [Real.norm_of_nonneg (Real.log_nonneg (hh1 x))] - refine Real.log_le_log (hh0 x) ?_ - simp only [h] - nlinarith [hsum x] - have hlogh : Integrable (fun x ↦ Real.log (h x) - Real.log (1 - ε)) Q := + have hlogh0 : Integrable (fun x ↦ Real.log (1 + δ * ∑ i, |g i x|)) Q := + hQ.log_one_add_const_mul (by fun_prop) + (fun x ↦ Finset.sum_nonneg fun i _ ↦ abs_nonneg _) hδ.le hδ1 + have hlogh : Integrable + (fun x ↦ Real.log (1 + δ * ∑ i, |g i x|) - Real.log (1 - ε)) Q := hlogh0.sub (integrable_const _) - have hrn : ∀ᵐ x ∂Q, ENNReal.log ((μ.rnDeriv Q)⁻¹ x) = - ENNReal.log (E x) + ((Real.log (h x) - Real.log (1 - ε) : ℝ) : EReal) := by - filter_upwards [Measure.rnDeriv_withDensity Q hd, hE_top] with x hx hxt - have hpos : 0 < (1 - ε) / h x := div_pos (by linarith) (hh0 x) - rw [Pi.inv_apply, hx] - simp only [d] - rw [ENNReal.mul_inv (Or.inr ENNReal.ofReal_ne_top) (Or.inr (ENNReal.ofReal_pos.2 hpos).ne'), - inv_inv, ENNReal.log_mul_add, ← ENNReal.ofReal_inv_of_pos hpos, - ENNReal.log_ofReal_of_pos (inv_pos.2 hpos), inv_div, - Real.log_div (hh0 x).ne' (by linarith)] -- the relative entropy from `Q` to `P` is at most that of the likelihood ratio of `Q` to `μ` refine iSup₂_le fun X hX ↦ (eintegral_log_isEVar_le_eintegral_rnDeriv hμeff hac hX).trans ?_ have hI := eintegral_eq_integral hlogh - have hI_bot : ∫ᵉ x, ((Real.log (h x) - Real.log (1 - ε) : ℝ) : EReal) ∂Q ≠ ⊥ := by + have hI_bot : ∫ᵉ x, ((Real.log (1 + δ * ∑ i, |g i x|) - Real.log (1 - ε) : ℝ) : EReal) ∂Q ≠ + ⊥ := by rw [hI] exact EReal.coe_ne_bot _ - have hI_top : ∫ᵉ x, ((Real.log (h x) - Real.log (1 - ε) : ℝ) : EReal) ∂Q ≠ ⊤ := by + have hI_top : ∫ᵉ x, ((Real.log (1 + δ * ∑ i, |g i x|) - Real.log (1 - ε) : ℝ) : EReal) ∂Q ≠ + ⊤ := by rw [hI] exact EReal.coe_ne_top _ - rw [eintegral_congr_ae hrn, eintegral_add (by fun_prop) (by fun_prop) - (eintegrable_of_eintegral_ne_bot hI_bot) (.inr hI_top) (.inr hI_bot), hI, ← hsE, - integral_sub hlogh0 (integrable_const _)] - simp [h] + rw [eintegral_congr_ae (log_inv_rnDeriv_withDensity_inv_mul_ofReal_div hEm hg hδ.le hε1), + eintegral_add (by fun_prop) (by fun_prop) (eintegrable_of_eintegral_ne_bot hI_bot) + (.inr hI_top) (.inr hI_bot), hI, ← hsE, integral_sub hlogh0 (integrable_const _)] + simp /-- **Strong duality on a set without arbitrage**: when `Q` is carried by a set `Y` without arbitrage that carries the null, and `log (1 + ∑ i, |g i|)` is `Q`-integrable, the smallest @@ -357,9 +380,8 @@ theorem iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn (hg : ∀ i, Me (hQ : Integrable (fun x ↦ Real.log (1 + ∑ i, |g i x|)) Q) : ⨅ P ∈ constraintNull (range g), ((klDiv Q P : ℝ≥0∞) : EReal) ≤ maxUtility Q (constraintNull (range g)) logUtility := by - have hS : ∀ μ ∈ constraintNull (range g), IsFiniteMeasure μ := fun μ hμ ↦ by - have := isProbabilityMeasure_of_mem_constraintNull hμ - infer_instance + have hS : ∀ μ ∈ constraintNull (range g), IsFiniteMeasure μ := + fun _ ↦ isFiniteMeasure_of_mem_constraintNull set s := maxUtility Q (constraintNull (range g)) logUtility with hs_def rcases eq_or_ne s ⊤ with hs | hs · rw [hs] @@ -368,24 +390,17 @@ theorem iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn (hg : ∀ i, Me maxUtility_eq_eintegral_numeraire Q hS have hs_bot : s ≠ ⊥ := ne_bot_of_le_ne_bot (by simp) (show (0 : EReal) ≤ s from hsE ▸ (isNumeraire_numeraire Q hS).eintegral_log_nonneg) + have hδ1 : ∀ n : ℕ, 1 / ((n : ℝ) + 1) ≤ 1 := fun n ↦ div_le_one_of_le₀ (by simp) (by positivity) -- the damping tends to zero, by dominated convergence have hlim : Filter.Tendsto (fun n : ℕ ↦ ∫ x, Real.log (1 + (1 / ((n : ℝ) + 1)) * ∑ i, |g i x|) ∂Q) Filter.atTop (nhds 0) := by - have hsum : ∀ x, 0 ≤ ∑ i, |g i x| := fun x ↦ Finset.sum_nonneg fun i _ ↦ abs_nonneg _ rw [← integral_zero 𝓧 ℝ (μ := Q)] refine tendsto_integral_of_dominated_convergence _ (fun n ↦ (by fun_prop : Measurable fun x ↦ Real.log (1 + (1 / ((n : ℝ) + 1)) * ∑ i, |g i x|)).aestronglyMeasurable) hQ (fun n ↦ ae_of_all _ fun x ↦ ?_) (ae_of_all _ fun x ↦ ?_) - · have h1 : 1 / ((n : ℝ) + 1) ≤ 1 := by - rw [div_le_one (by positivity)] - linarith [n.cast_nonneg (α := ℝ)] - have h2 : (1 / ((n : ℝ) + 1)) * ∑ i, |g i x| ≤ ∑ i, |g i x| := by - nlinarith [hsum x] - have h3 : 0 ≤ (1 / ((n : ℝ) + 1)) * ∑ i, |g i x| := by - have := hsum x - positivity - rw [Real.norm_of_nonneg (Real.log_nonneg (by linarith))] - exact Real.log_le_log (by linarith) (by linarith) + · rw [Real.norm_eq_abs] + exact Real.abs_log_one_add_mul_le (by positivity) (hδ1 n) + (Finset.sum_nonneg fun i _ ↦ abs_nonneg _) · have : Filter.Tendsto (fun n : ℕ ↦ 1 + (1 / ((n : ℝ) + 1)) * ∑ i, |g i x|) Filter.atTop (nhds 1) := by simpa using (tendsto_one_div_add_atTop_nhds_zero_nat.mul_const (∑ i, |g i x|)).const_add 1 @@ -409,16 +424,15 @@ theorem iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn (hg : ∀ i, Me have hlogε : Real.log (1 - ε) = -(η / 2) := by rw [hε_def, sub_sub_cancel, Real.log_exp] refine (iInf_klDiv_constraintNull_le_maxUtility_add hg hY hYμ hQY hQ hs - (δ := 1 / ((n : ℝ) + 1)) (by positivity) (by - rw [div_le_one (by positivity)] - linarith [n.cast_nonneg (α := ℝ)]) hε hε1).trans ?_ + (δ := 1 / ((n : ℝ) + 1)) (by positivity) (hδ1 n) hε hε1).trans ?_ rw [← hs_def, hs_eq, ← EReal.coe_add, EReal.coe_le_coe_iff, hlogε] linarith /-! ### E-variables and bets -/ /-- On a set `Y` without arbitrage that carries the null and `Q`, the largest expected logarithm -of an e-variable is at most that of a bet: every e-variable is at most a bet on `Y`. -/ +of an e-variable is at most that of a bet: every e-variable is at most a bet on `Y`, by the +complete class theorem [LRR26, Theorem 3.1]. -/ theorem maxUtility_constraintNull_le_iSup_eintegral_log_of_noArbitrageOn (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) (hQY : Q Yᶜ = 0) : @@ -426,20 +440,12 @@ theorem maxUtility_constraintNull_le_iSup_eintegral_log_of_noArbitrageOn ⨆ π ∈ constraintBets g, ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q := by refine iSup₂_le fun X hX ↦ ?_ - obtain ⟨π, hπK, hπ⟩ := exists_mem_nonredundantWeights_toReal_le_of_isEVar hg hY hX - have hcoe : ∀ i, ((π i).toNNReal : ℝ) = π i := fun i ↦ - Real.coe_toNNReal _ ((mem_nonredundantWeights_iff.1 hπK).1 i) - have hbet : (fun i ↦ (π i).toNNReal) ∈ constraintBets g := - mem_constraintBets_iff.2 fun ν hν ↦ - Filter.eventually_of_mem (mem_ae_iff.2 (hYμ ν hν)) fun x hx ↦ by - simpa only [hcoe] using ENNReal.toReal_nonneg.trans (hπ x hx) + obtain ⟨π, hπ, hXπ⟩ := hX.exists_mem_constraintBets_le_of_noArbitrageOn hg hY hYμ refine le_trans ?_ (le_iSup₂ (f := fun π (_ : π ∈ constraintBets g) ↦ - ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q) _ hbet) + ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q) _ hπ) refine eintegral_mono_ae (Filter.eventually_of_mem (mem_ae_iff.2 hQY) fun x hx ↦ ?_) - simp only [Function.comp_apply, logUtility_apply, hcoe] - refine ENNReal.log_le_log ?_ - rw [← ENNReal.ofReal_toReal (lt_top_of_isEVar_of_noArbitrageOn hg hY hX hx).ne] - exact ENNReal.ofReal_le_ofReal (hπ x hx) + simp only [Function.comp_apply, logUtility_apply] + exact ENNReal.log_le_log (hXπ x hx) /-- If a nonnegative combination of the constraints is nonnegative almost surely under every member of the null and under a finite measure `Q`, and positive on a set of positive `Q`-measure, @@ -519,7 +525,7 @@ theorem iSup_eintegral_log_ofReal_one_add_eq_top (hg : ∀ i, Measurable (g i)) measurable constraints `g i` and a finite measure `Q`, the largest expected logarithm under `Q` of an e-variable for the null is the supremum of the expected logarithms of the bets `1 + ∑ i, π i * g i`. The expected logarithm of a bet is `⊥` when the bet vanishes or is negative -on a set of positive `Q`-measure. -/ +on a set of positive `Q`-measure. This follows [EVR26, Note 20]. -/ theorem maxUtility_constraintNull_eq_iSup_eintegral_log (hg : ∀ i, Measurable (g i)) (Q : Measure 𝓧) [IsFiniteMeasure Q] : maxUtility Q (constraintNull (range g)) logUtility = @@ -538,7 +544,7 @@ theorem maxUtility_constraintNull_eq_iSup_eintegral_log (hg : ∀ i, Measurable /-- **The smallest relative entropy to the null is the largest expected logarithm of an e-variable**: for finitely many measurable constraints `g i` and a probability measure `Q` under which every `log⁺ |g i|` is integrable, with no constraint qualification. The null may be empty: -both sides are then `⊤`. -/ +both sides are then `⊤`. This follows [EVR26, Note 20]. -/ theorem iInf_klDiv_constraintNull_eq_maxUtility {κ : Type*} [Finite κ] {g : κ → 𝓧 → ℝ} (hg : ∀ i, Measurable (g i)) (Q : Measure 𝓧) [IsProbabilityMeasure Q] (hQ : ∀ i, Integrable (fun x ↦ Real.posLog (g i x)) Q) : @@ -549,7 +555,7 @@ theorem iInf_klDiv_constraintNull_eq_maxUtility {κ : Type*} [Finite κ] {g : κ · obtain ⟨Y, -, hYμ, hQY, hY⟩ | ⟨ρ, hρ, hρμ, hρQ, hQρ⟩ := exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos hg Q · exact iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn hg hY hYμ hQY - (integrable_log_one_add_sum_abs hg hQ) + (integrable_log_one_add_sum_abs (fun i ↦ (hg i).aemeasurable) hQ) · rw [maxUtility_constraintNull_eq_iSup_eintegral_log hg Q, iSup_eintegral_log_ofReal_one_add_eq_top hg hρ hρμ hρQ hQρ] exact le_top @@ -561,7 +567,7 @@ theorem iInf_klDiv_constraintNull_eq_maxUtility {κ : Type*} [Finite κ] {g : κ constraints**: for measurable constraints `g i` and a probability measure `Q` under which every `log⁺ |g i|` is integrable, the smallest relative entropy from `Q` to the null is the supremum of the expected logarithms of the bets `1 + ∑ i, π i * g i`, with no constraint qualification. The -formulas of [HT15] for one mean constraint are cases of it. -/ +formulas of [HT15] for one mean constraint are cases of it. This follows [EVR26, Note 20]. -/ theorem iInf_klDiv_constraintNull_eq_iSup_eintegral_log (hg : ∀ i, Measurable (g i)) (Q : Measure 𝓧) [IsProbabilityMeasure Q] (hQ : ∀ i, Integrable (fun x ↦ Real.posLog (g i x)) Q) : From 5fe007473f513f5df0cb05a09e6d9350021f8e30 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:15:56 +0100 Subject: [PATCH 3/6] refactor: factor the general steps of the dual-formula proofs and cite [LRR25] Move the dominated-convergence step to `MeasureTheory.Integrable.tendsto_integral_log_one_add_mul` and the positive-measure superlevel set to `MeasureTheory.exists_gt_measure_setOf_le_ne_zero`; extract the completion of the damped reverse information projection into a private lemma; replace the repeated positivity and sum-division arguments by `positivity` and `simp`. Cite [LRR25] for the numeraire and the reverse information projection, and fix two docstrings that overclaimed. Co-Authored-By: Claude Code --- .../Integrability/PosLog.lean | 28 ++- LMLExplore/EValues/ConstraintNull/KLInf.lean | 163 ++++++++---------- .../Measure/MeasureSpaceDef.lean | 51 ++++++ 3 files changed, 151 insertions(+), 91 deletions(-) create mode 100644 LMLExplore/MeasureTheory/Measure/MeasureSpaceDef.lean diff --git a/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean b/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean index f7c842c3..cf5fdc65 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean @@ -7,14 +7,17 @@ module public import Mathlib.Analysis.SpecialFunctions.Log.PosLog public import Mathlib.MeasureTheory.Function.L1Space.Integrable +public import Mathlib.MeasureTheory.Integral.Bochner.Basic import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic +import Mathlib.MeasureTheory.Integral.DominatedConvergence /-! # Integrability of `log (1 + ∑ i, |f i|)` Finitely many real functions whose positive logarithms `log⁺ (f i)` are integrable under a finite measure have an integrable `log (1 + ∑ i, |f i|)`, and damping the sum by a factor in `[0, 1]` -keeps the integrability. +keeps the integrability. As the damping factor tends to `0`, so does the integral of the damped +logarithm, by dominated convergence. ## Main statements @@ -23,11 +26,13 @@ keeps the integrability. finite measure, so is `log (1 + ∑ i, |f i|)`. * `MeasureTheory.Integrable.log_one_add_const_mul`: if `log (1 + f)` is integrable for a nonnegative `f`, so is `log (1 + δ f)` for `δ ∈ [0, 1]`. +* `MeasureTheory.Integrable.tendsto_integral_log_one_add_mul`: if `log (1 + f)` is integrable for + a nonnegative `f`, then `∫ log (1 + δ f)` tends to `0` as `δ ≥ 0` tends to `0`. -/ public section -open MeasureTheory +open MeasureTheory Filter Topology namespace Real @@ -71,4 +76,23 @@ theorem Integrable.log_one_add_const_mul {f : α → ℝ} rw [Real.norm_eq_abs] exact Real.abs_log_one_add_mul_le hδ hδ1 (hf x) +/-- If `log (1 + f)` is integrable for a nonnegative `f`, then `∫ log (1 + δ f)` tends to `0` as +the damping factor `δ ≥ 0` tends to `0`, by dominated convergence. -/ +theorem Integrable.tendsto_integral_log_one_add_mul {f : α → ℝ} + (h : Integrable (fun x ↦ Real.log (1 + f x)) μ) (hfm : AEMeasurable f μ) (hf : ∀ x, 0 ≤ f x) + {β : Type*} {l : Filter β} [l.IsCountablyGenerated] {δ : β → ℝ} (hδ : Tendsto δ l (𝓝 0)) + (hδ0 : ∀ᶠ n in l, 0 ≤ δ n) : + Tendsto (fun n ↦ ∫ x, Real.log (1 + δ n * f x) ∂μ) l (𝓝 0) := by + rw [← integral_zero α ℝ (μ := μ)] + refine tendsto_integral_filter_of_dominated_convergence _ + (.of_forall fun n ↦ (by fun_prop : AEMeasurable (fun x ↦ Real.log (1 + δ n * f x)) μ) + |>.aestronglyMeasurable) + ((hδ0.and (hδ.eventually (ge_mem_nhds one_pos))).mono fun n hn ↦ ae_of_all _ fun x ↦ ?_) h + (ae_of_all _ fun x ↦ ?_) + · rw [Real.norm_eq_abs] + exact Real.abs_log_one_add_mul_le hn.1 hn.2 (hf x) + · have : Tendsto (fun n ↦ 1 + δ n * f x) l (𝓝 1) := by + simpa using (hδ.mul_const (f x)).const_add 1 + simpa [Function.comp_def] using (Real.continuousAt_log one_ne_zero).tendsto.comp this + end MeasureTheory diff --git a/LMLExplore/EValues/ConstraintNull/KLInf.lean b/LMLExplore/EValues/ConstraintNull/KLInf.lean index 23ff951f..2f608097 100644 --- a/LMLExplore/EValues/ConstraintNull/KLInf.lean +++ b/LMLExplore/EValues/ConstraintNull/KLInf.lean @@ -9,6 +9,7 @@ public import LMLExplore.EValues.ConstraintNull.CompleteClass public import Mathlib.Analysis.SpecialFunctions.Log.PosLog public import Statlib.EValues.RIPr import LMLExplore.Analysis.SpecialFunctions.Integrability.PosLog +import LMLExplore.MeasureTheory.Measure.MeasureSpaceDef /-! # The dual formula for the smallest relative entropy to a null generated by constraints @@ -28,7 +29,7 @@ The formulas of Honda and Takemura for one mean constraint on the laws on `[0, 1 follow [EVR26, Note 20], whose Lean library EValuesResearch proves them; the proofs here are adapted from it. The proof does not go through Lagrange duality, which needs Slater's condition. It compares both sides with the largest expected -logarithm of an e-variable, which Statlib's numeraire attains, and splits along +logarithm of an e-variable, which Statlib's numeraire [LRR25] attains, and splits along `exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos`. * If a nonnegative combination of the constraints is nonnegative almost surely under the null and @@ -38,7 +39,7 @@ logarithm of an e-variable, which Statlib's numeraire attains, and splits along on `Y`. On `Y` every e-variable is at most a bet, by the complete class theorem [LRR26, Theorem 3.1], which gives the second equality. For the first, let `E` be the numeraire. The measure with density `1 / E` with respect to `Q`, the - reverse information projection, is damped by `1 + δ ∑ i, |g i|`, so that it integrates the + reverse information projection [LRR25], is damped by `1 + δ ∑ i, |g i|`, so that it integrates the constraints, and scaled by `1 - ε`. It is then completed into a member of the null by a finitely supported measure on `Y`: the complete class theorem [LRR26, Theorem 3.1], applied to the constraints shifted by their means under the damped projection, gives the points and the @@ -49,14 +50,15 @@ logarithm of an e-variable, which Statlib's numeraire attains, and splits along ## Main statements * `ProbabilityTheory.maxUtility_constraintNull_eq_iSup_eintegral_log`: the largest expected - logarithm of an e-variable for the null is that of a bet. + logarithm of an e-variable for the null equals the supremum of the expected logarithms of the + bets. * `ProbabilityTheory.iInf_klDiv_constraintNull_eq_maxUtility`: the smallest relative entropy to the null is the largest expected logarithm of an e-variable. * `ProbabilityTheory.iInf_klDiv_constraintNull_eq_iSup_eintegral_log`: **the dual formula**. -* `ProbabilityTheory.exists_add_sum_smul_dirac_mem_constraintNull`: on a set without arbitrage - that carries the null, a finite measure carried by that set that integrates the constraints and - under which every e-variable has mean at most `c < 1` is completed into a member of the null by - a finitely supported measure. +* `ProbabilityTheory.exists_add_sum_smul_dirac_mem_constraintNull`: on a nonempty set without + arbitrage that carries the null, a finite measure carried by that set that integrates the + constraints and under which every e-variable has mean at most `c < 1` is completed into a member + of the null by a finitely supported measure. ## References @@ -64,6 +66,8 @@ logarithm of an e-variable, which Statlib's numeraire attains, and splits along Lean library EValuesResearch, github.com/RemyDegenne/evalues_research (2026). * [HT15] J. Honda and A. Takemura, *Non-asymptotic analysis of a new bandit algorithm for semi-bounded rewards*, J. Mach. Learn. Res. 16 (2015). +* [LRR25] M. Larsson, A. Ramdas and J. Ruf, *The numeraire e-variable and reverse information + projection*, Ann. Statist. 53 (2025), arXiv:2402.18810. * [LRR26] M. Larsson, A. Ramdas and J. Ruf, *Testing hypotheses generated by constraints*, Math. Oper. Res. (2026), arXiv:2504.02974v5. -/ @@ -95,8 +99,7 @@ theorem noArbitrageOn_add_integral_div_of_lintegral_le (hg : ∀ i, Measurable ( refine noArbitrageOn_iff.2 fun π hπ hπY ↦ ?_ set σ := (∑ i, π i * ∫ x, g i x ∂μ) / m with hσ_def have hσa : ∑ i, π i * ((∫ x, g i x ∂μ) / m) = σ := by - rw [hσ_def, Finset.sum_div] - exact Finset.sum_congr rfl fun i _ ↦ by ring + simp only [hσ_def, Finset.sum_div, mul_div_assoc] have hπg : ∀ x ∈ Y, -σ ≤ ∑ i, π i * g i x := by intro x hx have := hπY x hx @@ -107,8 +110,7 @@ theorem noArbitrageOn_add_integral_div_of_lintegral_le (hg : ∀ i, Measurable ( -- would have mean `1` under `μ` exfalso have hsum : ∀ x, ∑ i, π i / σ * g i x = (∑ i, π i * g i x) / σ := fun x ↦ by - rw [Finset.sum_div] - exact Finset.sum_congr rfl fun i _ ↦ by ring + simp only [Finset.sum_div, div_mul_eq_mul_div] have hEY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i / σ * g i x := by intro x hx rw [hsum] @@ -125,8 +127,7 @@ theorem noArbitrageOn_add_integral_div_of_lintegral_le (hg : ∀ i, Measurable ( (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hEY)] at h1 have h2 : ∑ i, π i / σ * ∫ x, g i x ∂μ = m := by have : ∑ i, π i / σ * ∫ x, g i x ∂μ = (∑ i, π i * ∫ x, g i x ∂μ) / σ := by - rw [Finset.sum_div] - exact Finset.sum_congr rfl fun i _ ↦ by ring + simp only [Finset.sum_div, div_mul_eq_mul_div] rw [this, hσ_def, div_div_cancel₀ (by intro h0 rw [h0, zero_div] at hσ_def @@ -146,11 +147,11 @@ theorem noArbitrageOn_add_integral_div_of_lintegral_le (hg : ∀ i, Measurable ( simp only [mul_add, Finset.sum_add_distrib, hσa, hσ0, add_zero] exact hzero x hx -/-- **Completion by a finitely supported measure**: on a set `Y` without arbitrage that carries -the null, a finite measure carried by `Y` that integrates the constraints and under which every -e-variable has mean at most `c`, for some `c < 1`, becomes a member of the null once a finitely -supported measure is added. It rests on the complete class theorem [LRR26, Theorem 3.1], and -follows [EVR26, Note 20]. -/ +/-- **Completion by a finitely supported measure**: on a nonempty set `Y` without arbitrage that +carries the null, a finite measure carried by `Y` that integrates the constraints and under which +every e-variable has mean at most `c`, for some `c < 1`, becomes a member of the null once a +finitely supported measure is added. It rests on the complete class theorem [LRR26, Theorem 3.1], +and follows [EVR26, Note 20]. -/ theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) (hYne : Y.Nonempty) {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) @@ -216,8 +217,7 @@ private lemma integrable_withDensity_inv_mul_ofReal_div {E : 𝓧 → ℝ≥0∞ fun x ↦ ‖g i x‖ₑ) x ∂Q ≤ ∫⁻ x, ENNReal.ofReal (1 / δ) * (E x)⁻¹ ∂Q := by refine lintegral_mono fun x ↦ ?_ - have hsum : 0 ≤ ∑ j, |g j x| := Finset.sum_nonneg fun j _ ↦ abs_nonneg _ - have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by nlinarith + have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by positivity have hgi : |g i x| ≤ ∑ j, |g j x| := Finset.single_le_sum (f := fun j ↦ |g j x|) (fun j _ ↦ abs_nonneg _) (Finset.mem_univ i) @@ -249,9 +249,8 @@ private lemma lintegral_withDensity_inv_mul_ofReal_div_le {E F : 𝓧 → ℝ≥ rw [lintegral_withDensity_eq_lintegral_mul _ (by fun_prop) hF, ← lintegral_const_mul' _ _ ENNReal.ofReal_ne_top] refine lintegral_mono fun x ↦ ?_ - have hsum : 0 ≤ ∑ j, |g j x| := Finset.sum_nonneg fun j _ ↦ abs_nonneg _ have : ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) ≤ ENNReal.ofReal (1 - ε) := - ENNReal.ofReal_le_ofReal (div_le_self (by linarith) (by nlinarith)) + ENNReal.ofReal_le_ofReal (div_le_self (by linarith) (le_add_of_nonneg_right (by positivity))) calc ((fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) * F) x = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) * F x := rfl _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 - ε) * F x := by gcongr @@ -268,14 +267,45 @@ private lemma log_inv_rnDeriv_withDensity_inv_mul_ofReal_div [SigmaFinite Q] {E ((Real.log (1 + δ * ∑ j, |g j x|) - Real.log (1 - ε) : ℝ) : EReal) := by filter_upwards [Measure.rnDeriv_withDensity Q (by fun_prop : Measurable fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)))] with x hx - have hsum : 0 ≤ ∑ j, |g j x| := Finset.sum_nonneg fun j _ ↦ abs_nonneg _ - have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by nlinarith + have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by positivity have hpos : 0 < (1 - ε) / (1 + δ * ∑ j, |g j x|) := div_pos (by linarith) hh0 rw [Pi.inv_apply, hx] rw [ENNReal.mul_inv (Or.inr ENNReal.ofReal_ne_top) (Or.inr (ENNReal.ofReal_pos.2 hpos).ne'), inv_inv, ENNReal.log_mul_add, ← ENNReal.ofReal_inv_of_pos hpos, ENNReal.log_ofReal_of_pos (inv_pos.2 hpos), inv_div, Real.log_div hh0.ne' (by linarith)] +/-- **Completion of the damped reverse information projection**: when `Q` is carried by a set `Y` +without arbitrage that carries the null, and `E` is such that `∫ F / E ∂Q ≤ 1` for every +e-variable `F`, as the numeraire is [LRR25], the reverse information projection `Q / E` damped by +`1 + δ ∑ i, |g i|` and scaled by `1 - ε` becomes a member of the null once a finitely supported +measure is added. -/ +private lemma exists_withDensity_inv_mul_ofReal_div_add_sum_smul_dirac_mem_constraintNull + (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) + (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) [IsProbabilityMeasure Q] (hQY : Q Yᶜ = 0) + {E : 𝓧 → ℝ≥0∞} (hE : Measurable E) + (hEF : ∀ F, IsEVar F (constraintNull (range g)) → ∫⁻ x, F x / E x ∂Q ≤ 1) {δ ε : ℝ} + (hδ : 0 < δ) (hε : 0 < ε) (hε1 : ε < 1) : + ∃ (α : Type) (_ : Fintype α) (x : α → 𝓧) (w : α → ℝ), + Q.withDensity (fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ i, |g i x|))) + + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) ∈ constraintNull (range g) := by + have hYne : Y.Nonempty := by + by_contra h + rw [not_nonempty_iff_eq_empty] at h + simp [h] at hQY + have hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≤ 1 := by simpa using hEF 1 (isEVar_one _) + set μ := Q.withDensity fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ i, |g i x|)) + have hμE : ∀ F, IsEVar F (constraintNull (range g)) → + ∫⁻ x, F x ∂μ ≤ ENNReal.ofReal (1 - ε) := fun F hF ↦ + (lintegral_withDensity_inv_mul_ofReal_div_le hE hF.measurable hg hδ.le hε1.le).trans + (mul_le_of_le_one_right' (hEF F hF)) + have : IsFiniteMeasure μ := + ⟨by simpa using (hμE 1 (isEVar_one _)).trans_lt ENNReal.ofReal_lt_top⟩ + obtain ⟨α, _, x, w, -, hP⟩ := exists_add_sum_smul_dirac_mem_constraintNull hg hY hYμ hYne + (withDensity_absolutelyContinuous Q _ hQY) + (integrable_withDensity_inv_mul_ofReal_div hE hg (hEinv.trans_lt ENNReal.one_lt_top).ne hδ + hε.le hε1.le) (ENNReal.ofReal_lt_one.2 (by linarith)) hμE + exact ⟨α, inferInstance, x, w, hP⟩ + /-! ### Strong duality on a set without arbitrage -/ /-- The bound of strong duality for a damping `δ` and a slack `ε`: when `Q` is carried by a set @@ -304,53 +334,33 @@ private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurabl have := ae_ne_top_of_eintegral_ne_top (by fun_prop) hEnum.eintegrable_log (hsE ▸ hs) filter_upwards [this] with x hx simpa using hx - have hYne : Y.Nonempty := by - by_contra h - rw [not_nonempty_iff_eq_empty] at h - simp [h] at hQY - have hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≤ 1 := by - simpa using hEnum.lintegral_div_le_one (isEVar_one _) - -- the damped and scaled reverse information projection + -- the damped and scaled reverse information projection, and its completion into a member `P` + -- of the null + obtain ⟨α, _, x, w, hP⟩ := + exists_withDensity_inv_mul_ofReal_div_add_sum_smul_dirac_mem_constraintNull hg hY hYμ hQY hEm + (fun F hF ↦ hEnum.lintegral_div_le_one hF) hδ hε hε1 set d : 𝓧 → ℝ≥0∞ := fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ i, |g i x|)) with hd_def have hd : Measurable d := by fun_prop set μ := Q.withDensity d with hμ_def - have hμE : ∀ F, IsEVar F (constraintNull (range g)) → - ∫⁻ x, F x ∂μ ≤ ENNReal.ofReal (1 - ε) := fun F hF ↦ - (lintegral_withDensity_inv_mul_ofReal_div_le hEm hF.measurable hg hδ.le hε1.le).trans - (by - calc ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q ≤ ENNReal.ofReal (1 - ε) * 1 := by - gcongr - exact hEnum.lintegral_div_le_one hF - _ = _ := mul_one _) - have hμfin : IsFiniteMeasure μ := ⟨by - have := hμE 1 (isEVar_one _) - simp only [Pi.one_apply, lintegral_one] at this - exact this.trans_lt ENNReal.ofReal_lt_top⟩ - have hμY : μ Yᶜ = 0 := withDensity_absolutelyContinuous Q d hQY - have hgμ : ∀ i, Integrable (g i) μ := integrable_withDensity_inv_mul_ofReal_div hEm hg - (hEinv.trans_lt ENNReal.one_lt_top).ne hδ hε.le hε1.le - -- its completion into a member `P` of the null - obtain ⟨α, _, x, w, -, hP⟩ := exists_add_sum_smul_dirac_mem_constraintNull hg hY hYμ hYne hμY - hgμ (ENNReal.ofReal_lt_one.2 (by linarith)) hμE set P := μ + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) with hP_def have := isProbabilityMeasure_of_mem_constraintNull hP + have hμP : μ ≤ P := Measure.le_add_right le_rfl + have : IsFiniteMeasure μ := isFiniteMeasure_of_le P hμP refine (iInf₂_le P hP).trans ?_ rw [← maxUtility_singleton_eq_klDiv Q P] have hμeff : μ ∈ effectiveSet {P} := fun X hX ↦ - calc ∫⁻ x, X x ∂μ ≤ ∫⁻ x, X x ∂P := lintegral_mono' (Measure.le_add_right le_rfl) le_rfl + calc ∫⁻ x, X x ∂μ ≤ ∫⁻ x, X x ∂P := lintegral_mono' hμP le_rfl _ ≤ P univ := hX.lintegral_le_measure_univ P rfl _ = 1 := measure_univ have hdpos : ∀ x, E x ≠ ∞ → d x ≠ 0 := fun x hx ↦ by - have hsum : 0 ≤ ∑ i, |g i x| := Finset.sum_nonneg fun i _ ↦ abs_nonneg _ simp only [d, ne_eq, mul_eq_zero, ENNReal.inv_eq_zero, hx, ENNReal.ofReal_eq_zero, not_le, false_or] - exact div_pos (by linarith) (by nlinarith) + exact div_pos (by linarith) (by positivity) have hac : Q ≪ μ := withDensity_absolutelyContinuous' hd.aemeasurable (by filter_upwards [hE_top] with x hx using hdpos x hx) have hlogh0 : Integrable (fun x ↦ Real.log (1 + δ * ∑ i, |g i x|)) Q := - hQ.log_one_add_const_mul (by fun_prop) - (fun x ↦ Finset.sum_nonneg fun i _ ↦ abs_nonneg _) hδ.le hδ1 + hQ.log_one_add_const_mul (by fun_prop) (fun x ↦ by positivity) hδ.le hδ1 have hlogh : Integrable (fun x ↦ Real.log (1 + δ * ∑ i, |g i x|) - Real.log (1 - ε)) Q := hlogh0.sub (integrable_const _) @@ -388,24 +398,12 @@ theorem iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn (hg : ∀ i, Me exact le_top have hsE : s = ∫ᵉ x, ENNReal.log (numeraire Q (constraintNull (range g)) x) ∂Q := maxUtility_eq_eintegral_numeraire Q hS - have hs_bot : s ≠ ⊥ := ne_bot_of_le_ne_bot (by simp) - (show (0 : EReal) ≤ s from hsE ▸ (isNumeraire_numeraire Q hS).eintegral_log_nonneg) + have hs0 : (0 : EReal) ≤ s := hsE ▸ (isNumeraire_numeraire Q hS).eintegral_log_nonneg + have hs_bot : s ≠ ⊥ := ne_bot_of_le_ne_bot (by simp) hs0 have hδ1 : ∀ n : ℕ, 1 / ((n : ℝ) + 1) ≤ 1 := fun n ↦ div_le_one_of_le₀ (by simp) (by positivity) -- the damping tends to zero, by dominated convergence - have hlim : Filter.Tendsto (fun n : ℕ ↦ ∫ x, Real.log (1 + (1 / ((n : ℝ) + 1)) * - ∑ i, |g i x|) ∂Q) Filter.atTop (nhds 0) := by - rw [← integral_zero 𝓧 ℝ (μ := Q)] - refine tendsto_integral_of_dominated_convergence _ (fun n ↦ (by fun_prop : - Measurable fun x ↦ Real.log (1 + (1 / ((n : ℝ) + 1)) * ∑ i, |g i x|)).aestronglyMeasurable) - hQ (fun n ↦ ae_of_all _ fun x ↦ ?_) (ae_of_all _ fun x ↦ ?_) - · rw [Real.norm_eq_abs] - exact Real.abs_log_one_add_mul_le (by positivity) (hδ1 n) - (Finset.sum_nonneg fun i _ ↦ abs_nonneg _) - · have : Filter.Tendsto (fun n : ℕ ↦ 1 + (1 / ((n : ℝ) + 1)) * ∑ i, |g i x|) Filter.atTop - (nhds 1) := by - simpa using (tendsto_one_div_add_atTop_nhds_zero_nat.mul_const (∑ i, |g i x|)).const_add 1 - have h := (Real.continuousAt_log one_ne_zero).tendsto.comp this - rwa [Real.log_one] at h + have hlim := hQ.tendsto_integral_log_one_add_mul (by fun_prop) (fun x ↦ by positivity) + tendsto_one_div_add_atTop_nhds_zero_nat (.of_forall fun n ↦ by positivity) -- choose the damping and the slack for a given margin rw [← EReal.le_of_forall_lt_iff_le] intro z hz @@ -456,20 +454,7 @@ theorem iSup_eintegral_log_ofReal_one_add_eq_top (hg : ∀ i, Measurable (g i)) (hρQ : ∀ᵐ x ∂Q, 0 ≤ ∑ i, ρ i * g i x) (hQρ : Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0) : ⨆ π ∈ constraintBets g, ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q = ⊤ := by - obtain ⟨c, hc, hQc⟩ : ∃ c : ℝ, 0 < c ∧ Q {x | c ≤ ∑ i, ρ i * g i x} ≠ 0 := by - by_contra! h - refine hQρ ?_ - have : {x | 0 < ∑ i, ρ i * g i x} = ⋃ n : ℕ, {x | 1 / ((n : ℝ) + 1) ≤ ∑ i, ρ i * g i x} := by - ext x - simp only [mem_ofPred_eq, mem_iUnion] - constructor - · intro hx - obtain ⟨n, hn⟩ := exists_nat_one_div_lt hx - exact ⟨n, hn.le⟩ - · rintro ⟨n, hn⟩ - exact lt_of_lt_of_le (by positivity) hn - rw [this] - exact measure_iUnion_null fun n ↦ h _ (by positivity) + obtain ⟨c, hc, hQc⟩ := exists_gt_measure_setOf_le_ne_zero hQρ set A := {x | c ≤ ∑ i, ρ i * g i x} with hA_def have hA : MeasurableSet A := measurableSet_le measurable_const (by fun_prop) set q := (Q A).toReal with hq_def @@ -521,11 +506,11 @@ theorem iSup_eintegral_log_ofReal_one_add_eq_top (hg : ∀ i, Measurable (g i)) _ ≤ _ := le_iSup₂ (f := fun π (_ : π ∈ constraintBets g) ↦ ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, (π i : ℝ) * g i x)) ∂Q) _ hbet -/-- **The largest expected logarithm of an e-variable is that of a bet**: for finitely many -measurable constraints `g i` and a finite measure `Q`, the largest expected logarithm under `Q` -of an e-variable for the null is the supremum of the expected logarithms of the bets -`1 + ∑ i, π i * g i`. The expected logarithm of a bet is `⊥` when the bet vanishes or is negative -on a set of positive `Q`-measure. This follows [EVR26, Note 20]. -/ +/-- **The largest expected logarithm of an e-variable is the supremum of those of the bets**: for +finitely many measurable constraints `g i` and a finite measure `Q`, the largest expected +logarithm under `Q` of an e-variable for the null is the supremum of the expected logarithms of +the bets `1 + ∑ i, π i * g i`. The expected logarithm of a bet is `⊥` when the bet vanishes or is +negative on a set of positive `Q`-measure. This follows [EVR26, Note 20]. -/ theorem maxUtility_constraintNull_eq_iSup_eintegral_log (hg : ∀ i, Measurable (g i)) (Q : Measure 𝓧) [IsFiniteMeasure Q] : maxUtility Q (constraintNull (range g)) logUtility = diff --git a/LMLExplore/MeasureTheory/Measure/MeasureSpaceDef.lean b/LMLExplore/MeasureTheory/Measure/MeasureSpaceDef.lean new file mode 100644 index 00000000..6809a3f0 --- /dev/null +++ b/LMLExplore/MeasureTheory/Measure/MeasureSpaceDef.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.MeasureTheory.Measure.MeasureSpaceDef +public import Mathlib.Algebra.Order.Archimedean.Real.Basic + +/-! +# A superlevel set of positive measure + +If a real function exceeds `a` on a set of positive measure, then it is at least some `c > a` on a +set of positive measure: the set `{a < f}` is the countable union of the sets +`{a + 1 / (n + 1) ≤ f}`. + +## Main statements + +* `MeasureTheory.exists_gt_measure_setOf_le_ne_zero`: if `μ {a < f} ≠ 0`, then + `μ {c ≤ f} ≠ 0` for some `c > a`. +-/ + +public section + +open Set + +namespace MeasureTheory + +variable {α : Type*} [MeasurableSpace α] {μ : Measure α} + +/-- If a real function exceeds `a` on a set of positive measure, then it is at least some `c > a` +on a set of positive measure. The function need not be measurable. -/ +theorem exists_gt_measure_setOf_le_ne_zero {f : α → ℝ} {a : ℝ} (h : μ {x | a < f x} ≠ 0) : + ∃ c, a < c ∧ μ {x | c ≤ f x} ≠ 0 := by + by_contra! h' + refine h ?_ + have : {x | a < f x} = ⋃ n : ℕ, {x | a + 1 / ((n : ℝ) + 1) ≤ f x} := by + ext x + simp only [mem_ofPred_eq, mem_iUnion] + constructor + · intro hx + obtain ⟨n, hn⟩ := exists_nat_one_div_lt (sub_pos.2 hx) + exact ⟨n, by linarith⟩ + · rintro ⟨n, hn⟩ + have : 0 < 1 / ((n : ℝ) + 1) := by positivity + linarith + rw [this] + exact measure_iUnion_null fun n ↦ h' _ (lt_add_of_pos_right a (by positivity)) + +end MeasureTheory From 47fb2c76f2e75599aeafb3c852bb0dd9d86de51b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 16:14:14 +0100 Subject: [PATCH 4/6] refactor: name the damped density and drop "strong duality" from the one-sided bound Introduce the private `dampedDensity` with its measurability and positivity, and state the four lemmas on the damped reverse information projection in terms of it. Replace the definitional-unfolding steps (`rfl`, `show`) with explicit `simp`, split the two long rewrite chains into named steps, and retitle the one-sided inequality, its section and its private bound so that they no longer claim strong duality. Co-Authored-By: Claude Code --- LMLExplore/EValues/ConstraintNull/KLInf.lean | 109 +++++++++++-------- 1 file changed, 62 insertions(+), 47 deletions(-) diff --git a/LMLExplore/EValues/ConstraintNull/KLInf.lean b/LMLExplore/EValues/ConstraintNull/KLInf.lean index 2f608097..1ad932f4 100644 --- a/LMLExplore/EValues/ConstraintNull/KLInf.lean +++ b/LMLExplore/EValues/ConstraintNull/KLInf.lean @@ -182,11 +182,12 @@ theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g (integrable_dirac' hf.stronglyMeasurable (by simp)).smul_measure ENNReal.ofReal_ne_top refine mem_constraintNull_range_iff.2 ⟨⟨?_⟩, fun i ↦ ?_⟩ · simp only [add_apply, sum_apply, smul_apply, measure_univ, smul_eq_mul, mul_one] - rw [← ENNReal.ofReal_sum_of_nonneg fun k _ ↦ mul_nonneg hm0.le (hw0 k), ← Finset.mul_sum, - hw1, mul_one, ← ENNReal.ofReal_toReal (measure_ne_top μ univ), - ← ENNReal.ofReal_add ENNReal.toReal_nonneg hm0.le] - rw [← measureReal_def, ← hr_def, hm_def] - simp + -- the added mass is `m = 1 - r`, the mass that `μ` lacks + have hmass : ∑ k, ENNReal.ofReal (m * w k) = ENNReal.ofReal m := by + rw [← ENNReal.ofReal_sum_of_nonneg fun k _ ↦ mul_nonneg hm0.le (hw0 k), ← Finset.mul_sum, + hw1, mul_one] + rw [hmass, ← ofReal_measureReal, ← hr_def, ← ENNReal.ofReal_add measureReal_nonneg hm0.le, + hm_def, add_sub_cancel, ENNReal.ofReal_one] · refine ⟨(hgμ i).add_measure (integrable_finsetSum_measure.2 (hdirac _ (hg i))), ?_⟩ rw [integral_add_measure (hgμ i) (integrable_finsetSum_measure.2 (hdirac _ (hg i))), integral_finsetSum_measure (hdirac _ (hg i))] @@ -204,17 +205,34 @@ theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g /-! ### The damped reverse information projection -/ +/-- The density with respect to `Q` of the reverse information projection `Q / E` damped by +`1 + δ ∑ i, |g i|` and scaled by `1 - ε`: `x ↦ (1 - ε) / (E x * (1 + δ ∑ i, |g i x|))`. -/ +private noncomputable def dampedDensity (E : 𝓧 → ℝ≥0∞) (g : ι → 𝓧 → ℝ) (δ ε : ℝ) (x : 𝓧) : + ℝ≥0∞ := + (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) + +private lemma measurable_dampedDensity {E : 𝓧 → ℝ≥0∞} (hE : Measurable E) + (hg : ∀ i, Measurable (g i)) (δ ε : ℝ) : Measurable (dampedDensity E g δ ε) := by + unfold dampedDensity + fun_prop + +omit [MeasurableSpace 𝓧] in +private lemma dampedDensity_ne_zero {E : 𝓧 → ℝ≥0∞} {δ ε : ℝ} (hδ : 0 ≤ δ) (hε1 : ε < 1) {x : 𝓧} + (hx : E x ≠ ∞) : dampedDensity E g δ ε x ≠ 0 := by + simp only [dampedDensity, ne_eq, mul_eq_zero, ENNReal.inv_eq_zero, hx, ENNReal.ofReal_eq_zero, + not_le, false_or] + exact div_pos (by linarith) (by positivity) + /-- The reverse information projection `Q / E` damped by `1 + δ ∑ i, |g i|` and scaled by `1 - ε` integrates the constraints, as soon as `∫ 1 / E ∂Q` is finite. -/ private lemma integrable_withDensity_inv_mul_ofReal_div {E : 𝓧 → ℝ≥0∞} (hE : Measurable E) (hg : ∀ i, Measurable (g i)) (hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≠ ∞) {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 ≤ ε) (hε1 : ε ≤ 1) (i : ι) : - Integrable (g i) - (Q.withDensity fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) := by + Integrable (g i) (Q.withDensity (dampedDensity E g δ ε)) := by refine ⟨(hg i).aestronglyMeasurable, ?_⟩ - rw [HasFiniteIntegral, lintegral_withDensity_eq_lintegral_mul _ (by fun_prop) (by fun_prop)] - calc ∫⁻ x, ((fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) * - fun x ↦ ‖g i x‖ₑ) x ∂Q + rw [HasFiniteIntegral, lintegral_withDensity_eq_lintegral_mul _ + (measurable_dampedDensity hE hg δ ε) (by fun_prop)] + calc ∫⁻ x, (dampedDensity E g δ ε * fun x ↦ ‖g i x‖ₑ) x ∂Q ≤ ∫⁻ x, ENNReal.ofReal (1 / δ) * (E x)⁻¹ ∂Q := by refine lintegral_mono fun x ↦ ?_ have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by positivity @@ -227,10 +245,9 @@ private lemma integrable_withDensity_inv_mul_ofReal_div {E : 𝓧 → ℝ≥0∞ nlinarith [mul_nonneg (mul_nonneg hε hδ.le) (abs_nonneg (g i x))] have h3 : δ * |g i x| ≤ δ * ∑ j, |g j x| := mul_le_mul_of_nonneg_left hgi hδ.le linarith - calc ((fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) * - fun x ↦ ‖g i x‖ₑ) x + calc (dampedDensity E g δ ε * fun x ↦ ‖g i x‖ₑ) x = (E x)⁻¹ * (ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) * ‖g i x‖ₑ) := by - simp only [Pi.mul_apply, mul_assoc] + simp only [Pi.mul_apply, dampedDensity, mul_assoc] _ = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|) * |g i x|) := by rw [Real.eNorm_eq_ofReal_abs, ← ENNReal.ofReal_mul (div_nonneg (by linarith) hh0.le)] @@ -244,15 +261,16 @@ private lemma integrable_withDensity_inv_mul_ofReal_div {E : 𝓧 → ℝ≥0∞ `1 - ε` times its mean divided by `E` under `Q`. -/ private lemma lintegral_withDensity_inv_mul_ofReal_div_le {E F : 𝓧 → ℝ≥0∞} (hE : Measurable E) (hF : Measurable F) (hg : ∀ i, Measurable (g i)) {δ ε : ℝ} (hδ : 0 ≤ δ) (hε1 : ε ≤ 1) : - ∫⁻ x, F x ∂(Q.withDensity fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) + ∫⁻ x, F x ∂(Q.withDensity (dampedDensity E g δ ε)) ≤ ENNReal.ofReal (1 - ε) * ∫⁻ x, F x / E x ∂Q := by - rw [lintegral_withDensity_eq_lintegral_mul _ (by fun_prop) hF, + rw [lintegral_withDensity_eq_lintegral_mul _ (measurable_dampedDensity hE hg δ ε) hF, ← lintegral_const_mul' _ _ ENNReal.ofReal_ne_top] refine lintegral_mono fun x ↦ ?_ have : ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) ≤ ENNReal.ofReal (1 - ε) := ENNReal.ofReal_le_ofReal (div_le_self (by linarith) (le_add_of_nonneg_right (by positivity))) - calc ((fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))) * F) x - = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) * F x := rfl + calc (dampedDensity E g δ ε * F) x + = (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)) * F x := by + simp only [Pi.mul_apply, dampedDensity] _ ≤ (E x)⁻¹ * ENNReal.ofReal (1 - ε) * F x := by gcongr _ = ENNReal.ofReal (1 - ε) * (F x / E x) := by rw [div_eq_mul_inv]; ring @@ -261,18 +279,19 @@ projection is `log E + log (1 + δ ∑ i, |g i|) - log (1 - ε)`, `Q`-almost eve private lemma log_inv_rnDeriv_withDensity_inv_mul_ofReal_div [SigmaFinite Q] {E : 𝓧 → ℝ≥0∞} (hE : Measurable E) (hg : ∀ i, Measurable (g i)) {δ ε : ℝ} (hδ : 0 ≤ δ) (hε1 : ε < 1) : - ∀ᵐ x ∂Q, ENNReal.log (((Q.withDensity fun x ↦ - (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|))).rnDeriv Q)⁻¹ x) = + ∀ᵐ x ∂Q, ENNReal.log (((Q.withDensity (dampedDensity E g δ ε)).rnDeriv Q)⁻¹ x) = ENNReal.log (E x) + ((Real.log (1 + δ * ∑ j, |g j x|) - Real.log (1 - ε) : ℝ) : EReal) := by - filter_upwards [Measure.rnDeriv_withDensity Q (by fun_prop : Measurable fun x ↦ - (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ j, |g j x|)))] with x hx + filter_upwards [Measure.rnDeriv_withDensity Q (measurable_dampedDensity hE hg δ ε)] with x hx have hh0 : 0 < 1 + δ * ∑ j, |g j x| := by positivity have hpos : 0 < (1 - ε) / (1 + δ * ∑ j, |g j x|) := div_pos (by linarith) hh0 - rw [Pi.inv_apply, hx] - rw [ENNReal.mul_inv (Or.inr ENNReal.ofReal_ne_top) (Or.inr (ENNReal.ofReal_pos.2 hpos).ne'), - inv_inv, ENNReal.log_mul_add, ← ENNReal.ofReal_inv_of_pos hpos, - ENNReal.log_ofReal_of_pos (inv_pos.2 hpos), inv_div, Real.log_div hh0.ne' (by linarith)] + -- the likelihood ratio is `E x * (1 + δ ∑ j, |g j x|) / (1 - ε)` + have hinv : (dampedDensity E g δ ε x)⁻¹ = + E x * ENNReal.ofReal ((1 + δ * ∑ j, |g j x|) / (1 - ε)) := by + rw [dampedDensity, ENNReal.mul_inv (.inr ENNReal.ofReal_ne_top) + (.inr (ENNReal.ofReal_pos.2 hpos).ne'), inv_inv, ← ENNReal.ofReal_inv_of_pos hpos, inv_div] + rw [Pi.inv_apply, hx, hinv, ENNReal.log_mul_add, + ENNReal.log_ofReal_of_pos (div_pos hh0 (by linarith)), Real.log_div hh0.ne' (by linarith)] /-- **Completion of the damped reverse information projection**: when `Q` is carried by a set `Y` without arbitrage that carries the null, and `E` is such that `∫ F / E ∂Q ≤ 1` for every @@ -286,14 +305,14 @@ private lemma exists_withDensity_inv_mul_ofReal_div_add_sum_smul_dirac_mem_const (hEF : ∀ F, IsEVar F (constraintNull (range g)) → ∫⁻ x, F x / E x ∂Q ≤ 1) {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) (hε1 : ε < 1) : ∃ (α : Type) (_ : Fintype α) (x : α → 𝓧) (w : α → ℝ), - Q.withDensity (fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ i, |g i x|))) + + Q.withDensity (dampedDensity E g δ ε) + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) ∈ constraintNull (range g) := by have hYne : Y.Nonempty := by by_contra h rw [not_nonempty_iff_eq_empty] at h simp [h] at hQY have hEinv : ∫⁻ x, (E x)⁻¹ ∂Q ≤ 1 := by simpa using hEF 1 (isEVar_one _) - set μ := Q.withDensity fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ i, |g i x|)) + set μ := Q.withDensity (dampedDensity E g δ ε) have hμE : ∀ F, IsEVar F (constraintNull (range g)) → ∫⁻ x, F x ∂μ ≤ ENNReal.ofReal (1 - ε) := fun F hF ↦ (lintegral_withDensity_inv_mul_ofReal_div_le hE hF.measurable hg hδ.le hε1.le).trans @@ -306,14 +325,14 @@ private lemma exists_withDensity_inv_mul_ofReal_div_add_sum_smul_dirac_mem_const hε.le hε1.le) (ENNReal.ofReal_lt_one.2 (by linarith)) hμE exact ⟨α, inferInstance, x, w, hP⟩ -/-! ### Strong duality on a set without arbitrage -/ +/-! ### The nontrivial inequality of the dual formula, on a set without arbitrage -/ -/-- The bound of strong duality for a damping `δ` and a slack `ε`: when `Q` is carried by a set -`Y` without arbitrage that carries the null, and the largest expected logarithm `s` of an -e-variable is finite, the reverse information projection `Q / E`, for the numeraire `E`, damped by -`1 + δ ∑ i, |g i|` so that it integrates the constraints, and scaled by `1 - ε`, is completed into -a member of the null by a finitely supported measure, at a relative entropy at most -`s + E_Q[log (1 + δ ∑ i, |g i|)] - log (1 - ε)`. -/ +/-- The nontrivial inequality of the dual formula, up to a damping `δ` and a slack `ε`: when `Q` +is carried by a set `Y` without arbitrage that carries the null, and the largest expected +logarithm `s` of an e-variable is finite, the reverse information projection `Q / E`, for the +numeraire `E`, damped by `1 + δ ∑ i, |g i|` so that it integrates the constraints, and scaled by +`1 - ε`, is completed into a member of the null by a finitely supported measure, at a relative +entropy at most `s + E_Q[log (1 + δ ∑ i, |g i|)] - log (1 - ε)`. -/ private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurable (g i)) (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) [IsProbabilityMeasure Q] (hQY : Q Yᶜ = 0) @@ -339,10 +358,7 @@ private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurabl obtain ⟨α, _, x, w, hP⟩ := exists_withDensity_inv_mul_ofReal_div_add_sum_smul_dirac_mem_constraintNull hg hY hYμ hQY hEm (fun F hF ↦ hEnum.lintegral_div_le_one hF) hδ hε hε1 - set d : 𝓧 → ℝ≥0∞ := fun x ↦ (E x)⁻¹ * ENNReal.ofReal ((1 - ε) / (1 + δ * ∑ i, |g i x|)) - with hd_def - have hd : Measurable d := by fun_prop - set μ := Q.withDensity d with hμ_def + set μ := Q.withDensity (dampedDensity E g δ ε) with hμ_def set P := μ + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) with hP_def have := isProbabilityMeasure_of_mem_constraintNull hP have hμP : μ ≤ P := Measure.le_add_right le_rfl @@ -353,12 +369,9 @@ private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurabl calc ∫⁻ x, X x ∂μ ≤ ∫⁻ x, X x ∂P := lintegral_mono' hμP le_rfl _ ≤ P univ := hX.lintegral_le_measure_univ P rfl _ = 1 := measure_univ - have hdpos : ∀ x, E x ≠ ∞ → d x ≠ 0 := fun x hx ↦ by - simp only [d, ne_eq, mul_eq_zero, ENNReal.inv_eq_zero, hx, ENNReal.ofReal_eq_zero, - not_le, false_or] - exact div_pos (by linarith) (by positivity) - have hac : Q ≪ μ := withDensity_absolutelyContinuous' hd.aemeasurable - (by filter_upwards [hE_top] with x hx using hdpos x hx) + have hac : Q ≪ μ := withDensity_absolutelyContinuous' + (measurable_dampedDensity hEm hg δ ε).aemeasurable + (by filter_upwards [hE_top] with x hx using dampedDensity_ne_zero hδ.le hε1 hx) have hlogh0 : Integrable (fun x ↦ Real.log (1 + δ * ∑ i, |g i x|)) Q := hQ.log_one_add_const_mul (by fun_prop) (fun x ↦ by positivity) hδ.le hδ1 have hlogh : Integrable @@ -380,7 +393,8 @@ private lemma iInf_klDiv_constraintNull_le_maxUtility_add (hg : ∀ i, Measurabl (.inr hI_top) (.inr hI_bot), hI, ← hsE, integral_sub hlogh0 (integrable_const _)] simp -/-- **Strong duality on a set without arbitrage**: when `Q` is carried by a set `Y` without +/-- **The smallest relative entropy is at most the largest expected logarithm, on a set without +arbitrage**: when `Q` is carried by a set `Y` without arbitrage that carries the null, and `log (1 + ∑ i, |g i|)` is `Q`-integrable, the smallest relative entropy from `Q` to the null is at most the largest expected logarithm of an e-variable. -/ @@ -493,9 +507,10 @@ theorem iSup_eintegral_log_ofReal_one_add_eq_top (hg : ∀ i, Measurable (g i)) have h1 : 0 < 1 + t * ∑ i, ρ i * g i x := by nlinarith rw [ENNReal.log_ofReal_of_pos h1] by_cases hxA : x ∈ A - · rw [indicator_of_mem hxA, EReal.coe_ennreal_ofReal, max_eq_left hlc, + · have hcx : c ≤ ∑ i, ρ i * g i x := by simpa [hA_def] using hxA + rw [indicator_of_mem hxA, EReal.coe_ennreal_ofReal, max_eq_left hlc, EReal.coe_le_coe_iff] - exact Real.log_le_log (by nlinarith) (by nlinarith [show c ≤ _ from hxA]) + exact Real.log_le_log (by nlinarith) (by nlinarith [hcx]) · rw [indicator_of_notMem hxA, EReal.coe_ennreal_zero, ← EReal.coe_zero, EReal.coe_le_coe_iff] exact Real.log_nonneg (by nlinarith) From 3f2b591a96b5d4ed92070f17768c988ed7a36efd Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 16:38:47 +0100 Subject: [PATCH 5/6] refactor: reuse integral_sum_smul_dirac and move abs_log_one_add_mul_le to the log bounds file Co-Authored-By: Claude Code --- .../SpecialFunctions/Integrability/PosLog.lean | 14 +------------- .../Analysis/SpecialFunctions/Log/Basic.lean | 9 +++++++++ LMLExplore/EValues/ConstraintNull/KLInf.lean | 5 ++--- 3 files changed, 12 insertions(+), 16 deletions(-) diff --git a/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean b/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean index cf5fdc65..74c50198 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.SpecialFunctions.Log.PosLog public import Mathlib.MeasureTheory.Function.L1Space.Integrable public import Mathlib.MeasureTheory.Integral.Bochner.Basic +import LMLExplore.Analysis.SpecialFunctions.Log.Basic import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic import Mathlib.MeasureTheory.Integral.DominatedConvergence @@ -21,7 +22,6 @@ logarithm, by dominated convergence. ## Main statements -* `Real.abs_log_one_add_mul_le`: `|log (1 + δ t)| ≤ log (1 + t)` for `t ≥ 0` and `δ ∈ [0, 1]`. * `MeasureTheory.integrable_log_one_add_sum_abs`: if every `log⁺ (f i)` is integrable under a finite measure, so is `log (1 + ∑ i, |f i|)`. * `MeasureTheory.Integrable.log_one_add_const_mul`: if `log (1 + f)` is integrable for a @@ -34,18 +34,6 @@ public section open MeasureTheory Filter Topology -namespace Real - -/-- Damping by a factor `δ ∈ [0, 1]` decreases `log (1 + t)`, for `t ≥ 0`, and keeps it -nonnegative. -/ -theorem abs_log_one_add_mul_le {δ t : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (ht : 0 ≤ t) : - |log (1 + δ * t)| ≤ log (1 + t) := by - have h0 : 0 ≤ δ * t := mul_nonneg hδ ht - rw [abs_of_nonneg (log_nonneg (by linarith))] - exact log_le_log (by linarith) (by nlinarith) - -end Real - namespace MeasureTheory variable {α ι : Type*} [MeasurableSpace α] {μ : Measure α} diff --git a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean index 01d032c0..02e0c2c6 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean @@ -67,6 +67,7 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv RF-Express [MDJKLV21]. * `Real.sum_div_max_one_le_four_mul_log`: the form of [MDJKLV21, Lemma 9], for `u k ∈ [0, 1]` and with the constant `4`. +* `Real.abs_log_one_add_mul_le`: `|log (1 + δ t)| ≤ log (1 + t)` for `t ≥ 0` and `δ ∈ [0, 1]`. * `Real.tendsto_sub_one_sub_log_atTop`, `Real.tendsto_sub_one_sub_log_nhdsGT_zero`: `t - 1 - log t → ∞` as `t → ∞` and as `t → 0⁺`. The divergences of the Poisson and gamma families are multiples of this function of a ratio of means. @@ -674,4 +675,12 @@ theorem tendsto_sub_one_sub_log_nhdsGT_zero : simp only [Function.comp_apply] linarith +/-- Damping by a factor `δ ∈ [0, 1]` decreases `log (1 + t)`, for `t ≥ 0`, and keeps it +nonnegative. -/ +theorem abs_log_one_add_mul_le {δ t : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (ht : 0 ≤ t) : + |log (1 + δ * t)| ≤ log (1 + t) := by + have h0 : 0 ≤ δ * t := mul_nonneg hδ ht + rw [abs_of_nonneg (log_nonneg (by linarith))] + exact log_le_log (by linarith) (by nlinarith) + end Real diff --git a/LMLExplore/EValues/ConstraintNull/KLInf.lean b/LMLExplore/EValues/ConstraintNull/KLInf.lean index 1ad932f4..9918558e 100644 --- a/LMLExplore/EValues/ConstraintNull/KLInf.lean +++ b/LMLExplore/EValues/ConstraintNull/KLInf.lean @@ -190,9 +190,8 @@ theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g hm_def, add_sub_cancel, ENNReal.ofReal_one] · refine ⟨(hgμ i).add_measure (integrable_finsetSum_measure.2 (hdirac _ (hg i))), ?_⟩ rw [integral_add_measure (hgμ i) (integrable_finsetSum_measure.2 (hdirac _ (hg i))), - integral_finsetSum_measure (hdirac _ (hg i))] - simp_rw [integral_smul_measure, integral_dirac' _ _ (hg i).stronglyMeasurable, - ENNReal.toReal_ofReal (mul_nonneg hm0.le (hw0 _)), smul_eq_mul] + integral_sum_smul_dirac (fun k ↦ mul_nonneg hm0.le (hw0 k)) (hg i).stronglyMeasurable] + simp_rw [smul_eq_mul] have h1 := hwz i simp only [mul_add, Finset.sum_add_distrib, ← Finset.sum_mul, hw1, one_mul] at h1 have h2 : ∑ k, m * w k * g i (x k) = m * ∑ k, w k * g i (x k) := by From 8aababa705b3385576c375c88bdbf0ec91960d7e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 17:00:55 +0100 Subject: [PATCH 6/6] refactor: move the completion into a member of the null to the complete class file The two completion lemmas use only the constraint-null and complete class API, so they now sit in CompleteClass.lean, listed in its main statements. Co-Authored-By: Claude Code --- .../EValues/ConstraintNull/CompleteClass.lean | 127 ++++++++++++++++++ LMLExplore/EValues/ConstraintNull/KLInf.lean | 124 ----------------- 2 files changed, 127 insertions(+), 124 deletions(-) diff --git a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean index 8ee1cbb8..c4240ea4 100644 --- a/LMLExplore/EValues/ConstraintNull/CompleteClass.lean +++ b/LMLExplore/EValues/ConstraintNull/CompleteClass.lean @@ -79,9 +79,16 @@ supported member of the null, so that e-variables are finite on `Y`. `ProbabilityTheory.isEVar_constraintNull_iff`: the complete class theorem for e-variables [LRR26, Theorem 3.1]: every e-variable is dominated by a bet, on a set without arbitrage that carries the null, and almost surely under every member of the null. +* `ProbabilityTheory.noArbitrageOn_add_integral_div_of_lintegral_le`, + `ProbabilityTheory.exists_add_sum_smul_dirac_mem_constraintNull`: on a nonempty set without + arbitrage that carries the null, a finite measure carried by that set that integrates the + constraints and under which every e-variable has mean at most `c < 1` is completed into a member + of the null by a finitely supported measure [EVR26, Note 20]. ## References +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, notes 01–34 and the + Lean library EValuesResearch, github.com/RemyDegenne/evalues_research (2026). * [LRR26] M. Larsson, A. Ramdas and J. Ruf, *Testing hypotheses generated by constraints*, Math. Oper. Res. (2026), arXiv:2504.02974v5. -/ @@ -636,4 +643,124 @@ theorem isEVar_constraintNull_iff (hg : ∀ i, Measurable (g i)) : fun μ hμ ↦ (lintegral_mono_ae (hEπ μ hμ)).trans (lintegral_ofReal_one_add_le_one_of_mem_constraintBets hπ hμ)⟩ +/-! ### Completion into a member of the null -/ + +/-- **The shifted constraints admit no arbitrage**: on a set `Y` without arbitrage that carries +the null, let `μ` be a finite measure carried by `Y` that integrates the constraints and under +which every e-variable has mean at most `c`, for some `c < 1`. Then the constraints shifted by +their means under `μ` divided by the mass `1 - μ 𝓧` that `μ` lacks, +`g i + (∫ g i ∂μ) / (1 - μ 𝓧)`, admit no arbitrage on `Y`. -/ +theorem noArbitrageOn_add_integral_div_of_lintegral_le (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) + {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) (hgμ : ∀ i, Integrable (g i) μ) + {c : ℝ≥0∞} (hc : c < 1) + (hμE : ∀ E, IsEVar E (constraintNull (range g)) → ∫⁻ x, E x ∂μ ≤ c) : + NoArbitrageOn (fun i x ↦ g i x + (∫ y, g i y ∂μ) / (1 - μ.real univ)) Y := by + set m := 1 - μ.real univ with hm_def + refine noArbitrageOn_iff.2 fun π hπ hπY ↦ ?_ + set σ := (∑ i, π i * ∫ x, g i x ∂μ) / m with hσ_def + have hσa : ∑ i, π i * ((∫ x, g i x ∂μ) / m) = σ := by + simp only [hσ_def, Finset.sum_div, mul_div_assoc] + have hπg : ∀ x ∈ Y, -σ ≤ ∑ i, π i * g i x := by + intro x hx + have := hπY x hx + simp only [mul_add, Finset.sum_add_distrib, hσa] at this + linarith + rcases lt_or_ge 0 σ with hσ | hσ + · -- a positive deficit would be paid by the mass that `μ` lacks: the bet with weights `π / σ` + -- would have mean `1` under `μ` + exfalso + have hsum : ∀ x, ∑ i, π i / σ * g i x = (∑ i, π i * g i x) / σ := fun x ↦ by + simp only [Finset.sum_div, div_mul_eq_mul_div] + have hEY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i / σ * g i x := by + intro x hx + rw [hsum] + have : -1 ≤ (∑ i, π i * g i x) / σ := by + rw [le_div_iff₀ hσ] + linarith [hπg x hx] + linarith + have hcoe : ∀ i, ((π i / σ).toNNReal : ℝ) = π i / σ := fun i ↦ + Real.coe_toNNReal _ (div_nonneg (hπ i) hσ.le) + have h1 := hμE _ (isEVar_ofReal_one_add_of_mem_constraintBets hg + (toNNReal_mem_constraintBets hYμ (fun i ↦ div_nonneg (hπ i) hσ.le) hEY)) + simp only [hcoe] at h1 + rw [lintegral_ofReal_one_add_sum_mul hgμ _ + (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hEY)] at h1 + have h2 : ∑ i, π i / σ * ∫ x, g i x ∂μ = m := by + have : ∑ i, π i / σ * ∫ x, g i x ∂μ = (∑ i, π i * ∫ x, g i x ∂μ) / σ := by + simp only [Finset.sum_div, div_mul_eq_mul_div] + rw [this, hσ_def, div_div_cancel₀ (by + intro h0 + rw [h0, zero_div] at hσ_def + exact hσ.ne' hσ_def)] + rw [h2, hm_def, add_sub_cancel, ENNReal.ofReal_one] at h1 + exact lt_irrefl _ (h1.trans_lt hc) + · -- no deficit: the combination is nonnegative, hence zero, on `Y` + have h0 : ∀ x ∈ Y, 0 ≤ ∑ i, π i * g i x := fun x hx ↦ by linarith [hπg x hx] + have hzero := noArbitrageOn_iff.1 hY π hπ h0 + have hb : ∑ i, π i * ∫ x, g i x ∂μ = 0 := by + have hgi : ∀ i, Integrable (fun x ↦ π i * g i x) μ := fun i ↦ (hgμ i).const_mul (π i) + simp_rw [← integral_const_mul] + rw [← integral_finsetSum _ fun i _ ↦ hgi i] + exact integral_eq_zero_of_ae (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hzero) + have hσ0 : σ = 0 := by rw [hσ_def, hb, zero_div] + intro x hx + simp only [mul_add, Finset.sum_add_distrib, hσa, hσ0, add_zero] + exact hzero x hx + +/-- **Completion by a finitely supported measure**: on a nonempty set `Y` without arbitrage that +carries the null, a finite measure carried by `Y` that integrates the constraints and under which +every e-variable has mean at most `c`, for some `c < 1`, becomes a member of the null once a +finitely supported measure is added. It rests on the complete class theorem [LRR26, Theorem 3.1], +and follows [EVR26, Note 20]. -/ +theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g i)) + (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) + (hYne : Y.Nonempty) {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) + (hgμ : ∀ i, Integrable (g i) μ) {c : ℝ≥0∞} (hc : c < 1) + (hμE : ∀ E, IsEVar E (constraintNull (range g)) → ∫⁻ x, E x ∂μ ≤ c) : + ∃ (α : Type) (_ : Fintype α) (x : α → 𝓧) (w : α → ℝ), (∀ k, 0 ≤ w k) ∧ + μ + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) ∈ constraintNull (range g) := by + classical + set r := μ.real univ with hr_def + set m := 1 - r with hm_def + have hm0 : 0 < m := by + have h1 := hμE 1 (isEVar_one _) + simp only [Pi.one_apply, lintegral_one] at h1 + have h2 : r < 1 := by + rw [hr_def, measureReal_def] + exact ENNReal.toReal_lt_of_lt_ofReal (by simpa using h1.trans_lt hc) + linarith + -- the complete class theorem, applied to the constraints shifted by multiples of their means + -- under `μ`, gives a finitely supported law under which the shifted constraints have + -- nonpositive means + obtain ⟨x₀, hx₀⟩ := hYne + obtain ⟨α, _, x, w, -, hw, hwz, -⟩ := exists_charging_family_of_noArbitrageOn + (noArbitrageOn_add_integral_div_of_lintegral_le hg hY hYμ hμY hgμ hc hμE) hx₀ + obtain ⟨hw0, hw1⟩ := mem_simplex_iff.1 hw + refine ⟨α, inferInstance, x, fun k ↦ m * w k, fun k ↦ mul_nonneg hm0.le (hw0 k), ?_⟩ + have hdirac : ∀ (f : 𝓧 → ℝ), Measurable f → ∀ k ∈ Finset.univ, + Integrable f (ENNReal.ofReal (m * w k) • Measure.dirac (x k)) := fun f hf k _ ↦ + (integrable_dirac' hf.stronglyMeasurable (by simp)).smul_measure ENNReal.ofReal_ne_top + refine mem_constraintNull_range_iff.2 ⟨⟨?_⟩, fun i ↦ ?_⟩ + · simp only [add_apply, sum_apply, smul_apply, measure_univ, smul_eq_mul, mul_one] + -- the added mass is `m = 1 - r`, the mass that `μ` lacks + have hmass : ∑ k, ENNReal.ofReal (m * w k) = ENNReal.ofReal m := by + rw [← ENNReal.ofReal_sum_of_nonneg fun k _ ↦ mul_nonneg hm0.le (hw0 k), ← Finset.mul_sum, + hw1, mul_one] + rw [hmass, ← ofReal_measureReal, ← hr_def, ← ENNReal.ofReal_add measureReal_nonneg hm0.le, + hm_def, add_sub_cancel, ENNReal.ofReal_one] + · refine ⟨(hgμ i).add_measure (integrable_finsetSum_measure.2 (hdirac _ (hg i))), ?_⟩ + rw [integral_add_measure (hgμ i) (integrable_finsetSum_measure.2 (hdirac _ (hg i))), + integral_sum_smul_dirac (fun k ↦ mul_nonneg hm0.le (hw0 k)) (hg i).stronglyMeasurable] + simp_rw [smul_eq_mul] + have h1 := hwz i + simp only [mul_add, Finset.sum_add_distrib, ← Finset.sum_mul, hw1, one_mul] at h1 + have h2 : ∑ k, m * w k * g i (x k) = m * ∑ k, w k * g i (x k) := by + rw [Finset.mul_sum] + exact Finset.sum_congr rfl fun k _ ↦ by ring + have h3 : m * ((∫ x, g i x ∂μ) / m) = ∫ x, g i x ∂μ := by + field_simp + rw [h2] + nlinarith + end ProbabilityTheory diff --git a/LMLExplore/EValues/ConstraintNull/KLInf.lean b/LMLExplore/EValues/ConstraintNull/KLInf.lean index 9918558e..720cfc4c 100644 --- a/LMLExplore/EValues/ConstraintNull/KLInf.lean +++ b/LMLExplore/EValues/ConstraintNull/KLInf.lean @@ -55,10 +55,6 @@ logarithm of an e-variable, which Statlib's numeraire [LRR25] attains, and split * `ProbabilityTheory.iInf_klDiv_constraintNull_eq_maxUtility`: the smallest relative entropy to the null is the largest expected logarithm of an e-variable. * `ProbabilityTheory.iInf_klDiv_constraintNull_eq_iSup_eintegral_log`: **the dual formula**. -* `ProbabilityTheory.exists_add_sum_smul_dirac_mem_constraintNull`: on a nonempty set without - arbitrage that carries the null, a finite measure carried by that set that integrates the - constraints and under which every e-variable has mean at most `c < 1` is completed into a member - of the null by a finitely supported measure. ## References @@ -82,126 +78,6 @@ namespace ProbabilityTheory variable {𝓧 ι : Type*} [Fintype ι] [MeasurableSpace 𝓧] {g : ι → 𝓧 → ℝ} {Y : Set 𝓧} {Q : Measure 𝓧} -/-! ### Completion into a member of the null -/ - -/-- **The shifted constraints admit no arbitrage**: on a set `Y` without arbitrage that carries -the null, let `μ` be a finite measure carried by `Y` that integrates the constraints and under -which every e-variable has mean at most `c`, for some `c < 1`. Then the constraints shifted by -their means under `μ` divided by the mass `1 - μ 𝓧` that `μ` lacks, -`g i + (∫ g i ∂μ) / (1 - μ 𝓧)`, admit no arbitrage on `Y`. -/ -theorem noArbitrageOn_add_integral_div_of_lintegral_le (hg : ∀ i, Measurable (g i)) - (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) - {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) (hgμ : ∀ i, Integrable (g i) μ) - {c : ℝ≥0∞} (hc : c < 1) - (hμE : ∀ E, IsEVar E (constraintNull (range g)) → ∫⁻ x, E x ∂μ ≤ c) : - NoArbitrageOn (fun i x ↦ g i x + (∫ y, g i y ∂μ) / (1 - μ.real univ)) Y := by - set m := 1 - μ.real univ with hm_def - refine noArbitrageOn_iff.2 fun π hπ hπY ↦ ?_ - set σ := (∑ i, π i * ∫ x, g i x ∂μ) / m with hσ_def - have hσa : ∑ i, π i * ((∫ x, g i x ∂μ) / m) = σ := by - simp only [hσ_def, Finset.sum_div, mul_div_assoc] - have hπg : ∀ x ∈ Y, -σ ≤ ∑ i, π i * g i x := by - intro x hx - have := hπY x hx - simp only [mul_add, Finset.sum_add_distrib, hσa] at this - linarith - rcases lt_or_ge 0 σ with hσ | hσ - · -- a positive deficit would be paid by the mass that `μ` lacks: the bet with weights `π / σ` - -- would have mean `1` under `μ` - exfalso - have hsum : ∀ x, ∑ i, π i / σ * g i x = (∑ i, π i * g i x) / σ := fun x ↦ by - simp only [Finset.sum_div, div_mul_eq_mul_div] - have hEY : ∀ x ∈ Y, 0 ≤ 1 + ∑ i, π i / σ * g i x := by - intro x hx - rw [hsum] - have : -1 ≤ (∑ i, π i * g i x) / σ := by - rw [le_div_iff₀ hσ] - linarith [hπg x hx] - linarith - have hcoe : ∀ i, ((π i / σ).toNNReal : ℝ) = π i / σ := fun i ↦ - Real.coe_toNNReal _ (div_nonneg (hπ i) hσ.le) - have h1 := hμE _ (isEVar_ofReal_one_add_of_mem_constraintBets hg - (toNNReal_mem_constraintBets hYμ (fun i ↦ div_nonneg (hπ i) hσ.le) hEY)) - simp only [hcoe] at h1 - rw [lintegral_ofReal_one_add_sum_mul hgμ _ - (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hEY)] at h1 - have h2 : ∑ i, π i / σ * ∫ x, g i x ∂μ = m := by - have : ∑ i, π i / σ * ∫ x, g i x ∂μ = (∑ i, π i * ∫ x, g i x ∂μ) / σ := by - simp only [Finset.sum_div, div_mul_eq_mul_div] - rw [this, hσ_def, div_div_cancel₀ (by - intro h0 - rw [h0, zero_div] at hσ_def - exact hσ.ne' hσ_def)] - rw [h2, hm_def, add_sub_cancel, ENNReal.ofReal_one] at h1 - exact lt_irrefl _ (h1.trans_lt hc) - · -- no deficit: the combination is nonnegative, hence zero, on `Y` - have h0 : ∀ x ∈ Y, 0 ≤ ∑ i, π i * g i x := fun x hx ↦ by linarith [hπg x hx] - have hzero := noArbitrageOn_iff.1 hY π hπ h0 - have hb : ∑ i, π i * ∫ x, g i x ∂μ = 0 := by - have hgi : ∀ i, Integrable (fun x ↦ π i * g i x) μ := fun i ↦ (hgμ i).const_mul (π i) - simp_rw [← integral_const_mul] - rw [← integral_finsetSum _ fun i _ ↦ hgi i] - exact integral_eq_zero_of_ae (Filter.eventually_of_mem (mem_ae_iff.2 hμY) hzero) - have hσ0 : σ = 0 := by rw [hσ_def, hb, zero_div] - intro x hx - simp only [mul_add, Finset.sum_add_distrib, hσa, hσ0, add_zero] - exact hzero x hx - -/-- **Completion by a finitely supported measure**: on a nonempty set `Y` without arbitrage that -carries the null, a finite measure carried by `Y` that integrates the constraints and under which -every e-variable has mean at most `c`, for some `c < 1`, becomes a member of the null once a -finitely supported measure is added. It rests on the complete class theorem [LRR26, Theorem 3.1], -and follows [EVR26, Note 20]. -/ -theorem exists_add_sum_smul_dirac_mem_constraintNull (hg : ∀ i, Measurable (g i)) - (hY : NoArbitrageOn g Y) (hYμ : ∀ ν ∈ constraintNull (range g), ν Yᶜ = 0) - (hYne : Y.Nonempty) {μ : Measure 𝓧} [IsFiniteMeasure μ] (hμY : μ Yᶜ = 0) - (hgμ : ∀ i, Integrable (g i) μ) {c : ℝ≥0∞} (hc : c < 1) - (hμE : ∀ E, IsEVar E (constraintNull (range g)) → ∫⁻ x, E x ∂μ ≤ c) : - ∃ (α : Type) (_ : Fintype α) (x : α → 𝓧) (w : α → ℝ), (∀ k, 0 ≤ w k) ∧ - μ + ∑ k, ENNReal.ofReal (w k) • Measure.dirac (x k) ∈ constraintNull (range g) := by - classical - set r := μ.real univ with hr_def - set m := 1 - r with hm_def - have hm0 : 0 < m := by - have h1 := hμE 1 (isEVar_one _) - simp only [Pi.one_apply, lintegral_one] at h1 - have h2 : r < 1 := by - rw [hr_def, measureReal_def] - exact ENNReal.toReal_lt_of_lt_ofReal (by simpa using h1.trans_lt hc) - linarith - -- the complete class theorem, applied to the constraints shifted by multiples of their means - -- under `μ`, gives a finitely supported law under which the shifted constraints have - -- nonpositive means - obtain ⟨x₀, hx₀⟩ := hYne - obtain ⟨α, _, x, w, -, hw, hwz, -⟩ := exists_charging_family_of_noArbitrageOn - (noArbitrageOn_add_integral_div_of_lintegral_le hg hY hYμ hμY hgμ hc hμE) hx₀ - obtain ⟨hw0, hw1⟩ := mem_simplex_iff.1 hw - refine ⟨α, inferInstance, x, fun k ↦ m * w k, fun k ↦ mul_nonneg hm0.le (hw0 k), ?_⟩ - have hdirac : ∀ (f : 𝓧 → ℝ), Measurable f → ∀ k ∈ Finset.univ, - Integrable f (ENNReal.ofReal (m * w k) • Measure.dirac (x k)) := fun f hf k _ ↦ - (integrable_dirac' hf.stronglyMeasurable (by simp)).smul_measure ENNReal.ofReal_ne_top - refine mem_constraintNull_range_iff.2 ⟨⟨?_⟩, fun i ↦ ?_⟩ - · simp only [add_apply, sum_apply, smul_apply, measure_univ, smul_eq_mul, mul_one] - -- the added mass is `m = 1 - r`, the mass that `μ` lacks - have hmass : ∑ k, ENNReal.ofReal (m * w k) = ENNReal.ofReal m := by - rw [← ENNReal.ofReal_sum_of_nonneg fun k _ ↦ mul_nonneg hm0.le (hw0 k), ← Finset.mul_sum, - hw1, mul_one] - rw [hmass, ← ofReal_measureReal, ← hr_def, ← ENNReal.ofReal_add measureReal_nonneg hm0.le, - hm_def, add_sub_cancel, ENNReal.ofReal_one] - · refine ⟨(hgμ i).add_measure (integrable_finsetSum_measure.2 (hdirac _ (hg i))), ?_⟩ - rw [integral_add_measure (hgμ i) (integrable_finsetSum_measure.2 (hdirac _ (hg i))), - integral_sum_smul_dirac (fun k ↦ mul_nonneg hm0.le (hw0 k)) (hg i).stronglyMeasurable] - simp_rw [smul_eq_mul] - have h1 := hwz i - simp only [mul_add, Finset.sum_add_distrib, ← Finset.sum_mul, hw1, one_mul] at h1 - have h2 : ∑ k, m * w k * g i (x k) = m * ∑ k, w k * g i (x k) := by - rw [Finset.mul_sum] - exact Finset.sum_congr rfl fun k _ ↦ by ring - have h3 : m * ((∫ x, g i x ∂μ) / m) = ∫ x, g i x ∂μ := by - field_simp - rw [h2] - nlinarith - /-! ### The damped reverse information projection -/ /-- The density with respect to `Q` of the reverse information projection `Q / E` damped by