feat: conditional Bernoulli domination of [0, 1]-valued variables and GC11 Theorem 10 along a filtration

LMLExplore/MeasureTheory/Function/ConditionalExpectation/Real.lean

@@ -0,0 +1,55 @@
+/-
+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.Function.ConditionalExpectation.Basic
+
+/-!
+# Constant bounds on the conditional expectation of a bounded real function
+
+If an integrable real function `f` is at least `a` almost everywhere under a nonzero finite
+measure `μ`, then its conditional expectation given a sub-σ-algebra `m` is at least `a` almost
+everywhere, so an almost sure constant upper bound `μ[f | m] ≤ c` forces `a ≤ c`. Symmetrically,
+if `f ≤ b` almost everywhere, an almost sure constant lower bound `c ≤ μ[f | m]` forces `c ≤ b`.
+For instance, the conditional mean of a variable with values in `[0, 1]` cannot be bounded above
+by a negative constant, nor below by a constant larger than `1`.
+
+## Main statements
+
+* `LMLExplore.le_of_ae_le_of_condExp_le`: if `a ≤ f` and `μ[f | m] ≤ c` almost everywhere, then
+  `a ≤ c`.
+* `LMLExplore.le_of_le_condExp_of_ae_le`: if `c ≤ μ[f | m]` and `f ≤ b` almost everywhere, then
+  `c ≤ b`.
+-/
+
+public section
+
+open MeasureTheory
+
+namespace LMLExplore
+
+variable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] [NeZero μ]
+  {f : Ω → ℝ} {a b c : ℝ}
+
+/-- If `a ≤ f` almost everywhere and the conditional expectation of `f` given a sub-σ-algebra `m`
+is at most `c` almost everywhere, under a nonzero finite measure, then `a ≤ c`. -/
+lemma le_of_ae_le_of_condExp_le (hm : m ≤ mΩ) (hf : Integrable f μ) (ha : ∀ᵐ ω ∂μ, a ≤ f ω)
+    (hc : μ[f | m] ≤ᵐ[μ] fun _ ↦ c) : a ≤ c := by
+  have h := condExp_mono (m := m) (integrable_const a) hf ha
+  rw [condExp_const hm] at h
+  obtain ⟨_, h1, h2⟩ := (h.and hc).exists
+  exact h1.trans h2
+
+/-- If the conditional expectation of `f` given a sub-σ-algebra `m` is at least `c` almost
+everywhere and `f ≤ b` almost everywhere, under a nonzero finite measure, then `c ≤ b`. -/
+lemma le_of_le_condExp_of_ae_le (hm : m ≤ mΩ) (hf : Integrable f μ)
+    (hc : (fun _ ↦ c) ≤ᵐ[μ] μ[f | m]) (hb : ∀ᵐ ω ∂μ, f ω ≤ b) : c ≤ b := by
+  have h := condExp_mono (m := m) hf (integrable_const b) hb
+  rw [condExp_const hm] at h
+  obtain ⟨_, h1, h2⟩ := (hc.and h).exists
+  exact h1.trans h2
+
+end LMLExplore

LMLExplore/Probability/Kernel/Condexp.lean

@@ -9,7 +9,10 @@ public import Mathlib.Probability.ConditionalExpectation
 public import Mathlib.Probability.Kernel.Condexp
 
 /-!
-# The conditional expectation kernel: freezing and independence
+# The conditional expectation kernel: almost sure properties, freezing and independence
+
+A property that holds `μ`-almost everywhere holds, for almost every `ω`, almost everywhere under
+the conditional expectation kernel at `ω`.
 
 If `Z` is measurable with respect to a sub-σ-algebra `m`, then integrating a function of `(Z, ω)`
 amounts to integrating out `ω` against the conditional expectation kernel with `Z` frozen:
@@ -20,6 +23,8 @@ of the conditional expectation kernel by `X`, is almost surely the law of `X`.
 
 ## Main statements
 
+* `LMLExplore.ae_trim_ae_condExpKernel`: a `μ`-almost everywhere property holds almost everywhere
+  under `condExpKernel μ m ω` for `μ.trim hm`-almost every `ω`.
 * `LMLExplore.lintegral_comp_condExpKernel`: the freezing lemma for nonnegative functions.
 * `LMLExplore.ae_trim_map_condExpKernel_eq_of_indep`: for `X` independent of `m`,
   `(condExpKernel μ m ω).map X = μ.map X` for almost every `ω`.
@@ -40,6 +45,12 @@ namespace LMLExplore
 variable {Ω E : Type*} {m mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] {mE : MeasurableSpace E}
   {μ : Measure Ω} [IsFiniteMeasure μ]
 
+/-- A property that holds `μ`-almost everywhere holds, for `μ.trim hm`-almost every `ω`, almost
+everywhere under the conditional expectation kernel at `ω`. -/
+lemma ae_trim_ae_condExpKernel (hm : m ≤ mΩ) {p : Ω → Prop} (h : ∀ᵐ ω ∂μ, p ω) :
+    ∀ᵐ ω ∂(μ.trim hm), ∀ᵐ ω' ∂(condExpKernel μ m ω), p ω' :=
+  Measure.ae_ae_of_ae_comp (by rwa [condExpKernel_comp_trim hm])
+
 /-- **Freezing lemma for the conditional expectation kernel**: if `Z` is `m`-measurable, then for
 every measurable `Φ ≥ 0`,
 `∫⁻ ω, Φ (Z ω, ω) ∂μ = ∫⁻ ω, ∫⁻ ω', Φ (Z ω, ω') ∂(condExpKernel μ m ω) ∂μ`. -/