feat: the dual formula for the smallest relative entropy to a null generated by finitely many constraints, with no constraint qualification

LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean

@@ -0,0 +1,86 @@
+/-
+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
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+import LMLExplore.Analysis.SpecialFunctions.Log.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. As the damping factor tends to `0`, so does the integral of the damped
+logarithm, by dominated convergence.
+
+## Main statements
+
+* `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]`.
+* `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 Filter Topology
+
+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)
+
+/-- 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

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

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 :=

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