Mathlib.MeasureTheory
Measure-theoretic helpers staged for Mathlib: integral identities, finite-dimensional polynomial zero-locus nullity, and kernel-composition lemmas.
AnalyticSetUniversalMeasurability 8 core · 14 supporting · 3 submodules This module gathers the Choquet-capacity proof that analytic events in Polish Borel spaces are measurable for every completed finite measure, together with the corresponding completed measurability and outer-integral bri Integral 1 core · 0 supporting · 1 submodule Integration helpers for continuity under uniform convergence on finite-measure sets. UnitInterval 0 core · 1 supporting · 1 submodule Measure-theoretic infrastructure for the closed real unit interval.
CompactArgminSelection 2 core · 0 supporting This module provides an exact Borel measurable argmin rule for a jointly Borel objective whose action sections are continuous on a fixed nonempty compact subset of a finite-dimensional Euclidean space. ★ borelMeasurable_compact_argmin_selector★ borelMeasurable_nearestPoint_selector
Measurable minimizers on compact Euclidean action sets
This module provides an exact Borel measurable argmin rule for a jointly Borel objective whose action sections are continuous on a fixed nonempty compact subset of a finite-dimensional Euclidean space. It also specializes the result to a measurable nearest-point rule. Neither result assumes convexity or uniqueness of the minimizer.
The hypotheses are the compact-action specialization of Brown--Purves, Measurable Selections of Extrema (1973), Corollary 1: the fixed feasible sections are compact, hence sigma-compact, and continuity supplies the required lower semicontinuity and exact attainment.
theorem borelMeasurable_compact_argmin_selector reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
A jointly Borel real objective with continuous action sections on a fixed nonempty compact action set in finite-dimensional Euclidean space admits a Borel measurable, feasible rule that minimizes the objective at every parameter.
Formal statement
hypotheses
X :
ι :
Type*
Fintype ι
K :
Set (EuclideanSpace ℝ ι)
hK :
hKne :
K.Nonempty
f :
X × EuclideanSpace ℝ ι → ℝ
hf :
hfc :
∀ x, ContinuousOn (fun y => f (x, y)) K
Proof (Lean source)
theorem borelMeasurable_compact_argmin_selector
{X : Type*} [MeasurableSpace X] [StandardBorelSpace X]
{ι : Type*} [Fintype ι]
(K : Set (EuclideanSpace ℝ ι)) (hK : IsCompact K) (hKne : K.Nonempty)
(f : X × EuclideanSpace ℝ ι → ℝ) (hf : Measurable f)
(hfc : ∀ x, ContinuousOn (fun y => f (x, y)) K) :
∃ π : X → EuclideanSpace ℝ ι,
Measurable π ∧ ∀ x, π x ∈ K ∧ ∀ y ∈ K, f (x, π x) ≤ f (x, y) := by
classical
let v : X → ℝ := fun x => sInf ((fun y => f (x, y)) '' K)
have hv : Measurable v := measurable_compact_sInf K hKne f hf hfc
have hmin : ∀ x, ∃ z ∈ K, f (x, z) = v x ∧ ∀ y ∈ K, f (x, z) ≤ f (x, y) := by
intro x
obtain ⟨z, hzK, hzv, hzmin⟩ := hK.exists_sInf_image_eq_and_le hKne (hfc x)
exact ⟨z, hzK, hzv.symm, hzmin⟩
letI : Nonempty K := Set.nonempty_coe_sort.mpr hKne
let d : ℕ → K := TopologicalSpace.denseSeq K
have hd : DenseRange d := TopologicalSpace.denseRange_denseSeq K
let r : ℕ → ℝ := fun n => 1 / 2 ^ n
have hr_pos : ∀ n, 0 < r n := by
intro n
simp only [r]
positivity
let Approx : ℕ → Type _ := fun n =>
{a : X → EuclideanSpace ℝ ι //
Measurable a ∧ ∀ x, ∃ z ∈ K, f (x, z) = v x ∧ dist z (a x) ≤ r n}
have hbase : Approx 0 := by
let p : ℕ → X → Prop := fun k x =>
∃ z ∈ K,
|f (x, z) - v x| + max (dist z (d k : EuclideanSpace ℝ ι) - r 0) 0 = 0
have hp : ∀ k, MeasurableSet {x | p k x} := by
intro k
simpa only [p] using measurableSet_exists_compact_eq_zero K hK hKne
(fun xz => |f xz - v xz.1| +
max (dist xz.2 (d k : EuclideanSpace ℝ ι) - r 0) 0)
((hf.sub (hv.comp measurable_fst)).norm.add
(((measurable_snd.dist measurable_const).sub_const (r 0)).max measurable_const))
(fun x => by
change ContinuousOn (fun y => |f (x, y) - v x| +
max (dist y (d k : EuclideanSpace ℝ ι) - r 0) 0) K
exact ((hfc x).sub continuousOn_const).abs.add
((((continuous_id.dist continuous_const).sub continuous_const).max
continuous_const).continuousOn))
(fun _ _ _ => add_nonneg (abs_nonneg _) (le_max_right _ _))
have hex : ∀ x, ∃ k, p k x := by
intro x
obtain ⟨z, hzK, hzv, _⟩ := hmin x
obtain ⟨k, hk⟩ := hd.exists_dist_lt (⟨z, hzK⟩ : K) (hr_pos 0)
refine ⟨k, z, hzK, ?_⟩
rw [hzv, sub_self, abs_zero]
have hk' : dist z (d k : EuclideanSpace ℝ ι) ≤ r 0 := by
simpa only [Subtype.dist_eq] using hk.le
simp [hk']
let a : X → EuclideanSpace ℝ ι := fun x =>
(d (find (hex x)) : EuclideanSpace ℝ ι)
have ha : Measurable a := by
simpa only [a] using
(Measurable.find (f := fun k (_ : X) => (d k : EuclideanSpace ℝ ι))
(fun _ => measurable_const) hp hex)
refine ⟨a, ha, ?_⟩
intro x
obtain ⟨z, hzK, hz⟩ := Nat.find_spec (hex x)
have hz' := (abs_add_max_eq_zero_iff
(f (x, z) - v x) (dist z (d (find (hex x)) : EuclideanSpace ℝ ι) - r 0)).mp hz
refine ⟨z, hzK, sub_eq_zero.mp hz'.1, ?_⟩
change dist z (d (find (hex x)) : EuclideanSpace ℝ ι) ≤ r 0
linarith [hz'.2]
have hstep : ∀ n, ∀ prev : Approx n,
{next : Approx (n + 1) //
∀ x, dist (prev.1 x) (next.1 x) ≤ r n + r (n + 1)} := by
intro n prev
let p : ℕ → X → Prop := fun k x =>
∃ z ∈ K,
|f (x, z) - v x| + max (dist z (prev.1 x) - r n) 0 +
max (dist z (d k : EuclideanSpace ℝ ι) - r (n + 1)) 0 = 0
have hp : ∀ k, MeasurableSet {x | p k x} := by
intro k
simpa only [p] using measurableSet_exists_compact_eq_zero K hK hKne
(fun xz => |f xz - v xz.1| + max (dist xz.2 (prev.1 xz.1) - r n) 0 +
max (dist xz.2 (d k : EuclideanSpace ℝ ι) - r (n + 1)) 0)
(((hf.sub (hv.comp measurable_fst)).norm.add
(((measurable_snd.dist (prev.2.1.comp measurable_fst)).sub_const (r n)).max
measurable_const)).add
(((measurable_snd.dist measurable_const).sub_const (r (n + 1))).max
measurable_const))
(fun x => by
change ContinuousOn (fun y => |f (x, y) - v x| +
max (dist y (prev.1 x) - r n) 0 +
max (dist y (d k : EuclideanSpace ℝ ι) - r (n + 1)) 0) K
exact (((hfc x).sub continuousOn_const).abs.add
((((continuous_id.dist continuous_const).sub continuous_const).max
continuous_const).continuousOn)).add
((((continuous_id.dist continuous_const).sub continuous_const).max
continuous_const).continuousOn))
(fun _ _ _ => add_nonneg
(add_nonneg (abs_nonneg _) (le_max_right _ _)) (le_max_right _ _))
have hex : ∀ x, ∃ k, p k x := by
intro x
obtain ⟨z, hzK, hzv, hzprev⟩ := prev.2.2 x
obtain ⟨k, hk⟩ := hd.exists_dist_lt (⟨z, hzK⟩ : K) (hr_pos (n + 1))
refine ⟨k, z, hzK, ?_⟩
rw [hzv, sub_self, abs_zero]
have hk' : dist z (d k : EuclideanSpace ℝ ι) ≤ r (n + 1) := by
simpa only [Subtype.dist_eq] using hk.le
simp [hzprev, hk']
let a : X → EuclideanSpace ℝ ι := fun x =>
(d (find (hex x)) : EuclideanSpace ℝ ι)
have ha : Measurable a := by
simpa only [a] using
(Measurable.find (f := fun k (_ : X) => (d k : EuclideanSpace ℝ ι))
(fun _ => measurable_const) hp hex)
refine ⟨⟨a, ha, ?_⟩, ?_⟩
· intro x
obtain ⟨z, hzK, hz⟩ := Nat.find_spec (hex x)
have hz' := (abs_add_max_add_max_eq_zero_iff
(f (x, z) - v x) (dist z (prev.1 x) - r n)
(dist z (d (find (hex x)) : EuclideanSpace ℝ ι) - r (n + 1))).mp hz
refine ⟨z, hzK, sub_eq_zero.mp hz'.1, ?_⟩
change dist z (d (find (hex x)) : EuclideanSpace ℝ ι) ≤ r (n + 1)
linarith [hz'.2.2]
· intro x
obtain ⟨z, _, hz⟩ := Nat.find_spec (hex x)
have hz' := (abs_add_max_add_max_eq_zero_iff
(f (x, z) - v x) (dist z (prev.1 x) - r n)
(dist z (d (find (hex x)) : EuclideanSpace ℝ ι) - r (n + 1))).mp hz
change dist (prev.1 x) (d (find (hex x)) : EuclideanSpace ℝ ι) ≤
r n + r (n + 1)
calc
dist (prev.1 x) (d (find (hex x)) : EuclideanSpace ℝ ι) ≤
dist (prev.1 x) z + dist z (d (find (hex x)) : EuclideanSpace ℝ ι) :=
dist_triangle _ _ _
_ ≤ r n + r (n + 1) := by
have h₁ : dist z (prev.1 x) ≤ r n := by linarith [hz'.2.1]
have h₂ : dist z (d (find (hex x)) : EuclideanSpace ℝ ι) ≤ r (n + 1) := by
linarith [hz'.2.2]
exact add_le_add (dist_comm z _ ▸ h₁) h₂
let approximants : ∀ n, Approx n := fun n =>
Nat.rec hbase (fun n prev => (hstep n prev).1) n
let a : ℕ → X → EuclideanSpace ℝ ι := fun n => (approximants n).1
have ha_meas : ∀ n, Measurable (a n) := fun n => (approximants n).2.1
have ha_near : ∀ n x, ∃ z ∈ K, f (x, z) = v x ∧ dist z (a n x) ≤ r n :=
fun n => (approximants n).2.2
have ha_step : ∀ n x, dist (a n x) (a (n + 1) x) ≤ r n + r (n + 1) := by
intro n x
exact (hstep n (approximants n)).2 x
have ha_cauchy : ∀ x, CauchySeq (fun n => a n x) := by
intro x
apply cauchySeq_of_le_geometric_two (C := 3)
intro n
calc
dist (a n x) (a (n + 1) x) ≤ r n + r (n + 1) := ha_step n x
_ = 3 / 2 / 2 ^ n := by
simp only [r, pow_succ]
field_simp
ring
choose π hπ using fun x => cauchySeq_tendsto_of_complete (ha_cauchy x)
have hπ_meas : Measurable π := by
apply measurable_of_tendsto_metrizable ha_meas
exact tendsto_pi_nhds.mpr hπ
refine ⟨π, hπ_meas, ?_⟩
intro x
have hr_zero : Tendsto r atTop (nhds 0) := by
simpa only [r, one_div, inv_pow] using
(tendsto_pow_atTop_nhds_zero_of_lt_one (𝕜 := ℝ) (by positivity : 0 ≤ (2 : ℝ)⁻¹)
(by norm_num : (2 : ℝ)⁻¹ < 1))
choose z hzK hzv hza using fun n => ha_near n x
have hzπ : Tendsto z atTop (nhds (π x)) := by
rw [tendsto_iff_dist_tendsto_zero]
have hza0 : Tendsto (fun n => dist (z n) (a n x)) atTop (nhds 0) := by
apply squeeze_zero' (Filter.Eventually.of_forall fun _ => dist_nonneg)
(Filter.Eventually.of_forall hza)
exact hr_zero
have haπ0 : Tendsto (fun n => dist (a n x) (π x)) atTop (nhds 0) :=
tendsto_iff_dist_tendsto_zero.mp (hπ x)
apply squeeze_zero' (Filter.Eventually.of_forall fun _ => dist_nonneg)
(Filter.Eventually.of_forall fun n => dist_triangle (z n) (a n x) (π x))
simpa only [zero_add] using hza0.add haπ0
have hπK : π x ∈ K := hK.isClosed.mem_of_tendsto hzπ (Filter.Eventually.of_forall hzK)
refine ⟨hπK, ?_⟩
intro y hyK
have hzπK : Tendsto z atTop (nhdsWithin (π x) K) :=
tendsto_nhdsWithin_iff.mpr ⟨hzπ, Filter.Eventually.of_forall hzK⟩
have hcomp : Tendsto (fun n => f (x, z n)) atTop
(nhds (f (x, π x))) := ((hfc x) (π x) hπK).tendsto.comp hzπK
have hconst : Tendsto (fun _ : ℕ => v x) atTop (nhds (v x)) :=
tendsto_const_nhds
have : f (x, π x) = v x := tendsto_nhds_unique hcomp (by simpa only [hzv] using hconst)
rw [this]
obtain ⟨z₀, _, hz₀, hz₀min⟩ := hmin x
rw [← hz₀]
exact hz₀min y hyK
theorem borelMeasurable_nearestPoint_selector reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Every nonempty compact subset of a finite-dimensional Euclidean space admits a total Borel measurable nearest-point rule whose chosen point is feasible and realizes the exact distance infimum.
Formal statement
hypotheses
conclusion
∃ π : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι,
Proof (Lean source)
theorem borelMeasurable_nearestPoint_selector
{ι : Type*} [Fintype ι]
(K : Set (EuclideanSpace ℝ ι)) (hK : IsCompact K) (hKne : K.Nonempty) :
∃ π : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι,
Measurable π ∧ ∀ x, π x ∈ K ∧ dist x (π x) = infDist x K := by
obtain ⟨π, hπmeas, hπ⟩ := borelMeasurable_compact_argmin_selector K hK hKne
(fun xy => dist xy.1 xy.2 ^ 2)
((continuous_fst.dist continuous_snd).pow 2).measurable
(fun _ => ((continuous_const.dist continuous_id).pow 2).continuousOn)
refine ⟨π, hπmeas, fun x => ⟨(hπ x).1, ?_⟩⟩
obtain ⟨y, hyK, hy⟩ := hK.exists_infDist_eq_dist hKne x
apply le_antisymm
· rw [hy]
have hsquare := (hπ x).2 y hyK
have hπnonneg : 0 ≤ dist x (π x) := dist_nonneg
have hynonneg : 0 ≤ dist x y := dist_nonneg
nlinarith
· exact infDist_le_dist_of_mem (hπ x).1
CondExpIndicatorTower 1 core · 0 supporting The theorem condExp_setIndicator_condExp_of_le is a generic conditional-expectation identity (no probability/causal content): for a tower of σ-algebras m ≤ m', an m'-measurable set s, and integrable f, conditioning the m ★ condExp_setIndicator_condExp_of_le
Conditioning ↔ inner-regression weighting across a σ-algebra tower
The theorem condExp_setIndicator_condExp_of_le is a generic
conditional-expectation identity (no probability/causal content): for a tower of
σ-algebras m ≤ m', an m'-measurable set s, and integrable f, conditioning the
masked outcome 1_s · f on the coarse m is the same as first replacing f by its
inner regression μ[f | m'] and then conditioning on m:
μ[1_s · f | m] =ᵐ μ[1_s · μ[f | m'] | m].
This is the measure-theoretic kernel behind "regression adjustment = inverse-
propensity weighting": with m = σ(X), m' = σ(D, X), s = {D = d}, dividing both
sides by μ[1_s | m] = P[D=d | σX] turns the left side into the IPW/adjustment
functional and the right side into the outcome regression. It recurs across ATE /
ATT / DTR back-door arguments, so it is factored out here as a reusable lemma and a
candidate Mathlib contribution.
Proof is the inner condExp_indicator (s is m'-measurable) followed by the
tower condExp_condExp_of_le.
theorem condExp_setIndicator_condExp_of_le reviewed
⚑ flagged
MeasureTheory
Conditioning a masked outcome equals conditioning its inner regression. Given a tower of σ-algebras m ≤ m' ≤ m0 on the sample space, with the trim of the measure μ to m' σ-finite, a set s measurable with respect to the finer σ-algebra m', and an integrable function f, the conditional expectation given m of the masked outcome 1_s · f agrees μ-almost everywhere with the conditional expectation given m of f — first replaced by its conditional expectation given m', then masked by s.
Formal statement
hypotheses
E :
hm :
m ≤ m'
hm' :
m' ≤ m0
SigmaFinite (μ.trim hm')
s :
Set Ω
hs :
MeasurableSet[m'] s
f :
Ω → E
hf :
Integrable f μ
conclusion
(μ[s.indicator f | m]) =ᵐ[μ] (μ[s.indicator (μ[f | m']) | m])
Proof (Lean source)
theorem condExp_setIndicator_condExp_of_le
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
(hm : m ≤ m') (hm' : m' ≤ m0) [SigmaFinite (μ.trim hm')]
{s : Set Ω} (hs : MeasurableSet[m'] s) {f : Ω → E} (hf : Integrable f μ) :
(μ[s.indicator f | m]) =ᵐ[μ] (μ[s.indicator (μ[f | m']) | m]) := by
exact (MeasureTheory.condExp_condExp_of_le (μ := μ) (f := s.indicator f) hm hm').symm.trans
(MeasureTheory.condExp_congr_ae (m := m) (μ := μ)
(MeasureTheory.condExp_indicator (m := m') (μ := μ) hf hs))
CondExpLinearity 1 core · 2 supporting Mathlib's condExp_add, condExp_sub and condExp_finsetSum take the integrability of each summand as an explicit argument, so every call site must first *name* those facts — in this library that is typically a chain of hav ★ condExp_add'
Integrability-free linearity of conditional expectation
Mathlib's condExp_add, condExp_sub and condExp_finsetSum take the integrability of
each summand as an explicit argument, so every call site must first name those facts —
in this library that is typically a chain of have _ : Integrable … lines whose only
content is Integrable.add/Integrable.sub bookkeeping.
This file restates the three lemmas with the integrability hypotheses as autoParams
discharged by fun_prop, which the Causalean side-condition layer has been tagged for.
At a call site that already holds the witnesses, fun_prop finds them by assumption;
where the integrand is built from tagged project constructions, it proves them outright.
Passing the hypotheses explicitly still works, so the primed forms are a strict
convenience layer over the Mathlib originals — no mathematics is added.
The wrapper analogues for POVar.condExpGiven and POCFBundle.condExpGiven live next to
those definitions, in Causalean/PO/Conditioning/.
theorem condExp_add' reviewed
⚑ flagged
MeasureTheory
Conditional expectation is additive: the conditional expectation of a sum of two integrable functions is the sum of their conditional expectations, almost everywhere.
Formal statement
hypotheses
α :
Type u_1
E :
Type u_2
f :
α → E
g :
α → E
m :
hf :
Integrable f μ := by fun_prop
hg :
Integrable g μ := by fun_prop
conclusion
μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]
Proof (Lean source)
theorem condExp_add' (m : MeasurableSpace α)
(hf : Integrable f μ := by fun_prop) (hg : Integrable g μ := by fun_prop) :
μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m] :=
condExp_add hf hg m
2 supporting declarations (lemmas, instances)
-
condExp_sub'theorem — Conditional expectation respects differences: the conditional expectation of the difference of two integrable functions is the difference of their conditional expectations, almost everywhere.hypothesesα :sharedType u_1E :sharedType u_2f :sharedα → Eg :sharedα → Em :hf :Integrable f μ := by fun_prophg :Integrable g μ := by fun_propconclusionμ[f - g | m] =ᵐ[μ] μ[f | m] - μ[g | m]Proof (Lean source)
theorem condExp_sub' (m : MeasurableSpace α) (hf : Integrable f μ := by fun_prop) (hg : Integrable g μ := by fun_prop) : μ[f - g | m] =ᵐ[μ] μ[f | m] - μ[g | m] := condExp_sub hf hg m -
condExp_finsetSum'theorem — Conditional expectation commutes with a finite sum: conditioning a finite sum of integrable functions is the same, almost everywhere, as summing their conditional expectations.hypothesesα :sharedType u_1E :sharedType u_2ι :m :hF :∀ i ∈ s, Integrable (F i) μ := by intro i _; fun_propconclusionμ[∑ i ∈ s, F i | m] =ᵐ[μ] ∑ i ∈ s, μ[F i | m]Proof (Lean source)
theorem condExp_finsetSum' {ι : Type*} {s : Finset ι} {F : ι → α → E} (m : MeasurableSpace α) (hF : ∀ i ∈ s, Integrable (F i) μ := by intro i _; fun_prop) : μ[∑ i ∈ s, F i | m] =ᵐ[μ] ∑ i ∈ s, μ[F i | m] := condExp_finsetSum hF m
CondExpPreimage 1 core · 0 supporting This module packages the uniqueness characterization of conditional expectation in the form used by random-design models: it is enough to match restricted integrals on every measurable preimage of the design map. ★ condExp_eq_of_integral_preimage_eq
Conditional expectation identified on design preimages
This module packages the uniqueness characterization of conditional expectation in the form used by random-design models: it is enough to match restricted integrals on every measurable preimage of the design map.
theorem condExp_eq_of_integral_preimage_eq reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a finite sampling measure, a measurable design map, an integrable outcome and candidate regression, a candidate regression that is almost-everywhere strongly measurable with respect to the design σ-algebra, and matching outcome and candidate-regression integrals on every measurable design event, the candidate regression is a version of the outcome's conditional expectation given the design.
Formal statement
hypotheses
Omega D :
mu :
Measure Omega
design :
Omega -> D
hdesign :
Measurable design
Y m :
Omega -> Real
hY :
Integrable Y mu
hm :
Integrable m mu
hm_design :
hintegral :
forall S : Set D, MeasurableSet S -> ∫ omega in design ⁻¹' S, Y omega ∂mu
= ∫ omega in design ⁻¹' S, m omega ∂mu
conclusion
mu[Y | comap design inferInstance] =ᵐ[mu] m
Proof (Lean source)
theorem condExp_eq_of_integral_preimage_eq
{Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D]
(mu : Measure Omega) [IsFiniteMeasure mu]
(design : Omega -> D) (hdesign : Measurable design)
(Y m : Omega -> Real)
(hY : Integrable Y mu) (hm : Integrable m mu)
(hm_design :
AEStronglyMeasurable[comap design inferInstance] m mu)
(hintegral : forall S : Set D, MeasurableSet S ->
∫ omega in design ⁻¹' S, Y omega ∂mu =
∫ omega in design ⁻¹' S, m omega ∂mu) :
mu[Y | comap design inferInstance] =ᵐ[mu] m := by
have hversion :
m =ᵐ[mu] mu[Y | comap design inferInstance] := by
refine ae_eq_condExp_of_forall_setIntegral_eq hdesign.comap_le hY ?_ ?_ hm_design
· intro S _ _
exact hm.integrableOn
· intro S hS _
rcases hS with ⟨T, hT, rfl⟩
exact (hintegral T hT).symm
exact hversion.symm
EqOfRnDerivEq 1 core · 0 supporting The theorem Measure.eq_of_rnDeriv_eq says that two measures which are both absolutely continuous with respect to a common reference and whose Radon–Nikodym derivatives against that reference agree almost everywhere are e ★ eq_of_rnDeriv_eq
Equality of measures from equality of Radon–Nikodym derivatives
The theorem Measure.eq_of_rnDeriv_eq says that two measures which are both absolutely
continuous with respect to a common reference and whose Radon–Nikodym derivatives against
that reference agree almost everywhere are equal. This is the "uniqueness" direction of
the Radon–Nikodym theorem, packaged as a term-mode lemma so that it can be applied by
unification rather than by syntactic rewriting — the latter is brittle when the measures
carry heavy dependent-type indexing.
It is a project-independent statement about measures over a generic measurable space and a candidate Mathlib contribution.
theorem eq_of_rnDeriv_eq reviewed
⚑ flagged
MeasureTheory.Measure
A measure is determined by its Radon–Nikodym derivative against a fixed reference. If the measure μ is absolutely continuous with respect to a σ-finite reference measure ρ, the measure ν is likewise absolutely continuous with respect to ρ, and their Radon–Nikodym densities dμ/dρ and dν/dρ agree ρ-almost everywhere, then μ and ν are equal as measures.
Formal statement
hypotheses
hμ :
μ ≪ ρ
hν :
ν ≪ ρ
h :
μ.rnDeriv ρ =ᵐ[ρ] ν.rnDeriv ρ
conclusion
μ = ν
Proof (Lean source)
theorem eq_of_rnDeriv_eq {μ ν ρ : Measure α} [SigmaFinite ρ]
(hμ : μ ≪ ρ) (hν : ν ≪ ρ)
(h : μ.rnDeriv ρ =ᵐ[ρ] ν.rnDeriv ρ) : μ = ν := by
letI : SFinite μ := sFinite_of_absolutelyContinuous hμ
letI : SFinite ν := sFinite_of_absolutelyContinuous hν
rw [← Measure.withDensity_rnDeriv_eq μ ρ hμ, ← Measure.withDensity_rnDeriv_eq ν ρ hν]
exact MeasureTheory.withDensity_congr_ae h
FiniteAtomicMeasure 1 core · 2 supporting This file provides decomposition, pointwise recovery, and integrability facts for finite measures concentrated on a finite family of measurable atoms. ★ measure_eq_fin_sum_smul_dirac_of_range
Measures carried by finitely many atoms
This file provides decomposition, pointwise recovery, and integrability facts for finite measures concentrated on a finite family of measurable atoms.
lemma measure_eq_fin_sum_smul_dirac_of_range reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Let μ be a finite measure and cell an injective family of finitely many points of the sample space, indexed by a finite type ι. If every singleton {cell i} is measurable and μ assigns its full mass to the range of cell, i.e. μ puts no mass outside these finitely many points, then μ equals the sum, over the index i, of the point mass μ {cell i} scaling the Dirac measure at cell i.
Formal statement
hypotheses
conclusion
μ = ∑ i, μ {cell i} • Measure.dirac (cell i)
Proof (Lean source)
lemma measure_eq_fin_sum_smul_dirac_of_range
(μ : Measure 𝒳) [IsFiniteMeasure μ] {ι : Type*} [Fintype ι]
(cell : ι ↪ 𝒳) (hcell : ∀ i, MeasurableSet {cell i})
(hrange : μ (range cell) = μ univ) :
μ = ∑ i, μ {cell i} • Measure.dirac (cell i) := by
have hrangeMeas : MeasurableSet (range cell) := by
rw [show range cell = ⋃ i, {cell i} by
ext x
simp]
exact MeasurableSet.iUnion hcell
have hae : ∀ᵐ x ∂μ, x ∈ range cell := by
change range cell ∈ ae μ
rw [mem_ae_iff, measure_compl hrangeMeas (measure_ne_top μ _), hrange]
simp
ext A hA
rw [← Measure.measure_inter_eq_of_ae hae]
rw [show range cell ∩ A = ⋃ i, ({cell i} ∩ A) by
ext x
constructor
· rintro ⟨⟨i, hix⟩, hxA⟩
simp only [Set.mem_iUnion, Set.mem_inter_iff, Set.mem_singleton_iff]
exact ⟨i, hix.symm, hxA⟩
· intro hx
simp only [Set.mem_iUnion, Set.mem_inter_iff, Set.mem_singleton_iff] at hx
obtain ⟨i, hxi, hxA⟩ := hx
exact ⟨⟨i, hxi.symm⟩, hxA⟩]
rw [measure_iUnion]
· simp only [Measure.finset_sum_apply, Measure.smul_apply, smul_eq_mul,
Measure.dirac_apply' _ hA, tsum_fintype]
apply Finset.sum_congr rfl
intro i hi
by_cases hmem : cell i ∈ A
· simp [hmem]
· have hinter : {cell i} ∩ A = ∅ := by
ext x
constructor
· intro hx
rcases hx with ⟨rfl, hxA⟩
exact (hmem hxA).elim
· simp
simp [hinter, hmem]
· intro i j hij
change Disjoint ({cell i} ∩ A) ({cell j} ∩ A)
rw [Set.disjoint_left]
intro x hxi hxj
simp only [Set.mem_inter_iff, Set.mem_singleton_iff] at hxi hxj
exact hij ((cell.injective (hxi.1.symm.trans hxj.1)))
· intro i
exact (hcell i).inter hA
2 supporting declarations (lemmas, instances)
-
property_at_of_ae_of_singleton_poslemma — An almost-sure property holds at every point to which the measure assigns nonzero mass.hypothesesconclusionp xProof (Lean source)
lemma property_at_of_ae_of_singleton_pos (μ : Measure 𝒳) (p : 𝒳 → Prop) {x : 𝒳} (hp : ∀ᵐ y ∂μ, p y) (hx : μ {x} ≠ 0) : p x := by by_contra hpx have hnull : μ {y | ¬p y} = 0 := by change {y | p y} ∈ ae μ at hp rw [mem_ae_iff] at hp simpa only [Set.compl_setOf] using hp apply hx exact measure_mono_null (by simpa [Set.singleton_subset_iff]) hnull -
integrable_of_finite_atomic_supportlemma — Every strongly measurable normed-vector-valued function is integrable under a finite measure concentrated on finitely many measurable points.hypotheses𝒳 :sharedType u_1μ :ι :Type*Finite ιcell :ι ↪ 𝒳hcell :∀ i, MeasurableSet {cell i}E :Type*f :𝒳 → Ehf :conclusionIntegrable f μProof (Lean source)
lemma integrable_of_finite_atomic_support (μ : Measure 𝒳) [IsFiniteMeasure μ] {ι : Type*} [Finite ι] (cell : ι ↪ 𝒳) (hcell : ∀ i, MeasurableSet {cell i}) (hrange : μ (range cell) = μ univ) {E : Type*} [NormedAddCommGroup E] (f : 𝒳 → E) (hf : StronglyMeasurable f) : Integrable f μ := by letI := ofFinite ι rw [measure_eq_fin_sum_smul_dirac_of_range μ cell hcell hrange] apply integrable_finset_sum_measure.2 intro i hi exact (integrable_dirac' hf (by simp)).smul_measure (measure_ne_top μ {cell i})
FiniteCoordinateDependence 4 core · 9 supporting This module provides measure theory on dependent products indexed by a type, relative to a finite set of coordinates. ★ map_coordinateProjection_withDensity_eq_of_lmarginal_eq
Finite coordinate dependence and density marginalization
This module provides measure theory on dependent products indexed by a type, relative to a finite
set of coordinates. It defines what it means for a function of an assignment to depend only on
those coordinates, the measurable restriction and extension maps between full and restricted
assignments, and the analytic bridge from equality of lmarginal densities to equality of the
projected withDensity measures.
The declarations live in the FiniteCoordinate sub-namespace so that opening
Causalean.Mathlib.MeasureTheory does not overload Mathlib's root DependsOn (which uses a
Set of coordinates and the opposite argument order).
def DependsOn reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory.FiniteCoordinate
A finite coordinate set and an assignment-valued function determine the property that the function is unchanged whenever two assignments agree on that set.
Definition (Lean source)
parameters
V :
Type u_1
V → Type u_2
Y :
Type*
S :
Finset V
f :
(∀ i, X i) → Y
x y :
(∀ i, i ∈ S → x i = y i)
def
DependsOn S f :
Prop
given by
f x = f y
def coordinateProjection reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory.FiniteCoordinate
A finite coordinate set and a full assignment determine its restriction to those coordinates.
Definition (Lean source)
parameters
def
coordinateProjection S x i :
X i
given by
fun i ↦ x i
def coordinateExtension reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory.FiniteCoordinate
A finite coordinate set, an anchor assignment, and a restricted assignment determine the full assignment that uses the restriction on the set and the anchor elsewhere.
Definition (Lean source)
parameters
def
coordinateExtension S x₀ z i :
X i
given by
fun i ↦ if hi : i ∈ S then z ⟨i, hi⟩ else x₀ i
theorem map_coordinateProjection_withDensity_eq_of_lmarginal_eq reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory.FiniteCoordinate
A finite coordinate set, measurable observational density, measurable comparison density, and equality after integrating out all complementary coordinates imply equality of the projected measures induced by those densities.
Formal statement
hypotheses
conclusion
Measure.map (coordinateProjection (X := X) S) ((Measure.pi μ).withDensity f)
= Measure.map (coordinateProjection (X := X) S) ((Measure.pi μ).withDensity g)
Proof (Lean source)
theorem map_coordinateProjection_withDensity_eq_of_lmarginal_eq
[Fintype V] {μ : ∀ i, Measure (X i)} [∀ i, SigmaFinite (μ i)]
(S : Finset V) {f g : (∀ i, X i) → ℝ≥0∞}
(hf : Measurable f) (hg : Measurable g)
(hmarginal : (∫⋯∫⁻_(univ \ S), f ∂μ) =
(∫⋯∫⁻_(univ \ S), g ∂μ)) :
Measure.map (coordinateProjection (X := X) S) ((Measure.pi μ).withDensity f) =
Measure.map (coordinateProjection (X := X) S) ((Measure.pi μ).withDensity g) := by
ext A hA
have hproj : Measurable (coordinateProjection (X := X) S) :=
measurable_coordinateProjection S
have hpre : MeasurableSet (coordinateProjection (X := X) S ⁻¹' A) := hproj hA
rw [Measure.map_apply hproj hA, Measure.map_apply hproj hA,
withDensity_apply _ hpre, withDensity_apply _ hpre]
rw [← lintegral_indicator hpre, ← lintegral_indicator hpre]
apply lintegral_eq_of_lmarginal_eq (univ \ S)
(hf.indicator hpre) (hg.indicator hpre)
funext x
simp only [lmarginal]
have hupdate (y : ∀ i : ↥(univ \ S), X i) :
coordinateProjection (X := X) S (updateFinset x (univ \ S) y) =
coordinateProjection S x := by
funext i
simp [coordinateProjection, updateFinset_def, i.property]
have hmem (y : ∀ i : ↥(univ \ S), X i) :
updateFinset x (univ \ S) y ∈ coordinateProjection (X := X) S ⁻¹' A ↔
x ∈ coordinateProjection (X := X) S ⁻¹' A := by
change coordinateProjection S (updateFinset x (univ \ S) y) ∈ A ↔
coordinateProjection S x ∈ A
rw [hupdate y]
by_cases hx : x ∈ coordinateProjection (X := X) S ⁻¹' A
· have hm := congrFun hmarginal x
simp only [lmarginal] at hm
simpa only [indicator, hmem, hx, if_pos] using hm
· simp only [indicator, hmem, hx, if_false]
9 supporting declarations (lemmas, instances)
-
dependsOn_applytheorem — A chosen coordinate can be read from an assignment using only that coordinate.hypothesesV :sharedType u_1V → Type u_2i :VconclusionDependsOn (X := X) {i} (fun x : ∀ k, X k ↦ x i)Proof (Lean source)
theorem dependsOn_apply (i : V) : DependsOn (X := X) {i} (fun x : ∀ k, X k ↦ x i) := by intro x y hxy exact hxy i (mem_singleton_self i) -
combinetheorem — Two functions depending on the same coordinate set, combined through a fixed binary operation, still depend only on that set.hypothesesV :sharedType u_1V → Type u_2Y Z W :Type*S :Finset Vf :(∀ i, X i) → Yg :(∀ i, X i) → Zhf :DependsOn S fhg :DependsOn S gop :Y → Z → WconclusionDependsOn S (fun x ↦ op (f x) (g x))Proof (Lean source)
-
measurable_coordinateProjectiontheorem — A finite coordinate set has a measurable assignment-restriction map.hypothesesV :sharedType u_1V → Type u_2S :Finset VconclusionMeasurable (coordinateProjection (X := X) S)Proof (Lean source)
@[fun_prop] theorem measurable_coordinateProjection (S : Finset V) : Measurable (coordinateProjection (X := X) S) := by refine measurable_pi_iff.mpr fun i ↦ ?_ simpa only [coordinateProjection] using (measurable_pi_apply (i : V) : Measurable (fun x : ∀ i, X i ↦ x (i : V))) -
measurable_coordinateExtensiontheorem — A finite coordinate set and an anchor assignment have a measurable extension map from restricted to full assignments.hypothesesconclusionMeasurable (coordinateExtension (X := X) S x₀)Proof (Lean source)
@[fun_prop] theorem measurable_coordinateExtension (S : Finset V) (x₀ : ∀ i, X i) : Measurable (coordinateExtension (X := X) S x₀) := by refine measurable_pi_iff.mpr fun i ↦ ?_ by_cases hi : i ∈ S · simp only [coordinateExtension, hi, ↓reduceDIte] exact measurable_pi_apply (⟨i, hi⟩ : S) · simp only [coordinateExtension, hi, ↓reduceDIte] exact measurable_const -
coordinateProjection_extensiontheorem — A finite coordinate set, an anchor assignment, and a restricted assignment are recovered unchanged after extension followed by restriction.hypothesesconclusioncoordinateProjection (X := X) S (coordinateExtension S x₀ z) = zProof (Lean source)
@[simp] theorem coordinateProjection_extension (S : Finset V) (x₀ : ∀ i, X i) (z : ∀ i : S, X i) : coordinateProjection (X := X) S (coordinateExtension S x₀ z) = z := by funext i simp [coordinateProjection, coordinateExtension, i.property] -
coordinateExtension_projectiontheorem — A function depending only on a coordinate set, together with an anchor assignment and a full assignment, has the same value after restricting and then extending that assignment.hypothesesV :sharedType u_1V → Type u_2Y :Type*S :Finset Vf :(∀ i, X i) → Yhf :DependsOn S fx₀ x :∀ i, X iconclusionf (coordinateExtension S x₀ (coordinateProjection S x)) = f xProof (Lean source)
theorem DependsOn.coordinateExtension_projection {Y : Type*} {S : Finset V} {f : (∀ i, X i) → Y} (hf : DependsOn S f) (x₀ x : ∀ i, X i) : f (coordinateExtension S x₀ (coordinateProjection S x)) = f x := by apply hf intro i hi simp [coordinateExtension, coordinateProjection, hi] -
map_eq_of_map_coordinateProjection_eqtheorem — An anchor assignment, a measurable outcome map, its dependence only on a finite coordinate set, and equality of the two corresponding coordinate marginals imply equality of the outcome laws under the two measures.hypothesesV :sharedType u_1V → Type u_2Y :Type*S :Finset Vμ ν :Measure (∀ i, X i)f :(∀ i, X i) → Yx₀ :∀ i, X ihf :hdepends :DependsOn S fhproj :Measure.map (coordinateProjection (X := X) S) μ= Measure.map (coordinateProjection (X := X) S) νconclusionMeasure.map f μ = Measure.map f νProof (Lean source)
theorem map_eq_of_map_coordinateProjection_eq {Y : Type*} [MeasurableSpace Y] {S : Finset V} {μ ν : Measure (∀ i, X i)} {f : (∀ i, X i) → Y} (x₀ : ∀ i, X i) (hf : Measurable f) (hdepends : DependsOn S f) (hproj : Measure.map (coordinateProjection (X := X) S) μ = Measure.map (coordinateProjection (X := X) S) ν) : Measure.map f μ = Measure.map f ν := by let e := coordinateExtension (X := X) S x₀ have he : Measurable e := measurable_coordinateExtension S x₀ calc Measure.map f μ = Measure.map (f ∘ e ∘ coordinateProjection S) μ := by congr 1 funext x exact (hdepends.coordinateExtension_projection x₀ x).symm _ = Measure.map (f ∘ e) (Measure.map (coordinateProjection S) μ) := by simpa only [Function.comp_def] using (Measure.map_map (hf.comp he) (measurable_coordinateProjection S) (μ := μ)).symm _ = Measure.map (f ∘ e) (Measure.map (coordinateProjection S) ν) := by rw [hproj] _ = Measure.map (f ∘ e ∘ coordinateProjection S) ν := by simpa only [Function.comp_def] using Measure.map_map (hf.comp he) (measurable_coordinateProjection S) (μ := ν) _ = Measure.map f ν := by congr 1 funext x exact hdepends.coordinateExtension_projection x₀ x -
map_comp_eq_of_map_eqtheorem — A measurable source map, a measurable common downstream map, and equality of the source laws imply equality after the common downstream mapping.hypothesesV :sharedType u_1V → Type u_2Y Z :μ ν :Measure (∀ i, X i)f :(∀ i, X i) → Ymix :Y → Zhf :hmix :Measurable mixhlaw :Measure.map f μ = Measure.map f νconclusionMeasure.map (mix ∘ f) μ = Measure.map (mix ∘ f) νProof (Lean source)
theorem map_comp_eq_of_map_eq {Y Z : Type*} [MeasurableSpace Y] [MeasurableSpace Z] {μ ν : Measure (∀ i, X i)} {f : (∀ i, X i) → Y} {mix : Y → Z} (hf : Measurable f) (hmix : Measurable mix) (hlaw : Measure.map f μ = Measure.map f ν) : Measure.map (mix ∘ f) μ = Measure.map (mix ∘ f) ν := by calc Measure.map (mix ∘ f) μ = Measure.map mix (Measure.map f μ) := (Measure.map_map hmix hf (μ := μ)).symm _ = Measure.map mix (Measure.map f ν) := by rw [hlaw] _ = Measure.map (mix ∘ f) ν := Measure.map_map hmix hf (μ := ν)
FinsetValues 7 core · 4 supporting This file provides the graph- and model-agnostic value-space infrastructure shared by the structural-causal-model and potential-outcome frameworks: typed value assignments over a finite node set (ValuesOn), their measura ★ measurable_valuesProjection★ comap_valuesProjection_le★ measurePreserving_valuesEquivOfEq
Value assignments over finite node sets
This file provides the graph- and model-agnostic value-space infrastructure shared by the
structural-causal-model and potential-outcome frameworks: typed value assignments over a finite
node set (ValuesOn), their measurable coordinate restrictions, and the canonical measurable
equivalence and measure transport between assignments over propositionally equal node sets.
Nothing here mentions graphs, SWIGs, or the SCM structure — it is pure product-space
bookkeeping over a finite index Finset, so it lives in the Mathlib staging area rather than
in SCM/. The restriction map coincides with Mathlib's Finset.restrict₂; we keep the named
valuesProjection/ValuesOn vocabulary because it reads better at the many downstream call
sites and because simp lemmas throughout the library are keyed on these names.
abbrev ValuesOn reviewed
⚑ flagged
Causalean
Given an underlying collection of nodes, a finite node set, and a family of value spaces, one for each node, a value assignment over that finite node set gives each node in the set one value from its associated value space.
def valuesProjection reviewed
⚑ flagged
Causalean
Given an underlying collection of nodes, finite node sets, a family of measurable value spaces, one for each node, and evidence that the second node set is contained in the first, the coordinate-restriction map sends each assignment on the first set to its values on the second set.
Definition (Lean source)
parameters
given by
fun ξ j => ξ ⟨j.val, hJI j.property⟩
theorem measurable_valuesProjection reviewed
⚑ flagged
Causalean
For value assignments over a finite node set, if a finite node set J is a subset of a larger finite node set I, then restricting a value assignment over I to its coordinates in J is a measurable map.
Formal statement
hypotheses
conclusion
Measurable (valuesProjection (Ω := Ω') hJI)
Proof (Lean source)
@[fun_prop]
theorem measurable_valuesProjection {M : Type*}
{I J : Finset M} {Ω' : M → Type*} [∀ n, MeasurableSpace (Ω' n)]
(hJI : J ⊆ I) : Measurable (valuesProjection (Ω := Ω') hJI) :=
Finset.measurable_restrict₂ hJI
theorem comap_valuesProjection_le reviewed
⚑ flagged
Causalean
For value assignments over a finite node set, if a finite node set W is a subset of a larger finite node set I, then the σ-algebra pulled back, via the coordinate restriction to W, from the measurable space on value assignments over W is a sub-σ-algebra of the ambient measurable space on value assignments over I.
Formal statement
hypotheses
conclusion
comap (valuesProjection (Ω := Ω') hW) inferInstance
≤ (inferInstance : MeasurableSpace (ValuesOn I Ω'))
Proof (Lean source)
theorem comap_valuesProjection_le {M : Type*}
{I W : Finset M} {Ω' : M → Type*} [∀ n, MeasurableSpace (Ω' n)]
(hW : W ⊆ I) :
comap (valuesProjection (Ω := Ω') hW) inferInstance ≤
(inferInstance : MeasurableSpace (ValuesOn I Ω')) :=
comap_le (measurable_valuesProjection hW)
def valuesEquivOfEq reviewed
⚑ flagged
Causalean
Given an underlying collection of nodes, finite node sets, a family of measurable value spaces, one for each node, and an equality of the two node sets, the canonical measurable equivalence identifies assignments over the first set with assignments over the second set by retaining the corresponding coordinate values.
Definition (Lean source)
parameters
given by
clause 1
clause 2
invFun := valuesProjection (le_of_eq h)
clause 3
left_inv := fun _ => rfl
clause 4
right_inv := fun _ => rfl
clause 5
measurable_toFun := measurable_valuesProjection (le_of_eq h.symm)
clause 6
measurable_invFun := measurable_valuesProjection (le_of_eq h)
lemma measurePreserving_valuesEquivOfEq reviewed
⚑ flagged
Causalean
Given two propositionally equal finite node sets I and J and a family μ of measures, one per coordinate of I, the canonical measurable equivalence between value assignments over I and over J carries the product measure Measure.pi μ to the product measure built from μ re-indexed along J through the equality.
Formal statement
hypotheses
conclusion
MeasurePreserving (valuesEquivOfEq (Ω := Ω) h) (pi μ) (pi (fun j : {j // j ∈ J} => μ ⟨j.val, h ▸ j.property⟩))
Proof (Lean source)
lemma measurePreserving_valuesEquivOfEq {M : Type*}
{I J : Finset M} {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)]
(h : I = J)
(μ : (i : {i // i ∈ I}) → Measure (Ω i.val)) :
MeasurePreserving (valuesEquivOfEq (Ω := Ω) h)
(pi μ)
(pi
(fun j : {j // j ∈ J} => μ ⟨j.val, h ▸ j.property⟩)) := by
subst h
refine ⟨(valuesEquivOfEq (Ω := Ω) rfl).measurable, ?_⟩
have hid : (⇑(valuesEquivOfEq (Ω := Ω) (rfl : I = I))
: ValuesOn I Ω → ValuesOn I Ω) = id := by
funext ξ; rfl
rw [show (map (valuesEquivOfEq (Ω := Ω) rfl)
(pi μ) : Measure _)
= map id (pi μ) from by rw [hid]]
rw [MeasureTheory.Measure.map_id]
def valuesUnionMk reviewed
⚑ flagged
Causalean
Given an underlying collection of nodes whose equality is decidable, a family of measurable value spaces, one for each node, finite node sets, and value assignments on the first and second sets, the combined assignment on their union uses the first assignment at nodes it contains and otherwise uses the second assignment.
Definition (Lean source)
parameters
def
given by
fun ⟨v, hv⟩
=> if hA : v ∈ A then a ⟨v, hA⟩ else b ⟨v, (Finset.mem_union.mp hv).resolve_left hA⟩
4 supporting declarations (lemmas, instances)
-
valuesUnionMk_apply_leftlemma — Projecting a union assignment to a coordinate from the first input returns that value.hypothesesconclusionvaluesUnionMk a b ⟨v, mem_union_left B hA⟩ = a ⟨v, hA⟩Proof (Lean source)
@[simp] lemma valuesUnionMk_apply_left {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)] {A B : Finset M} (a : ValuesOn A Ω) (b : ValuesOn B Ω) {v : M} (hA : v ∈ A) : valuesUnionMk a b ⟨v, mem_union_left B hA⟩ = a ⟨v, hA⟩ := by unfold valuesUnionMk exact dif_pos hA -
valuesUnionMk_apply_rightlemma — Projecting a union assignment outside the first input returns the second input's value.hypothesesM :∀ n, MeasurableSpace (Ω n)A B :Finset Ma :ValuesOn A Ωb :ValuesOn B Ωv :Mhv :v ∈ A ∪ BhA :v ∉ AconclusionvaluesUnionMk a b ⟨v, hv⟩ = b ⟨v, (Finset.mem_union.mp hv).resolve_left hA⟩Proof (Lean source)
@[simp] lemma valuesUnionMk_apply_right {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)] {A B : Finset M} (a : ValuesOn A Ω) (b : ValuesOn B Ω) {v : M} (hv : v ∈ A ∪ B) (hA : v ∉ A) : valuesUnionMk a b ⟨v, hv⟩ = b ⟨v, (Finset.mem_union.mp hv).resolve_left hA⟩ := by unfold valuesUnionMk exact dif_neg hA -
measurable_valuesUnionMk_rightlemma — Combining assignments is measurable in the second assignment with the first held fixed.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma measurable_valuesUnionMk_right {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)] {A B : Finset M} (a : ValuesOn A Ω) : Measurable (fun b : ValuesOn B Ω => valuesUnionMk a b) := by refine measurable_pi_iff.mpr ?_ rintro ⟨v, hv⟩ by_cases hA : v ∈ A · have h_eq : (fun b : ValuesOn B Ω => valuesUnionMk a b ⟨v, hv⟩) = (fun _ => a ⟨v, hA⟩) := funext fun _ => valuesUnionMk_apply_left a _ hA rw [h_eq] exact measurable_const · have hB : v ∈ B := (Finset.mem_union.mp hv).resolve_left hA have h_eq : (fun b : ValuesOn B Ω => valuesUnionMk a b ⟨v, hv⟩) = (fun b => b ⟨v, hB⟩) := funext fun _ => valuesUnionMk_apply_right a _ hv hA rw [h_eq] exact measurable_pi_apply _ -
measurable_valuesUnionMklemma — Combining assignments is jointly measurable in both input assignments.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma measurable_valuesUnionMk {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)] {A B : Finset M} : Measurable (fun p : ValuesOn A Ω × ValuesOn B Ω => valuesUnionMk p.1 p.2) := by refine measurable_pi_iff.mpr ?_ rintro ⟨v, hv⟩ by_cases hA : v ∈ A · have h_eq : (fun p : ValuesOn A Ω × ValuesOn B Ω => valuesUnionMk p.1 p.2 ⟨v, hv⟩) = (fun p => p.1 ⟨v, hA⟩) := by funext p exact valuesUnionMk_apply_left _ _ hA rw [h_eq] exact (measurable_pi_apply _).comp measurable_fst · have hB : v ∈ B := (Finset.mem_union.mp hv).resolve_left hA have h_eq : (fun p : ValuesOn A Ω × ValuesOn B Ω => valuesUnionMk p.1 p.2 ⟨v, hv⟩) = (fun p => p.2 ⟨v, hB⟩) := by funext p exact valuesUnionMk_apply_right _ _ hv hA rw [h_eq] exact (measurable_pi_apply _).comp measurable_snd
IntegralBind 6 core · 0 supporting This file proves Bochner-integral identities for Giry-monad binds and for binds whose fibres are pushforwards. ★ integral_bind★ integral_bind_map★ integral_bind_bind_map★ integral_bind_of_ae_eq_const★ map_bind_bind_map_proj★ integral_bind_bind_map_proj
Bochner Integrals Against Measure Binds
This file proves Bochner-integral identities for Giry-monad binds and for binds whose fibres are pushforwards. These identities convert an integral against a bound measure into the corresponding iterated integral, supporting nested-kernel calculations in the causal and statistical parts of the library.
The main public results are integral_bind, integral_bind_map,
integral_bind_bind_map, integral_bind_of_ae_eq_const, map_bind_bind_map_proj, and
integral_bind_bind_map_proj. Together they cover one-level binds, bind-then-map
integrals, doubly nested bind-then-map integrals, fibrewise constant collapses, and
projection back to a reattached base coordinate.
theorem integral_bind reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
If κ is a measurable family of measures, one per point of the base space (a measurable kernel) and f is Bochner-integrable against the measure m.bind κ obtained by mixing κ over the base measure m, then the Bochner integral of f against m.bind κ equals the iterated integral: first integrate f against κ a for each base point a, then integrate the result against m. This is the Bochner analogue of MeasureTheory.Measure.lintegral_bind.
Formal statement
hypotheses
conclusion
∫ x, f x ∂m.bind κ = ∫ a, ∫ x, f x ∂κ a ∂m
Proof (Lean source)
theorem integral_bind {α β E : Type*} [MeasurableSpace α] [MeasurableSpace β]
[NormedAddCommGroup E] [NormedSpace ℝ E]
{m : Measure α} {κ : α → Measure β} {f : β → E}
(hκ : Measurable κ)
(hf : Integrable f (m.bind κ)) :
∫ x, f x ∂m.bind κ = ∫ a, ∫ x, f x ∂κ a ∂m := by
let K : Kernel α β := ⟨κ, hκ⟩
have hcomp : (K ∘ₘ m) = m.bind κ := by
rw [Measure.comp_eq_comp_const_apply]
rfl
rw [← hcomp]
simpa [K, Kernel.comp_apply, Measure.comp_eq_comp_const_apply] using
(ProbabilityTheory.Kernel.integral_comp
(κ := Kernel.const Unit m) (η := K) (a := ()) (f := f)
(by simpa [K, Kernel.comp_apply, Measure.comp_eq_comp_const_apply] using hf))
theorem integral_bind_map reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Suppose each map g a is measurable, the kernel sending a base point a to the pushforward measure (κ a).map (g a) is itself measurable, and f is Bochner-integrable against the mixed measure m.bind (fun a => (κ a).map (g a)). Then the Bochner integral of f against that mixed measure equals the iterated integral of the pulled-back integrand a ↦ ∫ x, f (g a x) ∂κ a against the base measure m. This packages a single application of integral_bind with the fibrewise MeasureTheory.integral_map, supplying the bridge needed to expand a nested bind-then-map Bochner integral.
Formal statement
hypotheses
α β γ E :
hg :
∀ a, Measurable (g a)
hgm :
Measurable (fun a => (κ a).map (g a))
hf :
Integrable f (m.bind (fun a => (κ a).map (g a)))
conclusion
∫ z, f z ∂m.bind (fun a => (κ a).map (g a)) = ∫ a, ∫ x, f (g a x) ∂κ a ∂m
Proof (Lean source)
theorem integral_bind_map {α β γ E : Type*} [MeasurableSpace α] [MeasurableSpace β]
[MeasurableSpace γ] [NormedAddCommGroup E] [NormedSpace ℝ E]
{m : Measure α} {κ : α → Measure β} {g : α → β → γ} {f : γ → E}
(hg : ∀ a, Measurable (g a))
(hgm : Measurable (fun a => (κ a).map (g a)))
(hf : Integrable f (m.bind (fun a => (κ a).map (g a)))) :
∫ z, f z ∂m.bind (fun a => (κ a).map (g a)) = ∫ a, ∫ x, f (g a x) ∂κ a ∂m := by
let K : Kernel α γ := ⟨fun a => (κ a).map (g a), hgm⟩
have hcomp : (K ∘ₘ m) = m.bind fun a => (κ a).map (g a) := by
rw [Measure.comp_eq_comp_const_apply]
rfl
have hfK : Integrable f ((K ∘ₘ m)) := by simpa [hcomp] using hf
have hfiber_int_ae : ∀ᵐ a ∂m, Integrable f ((κ a).map (g a)) := by
simpa [K, Kernel.const_apply] using
(MeasureTheory.Integrable.ae_of_comp
(κ := Kernel.const Unit m) (η := K) (a := ()) (f := f) hfK)
have hfiber : (fun a => ∫ z, f z ∂(κ a).map (g a)) =ᶠ[ae m]
(fun a => ∫ x, f (g a x) ∂κ a) := by
filter_upwards [hfiber_int_ae] with a ha
exact integral_map (hg a).aemeasurable ha.aestronglyMeasurable
calc
∫ z, f z ∂m.bind (fun a => (κ a).map (g a))
= ∫ z, f z ∂(K ∘ₘ m) := by rw [hcomp]
_ = ∫ a, ∫ z, f z ∂K a ∂m := by
simpa [K, Kernel.comp_apply, Measure.comp_eq_comp_const_apply] using
(ProbabilityTheory.Kernel.integral_comp
(κ := Kernel.const Unit m) (η := K) (a := ()) (f := f) hfK)
_ = ∫ a, ∫ x, f (g a x) ∂κ a ∂m := integral_congr_ae hfiber
theorem integral_bind_bind_map reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Suppose each map g a b is measurable, for every base point a the pushforward kernel b ↦ (κ₂ a b).map (g a b) is measurable, the resulting doubly-nested mixed kernel a ↦ (κ₁ a).bind (fun b => (κ₂ a b).map (g a b)) is itself measurable, and f is Bochner-integrable against the measure obtained by mixing κ₁ over the base measure m and, within each fibre, mixing the pushforward of κ₂ under g. Then the Bochner integral of f against that triply-nested mixed measure equals the threefold iterated integral of the pulled-back integrand (a, b, c) ↦ f (g a b c), integrated successively against κ₂ a b, κ₁ a, and m. This is the single bridge for a bind-then-bind-then-map integrand, which neither integral_bind nor integral_bind_map covers in one step.
Formal statement
hypotheses
α β γ δ E :
hg :
∀ a b, Measurable (g a b)
hmap :
∀ a, Measurable fun b => (κ₂ a b).map (g a b)
hker :
hf :
Proof (Lean source)
theorem integral_bind_bind_map {α β γ δ E : Type*}
[MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
[MeasurableSpace δ] [NormedAddCommGroup E] [NormedSpace ℝ E]
{m : Measure α} {κ₁ : α → Measure β} {κ₂ : α → β → Measure γ}
{g : α → β → γ → δ} {f : δ → E}
(hg : ∀ a b, Measurable (g a b))
(hmap : ∀ a, Measurable fun b => (κ₂ a b).map (g a b))
(hker : Measurable fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b))
(hf : Integrable f (m.bind fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b))) :
∫ z, f z ∂(m.bind fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b))
= ∫ a, ∫ b, ∫ c, f (g a b c) ∂(κ₂ a b) ∂(κ₁ a) ∂m := by
let K : Kernel α δ := ⟨fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b), hker⟩
have hcomp : (K ∘ₘ m) = m.bind fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b) := by
rw [Measure.comp_eq_comp_const_apply]; rfl
have hfK : Integrable f (K ∘ₘ m) := by simpa [hcomp] using hf
have hfiber_int_ae : ∀ᵐ a ∂m,
Integrable f ((κ₁ a).bind fun b => (κ₂ a b).map (g a b)) := by
simpa [K, Kernel.const_apply] using
(MeasureTheory.Integrable.ae_of_comp
(κ := Kernel.const Unit m) (η := K) (a := ()) (f := f) hfK)
have hcollapse :
(fun a => ∫ z, f z ∂((κ₁ a).bind fun b => (κ₂ a b).map (g a b)))
=ᶠ[ae m] (fun a => ∫ b, ∫ c, f (g a b c) ∂(κ₂ a b) ∂(κ₁ a)) := by
filter_upwards [hfiber_int_ae] with a hfa
exact integral_bind_map (hg a) (hmap a) hfa
rw [integral_bind hker hf]
exact integral_congr_ae hcollapse
theorem integral_bind_of_ae_eq_const reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Suppose κ is a measurable family of measures, every fibre κ a is a probability measure, the integrand f agrees κ a-almost everywhere with a constant f' a on that fibre, for every base point a, and f is Bochner-integrable against the mixed measure m.bind κ. Then the Bochner integral of f against m.bind κ equals the integral of the fibrewise constant f' against the base measure m. This is the bridge for the situation where the integrand only depends on a coordinate that is constant within each inner kernel, so the inner integral evaluates to that constant and the bind reduces to ∫ a, f' a ∂m.
Formal statement
hypotheses
α β E :
hκ :
hp :
∀ a, IsProbabilityMeasure (κ a)
hconst :
∀ a, ∀ᵐ y ∂κ a, f y = f' a
hf :
Integrable f (m.bind κ)
conclusion
∫ y, f y ∂m.bind κ = ∫ a, f' a ∂m
Proof (Lean source)
theorem integral_bind_of_ae_eq_const {α β E : Type*} [MeasurableSpace α]
[MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℝ E]
{m : Measure α} {κ : α → Measure β} {f : β → E} {f' : α → E}
(hκ : Measurable κ) (hp : ∀ a, IsProbabilityMeasure (κ a))
(hconst : ∀ a, ∀ᵐ y ∂κ a, f y = f' a)
(hf : Integrable f (m.bind κ)) :
∫ y, f y ∂m.bind κ = ∫ a, f' a ∂m := by
rw [integral_bind hκ hf]
by_cases hE : CompleteSpace E
· have hfiber : (fun a => ∫ y, f y ∂κ a) =ᶠ[ae m] (fun a => f' a) := by
exact Filter.Eventually.of_forall fun a => by
calc
∫ y, f y ∂κ a = ∫ y, f' a ∂κ a := integral_congr_ae (hconst a)
_ = f' a := by
rw [integral_const, measureReal_def, isProbabilityMeasure_iff.mp (hp a)]
simp
exact integral_congr_ae hfiber
· simp [integral, hE]
theorem map_bind_bind_map_proj reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Suppose every fibre κ₁ a is a probability measure, every inner fibre κ₂ a b is a probability measure, each map g a b is measurable, for every base point a the pushforward kernel b ↦ (κ₂ a b).map (g a b) is measurable, the resulting doubly-nested mixed kernel is measurable, the projection π is measurable, and π undoes g by recovering the base point: π (g a b c) = a for all a, b, c. Then pushing the triply-nested mixed measure forward along π returns exactly the base measure m. This is the underlying measure identity behind integral_bind_bind_map_proj, stated without any integrability or integrand hypotheses: the two inner probability fibres each contribute total mass one over a fixed base point, so transporting back along π returns m unchanged (no hypothesis on m is needed). It is the bridge for marginalising a nested Giry-monad construction onto its reattached coordinate when only measurability of the eventual integrand is available.
Formal statement
hypotheses
hp₁ :
∀ a, IsProbabilityMeasure (κ₁ a)
hp₂ :
∀ a b, IsProbabilityMeasure (κ₂ a b)
hg :
∀ a b, Measurable (g a b)
hmap :
∀ a, Measurable fun b => (κ₂ a b).map (g a b)
hker :
hπ :
hπg :
∀ a b c, π (g a b c) = a
Proof (Lean source)
theorem map_bind_bind_map_proj {α β γ δ : Type*}
[MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
[MeasurableSpace δ]
{m : Measure α} {κ₁ : α → Measure β} {κ₂ : α → β → Measure γ}
{g : α → β → γ → δ} {π : δ → α}
(hp₁ : ∀ a, IsProbabilityMeasure (κ₁ a))
(hp₂ : ∀ a b, IsProbabilityMeasure (κ₂ a b))
(hg : ∀ a b, Measurable (g a b))
(hmap : ∀ a, Measurable fun b => (κ₂ a b).map (g a b))
(hker : Measurable fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b))
(hπ : Measurable π) (hπg : ∀ a b c, π (g a b c) = a) :
(m.bind fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b)).map π = m := by
have hdπ : Measurable (fun z => Measure.dirac (π z)) := by fun_prop
have key : ∀ a, ((κ₁ a).bind fun b => (κ₂ a b).map (g a b)).map π = Measure.dirac a := by
intro a
have hinner : (fun b => ((κ₂ a b).map (g a b)).map π) = fun _ => Measure.dirac a := by
funext b; rw [Measure.map_map hπ (hg a b)]
have hc : (π ∘ g a b) = fun _ => a := funext (hπg a b)
rw [hc, Measure.map_const, (hp₂ a b).measure_univ, one_smul]
rw [← Measure.bind_dirac_eq_map _ hπ, Measure.bind_bind (hmap a).aemeasurable hdπ.aemeasurable]
have hstep : (fun b => ((κ₂ a b).map (g a b)).bind fun z => Measure.dirac (π z))
= fun _ => Measure.dirac a := by
funext b; rw [Measure.bind_dirac_eq_map _ hπ]; exact congrFun hinner b
rw [hstep, Measure.bind_const, (hp₁ a).measure_univ, one_smul]
rw [← Measure.bind_dirac_eq_map _ hπ, Measure.bind_bind hker.aemeasurable hdπ.aemeasurable]
have hstep2 : (fun a => ((κ₁ a).bind fun b => (κ₂ a b).map (g a b)).bind
fun z => Measure.dirac (π z)) = fun a => Measure.dirac a := by
funext a; rw [Measure.bind_dirac_eq_map _ hπ]; exact key a
rw [hstep2, Measure.bind_dirac]
theorem integral_bind_bind_map_proj reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Suppose every fibre κ₁ a is a probability measure, every inner fibre κ₂ a b is a probability measure, each map g a b is measurable, for every base point a the pushforward kernel b ↦ (κ₂ a b).map (g a b) is measurable, the resulting doubly-nested mixed kernel is measurable, the projection π is measurable, π undoes g by recovering the base point: π (g a b c) = a for all a, b, c, and f is Bochner-integrable against the base measure m. Then integrating the pulled-back function f ∘ π against the triply-nested mixed measure equals integrating f directly against the base measure m. This is the one-step bridge for marginalising a nested Giry-monad construction back onto the coordinate that the innermost pushforward carries through; the fibrewise probability-mass-one hypotheses are what make the two inner integrals of the constant f a evaluate to f a (no assumption on m is needed).
Formal statement
hypotheses
α β γ δ E :
hp₁ :
∀ a, IsProbabilityMeasure (κ₁ a)
hp₂ :
∀ a b, IsProbabilityMeasure (κ₂ a b)
hg :
∀ a b, Measurable (g a b)
hmap :
∀ a, Measurable fun b => (κ₂ a b).map (g a b)
hker :
hπ :
hπg :
∀ a b c, π (g a b c) = a
hf' :
Integrable f m
Proof (Lean source)
theorem integral_bind_bind_map_proj {α β γ δ E : Type*}
[MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
[MeasurableSpace δ] [NormedAddCommGroup E] [NormedSpace ℝ E]
{m : Measure α} {κ₁ : α → Measure β} {κ₂ : α → β → Measure γ}
{g : α → β → γ → δ} {π : δ → α} {f : α → E}
(hp₁ : ∀ a, IsProbabilityMeasure (κ₁ a))
(hp₂ : ∀ a b, IsProbabilityMeasure (κ₂ a b))
(hg : ∀ a b, Measurable (g a b))
(hmap : ∀ a, Measurable fun b => (κ₂ a b).map (g a b))
(hker : Measurable fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b))
(hπ : Measurable π) (hπg : ∀ a b c, π (g a b c) = a)
(hf' : Integrable f m) :
∫ z, f (π z) ∂(m.bind fun a => (κ₁ a).bind fun b => (κ₂ a b).map (g a b))
= ∫ a, f a ∂m := by
have hmeq := map_bind_bind_map_proj (m := m)
hp₁ hp₂ hg hmap hker hπ hπg
conv_rhs => rw [← hmeq]
exact (integral_map hπ.aemeasurable (hmeq.symm ▸ hf'.aestronglyMeasurable)).symm
MemLp 1 core · 0 supporting This file proves MemLp.of_measurable_of_integral_sq_le, which turns an explicit integrability witness for the squared norm of an almost-everywhere strongly measurable function into membership of that function in L². ★ of_measurable_of_integral_sq_le
MemLp from square-integrability
This file proves MemLp.of_measurable_of_integral_sq_le, which turns an explicit
integrability witness for the squared norm of an almost-everywhere strongly measurable
function into membership of that function in L².
theorem of_measurable_of_integral_sq_le reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory.MemLp
If a normed-vector-space-valued function f is almost-everywhere strongly measurable with respect to Q and the squared norm ‖f x‖^2 is integrable against Q, then f belongs to .
Formal statement
Proof (Lean source)
@[deprecated MeasureTheory.memLp_two_iff_integrable_sq_norm (since := "2026-08-29")]
theorem MemLp.of_measurable_of_integral_sq_le
{X F : Type*} [MeasurableSpace X] [NormedAddCommGroup F] {Q : Measure X}
{f : X → F}
(hf_meas : AEStronglyMeasurable f Q)
(h_sq_int : Integrable (fun x => ‖f x‖ ^ 2) Q) :
MemLp f 2 Q :=
(MeasureTheory.memLp_two_iff_integrable_sq_norm hf_meas).2 h_sq_int
MomentSliceSupport 4 core · 11 supporting Let K = [a,b] be a compact interval and s : ℝ. ★ card_le_three_of_isExtremePoint
Moment-slice extreme-point support bound (Richter–Rogosinski / Winkler)
Let K = [a,b] be a compact interval and s : ℝ. The moment slice is the set of
probability measures on K with mean 0 and second moment s:
C = { μ | μ Kᶜ = 0 ∧ ∫ x ∂μ = 0 ∧ ∫ x² ∂μ = s }.
This file proves the support-size part of the Richter–Rogosinski / Karr / Winkler
canonical representation theorem for this two-moment slice. It starts with the
finite-atom perturbation argument: three homogeneous linear constraints (total mass,
mean, second moment) on four-or-more atom weights always admit a nonzero perturbation
δ, and μ ± ε·δ are then two distinct measures of C whose midpoint is μ,
contradicting extremality. The later support argument upgrades this from a finite atom
set to an arbitrary extreme probability measure in the slice.
Main results:
* exists_moment_perturbation — pure linear algebra: on 4-or-more reals there is a
nonzero weight perturbation killing the three moments 1, x, x² simultaneously.
* card_le_three_of_isExtremePoint — an extreme point of the moment slice supported on a
finite positive-weight atom set has at most three atoms.
* exists_isMinOn_momentSlice — on a compact Hausdorff space the moment slice is weak-*
compact, so a bounded-continuous objective attains its minimum over the slice.
* support_finite_ncard_le_three_of_isExtremePoint — any extreme probability measure in
the two-moment slice has finite topological support of cardinality at most three.
* isAtomic_le_three_of_isExtremePoint and
exists_cardSupportLe_three_of_isExtremePoint — the same conclusion as a positive
discrete-measure representation and as a finite support carrier.
def discreteMeasure reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a measurable sample space, a finite set of points in that space, and a real-valued weight function, the discrete measure is the sum of the Dirac measures at the points of , each multiplied by the nonnegative part of its weight.
Definition (Lean source)
def MomentSlice reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given real numbers , , and , the moment slice is the set of probability measures on the real line that [are supported on the closed interval from to ](step:1,step:2), have mean zero, and have second moment .
Definition (Lean source)
parameters
a b s :
ℝ
given by
{μ | IsProbabilityMeasure μ ∧ μ (Icc a b)ᶜ = 0 ∧ (∫ x, x ∂μ = 0) ∧ (∫ x, x ^ 2 ∂μ = s)}
def IsExtremePoint reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a set of measures on the real line and a measure on the real line, the extreme-point property holds when belongs to and, for every pair of measures in and every mixing weight strictly between zero and one, equality of to their weighted mixture implies that the two measures are equal.
theorem card_le_three_of_isExtremePoint reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Richter–Rogosinski support bound (finite-atom case). Consider the discrete probability measure μ = ∑_{x∈T} w x · δ_x carried by a finite set T ⊆ ℝ. If every atom weight w x is strictly positive for x ∈ T, every atom lies in the interval [a, b], and μ is an extreme point of the moment slice — the probability measures on [a, b] with mean 0 and second moment s, then T has at most three elements: μ is supported on at most three atoms.
Formal statement
Proof (Lean source)
theorem card_le_three_of_isExtremePoint {a b s : ℝ} {T : Finset ℝ} {w : ℝ → ℝ}
(hpos : ∀ x ∈ T, 0 < w x) (hTab : ∀ x ∈ T, x ∈ Icc a b)
(hext : IsExtremePoint (MomentSlice a b s) (discreteMeasure T w)) :
T.card ≤ 3 := by
by_contra hcon
push_neg at hcon
obtain ⟨δ, hδ0, hδ1, hδ2, x₀, hx₀T, hx₀ne⟩ := exists_moment_perturbation hcon
have hwnn : ∀ x ∈ T, 0 ≤ w x := fun x hx => (hpos x hx).le
obtain ⟨hμprob, _, hμmean, hμ2⟩ := hext.1
have hmean : ∑ x ∈ T, w x * x = 0 := by
simpa only [smul_eq_mul] using
(integral_discreteMeasure hwnn (fun x => x)).symm.trans hμmean
have hsec : ∑ x ∈ T, w x * x ^ 2 = s := by
simpa only [smul_eq_mul] using
(integral_discreteMeasure hwnn (fun x => x ^ 2)).symm.trans hμ2
have huniv : (discreteMeasure T w) univ = ofReal (∑ x ∈ T, w x) := by
rw [discreteMeasure, Measure.finset_sum_apply, ENNReal.ofReal_sum_of_nonneg hwnn]
apply Finset.sum_congr rfl; intro x hx; rw [Measure.smul_apply, smul_eq_mul]; simp
have hmass : ∑ x ∈ T, w x = 1 := by
have h1 := hμprob.measure_univ; rw [huniv] at h1; exact ENNReal.ofReal_eq_one.mp h1
have hTne : T.Nonempty := Finset.card_pos.mp (by omega)
set ε : ℝ := T.inf' hTne (fun x => w x / (|δ x| + 1)) with hεdef
have hεpos : 0 < ε := by
rw [hεdef, Finset.lt_inf'_iff]; intro x hx; have := hpos x hx; positivity
have hbound : ∀ x ∈ T, |ε * δ x| ≤ w x := by
intro x hx
rw [abs_mul, abs_of_pos hεpos]
have hle : ε ≤ w x / (|δ x| + 1) := Finset.inf'_le _ hx
have hden : (0 : ℝ) < |δ x| + 1 := by positivity
rw [le_div_iff₀ hden] at hle
nlinarith [hεpos, abs_nonneg (δ x)]
set wp : ℝ → ℝ := fun x => w x + ε * δ x with hwp
set wm : ℝ → ℝ := fun x => w x - ε * δ x with hwm
have hwpnn : ∀ x ∈ T, 0 ≤ wp x := by
intro x hx; have := (abs_le.mp (hbound x hx)).1; simp only [hwp]; linarith
have hwmnn : ∀ x ∈ T, 0 ≤ wm x := by
intro x hx; have := (abs_le.mp (hbound x hx)).2; simp only [hwm]; linarith
have hsump : ∑ x ∈ T, wp x = 1 := by
simp only [hwp, Finset.sum_add_distrib, ← Finset.mul_sum, hδ0, mul_zero, add_zero, hmass]
have hsumm : ∑ x ∈ T, wm x = 1 := by
simp only [hwm, Finset.sum_sub_distrib, ← Finset.mul_sum, hδ0, mul_zero, sub_zero, hmass]
have hmeanp : ∑ x ∈ T, wp x * x = 0 := by
simp only [hwp, add_mul]
rw [Finset.sum_add_distrib, hmean, zero_add]
rw [show (∑ x ∈ T, ε * δ x * x) = ε * ∑ x ∈ T, δ x * x by rw [Finset.mul_sum]; ring_nf,
hδ1, mul_zero]
have hmeanm : ∑ x ∈ T, wm x * x = 0 := by
simp only [hwm, sub_mul]
rw [Finset.sum_sub_distrib, hmean, zero_sub]
rw [show (∑ x ∈ T, ε * δ x * x) = ε * ∑ x ∈ T, δ x * x by rw [Finset.mul_sum]; ring_nf,
hδ1, mul_zero, neg_zero]
have hsecp : ∑ x ∈ T, wp x * x ^ 2 = s := by
simp only [hwp, add_mul]
rw [Finset.sum_add_distrib, hsec]
rw [show (∑ x ∈ T, ε * δ x * x ^ 2) = ε * ∑ x ∈ T, δ x * x ^ 2 by rw [Finset.mul_sum]; ring_nf,
hδ2, mul_zero, add_zero]
have hsecm : ∑ x ∈ T, wm x * x ^ 2 = s := by
simp only [hwm, sub_mul]
rw [Finset.sum_sub_distrib, hsec]
rw [show (∑ x ∈ T, ε * δ x * x ^ 2) = ε * ∑ x ∈ T, δ x * x ^ 2 by rw [Finset.mul_sum]; ring_nf,
hδ2, mul_zero, sub_zero]
have hmemp : discreteMeasure T wp ∈ MomentSlice a b s :=
⟨isProbabilityMeasure_discreteMeasure hwpnn hsump,
discreteMeasure_apply_compl_of_subset (K := Icc a b) hTab,
by rw [integral_discreteMeasure hwpnn (fun x => x)]; simpa only [smul_eq_mul] using hmeanp,
by rw [integral_discreteMeasure hwpnn (fun x => x ^ 2)]; simpa only [smul_eq_mul] using hsecp⟩
have hmemm : discreteMeasure T wm ∈ MomentSlice a b s :=
⟨isProbabilityMeasure_discreteMeasure hwmnn hsumm,
discreteMeasure_apply_compl_of_subset (K := Icc a b) hTab,
by rw [integral_discreteMeasure hwmnn (fun x => x)]; simpa only [smul_eq_mul] using hmeanm,
by rw [integral_discreteMeasure hwmnn (fun x => x ^ 2)]; simpa only [smul_eq_mul] using hsecm⟩
have hmid : ∀ x ∈ T, w x = (1 / 2) * wp x + (1 / 2) * wm x := by
intro x hx; simp only [hwp, hwm]; ring
have hmideq := discreteMeasure_midpoint hwpnn hwmnn hmid
have hne : discreteMeasure T wp ≠ discreteMeasure T wm := by
intro heq
have h1 := discreteMeasure_singleton (w := wp) hx₀T
have h2 := discreteMeasure_singleton (w := wm) hx₀T
rw [heq, h2] at h1
have hwx : wm x₀ = wp x₀ := by
have := congrArg toReal h1
rwa [ENNReal.toReal_ofReal (hwmnn x₀ hx₀T), ENNReal.toReal_ofReal (hwpnn x₀ hx₀T)] at this
simp only [hwp, hwm] at hwx
have hz : ε * δ x₀ = 0 := by linarith
rcases mul_eq_zero.mp hz with h | h
· exact hεpos.ne' h
· exact hx₀ne h
have ht : (1 : ℝ≥0∞) - 1 / 2 = 1 / 2 :=
ENNReal.sub_eq_of_eq_add (by simp) (ENNReal.add_halves 1).symm
refine absurd (hext.2 _ hmemp _ hmemm (1 / 2) (by norm_num) (by norm_num) ?_) hne
rw [ht]; exact hmideq
11 supporting declarations (lemmas, instances)
-
exists_moment_perturbationtheorem — Three-moment perturbation. On any finite set T ⊆ ℝ of more than three points there is a nonzero real weighting δ whose total mass, first moment and second moment all vanish. This is rank–nullity: three linear functionals (∑ δ, ∑ δ·x, ∑ δ·x²) on a space of dimension > 3 have a nonzero common kernel.hypothesesT :Finset ℝhT :3 < T.cardconclusion∃ δ : ℝ → ℝ,conclusion 1∑ x ∈ T, δ x = 0conclusion 2∑ x ∈ T, δ x * x = 0conclusion 3∑ x ∈ T, δ x * x ^ 2 = 0conclusion 4∃ x ∈ T, δ x ≠ 0Proof (Lean source)
theorem exists_moment_perturbation {T : Finset ℝ} (hT : 3 < T.card) : ∃ δ : ℝ → ℝ, (∑ x ∈ T, δ x = 0) ∧ (∑ x ∈ T, δ x * x = 0) ∧ (∑ x ∈ T, δ x * x ^ 2 = 0) ∧ (∃ x ∈ T, δ x ≠ 0) := by classical set φ : ℝ → (Fin 2 → ℝ) := fun x => ![x, x ^ 2] with hφ have hφinj : Injective φ := by intro x y h; have := congrFun h 0; simpa [hφ] using this have hinjOn : InjOn φ T := hφinj.injOn have hcard : finrank ℝ (Fin 2 → ℝ) + 1 < (T.image φ).card := by rw [Finset.card_image_of_injOn hinjOn, Module.finrank_pi]; simpa using hT obtain ⟨g, hsum0, hgsum, v, hv, hvne⟩ := Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card hcard rw [Finset.sum_image hinjOn] at hgsum hsum0 have h0 := congrFun hsum0 0 have h1 := congrFun hsum0 1 simp only [Finset.sum_apply, Pi.smul_apply, Pi.zero_apply, smul_eq_mul, hφ, Matrix.cons_val_zero, Matrix.cons_val_one] at h0 h1 obtain ⟨x, hxT, hxne⟩ : ∃ x ∈ T, g (φ x) ≠ 0 := by rw [mem_image] at hv; obtain ⟨x, hxT, rfl⟩ := hv; exact ⟨x, hxT, hvne⟩ exact ⟨fun x => g (φ x), hgsum, h0, h1, x, hxT, hxne⟩ -
discreteMeasure_apply_compl_of_subsettheorem — A discrete measure whose atoms all lie in a set gives zero mass to that set's complement.Proof (Lean source)
theorem discreteMeasure_apply_compl_of_subset {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] {T : Finset α} {w : α → ℝ} {K : Set α} (hTK : ∀ x ∈ T, x ∈ K) : discreteMeasure T w Kᶜ = 0 := by rw [discreteMeasure, Measure.finset_sum_apply] apply Finset.sum_eq_zero intro x hx rw [Measure.smul_apply, Measure.dirac_apply, smul_eq_mul] have : x ∉ Kᶜ := by simp [hTK x hx] simp [this] -
isProbabilityMeasure_discreteMeasuretheorem — A finite discrete measure is a probability measure when all atom weights are nonnegative and their sum is one.hypothesesconclusionProof (Lean source)
theorem isProbabilityMeasure_discreteMeasure {α : Type*} [MeasurableSpace α] {T : Finset α} {w : α → ℝ} (hw : ∀ x ∈ T, 0 ≤ w x) (hsum : ∑ x ∈ T, w x = 1) : IsProbabilityMeasure (discreteMeasure T w) := by constructor rw [discreteMeasure, Measure.finset_sum_apply] have : ∀ x ∈ T, (ofReal (w x) • Measure.dirac x) univ = ofReal (w x) := by intro x hx; rw [Measure.smul_apply, smul_eq_mul]; simp rw [Finset.sum_congr rfl this, ← ENNReal.ofReal_sum_of_nonneg hw, hsum, ENNReal.ofReal_one] -
integral_discreteMeasuretheorem — Integral against a discrete measure is the weighted sum of the integrand over the atoms. Every function into a real normed vector space is integrable because the measure has finite support.hypothesesconclusion∫ x, f x ∂(discreteMeasure T w) = ∑ x ∈ T, w x • f xProof (Lean source)
theorem integral_discreteMeasure {α E : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {T : Finset α} {w : α → ℝ} (hw : ∀ x ∈ T, 0 ≤ w x) (f : α → E) : ∫ x, f x ∂(discreteMeasure T w) = ∑ x ∈ T, w x • f x := by rw [discreteMeasure, integral_finset_sum_measure] · apply Finset.sum_congr rfl intro x hx rw [integral_smul_measure, integral_dirac, ENNReal.toReal_ofReal (hw x hx)] · intro x hx exact (integrable_dirac enorm_lt_top).smul_measure (by simp) -
discreteMeasure_singletontheorem — The mass assigned by a finite discrete measure to an atom in its support is the corresponding atom weight, coerced to ℝ≥0∞.Proof (Lean source)
theorem discreteMeasure_singleton {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] {T : Finset α} {w : α → ℝ} {x₀ : α} (hx₀ : x₀ ∈ T) : discreteMeasure T w {x₀} = ofReal (w x₀) := by classical rw [discreteMeasure, Measure.finset_sum_apply] have : ∀ x ∈ T, (ofReal (w x) • Measure.dirac x) {x₀} = if x = x₀ then ofReal (w x) else 0 := by intro x hx rw [Measure.smul_apply, Measure.dirac_apply, smul_eq_mul] by_cases h : x = x₀ <;> simp [h, Set.mem_singleton_iff] rw [Finset.sum_congr rfl this, Finset.sum_ite_eq' T x₀ (fun x => ofReal (w x))] simp [hx₀] -
discreteMeasure_midpointtheorem — A discrete measure whose atom weights are the pointwise average of two nonnegative weightings is the midpoint of the two corresponding discrete measures.hypothesesα :hp :∀ x ∈ T, 0 ≤ wp xhm :∀ x ∈ T, 0 ≤ wm xhmid :∀ x ∈ T, w x = (1 / 2) * wp x + (1 / 2) * wm xconclusiondiscreteMeasure T w= (1 / 2 : ℝ≥0∞) • discreteMeasure T wp + (1 / 2 : ℝ≥0∞) • discreteMeasure T wmProof (Lean source)
theorem discreteMeasure_midpoint {α : Type*} [MeasurableSpace α] {T : Finset α} {w wp wm : α → ℝ} (hp : ∀ x ∈ T, 0 ≤ wp x) (hm : ∀ x ∈ T, 0 ≤ wm x) (hmid : ∀ x ∈ T, w x = (1 / 2) * wp x + (1 / 2) * wm x) : discreteMeasure T w = (1 / 2 : ℝ≥0∞) • discreteMeasure T wp + (1 / 2 : ℝ≥0∞) • discreteMeasure T wm := by rw [discreteMeasure, discreteMeasure, discreteMeasure, Finset.smul_sum, Finset.smul_sum, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro x hx rw [smul_smul, smul_smul, ← add_smul] congr 1 have e2 : (1 / 2 : ℝ≥0∞) = ofReal (1 / 2) := by rw [ENNReal.ofReal_div_of_pos] <;> simp rw [e2, ← ENNReal.ofReal_mul (by norm_num), ← ENNReal.ofReal_mul (by norm_num), ← ENNReal.ofReal_add (mul_nonneg (by norm_num) (hp x hx)) (mul_nonneg (by norm_num) (hm x hx)), ← hmid x hx] -
exists_isMinOn_momentSlicetheorem — Attainment of the minimum over a moment slice. On a compact Hausdorff space Ω, the set of probability measures pinned by two bounded-continuous moment constraints ∫ g₁ = c₁, ∫ g₂ = c₂ is weak-* compact, so any bounded-continuous objective ∫ f attains its minimum over that (nonempty) slice. The number of constraints is immaterial; the two-moment case is stated to match the mean/second-moment slice.hypothesesΩ :g₁ g₂ f :Ω →ᵇ ℝc₁ c₂ :ℝhne :{μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂}.Nonemptyconclusion∃ μ ∈ {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂},∀ ν ∈ {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂},Proof (Lean source)
theorem exists_isMinOn_momentSlice {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [T2Space Ω] [BorelSpace Ω] [CompactSpace Ω] (g₁ g₂ f : Ω →ᵇ ℝ) (c₁ c₂ : ℝ) (hne : {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂}.Nonempty) : ∃ μ ∈ {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂}, ∀ ν ∈ {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂}, ∫ x, f x ∂(μ : Measure Ω) ≤ ∫ x, f x ∂(ν : Measure Ω) := by set C := {μ : ProbabilityMeasure Ω | ∫ x, g₁ x ∂μ = c₁ ∧ ∫ x, g₂ x ∂μ = c₂} with hC have hcont1 : Continuous fun μ : ProbabilityMeasure Ω => ∫ x, g₁ x ∂μ := ProbabilityMeasure.continuous_integral_boundedContinuousFunction g₁ have hcont2 : Continuous fun μ : ProbabilityMeasure Ω => ∫ x, g₂ x ∂μ := ProbabilityMeasure.continuous_integral_boundedContinuousFunction g₂ have hcontf : Continuous fun μ : ProbabilityMeasure Ω => ∫ x, f x ∂μ := ProbabilityMeasure.continuous_integral_boundedContinuousFunction f have hCclosed : IsClosed C := by have : C = (fun μ : ProbabilityMeasure Ω => ∫ x, g₁ x ∂μ) ⁻¹' {c₁} ∩ (fun μ : ProbabilityMeasure Ω => ∫ x, g₂ x ∂μ) ⁻¹' {c₂} := rfl rw [this] exact (isClosed_singleton.preimage hcont1).inter (isClosed_singleton.preimage hcont2) have hCcompact : IsCompact C := hCclosed.isCompact obtain ⟨μ, hμC, hmin⟩ := hCcompact.exists_isMinOn hne hcontf.continuousOn exact ⟨μ, hμC, fun ν hν => hmin hν⟩ -
not_four_distinct_in_supporttheorem — An extreme probability measure in the two-moment slice cannot have four distinct support points. Four separated neighborhoods would give a nonzero signed perturbation preserving mass, mean, and second moment, so the measure would be the midpoint of two different slice members.hypothesesa b s :ℝμ :Measure ℝhext :IsExtremePoint (MomentSlice a b s) μx :Fin 4 → ℝhinj :hsupp :∀ i, x i ∈ μ.supportconclusionProof (Lean source)
theorem not_four_distinct_in_support {a b s : ℝ} {μ : Measure ℝ} (hext : IsExtremePoint (MomentSlice a b s) μ) (x : Fin 4 → ℝ) (hinj : Injective x) (hsupp : ∀ i, x i ∈ μ.support) : False := by classical obtain ⟨hprob, hcompl, hmean, hsec⟩ := hext.1 -- (a) integrability of `id` and `t^2` against the probability measure `μ`. have hbdd : ∀ᵐ t ∂μ, t ∈ Icc a b := by rw [ae_iff]; exact hcompl set C : ℝ := max |a| |b| with hC_def have hCnn : 0 ≤ C := le_trans (abs_nonneg a) (le_max_left _ _) have hbound1 : ∀ᵐ t ∂μ, ‖(fun t => t) t‖ ≤ (fun _ => C) t := by filter_upwards [hbdd] with t ht obtain ⟨hat, htb⟩ := ht simp only [Real.norm_eq_abs] rw [abs_le] refine ⟨?_, ?_⟩ · have h1 : -|a| ≤ a := neg_abs_le a have h2 : |a| ≤ C := le_max_left _ _ linarith · have h1 : b ≤ |b| := le_abs_self b have h2 : |b| ≤ C := le_max_right _ _ linarith have hint1 : Integrable (fun t => t) μ := (integrable_const C).mono' (by fun_prop) hbound1 have hbound2 : ∀ᵐ t ∂μ, ‖(fun t => t ^ 2) t‖ ≤ (fun _ => C ^ 2) t := by filter_upwards [hbound1] with t ht simp only [Real.norm_eq_abs] at ht ⊢ rw [abs_pow] nlinarith [abs_nonneg t, ht, hCnn] have hint2 : Integrable (fun t => t ^ 2) μ := (integrable_const (C ^ 2)).mono' (by fun_prop) hbound2 -- (b) four pairwise-disjoint open balls around the support points. have hdist_pos : ∀ i j, i ≠ j → 0 < dist (x i) (x j) := fun i j hij => dist_pos.mpr (fun h => hij (hinj h)) set r : ℝ := (Finset.univ.inf' Finset.univ_nonempty (fun p : Fin 4 × Fin 4 => if p.1 = p.2 then (1 : ℝ) else dist (x p.1) (x p.2))) / 2 with hr_def have hr_pos : 0 < r := by have hpos : 0 < Finset.univ.inf' Finset.univ_nonempty (fun p : Fin 4 × Fin 4 => if p.1 = p.2 then (1 : ℝ) else dist (x p.1) (x p.2)) := by rw [Finset.lt_inf'_iff] intro p _ by_cases hp : p.1 = p.2 · simp [hp] · simp only [hp, if_false]; exact hdist_pos p.1 p.2 hp rw [hr_def]; linarith have hr_le : ∀ i j, i ≠ j → 2 * r ≤ dist (x i) (x j) := by intro i j hij have hle := Finset.inf'_le (fun p : Fin 4 × Fin 4 => if p.1 = p.2 then (1 : ℝ) else dist (x p.1) (x p.2)) (Finset.mem_univ (i, j)) simp only [hij, if_false] at hle rw [hr_def]; linarith set U : Fin 4 → Set ℝ := fun i => ball (x i) r with hU_def have hUopen : ∀ i, IsOpen (U i) := fun i => Metric.isOpen_ball have hxU : ∀ i, x i ∈ U i := fun i => Metric.mem_ball_self hr_pos have hUdisj : Pairwise (onFun Disjoint U) := by intro i j hij refine Metric.ball_disjoint_ball ?_ have := hr_le i j hij; linarith have hUmeas : ∀ i, MeasurableSet (U i) := fun i => (hUopen i).measurableSet have hUpos : ∀ i, 0 < μ (U i) := fun i => (Measure.mem_support_iff_forall (x i)).1 (hsupp i) (U i) ((hUopen i).mem_nhds (hxU i)) have hUne : ∀ i, μ (U i) ≠ ∞ := fun i => measure_ne_top μ (U i) -- (d)–(e) linear dependence of the four restriction moment vectors in ℝ³. set v : Fin 4 → (Fin 3 → ℝ) := fun i => ![(μ (U i)).toReal, ∫ t in U i, t ∂μ, ∫ t in U i, t ^ 2 ∂μ] with hv_def have hdep : ¬ LinearIndependent ℝ v := by intro hli have hcard := hli.fintype_card_le_finrank simp only [Fintype.card_fin, Module.finrank_pi] at hcard omega rw [Fintype.not_linearIndependent_iff] at hdep obtain ⟨g, hgsum, i₀, hi₀⟩ := hdep have H0 : ∑ i, g i * (μ (U i)).toReal = 0 := by have h := congrFun hgsum 0 simpa [Finset.sum_apply, Pi.smul_apply, hv_def, smul_eq_mul] using h have H1 : ∑ i, g i * (∫ t in U i, t ∂μ) = 0 := by have h := congrFun hgsum 1 simpa [Finset.sum_apply, Pi.smul_apply, hv_def, smul_eq_mul] using h have H2 : ∑ i, g i * (∫ t in U i, t ^ 2 ∂μ) = 0 := by have h := congrFun hgsum 2 simpa [Finset.sum_apply, Pi.smul_apply, hv_def, smul_eq_mul] using h -- (f) small step size keeping all perturbed weights nonnegative. set Mg : ℝ := Finset.univ.sup' Finset.univ_nonempty (fun i => |g i|) with hMg_def have hMgnn : 0 ≤ Mg := le_trans (abs_nonneg (g i₀)) (Finset.le_sup' (fun i => |g i|) (Finset.mem_univ i₀)) set ε : ℝ := 1 / (2 * (1 + Mg)) with hε_def have hden : 0 < 2 * (1 + Mg) := by positivity have hε_pos : 0 < ε := by rw [hε_def]; positivity have hε_bound : ∀ i, ε * |g i| ≤ 1 / 2 := by intro i have hgi : |g i| ≤ Mg := Finset.le_sup' (fun i => |g i|) (Finset.mem_univ i) have heq : ε * |g i| = |g i| / (2 * (1 + Mg)) := by rw [hε_def]; ring rw [heq, div_le_iff₀ hden]; nlinarith have hcoef_pos : ∀ (σ : ℝ), |σ| ≤ 1 → ∀ i, 0 ≤ 1 + σ * ε * g i := by intro σ hσ i have h1 : |σ * ε * g i| ≤ 1 / 2 := by have heq : |σ * ε * g i| = |σ| * (ε * |g i|) := by rw [abs_mul, abs_mul, abs_of_pos hε_pos]; ring rw [heq] calc |σ| * (ε * |g i|) ≤ 1 * (1 / 2) := mul_le_mul hσ (hε_bound i) (by positivity) (by norm_num) _ = 1 / 2 := by norm_num have := (abs_le.mp h1).1; linarith -- (g) measure decomposition over the disjoint cover. set W : Set ℝ := ⋃ i, U i with hW_def have hWmeas : MeasurableSet W := MeasurableSet.iUnion hUmeas have hrestrictW : μ.restrict W = ∑ i, μ.restrict (U i) := by rw [hW_def, Measure.restrict_iUnion hUdisj hUmeas, Measure.sum_fintype] have hdecomp : μ = μ.restrict Wᶜ + ∑ i, μ.restrict (U i) := by rw [← hrestrictW, add_comm] exact (Measure.restrict_add_restrict_compl hWmeas).symm -- (h) the two perturbed measures. set pert : ℝ → Measure ℝ := fun σ => μ.restrict Wᶜ + ∑ i, ofReal (1 + σ * ε * g i) • μ.restrict (U i) with hpert_def have hpert_integral : ∀ (σ : ℝ), |σ| ≤ 1 → ∀ (f : ℝ → ℝ), Integrable f μ → ∫ t, f t ∂(pert σ) = (∫ t in Wᶜ, f t ∂μ) + ∑ i, (1 + σ * ε * g i) * (∫ t in U i, f t ∂μ) := by intro σ hσ f hf have hsum_int : Integrable f (∑ i, ofReal (1 + σ * ε * g i) • μ.restrict (U i)) := (integrable_finset_sum_measure).2 (fun i _ => (hf.restrict).smul_measure ENNReal.ofReal_ne_top) rw [hpert_def, integral_add_measure hf.restrict hsum_int, integral_finset_sum_measure (fun i _ => (hf.restrict).smul_measure ENNReal.ofReal_ne_top)] congr 1 apply Finset.sum_congr rfl intro i _ rw [integral_smul_measure, ENNReal.toReal_ofReal (hcoef_pos σ hσ i), smul_eq_mul] have hsplit : ∀ (f : ℝ → ℝ), Integrable f μ → (∫ t in Wᶜ, f t ∂μ) + ∑ i, (∫ t in U i, f t ∂μ) = ∫ t, f t ∂μ := by intro f hf conv_rhs => rw [hdecomp] rw [integral_add_measure hf.restrict ((integrable_finset_sum_measure).2 (fun i _ => hf.restrict)), integral_finset_sum_measure (fun i _ => hf.restrict)] have hmass1 : (μ Wᶜ).toReal + ∑ i, (μ (U i)).toReal = 1 := by have hsplit1 := hsplit (fun _ => (1 : ℝ)) (integrable_const 1) simpa [setIntegral_const, integral_const, hprob.measure_univ, measureReal_def] using hsplit1 have hpert_mem : ∀ (σ : ℝ), |σ| ≤ 1 → pert σ ∈ MomentSlice a b s := by intro σ hσ have hmean' : ∫ t, t ∂(pert σ) = 0 := by rw [hpert_integral σ hσ (fun t => t) hint1] have hcollect : (∫ t in Wᶜ, t ∂μ) + ∑ i, (1 + σ * ε * g i) * (∫ t in U i, t ∂μ) = ((∫ t in Wᶜ, t ∂μ) + ∑ i, (∫ t in U i, t ∂μ)) + σ * ε * ∑ i, g i * (∫ t in U i, t ∂μ) := by rw [add_assoc] congr 1 rw [Finset.mul_sum, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl; intro i _; ring rw [hcollect, hsplit (fun t => t) hint1, hmean, H1]; ring have hsec' : ∫ t, t ^ 2 ∂(pert σ) = s := by rw [hpert_integral σ hσ (fun t => t ^ 2) hint2] have hcollect : (∫ t in Wᶜ, t ^ 2 ∂μ) + ∑ i, (1 + σ * ε * g i) * (∫ t in U i, t ^ 2 ∂μ) = ((∫ t in Wᶜ, t ^ 2 ∂μ) + ∑ i, (∫ t in U i, t ^ 2 ∂μ)) + σ * ε * ∑ i, g i * (∫ t in U i, t ^ 2 ∂μ) := by rw [add_assoc] congr 1 rw [Finset.mul_sum, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl; intro i _; ring rw [hcollect, hsplit (fun t => t ^ 2) hint2, hsec, H2]; ring have hsupp' : (pert σ) (Icc a b)ᶜ = 0 := by rw [hpert_def] simp only [Measure.add_apply, Measure.finset_sum_apply, Measure.smul_apply, smul_eq_mul] have hWc : μ.restrict Wᶜ (Icc a b)ᶜ = 0 := by rw [Measure.restrict_apply measurableSet_Icc.compl] exact le_antisymm (le_trans (measure_mono Set.inter_subset_left) (le_of_eq hcompl)) zero_le have hUc : ∀ i, μ.restrict (U i) (Icc a b)ᶜ = 0 := by intro i rw [Measure.restrict_apply measurableSet_Icc.compl] exact le_antisymm (le_trans (measure_mono Set.inter_subset_left) (le_of_eq hcompl)) zero_le rw [hWc, zero_add] apply Finset.sum_eq_zero intro i _ rw [hUc i, mul_zero] have hprob' : IsProbabilityMeasure (pert σ) := by refine ⟨?_⟩ rw [hpert_def] simp only [Measure.add_apply, Measure.finset_sum_apply, Measure.smul_apply, smul_eq_mul, Measure.restrict_apply_univ] have hreg : ∀ i, (1 + σ * ε * g i) * (μ (U i)).toReal = (μ (U i)).toReal + (σ * ε) * (g i * (μ (U i)).toReal) := by intro i; ring have hreal : (μ Wᶜ).toReal + ∑ i, (1 + σ * ε * g i) * (μ (U i)).toReal = 1 := by rw [Finset.sum_congr rfl (fun i _ => hreg i), Finset.sum_add_distrib, ← Finset.mul_sum, H0, mul_zero, add_zero] exact hmass1 have hWfin : μ Wᶜ ≠ ∞ := measure_ne_top μ _ have hnn : (0 : ℝ) ≤ ∑ i, (1 + σ * ε * g i) * (μ (U i)).toReal := sum_nonneg (fun i _ => mul_nonneg (hcoef_pos σ hσ i) ENNReal.toReal_nonneg) calc μ Wᶜ + ∑ i, ofReal (1 + σ * ε * g i) * μ (U i) = ofReal ((μ Wᶜ).toReal + ∑ i, (1 + σ * ε * g i) * (μ (U i)).toReal) := by rw [ENNReal.ofReal_add ENNReal.toReal_nonneg hnn, ENNReal.ofReal_toReal hWfin] congr 1 rw [ENNReal.ofReal_sum_of_nonneg (fun i _ => mul_nonneg (hcoef_pos σ hσ i) ENNReal.toReal_nonneg)] apply Finset.sum_congr rfl intro i _ rw [ENNReal.ofReal_mul (hcoef_pos σ hσ i), ENNReal.ofReal_toReal (hUne i)] _ = ofReal 1 := by rw [hreal] _ = 1 := by simp exact ⟨hprob', hsupp', hmean', hsec'⟩ -- (j) the two perturbations are distinct, witnessed on `U i₀`. have hval : ∀ (σ : ℝ), (pert σ) (U i₀) = ofReal (1 + σ * ε * g i₀) * μ (U i₀) := by intro σ rw [hpert_def] simp only [Measure.add_apply, Measure.finset_sum_apply, Measure.smul_apply, smul_eq_mul] have hsubW : U i₀ ⊆ W := fun y hy => Set.mem_iUnion.2 ⟨i₀, hy⟩ have hWc0 : μ.restrict Wᶜ (U i₀) = 0 := by rw [Measure.restrict_apply (hUmeas i₀)] rw [(disjoint_compl_right.mono_left hsubW).inter_eq, measure_empty] have hUi : ∀ j, μ.restrict (U j) (U i₀) = if j = i₀ then μ (U i₀) else 0 := by intro j rw [Measure.restrict_apply (hUmeas i₀)] by_cases hji : j = i₀ · subst hji; rw [Set.inter_self]; simp · have hdis : Disjoint (U i₀) (U j) := hUdisj (fun h => hji h.symm) rw [hdis.inter_eq, measure_empty]; simp [hji] rw [hWc0, zero_add, Finset.sum_eq_single i₀ (fun j _ hj => by rw [hUi j]; simp [hj]) (fun h => absurd (Finset.mem_univ i₀) h)] rw [hUi i₀]; simp have hdistinct : pert 1 ≠ pert (-1) := by intro heq have e1 := hval 1 have e2 := hval (-1) rw [heq] at e1 rw [e1] at e2 -- e2 : ofReal (1+1εg i₀) * μ (U i₀) = ofReal (1+(-1)εg i₀) * μ (U i₀) have hreal := congrArg toReal e2 rw [ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (hcoef_pos 1 (by norm_num) i₀), ENNReal.toReal_ofReal (hcoef_pos (-1) (by norm_num) i₀)] at hreal have hpos : 0 < (μ (U i₀)).toReal := ENNReal.toReal_pos (hUpos i₀).ne' (hUne i₀) have hz : ε * g i₀ = 0 := by have h2 : (ε * g i₀) * (μ (U i₀)).toReal = 0 := by linear_combination hreal / 2 -- … truncated; follow the source link for the rest … -
support_finite_ncard_le_three_of_isExtremePointtheorem — An extreme probability measure in the two-moment slice has a finite topological support with at most three points.hypothesesconclusionconclusion 1μ.support.Finiteconclusion 2μ.support.ncard ≤ 3Proof (Lean source)
theorem support_finite_ncard_le_three_of_isExtremePoint {a b s : ℝ} {μ : Measure ℝ} (hext : IsExtremePoint (MomentSlice a b s) μ) : μ.support.Finite ∧ μ.support.ncard ≤ 3 := by classical let S : Set ℝ := μ.support have hno : ∀ (y : Fin 4 → ℝ), Injective y → (∀ i, y i ∈ S) → False := by intro y hyinj hysupp exact not_four_distinct_in_support hext y hyinj hysupp constructor · by_contra hinf have hInf : S.Infinite := by simpa [S, Set.not_finite] using hinf obtain ⟨t, hts, htfin, htc⟩ := hInf.exists_subset_ncard_eq 4 have hcard : htfin.toFinset.card = 4 := by simpa [Set.ncard_eq_toFinset_card t htfin] using htc let e : Fin 4 ↪o ℝ := htfin.toFinset.orderEmbOfFin hcard exact hno (fun i => e i) e.injective (fun i => by have hmemFin : e i ∈ htfin.toFinset := by change htfin.toFinset.orderEmbOfFin hcard i ∈ htfin.toFinset exact Finset.orderEmbOfFin_mem htfin.toFinset hcard i exact hts (by simpa [Set.Finite.mem_toFinset] using hmemFin)) · by_contra hle push_neg at hle have h4 : 4 ≤ S.ncard := Nat.succ_le_of_lt hle obtain ⟨t, hts, htc⟩ := Set.exists_subset_card_eq (s := S) h4 have htfin : t.Finite := Set.finite_of_ncard_ne_zero (by rw [htc]; simp) have hcard : htfin.toFinset.card = 4 := by simpa [Set.ncard_eq_toFinset_card t htfin] using htc let e : Fin 4 ↪o ℝ := htfin.toFinset.orderEmbOfFin hcard exact hno (fun i => e i) e.injective (fun i => by have hmemFin : e i ∈ htfin.toFinset := by change htfin.toFinset.orderEmbOfFin hcard i ∈ htfin.toFinset exact Finset.orderEmbOfFin_mem htfin.toFinset hcard i exact hts (by simpa [Set.Finite.mem_toFinset] using hmemFin)) -
isAtomic_le_three_of_isExtremePointtheorem — An extreme probability measure in the two-moment slice is a positive discrete measure supported on at most three points of the interval.hypothesesconclusion∃ (T : Finset ℝ) (w : ℝ → ℝ),conclusion 1x ∈ T :0 < w xconclusion 3T.card ≤ 3conclusion 4μ = discreteMeasure T wProof (Lean source)
theorem isAtomic_le_three_of_isExtremePoint {a b s : ℝ} {μ : Measure ℝ} (hext : IsExtremePoint (MomentSlice a b s) μ) : ∃ (T : Finset ℝ) (w : ℝ → ℝ), (∀ x ∈ T, 0 < w x) ∧ (∀ x ∈ T, x ∈ Icc a b) ∧ T.card ≤ 3 ∧ μ = discreteMeasure T w := by classical obtain ⟨hprob, hcompl, _, _⟩ := hext.1 obtain ⟨hsuppfin, hsuppcard⟩ := support_finite_ncard_le_three_of_isExtremePoint hext let T : Finset ℝ := hsuppfin.toFinset let w : ℝ → ℝ := fun x => (μ {x}).toReal have hTsupport : (T : Set ℝ) = μ.support := by simp [T] have hTcard : T.card ≤ 3 := by have hcard : T.card = μ.support.ncard := by simp [T, Set.ncard_eq_toFinset_card μ.support hsuppfin] omega have hsingle_pos : ∀ x ∈ μ.support, 0 < μ {x} := by intro x hx let V : Set ℝ := (μ.support \ {x})ᶜ have hVopen : IsOpen V := (hsuppfin.diff (t := ({x} : Set ℝ))).isClosed.isOpen_compl have hxV : x ∈ V := by simp [V] have hVpos : 0 < μ V := (Measure.mem_support_iff_forall x).1 hx V (hVopen.mem_nhds hxV) have hVS : V ∩ μ.support = {x} := by ext y by_cases hyx : y = x · subst hyx simp [V, hx] · simp [V, hyx] have hconull : μ μ.supportᶜ = 0 := Measure.measure_compl_support have hVeq : μ (V ∩ μ.support) = μ V := measure_inter_conull (μ := μ) (s := V) hconull rw [hVS] at hVeq rwa [hVeq] have hpos : ∀ x ∈ T, 0 < w x := by intro x hxT have hxS : x ∈ μ.support := hTsupport ▸ Finset.mem_coe.mpr hxT have hlt : μ {x} ≠ ∞ := by have hle : μ {x} ≤ μ univ := measure_mono (Set.subset_univ _) rw [hprob.measure_univ] at hle exact ne_top_of_le_ne_top ENNReal.one_ne_top hle have hxpos := hsingle_pos x hxS simpa only [w] using ENNReal.toReal_pos hxpos.ne' hlt have hTab : ∀ x ∈ T, x ∈ Icc a b := by intro x hxT by_contra hxnot have hxS : x ∈ μ.support := hTsupport ▸ Finset.mem_coe.mpr hxT have hxpos : 0 < μ {x} := hsingle_pos x hxS have hsub : ({x} : Set ℝ) ⊆ (Icc a b)ᶜ := by simpa [Set.subset_def] using hxnot have hle : μ {x} ≤ μ (Icc a b)ᶜ := measure_mono hsub rw [hcompl] at hle exact (ne_of_gt hxpos) (le_antisymm hle zero_le) refine ⟨T, w, hpos, hTab, hTcard, ?_⟩ refine Measure.ext fun A hA => ?_ have hconull : μ μ.supportᶜ = 0 := Measure.measure_compl_support have hAinter : μ (A ∩ μ.support) = μ A := measure_inter_conull (μ := μ) (s := A) hconull rw [← hAinter] have hUnion : A ∩ μ.support = ⋃ x ∈ T.filter (fun x => x ∈ A), ({x} : Set ℝ) := by ext y simp [T, Set.Finite.mem_toFinset, and_left_comm, and_assoc] rw [hUnion] rw [measure_biUnion_finset] · rw [discreteMeasure, Measure.finset_sum_apply, Finset.sum_filter] apply Finset.sum_congr rfl intro x hx rw [Measure.smul_apply, Measure.dirac_apply, smul_eq_mul] have hlt : μ {x} ≠ ∞ := by have hle : μ {x} ≤ μ univ := measure_mono (Set.subset_univ _) rw [hprob.measure_univ] at hle exact ne_top_of_le_ne_top ENNReal.one_ne_top hle by_cases hxA : x ∈ A · simp [hxA, w, ENNReal.ofReal_toReal hlt] · simp [hxA] · intro x _ y _ hxy exact Set.disjoint_singleton.2 hxy · intro x _ exact MeasurableSet.singleton x -
exists_cardSupportLe_three_of_isExtremePointtheorem — An extreme probability measure in the two-moment slice is carried by a finite set of at most three points.hypothesesProof (Lean source)
theorem exists_cardSupportLe_three_of_isExtremePoint {a b s : ℝ} {μ : Measure ℝ} (hext : IsExtremePoint (MomentSlice a b s) μ) : ∃ T : Finset ℝ, T.card ≤ 3 ∧ μ (↑T : Set ℝ)ᶜ = 0 := by classical obtain ⟨hsuppfin, hsuppcard⟩ := support_finite_ncard_le_three_of_isExtremePoint hext refine ⟨hsuppfin.toFinset, ?_, ?_⟩ · simpa [Set.ncard_eq_toFinset_card μ.support hsuppfin] using hsuppcard · rw [Set.Finite.coe_toFinset]; exact Measure.measure_compl_support
PartitionIntegral 2 core · 1 supporting This file decomposes integrals over the fibres of a finite-valued map with measurable fibres and proves that cell-constant weights can be pulled out fibre by fibre. ★ integral_eq_sum_setIntegral_fiber★ integral_cellConst_mul
Finite-partition integral algebra
This file decomposes integrals over the fibres of a finite-valued map with measurable fibres and
proves that cell-constant weights can be pulled out fibre by fibre. The public lemmas
are integral_eq_sum_setIntegral_fiber, integral_cellConst_mul, and
integral_cellConst, which turn a finite partition of a sample space into finite sums
of set integrals or cell weights.
theorem integral_eq_sum_setIntegral_fiber reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
If H is a finite-valued map on the sample space whose fibers H⁻¹{h} are all measurable and f is integrable with respect to the ambient measure, then the integral of f splits as the sum, over the finitely many values h of H, of the set integrals of f restricted to the fiber H⁻¹{h}.
Formal statement
hypotheses
conclusion
∫ ω, f ω ∂μ = ∑ h : ι, ∫ ω in H ⁻¹' {h}, f ω ∂μ
Proof (Lean source)
theorem integral_eq_sum_setIntegral_fiber {ι : Type*} [Fintype ι]
{H : Ω → ι} (hfiber : ∀ h, MeasurableSet (H ⁻¹' {h}))
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
{f : Ω → E} (hf : Integrable f μ) :
∫ ω, f ω ∂μ = ∑ h : ι, ∫ ω in H ⁻¹' {h}, f ω ∂μ := by
have hsplit :
∫ ω in ⋃ h, H ⁻¹' {h}, f ω ∂μ = ∑ h : ι, ∫ ω in H ⁻¹' {h}, f ω ∂μ :=
MeasureTheory.integral_iUnion_fintype hfiber
(pairwise_disjoint_fiber H) (fun _ => hf.integrableOn)
calc
∫ ω, f ω ∂μ = ∫ ω in (Set.univ : Set Ω), f ω ∂μ := by rw [setIntegral_univ]
_ = ∫ ω in ⋃ h, H ⁻¹' {h}, f ω ∂μ := by rw [iUnion_fiber]
_ = ∑ h : ι, ∫ ω in H ⁻¹' {h}, f ω ∂μ := hsplit
theorem integral_cellConst_mul reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Cell-constant pull-out. If H is a finite-valued map on the sample space whose fibers H⁻¹{h} are all measurable and f is integrable with respect to the ambient measure, then, for any weighting c of the fiber values, the integral of the ω-dependent product c (H ω) • f ω decomposes as the sum, over the values h of H, of c h scaling the set integral of f over the fiber H⁻¹{h}. No measurability of c is needed: on each fiber c (H ω) is the constant c h.
Formal statement
hypotheses
conclusion
∫ ω, c (H ω) • f ω ∂μ = ∑ h : ι, c h • ∫ ω in H ⁻¹' {h}, f ω ∂μ
Proof (Lean source)
theorem integral_cellConst_mul {ι : Type*} [Fintype ι]
{H : Ω → ι} (hfiber : ∀ h, MeasurableSet (H ⁻¹' {h})) (c : ι → ℝ)
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
{f : Ω → E} (hf : Integrable f μ) :
∫ ω, c (H ω) • f ω ∂μ = ∑ h : ι, c h • ∫ ω in H ⁻¹' {h}, f ω ∂μ := by
-- On each fiber the integrand equals the constant-multiple `c h • f`.
have hgint : ∀ h : ι, IntegrableOn (fun ω => c (H ω) • f ω) (H ⁻¹' {h}) μ := by
intro h
refine ((hf.smul (c h)).integrableOn).congr_fun ?_ (hfiber h)
intro ω hω
simp only [Set.mem_preimage, Set.mem_singleton_iff] at hω
simp [hω]
have hsplit :
∫ ω in ⋃ h, H ⁻¹' {h}, c (H ω) • f ω ∂μ
= ∑ h : ι, ∫ ω in H ⁻¹' {h}, c (H ω) • f ω ∂μ :=
MeasureTheory.integral_iUnion_fintype hfiber
(pairwise_disjoint_fiber H) hgint
calc
∫ ω, c (H ω) • f ω ∂μ
= ∫ ω in (Set.univ : Set Ω), c (H ω) • f ω ∂μ := by rw [setIntegral_univ]
_ = ∫ ω in ⋃ h, H ⁻¹' {h}, c (H ω) • f ω ∂μ := by rw [iUnion_fiber]
_ = ∑ h : ι, ∫ ω in H ⁻¹' {h}, c (H ω) • f ω ∂μ := hsplit
_ = ∑ h : ι, c h • ∫ ω in H ⁻¹' {h}, f ω ∂μ := by
refine Finset.sum_congr rfl fun h _ => ?_
have hcell :
∫ ω in H ⁻¹' {h}, c (H ω) • f ω ∂μ = ∫ ω in H ⁻¹' {h}, c h • f ω ∂μ := by
refine setIntegral_congr_fun (hfiber h) ?_
intro ω hω
simp only [Set.mem_preimage, Set.mem_singleton_iff] at hω
simp [hω]
rw [hcell, integral_smul]
1 supporting declaration (lemmas, instances)
-
integral_cellConsttheorem — Cell-weight aggregation. For a finite measure, the integral of a cell-constant function c (H ω) is the cell-weighted sum ∑ h, c h · μ(H⁻¹{h}). Special case of integral_cellConst_mul with f ≡ 1.hypothesesconclusion∫ ω, c (H ω) ∂μ = ∑ h : ι, c h * (μ (H ⁻¹' {h})).toRealProof (Lean source)
theorem integral_cellConst {ι : Type*} [Fintype ι] [IsFiniteMeasure μ] {H : Ω → ι} (hfiber : ∀ h, MeasurableSet (H ⁻¹' {h})) (c : ι → ℝ) : ∫ ω, c (H ω) ∂μ = ∑ h : ι, c h * (μ (H ⁻¹' {h})).toReal := by have h := integral_cellConst_mul hfiber c (f := fun _ => (1 : ℝ)) (hf := (integrable_const (1 : ℝ) : Integrable (fun _ : Ω => (1 : ℝ)) μ)) simpa [mul_one, setIntegral_const, smul_eq_mul, measureReal_def] using h
PartitionRnDeriv 2 core · 0 supporting This file proves two general measure-theoretic facts about a numerator measure μ that is a constant multiple of a denominator measure ν on each cell of a finite measurable partition (s i) of the ambient space (μ.restrict ★ partition_restrict_absolutelyContinuous★ partition_restrict_integrable_pow_rnDeriv
Radon–Nikodym derivative on a finite measurable partition
This file proves two general measure-theoretic facts about a numerator measure μ that is
a constant multiple of a denominator measure ν on each cell of a finite measurable
partition (s i) of the ambient space (μ.restrict (s i) = r i • ν.restrict (s i)):
* partition_restrict_absolutelyContinuous — μ ≪ ν (absolute continuity);
* partition_restrict_integrable_pow_rnDeriv — every natural-power deviation
((dμ/dν) − 1)^n of the Radon–Nikodym derivative from 1 is ν-integrable.
Both are the standard building blocks of a piecewise-constant least-favorable construction in a
two-point minimax lower bound: the per-cell density is the cell ratio, so the global density is
the simple function ∑ i, r i · 1_{s i}.
lemma partition_restrict_absolutelyContinuous reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Absolute continuity from a finite proportional partition. Suppose each cell s i of a finite family is measurable, the cells are pairwise disjoint, and the cells cover the whole ambient space — together, (s i) is a finite measurable partition — and suppose on every cell the numerator measure μ restricted to that cell equals the denominator measure ν restricted to the same cell, scaled by the constant r i. Then μ is absolutely continuous with respect to ν. The global density is the simple function whose value on cell i is r i, so μ = ν.withDensity d.
Formal statement
hypotheses
Ω :
Type*
ι :
Type*
Finite ι
μ ν :
Measure Ω
s :
ι → Set Ω
r :
ι → ENNReal
hs :
∀ i, MeasurableSet (s i)
hcover :
(⋃ i, s i) = univ
hrestrict :
∀ i, μ.restrict (s i) = r i • ν.restrict (s i)
conclusion
μ ≪ ν
Proof (Lean source)
lemma partition_restrict_absolutelyContinuous
{Ω : Type*} [MeasurableSpace Ω] {ι : Type*} [Finite ι]
(μ ν : Measure Ω)
(s : ι → Set Ω) (r : ι → ENNReal)
(hs : ∀ i, MeasurableSet (s i))
(hdisj : Pairwise (onFun Disjoint s))
(hcover : (⋃ i, s i) = univ)
(hrestrict : ∀ i, μ.restrict (s i) = r i • ν.restrict (s i)) :
μ ≪ ν := by
classical
letI := Fintype.ofFinite ι
let d : Ω → ENNReal :=
fun x => ∑ i : ι, (s i).indicator (fun _ => r i) x
have hμ_sum : μ = Measure.sum (fun i : ι => μ.restrict (s i)) := by
have h := Measure.restrict_iUnion (μ := μ) (s := s) hdisj hs
rw [hcover, Measure.restrict_univ] at h
exact h
have hν_density_sum :
ν.withDensity d =
Measure.sum (fun i : ι =>
ν.withDensity ((s i).indicator (fun _ => r i))) := by
ext t ht
rw [withDensity_apply _ ht]
simp_rw [Measure.sum_apply _ ht, withDensity_apply _ ht]
dsimp [d]
rw [lintegral_finset_sum]
· simp
· intro i _
exact measurable_const.indicator (hs i)
have hν_density :
ν.withDensity d =
Measure.sum (fun i : ι => r i • ν.restrict (s i)) := by
rw [hν_density_sum]
refine congrArg Measure.sum ?_
funext i
rw [withDensity_indicator (μ := ν) (hs i), withDensity_const]
have hμ_density : μ = ν.withDensity d := by
calc
μ = Measure.sum (fun i : ι => μ.restrict (s i)) := hμ_sum
_ = Measure.sum (fun i : ι => r i • ν.restrict (s i)) := by
refine congrArg Measure.sum ?_
funext i
exact hrestrict i
_ = ν.withDensity d := hν_density.symm
rw [hμ_density]
exact withDensity_absolutelyContinuous ν d
lemma partition_restrict_integrable_pow_rnDeriv reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Power-deviation integrability from a finite proportional partition. Under the same partition hypotheses as partition_restrict_absolutelyContinuous — the cells s i are measurable, pairwise disjoint, and cover the ambient space — and again assuming on every cell the numerator measure μ restricted to that cell equals the denominator measure ν restricted to the same cell, scaled by the constant r i, with ν finite, then for any natural number n, the n-th power of the deviation of the Radon–Nikodym derivative dμ/dν from 1 is integrable against ν. On each cell the derivative equals r i, so the function is a finite simple function and the integral is a finite sum of per-cell constants.
Formal statement
hypotheses
Ω :
Type*
ι :
Type*
Finite ι
μ ν :
s :
ι → Set Ω
r :
ι → ENNReal
n :
ℕ
hs :
∀ i, MeasurableSet (s i)
hcover :
(⋃ i, s i) = univ
hrestrict :
∀ i, μ.restrict (s i) = r i • ν.restrict (s i)
conclusion
Integrable (fun x => ((μ.rnDeriv ν x).toReal - 1) ^ n) ν
Proof (Lean source)
lemma partition_restrict_integrable_pow_rnDeriv
{Ω : Type*} [MeasurableSpace Ω] {ι : Type*} [Finite ι]
(μ ν : Measure Ω) [IsFiniteMeasure ν]
(s : ι → Set Ω) (r : ι → ENNReal) (n : ℕ)
(hs : ∀ i, MeasurableSet (s i))
(hdisj : Pairwise (onFun Disjoint s))
(hcover : (⋃ i, s i) = univ)
(hrestrict : ∀ i, μ.restrict (s i) = r i • ν.restrict (s i)) :
Integrable (fun x => ((μ.rnDeriv ν x).toReal - 1) ^ n) ν := by
classical
letI := Fintype.ofFinite ι
let d : Ω → ENNReal :=
fun x => ∑ i : ι, (s i).indicator (fun _ => r i) x
have hd_meas : Measurable d := by
dsimp [d]
exact measurable_sum _ (fun i _ => measurable_const.indicator (hs i))
have hd_cell : ∀ i, ∀ x ∈ s i, d x = r i := by
intro i x hx
dsimp [d]
change (∑ j : ι, (s j).indicator (fun _ => r j) x) =
r i
simpa [Set.indicator_of_mem hx] using
(Finset.sum_eq_single (s := univ)
(f := fun j : ι => (s j).indicator (fun _ => r j) x) i
(by
intro j _ hji
have hxnot : x ∉ s j := by
have hsd : Disjoint (s j) (s i) := hdisj hji
exact fun hxj => (Set.disjoint_left.mp hsd) hxj hx
simp [Set.indicator_of_notMem hxnot])
(by simp))
have hμ_sum : μ = Measure.sum (fun i : ι => μ.restrict (s i)) := by
have h := Measure.restrict_iUnion (μ := μ) (s := s) hdisj hs
rw [hcover, Measure.restrict_univ] at h
exact h
have hν_density_sum :
ν.withDensity d =
Measure.sum (fun i : ι =>
ν.withDensity ((s i).indicator (fun _ => r i))) := by
ext t ht
rw [withDensity_apply _ ht]
simp_rw [Measure.sum_apply _ ht, withDensity_apply _ ht]
dsimp [d]
rw [lintegral_finset_sum]
· simp
· intro i _
exact measurable_const.indicator (hs i)
have hν_density :
ν.withDensity d =
Measure.sum (fun i : ι => r i • ν.restrict (s i)) := by
rw [hν_density_sum]
refine congrArg Measure.sum ?_
funext i
rw [withDensity_indicator (μ := ν) (hs i), withDensity_const]
have hμ_density : μ = ν.withDensity d := by
calc
μ = Measure.sum (fun i : ι => μ.restrict (s i)) := hμ_sum
_ = Measure.sum (fun i : ι => r i • ν.restrict (s i)) := by
refine congrArg Measure.sum ?_
funext i
exact hrestrict i
_ = ν.withDensity d := hν_density.symm
have hrn : μ.rnDeriv ν =ᵐ[ν] d := by
rw [hμ_density]
exact Measure.rnDeriv_withDensity ν hd_meas
have hpiece_int :
∀ i, IntegrableOn (fun x => ((d x).toReal - 1) ^ n) (s i) ν := by
intro i
refine ((integrable_const (((r i).toReal - 1) ^ n) :
Integrable (fun _ : Ω => ((r i).toReal - 1) ^ n) ν).integrableOn.congr_fun ?_ (hs i))
intro x hx
dsimp
rw [hd_cell i x hx]
have hd_int_on :
IntegrableOn (fun x => ((d x).toReal - 1) ^ n) (⋃ i, s i) ν := by
exact integrableOn_finite_iUnion.2 hpiece_int
have hd_int : Integrable (fun x => ((d x).toReal - 1) ^ n) ν := by
rw [← integrableOn_univ, ← hcover]
exact hd_int_on
have heq :
(fun x => ((μ.rnDeriv ν x).toReal - 1) ^ n)
=ᵐ[ν] fun x => ((d x).toReal - 1) ^ n := by
filter_upwards [hrn] with x hx
rw [hx]
exact hd_int.congr heq.symm
PolynomialZeroLocus 3 core · 6 supporting This file proves that the zero locus of a nonzero real multivariate polynomial in finitely many variables is Lebesgue-null. ★ volume_zeroLocus_mvPolynomial_finite★ mvPolynomialZeroLocus_finset_prod
Null loci of real multivariate polynomials
This file proves that the zero locus of a nonzero real multivariate polynomial in finitely many variables is Lebesgue-null.
lemma volume_zeroLocus_mvPolynomial_finite reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a real polynomial indexed by an arbitrary finite variable type that is nonzero, its zero locus has Lebesgue measure zero.
Formal statement
hypotheses
Proof (Lean source)
lemma volume_zeroLocus_mvPolynomial_finite {α : Type*} [Fintype α]
(P : MvPolynomial α ℝ) (hP : P ≠ 0) :
volume {x : α → ℝ | eval x P = 0} = 0 := by
let e : α ≃ Fin (card α) := Fintype.equivFin α
let Q : MvPolynomial (Fin (card α)) ℝ := MvPolynomial.rename e P
have hQ : Q ≠ 0 := (MvPolynomial.renameEquiv ℝ e).injective.ne hP
let S : Set (Fin (card α) → ℝ) :=
{y | eval y Q = 0}
have hS : volume S = 0 := volume_mk_zeroLocus_mvPolynomial Q hQ
have hSmeas : MeasurableSet S := by
exact (MvPolynomial.continuous_eval Q).measurable (measurableSet_singleton 0)
let φ := MeasurableEquiv.piCongrLeft (fun _ : Fin (card α) ↦ ℝ) e
have hφ : MeasurePreserving φ := volume_measurePreserving_piCongrLeft
(fun _ : Fin (card α) ↦ ℝ) e
have hpre : φ ⁻¹' S = {x : α → ℝ | eval x P = 0} := by
ext x
simp only [Set.mem_preimage, Set.mem_setOf_eq]
change eval (φ x) Q = 0 ↔ eval x P = 0
rw [show Q = MvPolynomial.rename e P by rfl, MvPolynomial.eval_rename]
have hx : (φ x) ∘ e = x := by
funext i
simp only [Function.comp_apply]
rw [show φ = MeasurableEquiv.piCongrLeft
(fun _ : Fin (card α) ↦ ℝ) e by rfl]
rw [MeasurableEquiv.piCongrLeft_apply_apply]
rw [hx]
rw [← hpre, ← Measure.map_apply hφ.measurable hSmeas, hφ.map_eq]
exact hS
def mvPolynomialZeroLocus reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a real multivariate polynomial, its real zero locus is the set of real assignments at which the polynomial evaluates to zero.
Definition (Lean source)
theorem mvPolynomialZeroLocus_finset_prod reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a finite set of polynomial indices and an indexed family of real multivariate polynomials, the zero locus of their product equals the union of their zero loci.
Formal statement
hypotheses
conclusion
mvPolynomialZeroLocus (∏ i ∈ s, p i) = ⋃ i ∈ s, mvPolynomialZeroLocus (p i)
Proof (Lean source)
theorem mvPolynomialZeroLocus_finset_prod
(s : Finset κ) (p : κ → MvPolynomial σ ℝ) :
mvPolynomialZeroLocus (∏ i ∈ s, p i) =
⋃ i ∈ s, mvPolynomialZeroLocus (p i) := by
ext x
simp only [mvPolynomialZeroLocus, Set.mem_ofPred_eq, MvPolynomial.eval_prod,
Finset.prod_eq_zero_iff]
simp
6 supporting declarations (lemmas, instances)
-
volume_mk_zeroLocus_mvPolynomiallemma — For a real polynomial in finitely many numbered variables that is nonzero, its zero locus has Lebesgue measure zero.hypothesesProof (Lean source)
lemma volume_mk_zeroLocus_mvPolynomial {d : ℕ} (P : MvPolynomial (Fin d) ℝ) (hP : P ≠ 0) : volume {x : Fin d → ℝ | eval x P = 0} = 0 := by induction d with | zero => have hempty : {x : Fin 0 → ℝ | eval x P = 0} = ∅ := by ext x simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false] intro hx apply hP apply MvPolynomial.funext intro y rw [Subsingleton.elim y x, hx] simp rw [hempty, measure_empty] | succ n ih => let F : Polynomial (MvPolynomial (Fin n) ℝ) := MvPolynomial.finSuccEquiv ℝ n P have hF : F ≠ 0 := (MvPolynomial.finSuccEquiv ℝ n).injective.ne hP obtain ⟨i, hi⟩ : ∃ i, F.coeff i ≠ 0 := by simpa [Polynomial.ext_iff] using hF let Q : MvPolynomial (Fin n) ℝ := F.coeff i have hQ : Q ≠ 0 := hi have hQnull : volume {x : Fin n → ℝ | eval x Q = 0} = 0 := ih Q hQ let T : Set ((Fin n → ℝ) × ℝ) := {z | eval (cons z.2 z.1) P = 0} have hTmeas : MeasurableSet T := by apply (measurableSet_singleton (0 : ℝ)).preimage have hc : Continuous (fun z : (Fin n → ℝ) × ℝ ↦ @cons n (fun _ : Fin (n + 1) ↦ ℝ) z.2 z.1) := continuous_pi fun j ↦ Fin.cases (show Continuous (fun z : (Fin n → ℝ) × ℝ ↦ z.2) from continuous_snd) (fun k ↦ show Continuous (fun z : (Fin n → ℝ) × ℝ ↦ z.1 k) from (continuous_apply k).comp continuous_fst) j exact ((MvPolynomial.continuous_eval P).comp hc).measurable have hQae : ∀ᵐ y ∂(volume : Measure (Fin n → ℝ)), eval y Q ≠ 0 := by simpa only [Set.mem_setOf_eq] using measure_eq_zero_iff_ae_notMem.mp hQnull have hsections : (fun y : Fin n → ℝ ↦ volume (Prod.mk y ⁻¹' T)) =ᵐ[volume] 0 := by filter_upwards [hQae] with y hqy have hpoly : Polynomial.map (eval y) F ≠ 0 := by intro hz have hc := congrArg (fun R : Polynomial ℝ ↦ R.coeff i) hz simp only [Polynomial.coeff_zero, Polynomial.coeff_map] at hc exact hqy (by simpa [Q] using hc) have hfinite : Finite {x : ℝ | (Polynomial.map (eval y) F).IsRoot x} := Polynomial.finite_setOfPred_isRoot hpoly rw [show Prod.mk y ⁻¹' T = {x : ℝ | (Polynomial.map (eval y) F).IsRoot x} by ext x simp only [Set.mem_preimage, Set.mem_setOf_eq, Polynomial.IsRoot.def] rw [← MvPolynomial.eval_eq_eval_mv_eval'] rfl] exact hfinite.measure_zero volume have hprodT : (volume : Measure (Fin n → ℝ)).prod (volume : Measure ℝ) T = 0 := Measure.measure_prod_null_of_ae_null hTmeas hsections let S : Set (ℝ × (Fin n → ℝ)) := {z | eval (cons z.1 z.2) P = 0} have hSmeas : MeasurableSet S := by apply (measurableSet_singleton (0 : ℝ)).preimage have hc : Continuous (fun z : ℝ × (Fin n → ℝ) ↦ @cons n (fun _ : Fin (n + 1) ↦ ℝ) z.1 z.2) := continuous_pi fun j ↦ Fin.cases (show Continuous (fun z : ℝ × (Fin n → ℝ) ↦ z.1) from continuous_fst) (fun k ↦ show Continuous (fun z : ℝ × (Fin n → ℝ) ↦ z.2 k) from (continuous_apply k).comp continuous_snd) j exact ((MvPolynomial.continuous_eval P).comp hc).measurable have hprodS : (volume : Measure ℝ).prod (volume : Measure (Fin n → ℝ)) S = 0 := by rw [← Measure.prod_swap, Measure.map_apply measurable_swap hSmeas] simpa [T, S] using hprodT let e := MeasurableEquiv.piFinSuccAbove (fun _ : Fin (n + 1) ↦ ℝ) 0 have he : MeasurePreserving e := volume_preserving_piFinSuccAbove (fun _ : Fin (n + 1) ↦ ℝ) 0 have hpre : e ⁻¹' S = {x : Fin (n + 1) → ℝ | eval x P = 0} := by ext x simp [e, S] rw [← hpre, ← Measure.map_apply he.measurable hSmeas, he.map_eq] exact hprodS -
mvPolynomial_finset_prod_ne_zerotheorem — If every factor in a finite indexed family of real multivariate polynomials is nonzero, then their finite product is nonzero.hypothesesconclusion(∏ i ∈ s, p i) ≠ 0Proof (Lean source)
theorem mvPolynomial_finset_prod_ne_zero (s : Finset κ) (p : κ → MvPolynomial σ ℝ) (h : ∀ i ∈ s, p i ≠ 0) : (∏ i ∈ s, p i) ≠ 0 := by exact Finset.prod_ne_zero_iff.mpr h -
mvPolynomialZeroLocus_fintype_prodtheorem — For a finite-type-indexed family of real multivariate polynomials, the zero locus of the product over all indices equals the union of all factor zero loci.hypothesesconclusionmvPolynomialZeroLocus (∏ i, p i) = ⋃ i, mvPolynomialZeroLocus (p i)Proof (Lean source)
theorem mvPolynomialZeroLocus_fintype_prod [Fintype κ] (p : κ → MvPolynomial σ ℝ) : mvPolynomialZeroLocus (∏ i, p i) = ⋃ i, mvPolynomialZeroLocus (p i) := by simpa using mvPolynomialZeroLocus_finset_prod (univ) p -
mvPolynomial_fintype_prod_ne_zerotheorem — If every member of a finite-type-indexed family of real multivariate polynomials is nonzero, then the product over the whole index type is nonzero.hypothesesconclusion(∏ i, p i) ≠ 0Proof (Lean source)
theorem mvPolynomial_fintype_prod_ne_zero [Fintype κ] (p : κ → MvPolynomial σ ℝ) (h : ∀ i, p i ≠ 0) : (∏ i, p i) ≠ 0 := by apply mvPolynomial_finset_prod_ne_zero univ p simpa using h -
mvPolynomialZeroLocus_subtype_prodtheorem — Given a finite set of indices and a polynomial for every member of its finite subtype, the zero locus of the subtype product equals the union of the subtype-indexed zero loci.hypothesesconclusionmvPolynomialZeroLocus (∏ i, p i) = ⋃ i, mvPolynomialZeroLocus (p i)Proof (Lean source)
theorem mvPolynomialZeroLocus_subtype_prod (s : Finset κ) (p : {i // i ∈ s} → MvPolynomial σ ℝ) : mvPolynomialZeroLocus (∏ i, p i) = ⋃ i, mvPolynomialZeroLocus (p i) := by exact mvPolynomialZeroLocus_fintype_prod p -
mvPolynomial_subtype_prod_ne_zerotheorem — Given a finite set of indices, a polynomial for every member of its finite subtype, and a proof that every factor is nonzero, the product of the subtype-indexed factors is nonzero.hypothesesσ :sharedType u_1κ :sharedType u_2s :Finset κp :{i // i ∈ s} → MvPolynomial σ ℝh :∀ i, p i ≠ 0conclusion(∏ i, p i) ≠ 0Proof (Lean source)
theorem mvPolynomial_subtype_prod_ne_zero (s : Finset κ) (p : {i // i ∈ s} → MvPolynomial σ ℝ) (h : ∀ i, p i ≠ 0) : (∏ i, p i) ≠ 0 := by exact mvPolynomial_fintype_prod_ne_zero p h
RnDerivCompProdSigmaFinite 1 core · 1 supporting Mathlib's ProbabilityTheory.rnDeriv_compProd (Mathlib/Probability/Kernel/Composition/RadonNikodym.lean) computes (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) but leaves the conditional factor as (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) rather than the fi ★ rnDeriv_compProd_prod_sigmaFinite
Radon–Nikodym derivative of a composition-product against a σ-finite fibre reference
Mathlib's ProbabilityTheory.rnDeriv_compProd
(Mathlib/Probability/Kernel/Composition/RadonNikodym.lean) computes
(μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) but leaves the conditional factor as
(μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) rather than the fibre derivative ∂κ/∂η, and its
kernel Radon–Nikodym API requires the reference kernel to be finite.
This file proves the product-reference formula used when a composition product is
compared against a product reference ν ×ₘ ρ. It takes product
a.e.-measurability of the raw per-slice fibre derivative
(a, b) ↦ (dκ_a/dρ)(b) as an explicit hypothesis; with that representative in
hand the fibre reference ρ need only be σ-finite, so the public theorem
rnDeriv_compProd_prod_sigmaFinite covers continuous references (Lebesgue), not
just finite/discrete ones. It takes the μ-a.e. fibre domination κ_a ≪ ρ
directly as a hypothesis (rather than re-deriving it from joint domination, which
would route through the finite kernel Kernel.const α ρ), and assembles the
formula by withDensity bookkeeping that never needs ρ to be finite.
The remaining Mathlib gap is only in constructing that measurable fibre density
automatically: when ρ is infinite, Kernel.const α ρ is not a finite kernel, so
the current kernel RN API cannot build a jointly measurable σ-finite
representative. Callers that already possess such a representative (for instance
from a stepwise fibre Radon–Nikodym assumption) obtain the full σ-finite formula
here.
lemma rnDeriv_compProd_prod_sigmaFinite reviewed
⚑ flagged
MeasureTheory
σ-finite-reference Radon–Nikodym derivative of a composition-product. Fix an s-finite measure μ, a σ-finite base reference ν, a σ-finite fibre reference ρ, and an s-finite kernel κ from the base space to the fibre space, together with a candidate base density f. If μ is absolutely continuous with respect to ν, μ-almost every fibre κ a is absolutely continuous with respect to ρ, the raw per-slice fibre derivative (a, b) ↦ (dκ_a/dρ)(b) is almost-everywhere measurable with respect to the product reference ν × ρ, and f agrees ν-almost everywhere with the Radon–Nikodym derivative dμ/dν, then the Radon–Nikodym derivative of the composition-product μ ⊗ₘ κ with respect to the product reference ν × ρ agrees, ν × ρ-almost everywhere, with the pointwise product (a, b) ↦ f a · (dκ_a/dρ)(b) of the base density and the fibre derivative.
Formal statement
hypotheses
α :
Type u_1
β :
Type u_2
μ ν :
Measure α
ρ :
Measure β
κ :
Kernel α β
f :
α → ℝ≥0∞
hμν :
μ ≪ ν
hfiber :
∀ᵐ a ∂μ, κ a ≪ ρ
hfiber_meas :
AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (ν.prod ρ)
hf :
μ.rnDeriv ν =ᵐ[ν] f
conclusion
(μ ⊗ₘ κ).rnDeriv (ν.prod ρ) =ᵐ[ν.prod ρ] fun p => f p.1 * (κ p.1).rnDeriv ρ p.2
Proof (Lean source)
lemma rnDeriv_compProd_prod_sigmaFinite
(μ ν : Measure α) (ρ : Measure β) (κ : Kernel α β) (f : α → ℝ≥0∞)
[SigmaFinite ν] [SigmaFinite ρ] [IsSFiniteKernel κ]
(hμν : μ ≪ ν) (hfiber : ∀ᵐ a ∂μ, κ a ≪ ρ)
(hfiber_meas :
AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (ν.prod ρ))
(hf : μ.rnDeriv ν =ᵐ[ν] f) :
(μ ⊗ₘ κ).rnDeriv (ν.prod ρ)
=ᵐ[ν.prod ρ] fun p => f p.1 * (κ p.1).rnDeriv ρ p.2 := by
letI : SFinite μ := sFinite_of_absolutelyContinuous hμν
have hprod_ac : μ.prod ρ ≪ ν.prod ρ := hμν.prod Measure.AbsolutelyContinuous.rfl
have hfiber_meas_mu :
AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (μ.prod ρ) :=
hfiber_meas.mono_ac hprod_ac
have hcomp :
μ ⊗ₘ κ =
(μ.prod ρ).withDensity (fun p : α × β => (κ p.1).rnDeriv ρ p.2) :=
compProd_eq_prod_withDensity_fiber (μ := μ) (ρ := ρ) (κ := κ)
hfiber hfiber_meas_mu
have hbase :
μ.prod ρ = (ν.prod ρ).withDensity (fun p : α × β => μ.rnDeriv ν p.1) := by
calc
μ.prod ρ = (ν.withDensity (μ.rnDeriv ν)).prod ρ := by
rw [Measure.withDensity_rnDeriv_eq μ ν hμν]
_ = (ν.prod ρ).withDensity (fun p : α × β => μ.rnDeriv ν p.1) := by
exact prod_withDensity_left₀ (Measure.measurable_rnDeriv μ ν).aemeasurable
have hmain :
μ ⊗ₘ κ = (ν.prod ρ).withDensity
(fun p : α × β => μ.rnDeriv ν p.1 * (κ p.1).rnDeriv ρ p.2) := by
rw [hcomp, hbase]
rw [← withDensity_mul₀]
· rfl
· exact (Measure.measurable_rnDeriv μ ν).aemeasurable.comp_fst
· exact hfiber_meas
have hmeas_main :
AEMeasurable
(fun p : α × β => μ.rnDeriv ν p.1 * (κ p.1).rnDeriv ρ p.2)
(ν.prod ρ) := by
exact ((Measure.measurable_rnDeriv μ ν).aemeasurable.comp_fst).mul hfiber_meas
have hμrn :
(μ ⊗ₘ κ).rnDeriv (ν.prod ρ)
=ᵐ[ν.prod ρ]
fun p : α × β => μ.rnDeriv ν p.1 * (κ p.1).rnDeriv ρ p.2 := by
rw [hmain]
exact Measure.rnDeriv_withDensity₀ (ν.prod ρ) hmeas_main
have hf_fst : (fun p : α × β => μ.rnDeriv ν p.1) =ᵐ[ν.prod ρ] fun p => f p.1 := by
simpa [Function.comp_def] using
(Measure.quasiMeasurePreserving_fst (μ := ν) (ν := ρ)).ae_eq_comp hf
have h_prod :
(fun p : α × β => μ.rnDeriv ν p.1 * (κ p.1).rnDeriv ρ p.2)
=ᵐ[ν.prod ρ] fun p => f p.1 * (κ p.1).rnDeriv ρ p.2 := by
filter_upwards [hf_fst] with p hp
rw [hp]
exact hμrn.trans h_prod
1 supporting declaration (lemmas, instances)
-
compProd_eq_prod_withDensity_fiberlemma — A composition product is the product reference measure weighted by the fibrewise Radon–Nikodym derivative whenever the fibres are almost everywhere dominated by the reference measure and that derivative is almost everywhere measurable.hypothesesα :sharedType u_1β :sharedType u_2μ :Measure αρ :Measure βκ :Kernel α βSFinite μhfiber :∀ᵐ a ∂μ, κ a ≪ ρhmeas :AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (μ.prod ρ)conclusionμ ⊗ₘ κ = (μ.prod ρ).withDensity (fun p : α × β => (κ p.1).rnDeriv ρ p.2)Proof (Lean source)
lemma compProd_eq_prod_withDensity_fiber (μ : Measure α) (ρ : Measure β) (κ : Kernel α β) [SFinite μ] [SigmaFinite ρ] [IsSFiniteKernel κ] (hfiber : ∀ᵐ a ∂μ, κ a ≪ ρ) (hmeas : AEMeasurable (fun p : α × β => (κ p.1).rnDeriv ρ p.2) (μ.prod ρ)) : μ ⊗ₘ κ = (μ.prod ρ).withDensity (fun p : α × β => (κ p.1).rnDeriv ρ p.2) := by ext s hs rw [Measure.compProd_apply hs, withDensity_apply _ hs] rw [← lintegral_indicator hs] rw [lintegral_prod] · refine lintegral_congr_ae ?_ filter_upwards [hfiber] with a ha have hsec : MeasurableSet (Prod.mk a ⁻¹' s) := measurable_prodMk_left hs change (κ a) (Prod.mk a ⁻¹' s) = ∫⁻ y, (Prod.mk a ⁻¹' s).indicator (fun y => (κ a).rnDeriv ρ y) y ∂ρ rw [lintegral_indicator hsec] rw [← Measure.setLIntegral_rnDeriv ha (Prod.mk a ⁻¹' s)] · exact hmeas.indicator hs
SetIntegralRecovery 1 core · 1 supporting This file recovers either a weighted measure or an almost-everywhere pointwise bound from identities and inequalities known for every measurable set integral. ★ measure_eq_withDensity_of_toReal_setIntegral
Recovery from set integrals
This file recovers either a weighted measure or an almost-everywhere pointwise bound from identities and inequalities known for every measurable set integral.
lemma measure_eq_withDensity_of_toReal_setIntegral reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
If a weight function w is integrable with respect to a reference measure μ and a finite measure ν's mass on every measurable event A equals, as a real number, the integral of w over A against μ, then ν is obtained from μ by weighting with the nonnegative part of w: ν = μ.withDensity (fun x => ENNReal.ofReal (w x)).
Formal statement
hypotheses
conclusion
ν = μ.withDensity (fun x => ofReal (w x))
Proof (Lean source)
lemma measure_eq_withDensity_of_toReal_setIntegral
{α : Type*} [MeasurableSpace α] {μ ν : Measure α} [IsFiniteMeasure ν]
{w : α → ℝ} (hwint : Integrable w μ)
(hν : ∀ A, MeasurableSet A →
(ν A).toReal = ∫ x in A, w x ∂μ) :
ν = μ.withDensity (fun x => ofReal (w x)) := by
have hw0 : ∀ᵐ x ∂μ, 0 ≤ w x :=
ae_nonneg_of_forall_setIntegral_nonneg hwint fun A hA _ => by
rw [← hν A hA]
exact ENNReal.toReal_nonneg
ext A hA
rw [withDensity_apply _ hA]
rw [← ofReal_integral_eq_lintegral_ofReal hwint.integrableOn
((ae_restrict_iff' hA).2
(Filter.Eventually.mono hw0 fun _ hx _ => hx))]
rw [← hν A hA, ENNReal.ofReal_toReal (measure_ne_top ν A)]
1 supporting declaration (lemmas, instances)
-
abs_le_one_ae_of_setIntegral_le_measurelemma — A measurable function is bounded in absolute value by one almost everywhere if the absolute value of its integral over every measurable event is at most that event's measure.hypothesesconclusion∀ᵐ x ∂mu, |f x| ≤ 1Proof (Lean source)
lemma abs_le_one_ae_of_setIntegral_le_measure {Ω : Type*} [MeasurableSpace Ω] (mu : Measure Ω) [IsFiniteMeasure mu] (f : Ω → ℝ) (hf : Measurable f) (hdom : ∀ A, MeasurableSet A → |∫ x in A, f x ∂mu| ≤ (mu A).toReal) : ∀ᵐ x ∂mu, |f x| ≤ 1 := by have hupper : ∀ q : ℝ, 1 < q → ∀ᵐ x ∂mu, f x ≤ q := by intro q hq have hslice : ∀ m : ℕ, ∀ᵐ x ∂mu, ¬(q < f x ∧ f x ≤ (m : ℝ)) := by intro m let A : Set Ω := {x | q < f x ∧ f x ≤ (m : ℝ)} have hA : MeasurableSet A := (measurableSet_Ioi.preimage hf).inter (measurableSet_Iic.preimage hf) have hfin : mu A < ∞ := measure_lt_top mu A have hfA : IntegrableOn f A mu := by apply IntegrableOn.of_bound hfin hf.aestronglyMeasurable.restrict (m : ℝ) filter_upwards [self_mem_ae_restrict hA] with x hxA rw [Real.norm_eq_abs, abs_of_pos (lt_trans (by linarith) hxA.1)] exact hxA.2 have hconst : IntegrableOn (fun _ : Ω => q) A mu := integrableOn_const hfin.ne have hlower : q * (mu A).toReal ≤ ∫ x in A, f x ∂mu := by calc q * (mu A).toReal = ∫ _ in A, q ∂mu := by rw [setIntegral_const] simp [Measure.real] ring _ ≤ ∫ x in A, f x ∂mu := integral_mono_ae hconst hfA (ae_restrict_iff' hA |>.2 <| by filter_upwards with x hx exact hx.1.le) have hupperInt : (∫ x in A, f x ∂mu) ≤ (mu A).toReal := (le_abs_self _).trans (hdom A hA) have hzeroReal : (mu A).toReal = 0 := by have hnonneg : 0 ≤ (mu A).toReal := ENNReal.toReal_nonneg nlinarith have hzero : mu A = 0 := by rw [ENNReal.toReal_eq_zero_iff] at hzeroReal exact hzeroReal.resolve_right hfin.ne rw [ae_iff] simpa [A] using hzero rw [← ae_all_iff] at hslice filter_upwards [hslice] with x hx by_contra hqx have hqfx : q < f x := lt_of_not_ge hqx obtain ⟨m, hm⟩ := exists_nat_ge (f x) exact hx m ⟨hqfx, hm⟩ have hlower : ∀ q : ℝ, 1 < q → ∀ᵐ x ∂mu, -q ≤ f x := by intro q hq have hslice : ∀ m : ℕ, ∀ᵐ x ∂mu, ¬(-(m : ℝ) ≤ f x ∧ f x < -q) := by intro m let A : Set Ω := {x | -(m : ℝ) ≤ f x ∧ f x < -q} have hA : MeasurableSet A := (measurableSet_Ici.preimage hf).inter (measurableSet_Iio.preimage hf) have hfin : mu A < ∞ := measure_lt_top mu A have hfA : IntegrableOn f A mu := by apply IntegrableOn.of_bound hfin hf.aestronglyMeasurable.restrict (m : ℝ) filter_upwards [self_mem_ae_restrict hA] with x hxA rw [Real.norm_eq_abs, abs_of_neg (lt_trans hxA.2 (neg_lt_zero.mpr (by linarith)))] linarith [hxA.1] have hconst : IntegrableOn (fun _ : Ω => -q) A mu := integrableOn_const hfin.ne have hupperSlice : (∫ x in A, f x ∂mu) ≤ -q * (mu A).toReal := by calc (∫ x in A, f x ∂mu) ≤ ∫ _ in A, -q ∂mu := integral_mono_ae hfA hconst (ae_restrict_iff' hA |>.2 <| by filter_upwards with x hx exact hx.2.le) _ = -q * (mu A).toReal := by rw [setIntegral_const] simp [Measure.real] ring have hlowerInt : -(mu A).toReal ≤ ∫ x in A, f x ∂mu := by have := hdom A hA linarith [neg_abs_le (∫ x in A, f x ∂mu)] have hzeroReal : (mu A).toReal = 0 := by have hnonneg : 0 ≤ (mu A).toReal := ENNReal.toReal_nonneg nlinarith have hzero : mu A = 0 := by rw [ENNReal.toReal_eq_zero_iff] at hzeroReal exact hzeroReal.resolve_right hfin.ne rw [ae_iff] simpa [A] using hzero rw [← ae_all_iff] at hslice filter_upwards [hslice] with x hx by_contra hqx have hfxq : f x < -q := lt_of_not_ge hqx obtain ⟨m, hm⟩ := exists_nat_ge (-f x) exact hx m ⟨by linarith, hfxq⟩ have hupperOne : ∀ᵐ x ∂mu, f x ≤ 1 := by have hq := fun j : ℕ => hupper (1 + 1 / ((j + 1 : ℕ) : ℝ)) (by have : 0 < 1 / ((j + 1 : ℕ) : ℝ) := by positivity linarith) rw [← ae_all_iff] at hq filter_upwards [hq] with x hx by_contra hx1 have hpos : 0 < f x - 1 := sub_pos.mpr (lt_of_not_ge hx1) obtain ⟨j, hj⟩ := exists_nat_one_div_lt hpos have hxj := hx j norm_num [Nat.cast_add, cast_one] at hxj have hj' : ((j : ℝ) + 1)⁻¹ < f x - 1 := by simpa [one_div] using hj linarith have hlowerOne : ∀ᵐ x ∂mu, -1 ≤ f x := by have hq := fun j : ℕ => hlower (1 + 1 / ((j + 1 : ℕ) : ℝ)) (by have : 0 < 1 / ((j + 1 : ℕ) : ℝ) := by positivity linarith) rw [← ae_all_iff] at hq filter_upwards [hq] with x hx by_contra hx1 have hlt : f x < -1 := lt_of_not_ge hx1 have hpos : 0 < -f x - 1 := by linarith obtain ⟨j, hj⟩ := exists_nat_one_div_lt hpos have hxj := hx j norm_num [Nat.cast_add, cast_one] at hxj have hj' : ((j : ℝ) + 1)⁻¹ < -f x - 1 := by simpa [one_div] using hj linarith filter_upwards [hupperOne, hlowerOne] with x hxU hxL exact abs_le.mpr ⟨by linarith, hxU⟩
SupCountableDense 1 core · 3 supporting A recurring pattern in localized empirical-process arguments is the need to show that a supremum ω ↦ sSup { F ω π : π ∈ S } of a real process over an index class S is measurable and integrable, when S carries a *countabl ★ integrable_sSup_image_of_countable_dense
Integrability of suprema over a countable-dense-skeletoned index class
A recurring pattern in localized empirical-process arguments is the need to show that a
supremum ω ↦ sSup { F ω π : π ∈ S } of a real process over an index class S is
measurable and integrable, when S carries a countable dense skeleton D ⊆ S (every
point of S is approached by a D-valued sequence along which the process converges) and
the process is uniformly bounded.
This file packages that pattern into a small, paper-agnostic API on an arbitrary measurable space, so that individual empirical-process developments (policy-regret ERM suprema, orthogonal-learning localized processes, set-valued support processes, …) reduce their Bochner side conditions to a single invocation.
Main results:
* sSup_image_eq_of_dense_tendsto — for a real functional F bounded above on S, if
every x ∈ S is reached by a D-valued sequence along which F converges to F x,
then the supremum over S equals the supremum over the countable skeleton D.
* measurable_sSup_image_of_countable_dense — the pointwise supremum ω ↦ sSup (F ω '' S)
is measurable, given a countable D, per-index measurability on D, and the skeleton
supremum-equality for every ω.
* integrable_sSup_image_of_countable_dense — on a finite measure, the same supremum is
integrable, given in addition a uniform bound |F ω π| ≤ C over S; the accompanying
bddAbove_image_of_bound supplies the pointwise BddAbove fact for free.
theorem integrable_sSup_image_of_countable_dense reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
On a finite measure μ, if the bound C is nonnegative, the skeleton index set D is countable, each coordinate map ω ↦ F ω π is measurable for π in the skeleton D, the pointwise supremum of F ω over the index class S equals its supremum over the countable skeleton D, for every ω, and F ω π is bounded in absolute value by C uniformly over π ∈ S, then the pointwise supremum ω ↦ sSup ((F ω) '' S) is integrable against μ. This is the entry point that discharges the Bochner side conditions of a localized empirical-process supremum in one call.
Formal statement
hypotheses
Ω ι :
Type*
μ :
S D :
Set ι
F :
Ω → ι → ℝ
C :
ℝ
hC :
0 ≤ C
hD :
D.Countable
hF :
∀ π ∈ D, Measurable (fun ω => F ω π)
hbound :
∀ ω, ∀ π ∈ S, |F ω π| ≤ C
conclusion
Integrable (fun ω => sSup ((fun π => F ω π) '' S)) μ
Proof (Lean source)
theorem integrable_sSup_image_of_countable_dense {Ω ι : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) [IsFiniteMeasure μ]
(S D : Set ι) (F : Ω → ι → ℝ) (C : ℝ) (hC : 0 ≤ C)
(hD : D.Countable)
(hF : ∀ π ∈ D, Measurable (fun ω => F ω π))
(heq : ∀ ω, sSup ((fun π => F ω π) '' S) = sSup ((fun π => F ω π) '' D))
(hbound : ∀ ω, ∀ π ∈ S, |F ω π| ≤ C) :
Integrable (fun ω => sSup ((fun π => F ω π) '' S)) μ := by
have hmeas := measurable_sSup_image_of_countable_dense S D F hD hF heq
refine Integrable.of_bound hmeas.aestronglyMeasurable C
(Filter.Eventually.of_forall fun ω => ?_)
rw [Real.norm_eq_abs]
by_cases hne : ((fun π => F ω π) '' S).Nonempty
· apply abs_le.mpr
constructor
· obtain ⟨y, hy⟩ := hne
rcases hy with ⟨π, hπ, rfl⟩
exact (abs_le.mp (hbound ω π hπ)).1.trans
(le_csSup (bddAbove_image_of_bound S F C
(fun ω π hπ => (le_abs_self _).trans (hbound ω π hπ)) ω) ⟨π, hπ, rfl⟩)
· refine csSup_le hne fun y hy => ?_
rcases hy with ⟨π, hπ, rfl⟩
exact (abs_le.mp (hbound ω π hπ)).2
· rw [Set.not_nonempty_iff_eq_empty.mp hne, Real.sSup_empty]
simpa using hC
3 supporting declarations (lemmas, instances)
-
sSup_image_eq_of_dense_tendstotheorem — If F is bounded above on S, D ⊆ S, and every x ∈ S is the limit along a D-valued sequence of F-values (F (seq j) → F x), then the supremum of F over S coincides with the supremum over the countable skeleton D. This is the density-side input that turns a supremum over an uncountable class into a supremum over a countable skeleton (used both for measurability and for evaluating the supremum).Proof (Lean source)
theorem sSup_image_eq_of_dense_tendsto {ι : Type*} (F : ι → ℝ) (S D : Set ι) (hDS : D ⊆ S) (hbdd : BddAbove (F '' S)) (hdense : ∀ x ∈ S, ∃ seq : ℕ → ι, (∀ j, seq j ∈ D) ∧ Tendsto (fun j => F (seq j)) atTop (nhds (F x))) : sSup (F '' S) = sSup (F '' D) := by classical by_cases hS : S = ∅ · have hD : D = ∅ := Set.eq_empty_of_subset_empty (by simpa [hS] using hDS) simp [hS, hD] · obtain ⟨x0, hx0⟩ := Set.nonempty_iff_ne_empty.mpr hS obtain ⟨seq, hseqD, _⟩ := hdense x0 hx0 have hDne : D.Nonempty := ⟨seq 0, hseqD 0⟩ have himageDne : (F '' D).Nonempty := hDne.image F have hbddD : BddAbove (F '' D) := hbdd.mono (Set.image_mono hDS) apply le_antisymm · refine csSup_le (Set.image_nonempty.mpr ⟨x0, hx0⟩) ?_ rintro y ⟨x, hx, rfl⟩ obtain ⟨seq, hseqD, htendsto⟩ := hdense x hx refine le_of_tendsto htendsto (Filter.Eventually.of_forall fun j => ?_) exact le_csSup hbddD ⟨seq j, hseqD j, rfl⟩ · exact csSup_le_csSup hbdd himageDne (Set.image_mono hDS) -
measurable_sSup_image_of_countable_densetheorem — The pointwise supremum ω ↦ sSup ((F ω) '' S) of a real process over an index class S is measurable, provided S has a countable skeleton D on which the process is measurable in ω, and the supremum over S agrees pointwise with the supremum over D. Paper-agnostic generalization of the policy-class skeleton measurability step.hypothesesconclusionMeasurable (fun ω => sSup ((fun π => F ω π) '' S))Proof (Lean source)
theorem measurable_sSup_image_of_countable_dense {Ω ι : Type*} [MeasurableSpace Ω] (S D : Set ι) (F : Ω → ι → ℝ) (hD : D.Countable) (hF : ∀ π ∈ D, Measurable (fun ω => F ω π)) (heq : ∀ ω, sSup ((fun π => F ω π) '' S) = sSup ((fun π => F ω π) '' D)) : Measurable (fun ω => sSup ((fun π => F ω π) '' S)) := by classical let _ : Countable D := hD.to_subtype have hsup : Measurable (fun ω : Ω => ⨆ π : D, F ω π.1) := Measurable.iSup (fun π => hF π.1 π.2) convert hsup using 1 ext ω rw [heq ω] have himage : ((fun π : ι => F ω π) '' D) = ((fun π : D => F ω π.1) '' univ) := by ext y constructor · rintro ⟨π, hπ, rfl⟩ exact ⟨⟨π, hπ⟩, Set.mem_univ _, rfl⟩ · rintro ⟨π, _hπ, rfl⟩ exact ⟨π.1, π.2, rfl⟩ rw [himage] have huniv : ((fun π : D => F ω π.1) '' univ) = range (fun π : D => F ω π.1) := by ext y constructor · rintro ⟨π, _hπ, rfl⟩ exact ⟨π, rfl⟩ · rintro ⟨π, rfl⟩ exact ⟨π, Set.mem_univ _, rfl⟩ rw [huniv, sSup_range] -
bddAbove_image_of_boundtheorem — A uniform upper bound F ω π ≤ C over the index class S makes the image (F ω) '' S bounded above (for every ω). Companion BddAbove fact accompanying the integrability lemma.hypothesesconclusionBddAbove ((fun π => F ω π) '' S)Proof (Lean source)
theorem bddAbove_image_of_bound {Ω ι : Type*} (S : Set ι) (F : Ω → ι → ℝ) (C : ℝ) (hbound : ∀ ω, ∀ π ∈ S, F ω π ≤ C) (ω : Ω) : BddAbove ((fun π => F ω π) '' S) := by exact bddAbove_def.mpr ⟨C, by rintro _ ⟨π, hπ, rfl⟩ exact hbound ω π hπ⟩
SupportRnDerivTransport 2 core · 2 supporting This module localizes the global measurable-embedding invariance theorem for canonical Radon--Nikodym derivatives. ★ map_toReal_rnDeriv_eq_map_toReal_rnDeriv_map_of_support_equiv
Support-local Radon--Nikodym transport
This module localizes the global measurable-embedding invariance theorem for canonical Radon--Nikodym derivatives. The maps need only be measurable and mutually inverse on measurable sets carrying the two finite source measures.
def SupportMeasurableOn reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
A map and a set determine the proposition that the map is measurable on that set, by testing its restriction to the set's subtype.
Definition (Lean source)
theorem map_toReal_rnDeriv_eq_map_toReal_rnDeriv_map_of_support_equiv reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Finite numerator and denominator measures with absolute continuity, measurable source and target supports, concentration on the source support, and forward and reverse maps measurable on their supports, whose images stay in the matching supports and are mutual inverses there, give an unchanged pushforward law for the real-valued canonical Radon--Nikodym ratio.
Formal statement
Proof (Lean source)
theorem map_toReal_rnDeriv_eq_map_toReal_rnDeriv_map_of_support_equiv
{X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
[StandardBorelSpace X] [StandardBorelSpace Y]
(m n : Measure X) [IsFiniteMeasure m] [IsFiniteMeasure n]
(hmn : m ≪ n) (S : Set X) (T : Set Y)
(hS : MeasurableSet S) (hT : MeasurableSet T)
(hμS : m Sᶜ = 0) (hνS : n Sᶜ = 0)
(f : X → Y) (g : Y → X)
(hf : SupportMeasurableOn f S) (hg : SupportMeasurableOn g T)
(hfT : ∀ x ∈ S, f x ∈ T)
(hgS : ∀ y ∈ T, g y ∈ S)
(hgf : ∀ x ∈ S, g (f x) = x)
(hfg : ∀ y ∈ T, f (g y) = y) :
Measure.map (fun x ↦ (m.rnDeriv n x).toReal) n =
Measure.map (fun y ↦ ((m.map f).rnDeriv (n.map f) y).toReal) (n.map f) := by
cases isEmpty_or_nonempty X with
| inl hX =>
letI := hX
rw [Measure.eq_zero_of_isEmpty n]
simp
| inr hX =>
letI := hX
letI : Nonempty Y := ⟨f hX.some⟩
have hfn : AEMeasurable f n :=
aemeasurable_of_supportMeasurableOn hS hνS hf
have hrn := rnDeriv_map_of_support_equiv m n hmn S T hS hT hμS hνS
f g hf hg hfT hgS hgf hfg
have hreal :
(fun x ↦ ((m.map f).rnDeriv (n.map f) (f x)).toReal) =ᵐ[n]
fun x ↦ (m.rnDeriv n x).toReal := by
filter_upwards [hrn] with x hx
exact congrArg toReal hx
calc
Measure.map (fun x ↦ (m.rnDeriv n x).toReal) n =
Measure.map
((fun y ↦ ((m.map f).rnDeriv (n.map f) y).toReal) ∘ f) n :=
Measure.map_congr hreal.symm
_ = Measure.map (fun y ↦ ((m.map f).rnDeriv (n.map f) y).toReal)
(n.map f) := by
symm
apply AEMeasurable.map_map_of_aemeasurable
· exact (Measure.measurable_rnDeriv _ _).ennreal_toReal.aemeasurable
· exact hfn
2 supporting declarations (lemmas, instances)
-
aemeasurable_of_supportMeasurableOntheorem — A measurable support set, a measure concentrated on it, and a map measurable there give a map that is almost-everywhere measurable for that measure.Proof (Lean source)
theorem aemeasurable_of_supportMeasurableOn {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSingletonClass Y] [Nonempty Y] {m : Measure X} {S : Set X} {f : X → Y} (hS : MeasurableSet S) (hfull : m Sᶜ = 0) (hf : SupportMeasurableOn f S) : AEMeasurable f m := by obtain ⟨f', hf', hf'eq⟩ := (MeasurableEmbedding.subtype_coe hS).exists_measurable_extend hf (fun _ ↦ inferInstance) refine hf'.aemeasurable.congr ?_ filter_upwards [ae_iff.mpr hfull] with x hx exact congr_fun hf'eq ⟨x, hx⟩ -
rnDeriv_map_of_support_equivtheorem — Finite numerator and denominator measures with absolute continuity, measurable source and target supports, concentration on the source support, and forward and reverse maps measurable on their supports, whose images stay in the matching supports and are mutual inverses there, give a canonical Radon--Nikodym derivative preserved after the forward map.hypothesesX Y :m n :hmn :m ≪ nS :Set XT :Set YhS :hT :hμS :m Sᶜ = 0hνS :n Sᶜ = 0f :X → Yg :Y → Xhf :hg :hfT :∀ x ∈ S, f x ∈ ThgS :∀ y ∈ T, g y ∈ Shgf :∀ x ∈ S, g (f x) = xhfg :∀ y ∈ T, f (g y) = yconclusion(fun x ↦ (m.map f).rnDeriv (n.map f) (f x)) =ᵐ[n] m.rnDeriv nProof (Lean source)
theorem rnDeriv_map_of_support_equiv {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] [StandardBorelSpace X] [StandardBorelSpace Y] (m n : Measure X) [IsFiniteMeasure m] [IsFiniteMeasure n] (hmn : m ≪ n) (S : Set X) (T : Set Y) (hS : MeasurableSet S) (hT : MeasurableSet T) (hμS : m Sᶜ = 0) (hνS : n Sᶜ = 0) (f : X → Y) (g : Y → X) (hf : SupportMeasurableOn f S) (hg : SupportMeasurableOn g T) (hfT : ∀ x ∈ S, f x ∈ T) (hgS : ∀ y ∈ T, g y ∈ S) (hgf : ∀ x ∈ S, g (f x) = x) (hfg : ∀ y ∈ T, f (g y) = y) : (fun x ↦ (m.map f).rnDeriv (n.map f) (f x)) =ᵐ[n] m.rnDeriv n := by by_cases hSne : S.Nonempty · letI : Nonempty Y := ⟨f hSne.some⟩ let e : S ≃ᵐ T := { toEquiv := { toFun := fun x ↦ ⟨f x, hfT x x.2⟩ invFun := fun y ↦ ⟨g y, hgS y y.2⟩ left_inv := fun x ↦ Subtype.ext (hgf x x.2) right_inv := fun y ↦ Subtype.ext (hfg y y.2) } measurable_toFun := hf.subtype_mk measurable_invFun := hg.subtype_mk } let mS : Measure S := Measure.comap ((↑) : S → X) m let nS : Measure S := Measure.comap ((↑) : S → X) n have hmS_map : mS.map ((↑) : S → X) = m := by simp only [mS, map_comap_subtype_coe hS, Measure.restrict_eq_self_of_ae_mem (ae_iff.mpr hμS)] have hnS_map : nS.map ((↑) : S → X) = n := by simp only [nS, map_comap_subtype_coe hS, Measure.restrict_eq_self_of_ae_mem (ae_iff.mpr hνS)] have hfm : AEMeasurable f m := aemeasurable_of_supportMeasurableOn hS hμS hf have hfn : AEMeasurable f n := aemeasurable_of_supportMeasurableOn hS hνS hf have hm_map : (mS.map e).map ((↑) : T → Y) = m.map f := by calc (mS.map e).map ((↑) : T → Y) = mS.map (((↑) : T → Y) ∘ e) := Measure.map_map measurable_subtype_coe e.measurable _ = mS.map (f ∘ ((↑) : S → X)) := by rfl _ = (mS.map ((↑) : S → X)).map f := by symm apply AEMeasurable.map_map_of_aemeasurable · simpa only [hmS_map] using hfm · exact measurable_subtype_coe.aemeasurable _ = m.map f := by rw [hmS_map] have hn_map : (nS.map e).map ((↑) : T → Y) = n.map f := by calc (nS.map e).map ((↑) : T → Y) = nS.map (((↑) : T → Y) ∘ e) := Measure.map_map measurable_subtype_coe e.measurable _ = nS.map (f ∘ ((↑) : S → X)) := by rfl _ = (nS.map ((↑) : S → X)).map f := by symm apply AEMeasurable.map_map_of_aemeasurable · simpa only [hnS_map] using hfn · exact measurable_subtype_coe.aemeasurable _ = n.map f := by rw [hnS_map] have hTtransport := (MeasurableEmbedding.subtype_coe hT).rnDeriv_map (mS.map e) (nS.map e) rw [EventuallyEq, e.measurableEmbedding.ae_map_iff] at hTtransport have hStransport := e.measurableEmbedding.rnDeriv_map mS nS have hScoe := (MeasurableEmbedding.subtype_coe hS).rnDeriv_map mS nS have hsub := Filter.EventuallyEq.trans hTtransport (Filter.EventuallyEq.trans hStransport hScoe.symm) rw [hm_map, hn_map, hmS_map, hnS_map] at hsub have hlift : (fun x ↦ (m.map f).rnDeriv (n.map f) (f x)) =ᵐ[nS.map ((↑) : S → X)] m.rnDeriv n := (MeasurableEmbedding.subtype_coe hS).ae_map_iff.mpr (by filter_upwards [hsub] with x hx simpa only [show ((e x : T) : Y) = f x by rfl] using hx) simpa only [hnS_map] using hlift · have hnzero : n = 0 := by simpa [not_nonempty_iff_eq_empty.mp hSne] using hνS rw [hnzero] rw [EventuallyEq, ae_zero] simp