Earlier-filtration event integrals agree under any two laws matching on the filtration
ProvedAvramDividend.Classical.setIntegral_eq_of_measures_agree_on_subsigmaesscherfiltrationmartingalemeasure-theory
If two measures agree on every measurable set of a smaller σ-algebra, they have equal integrals of every strongly measurable earlier-observable f restricted to an earlier measurable event A. This is exactly the set-integral form required to transfer the projective Esscher exponential martingale identity to a single fixed terminal-horizon Esscher law.
Preamble
import Mathlib.MeasureTheory.Integral.Bochner.Set import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic import Theorems.Thm_AvramDividend_Classical_integral_eq_of_measures_agree_on_subsigma open MeasureTheory Set
Formal statement
theorem AvramDividend.Classical.setIntegral_eq_of_measures_agree_on_subsigma
{Ω : Type*} [m0 : MeasurableSpace Ω]
{m : MeasurableSpace Ω} (hm : m ≤ m0)
(μ ν : Measure Ω)
(hset : ∀ B : Set Ω, @MeasurableSet Ω m B → μ B = ν B)
(A : Set Ω) (hA : @MeasurableSet Ω m A)
(f : Ω → ℝ) (hf : StronglyMeasurable[m] f) :
(∫ ω in A, f ω ∂μ) = (∫ ω in A, f ω ∂ν) := by sorrySource
Apply the proven general equal-integrals-for-subσ theorem to the indicator of f on the smaller-algebra event A. Rewrite both indicators as restricted integrals using pinned Mathlib `integral_indicator`. The indicator is strongly measurable by pinned `StronglyMeasurable.indicator`.