Mathlib.MeasureTheory
Measure-theoretic helpers staged for Mathlib: integral identities, finite-dimensional polynomial zero-locus nullity, and kernel-composition lemmas.
Function 10 core · 14 supporting · 2 submodules Function — Mathlib-shaped helpers: (subdirectories). Integral 2 to review
6 core · 0 supporting · 4 submodules Uniform-convergence and likelihood-ratio results for integration. MeasurableSpace 2 core · 0 supporting · 2 submodules MeasurableSpace — Mathlib-shaped helpers: Embedding. UnitInterval 0 core · 1 supporting · 1 submodule Measure-theoretic infrastructure for the closed real unit interval.
BoundedCenteredDense 6 core · 2 supporting For a probability measure μ, this file realizes L²₀(μ) as the orthogonal complement of the constant-one function. ★ boundedCenteredLp_topologicalClosure
Bounded centered functions are dense in mean-zero L²
For a probability measure μ, this file realizes L²₀(μ) as the orthogonal
complement of the constant-one function. It centers the dense subspace of L²
simple functions and proves that the resulting bounded, measurable, mean-zero
functions are dense in L²₀(μ).
This is the functional-analytic density step used to generate nonparametric tangent spaces from bounded exponential tilts.
def lpOne reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a probability measure μ, the constant-one vector in L²(μ) is the L² equivalence class of the function equal to one everywhere.
Definition (Lean source)
def meanZeroLp reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a probability measure μ, the mean-zero subspace of L²(μ) is the orthogonal complement of the span of the constant-one vector.
Definition (Lean source)
def lpSimpleFuncSubmodule reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a measure μ, the real linear subspace of L²(μ) represented by measurable simple functions consists exactly of Mathlib's L² simple-function classes.
Definition (Lean source)
parameters
α :
Type u_1
μ :
Measure α
given by
clause 1
carrier := Lp.simpleFunc ℝ 2 μ
clause 2
zero_mem' := (Lp.simpleFunc ℝ 2 μ).zero_mem
clause 3
add_mem' := (Lp.simpleFunc ℝ 2 μ).add_mem
clause 4
smul_mem' := by rintro c f ⟨s, hs⟩ refine ⟨c • s, ?_⟩ change AEEqFun.mk (c • (s : α → ℝ)) _
= c • (f : α →ₘ[μ] ℝ) rw [← hs] exact (AEEqFun.smul_mk c s s.aestronglyMeasurable).symm
def lpCenter reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a probability measure μ, the continuous L² centering operator subtracts the constant component of a square-integrable function.
def boundedCenteredLp reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a probability measure μ, the bounded centered L² subspace is the image of the simple-function subspace under the continuous centering operator.
Definition (Lean source)
parameters
α :
Type u_1
μ :
given by
theorem boundedCenteredLp_topologicalClosure reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a probability measure μ, centered bounded measurable functions are dense in the mean-zero subspace of L²(μ): the topological closure of centered L² simple functions is exactly the orthogonal complement of the constants.
Formal statement
hypotheses
α :
Type u_1
μ :
conclusion
Proof (Lean source)
theorem boundedCenteredLp_topologicalClosure (μ : Measure α) [IsProbabilityMeasure μ] :
(boundedCenteredLp μ).topologicalClosure = meanZeroLp μ := by
apply le_antisymm
· apply Submodule.topologicalClosure_minimal
· rintro f ⟨x, _hx, rfl⟩
exact lpCenter_mem_meanZeroLp μ x
· exact Submodule.isClosed_orthogonal (ℝ ∙ lpOne μ)
· have hmap := (lpSimpleFuncSubmodule μ).topologicalClosure_map (lpCenter μ)
rw [lpSimpleFuncSubmodule_dense, Submodule.map_top, range_lpCenter] at hmap
exact hmap
2 supporting declarations (lemmas, instances)
-
inner_lpOne_eq_integraltheorem — Under a probability measure μ, inner product with the constant-one L² vector equals integration: ⟪f, 1⟫ = ∫ f dμ.hypothesesconclusion⟪f, lpOne μ⟫_ℝ = ∫ z, f z ∂μProof (Lean source)
theorem inner_lpOne_eq_integral (μ : Measure α) [IsProbabilityMeasure μ] (f : Lp ℝ 2 μ) : ⟪f, lpOne μ⟫_ℝ = ∫ z, f z ∂μ := by rw [L2.inner_def] refine integral_congr_ae ?_ filter_upwards [(memLp_const (1 : ℝ)).coeFn_toLp (p := 2) (μ := μ)] with z hz rw [show lpOne μ z = (1 : ℝ) from hz] simp -
mem_boundedCenteredLp_existstheorem — If an L² vector belongs to the centered-simple subspace under a probability measure μ, then it has an everywhere measurable, everywhere bounded, mean-zero representative whose L² class is that vector.hypothesesconclusion∃ (g : α → ℝ) (M : ℝ) (hg : MemLp g 2 μ),conclusion 1z :|g z| ≤ Mconclusion 2(∫ z, g z ∂μ) = 0conclusion 3hg.toLp g = fProof (Lean source)
theorem mem_boundedCenteredLp_exists (μ : Measure α) [IsProbabilityMeasure μ] (f : Lp ℝ 2 μ) (hf : f ∈ boundedCenteredLp μ) : ∃ (g : α → ℝ) (M : ℝ) (hg : MemLp g 2 μ), Measurable g ∧ (∀ z, |g z| ≤ M) ∧ (∫ z, g z ∂μ) = 0 ∧ hg.toLp g = f := by rcases hf with ⟨x, hx, rfl⟩ let sf : Lp.simpleFunc ℝ 2 μ := ⟨lpCenter μ x, lpCenter_mem_simple μ x hx⟩ let g : α → ℝ := Lp.simpleFunc.toSimpleFunc sf obtain ⟨M, hM⟩ := SimpleFunc.exists_forall_norm_le (Lp.simpleFunc.toSimpleFunc sf) have hg : MemLp g 2 μ := Lp.simpleFunc.memLp sf refine ⟨g, M, hg, Lp.simpleFunc.measurable sf, ?_, ?_, ?_⟩ · intro z simpa [g, Real.norm_eq_abs] using hM z · have hzero : ∫ z, (sf : Lp ℝ 2 μ) z ∂μ = 0 := by rw [← inner_lpOne_eq_integral] exact Submodule.mem_orthogonal_singleton_iff_inner_left.mp (show (sf : Lp ℝ 2 μ) ∈ meanZeroLp μ from lpCenter_mem_meanZeroLp μ x) exact (integral_congr_ae (Lp.simpleFunc.toSimpleFunc_eq_toFun sf)).trans hzero · exact congrArg val (Lp.simpleFunc.toLp_toSimpleFunc sf)
CastMeasurable 1 core · 1 supporting Moving a value between the fibres of an indexed family along a proof that the two indices are equal does not disturb measurability, and neither does transporting the codomain index of a measurable function. ★ measurable_cast_family
Measurability of transport along an equality of indices
Moving a value between the fibres of an indexed family along a proof that the two indices are equal does not disturb measurability, and neither does transporting the codomain index of a measurable function. Both facts are immediate once the index equality is substituted away, but they are needed wherever an indexed family is re-indexed, so they are stated once here.
theorem measurable_cast_family reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For an equality between two indices of a measurable family, transporting a value from the fibre over the first index to the fibre over the second is measurable.
Formal statement
hypotheses
conclusion
Measurable (cast (congrArg X hab) : X a → X b)
Proof (Lean source)
@[fun_prop]
theorem measurable_cast_family {I : Type*} {X : I → Type*}
[∀ i, MeasurableSpace (X i)] {a b : I} (hab : a = b) :
Measurable (cast (congrArg X hab) : X a → X b) := by
subst hab
exact measurable_id
1 supporting declaration (lemmas, instances)
-
measurable_family_casttheorem — For an equality between two indices of a measurable family and a measurable function into the fibre over the first index, transporting that function's codomain to the fibre over the second index leaves it measurable.hypothesesconclusionMeasurable (fun x => (h ▸ f x : X w))Proof (Lean source)
@[fun_prop] theorem measurable_family_cast {I γ : Type*} {X : I → Type*} [∀ i, MeasurableSpace (X i)] [MeasurableSpace γ] {v w : I} (h : v = w) {f : γ → X v} (hf : Measurable f) : Measurable (fun x => (h ▸ f x : X w)) := by subst h exact hf
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 This file proves that conditioning a function masked by an intermediate-measurable event on a coarser σ-algebra is unchanged when the function is first replaced by its conditional expectation at the intermediate level. ★ condExp_setIndicator_condExp_of_le
Conditioning an indicator across a σ-algebra tower
This file proves that conditioning a function masked by an intermediate-measurable event on a coarser σ-algebra is unchanged when the function is first replaced by its conditional expectation at the intermediate level.
For a tower of σ-algebras m ≤ m', an m'-measurable set s, and integrable f, the identity
is:
μ[1_s · f | m] =ᵐ μ[1_s · μ[f | m'] | m].
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 an indicator-masked function on a coarser σ-algebra is unchanged when the function is first replaced by its conditional expectation for an intermediate σ-algebra, provided the σ-algebras form a nested tower with a σ-finite trimmed measure, the masking set is measurable at the intermediate level, and the function is integrable.
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 where restricted integrals agree on every measurable preimage of a generating map. ★ condExp_eq_of_integral_preimage_eq
Conditional expectation identified on measurable preimages
This module packages the uniqueness characterization of conditional expectation in the form where restricted integrals agree on every measurable preimage of a generating map.
theorem condExp_eq_of_integral_preimage_eq reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
The conditional expectation of one integrable real function equals another almost everywhere for a finite measure and a measurable generating map, provided both functions are integrable, the second is strongly measurable for the pullback σ-algebra, and their restricted integrals agree on every measurable preimage.
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
CondExpWithDensity 2 core · 1 supporting This file proves the abstract Bayes formula for conditional expectation when a probability measure is changed by a nonnegative normalized density. ★ condExp_withDensity_ae_eq_div★ condExp_expTilt_ae_eq_div
Conditional expectation under a change of measure
This file proves the abstract Bayes formula for conditional expectation when a probability measure is changed by a nonnegative normalized density. It also specializes the formula to normalized exponential tilts by bounded measurable functions; strict positivity of an exponential density upgrades the conclusion from tilted-almost-everywhere to base-almost-everywhere.
Reference: Øksendal, Stochastic Differential Equations, 5th ed., Lemma 8.6.2, equation (8.6.3).
theorem condExp_withDensity_ae_eq_div reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Abstract conditional Bayes formula. If a measurable density is nonnegative, normalized to have integral one, the conditioning σ-algebra is contained in the ambient one, and the target function is integrable under the density-changed measure, then its conditional expectation under that measure is the base-measure conditional expectation of the density-weighted target divided by the conditional expectation of the density, almost everywhere under the changed measure.
Formal statement
hypotheses
m :
hm :
m ≤ m₀
w f :
Ω → ℝ
hw_meas :
@Measurable Ω ℝ m₀ _ w
hw_nonneg :
∀ x, 0 ≤ w x
hw_norm :
∫ x, w x ∂μ = 1
hf :
Integrable f (μ.withDensity fun x => ofReal (w x))
Proof (Lean source)
theorem condExp_withDensity_ae_eq_div [IsProbabilityMeasure μ]
{m : MeasurableSpace Ω} (hm : m ≤ m₀) {w f : Ω → ℝ}
(hw_meas : @Measurable Ω ℝ m₀ _ w) (hw_nonneg : ∀ x, 0 ≤ w x)
(hw_norm : ∫ x, w x ∂μ = 1)
(hf : Integrable f (μ.withDensity fun x => ofReal (w x))) :
@condExp Ω ℝ m m₀ _ _
(μ.withDensity fun x => ofReal (w x)) f =ᵐ[
μ.withDensity fun x => ofReal (w x)]
fun x => μ[fun y => f y * w y | m] x / μ[w | m] x := by
let ν : @Measure Ω m₀ := μ.withDensity fun x => ofReal (w x)
have hw_int : Integrable w μ := by
by_contra h
have hzero := integral_undef h
rw [hw_norm] at hzero
norm_num at hzero
have hdens_meas : @Measurable Ω ENNReal m₀ _ (fun x => ofReal (w x)) :=
hw_meas.ennreal_ofReal
have hdens_lt_top : ∀ᵐ x ∂μ, ofReal (w x) < ∞ :=
Eventually.of_forall fun x => ENNReal.ofReal_lt_top
have hν_prob : IsProbabilityMeasure
(μ.withDensity fun x => ofReal (w x)) := by
constructor
rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ,
← ofReal_integral_eq_lintegral_ofReal hw_int
(Eventually.of_forall hw_nonneg), hw_norm]
norm_num
let _ : IsProbabilityMeasure ν := by simpa only [ν] using hν_prob
have hf_weight : Integrable (fun x => f x * w x) μ := by
have h := (integrable_withDensity_iff hdens_meas hdens_lt_top).mp hf
simpa [ν, ENNReal.toReal_ofReal, hw_nonneg] using h
have hcond_weight : Integrable (fun x => ν[f | m] x * w x) μ := by
have hν : Integrable (ν[f | m]) ν := integrable_condExp
have h := (integrable_withDensity_iff hdens_meas hdens_lt_top).mp hν
simpa [ν, ENNReal.toReal_ofReal, hw_nonneg] using h
have hpull : μ[(fun x => ν[f | m] x * w x) | m] =ᵐ[μ]
fun x => ν[f | m] x * μ[w | m] x := by
exact condExp_mul_of_stronglyMeasurable_left
(stronglyMeasurable_condExp (μ := ν) (m := m) (f := f)) hcond_weight hw_int
have hcandidate_int : Integrable (fun x => ν[f | m] x * μ[w | m] x) μ :=
integrable_condExp.congr hpull
have hcandidate_meas : AEStronglyMeasurable[m]
(fun x => ν[f | m] x * μ[w | m] x) μ :=
((stronglyMeasurable_condExp (μ := ν) (m := m) (f := f)).mul
(stronglyMeasurable_condExp (μ := μ) (m := m) (f := w))).aestronglyMeasurable
have hproduct : (fun x => ν[f | m] x * μ[w | m] x) =ᵐ[μ]
μ[fun y => f y * w y | m] := by
apply ae_eq_condExp_of_forall_setIntegral_eq hm hf_weight
(fun _ _ _ => hcandidate_int.integrableOn) _ hcandidate_meas
intro s hs _
have hs₀ : @MeasurableSet Ω m₀ s := hm s hs
calc
∫ x in s, ν[f | m] x * μ[w | m] x ∂μ =
∫ x in s, μ[(fun y => ν[f | m] y * w y) | m] x ∂μ :=
setIntegral_congr_ae hs₀ (hpull.symm.mono fun _ h _ => h)
_ = ∫ x in s, ν[f | m] x * w x ∂μ :=
setIntegral_condExp hm hcond_weight hs
_ = ∫ x in s, ν[f | m] x ∂ν := by
symm
rw [show ν = μ.withDensity (fun x => ofReal (w x)) from rfl,
@setIntegral_withDensity_eq_setIntegral_toReal_smul Ω ℝ m₀ μ _ _
(fun x => ofReal (w x)) s hdens_meas
(hdens_lt_top.filter_mono (@ae_restrict_le Ω m₀ μ s))
(fun x => ν[f | m] x) hs₀]
apply setIntegral_congr_ae (mX := m₀) hs₀
filter_upwards with x _
simp [ν, ENNReal.toReal_ofReal, hw_nonneg, mul_comm]
_ = ∫ x in s, f x ∂ν := setIntegral_condExp hm hf hs
_ = ∫ x in s, f x * w x ∂μ := by
rw [show ν = μ.withDensity (fun x => ofReal (w x)) from rfl,
@setIntegral_withDensity_eq_setIntegral_toReal_smul Ω ℝ m₀ μ _ _
(fun x => ofReal (w x)) s hdens_meas
(hdens_lt_top.filter_mono (@ae_restrict_le Ω m₀ μ s)) f hs₀]
apply setIntegral_congr_ae (mX := m₀) hs₀
filter_upwards with x _
rw [ENNReal.toReal_ofReal (hw_nonneg x)]
simp [smul_eq_mul, mul_comm]
have hproduct_ν : (fun x => ν[f | m] x * μ[w | m] x) =ᵐ[ν]
μ[fun y => f y * w y | m] :=
hproduct.filter_mono (withDensity_absolutelyContinuous μ _).ae_le
have hpos : ∀ᵐ x ∂ν, 0 < μ[w | m] x := by
simpa [ν] using condExp_density_pos_ae hm hw_meas hw_nonneg hw_norm
filter_upwards [hproduct_ν, hpos] with x hprod hx
exact (eq_div_iff (ne_of_gt hx)).2 hprod
theorem condExp_expTilt_ae_eq_div reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Conditional Bayes formula for bounded exponential tilts. If the conditioning σ-algebra is contained in the ambient one, the score is measurable and bounded, and the target is integrable under the normalized exponential tilt, then the conditional Bayes ratio for the density exp (t s) / ∫ exp (t s) dμ holds almost everywhere under the base measure.
Formal statement
hypotheses
m :
hm :
m ≤ m₀
s f :
Ω → ℝ
t :
ℝ
hs_meas :
@Measurable Ω ℝ m₀ _ s
hs_bound :
∃ C : ℝ, ∀ x, |s x| ≤ C
hf :
Proof (Lean source)
theorem condExp_expTilt_ae_eq_div [IsProbabilityMeasure μ]
{m : MeasurableSpace Ω} (hm : m ≤ m₀) {s f : Ω → ℝ} (t : ℝ)
(hs_meas : @Measurable Ω ℝ m₀ _ s) (hs_bound : ∃ C : ℝ, ∀ x, |s x| ≤ C)
(hf : Integrable f (μ.withDensity fun x => ofReal
(exp (t * s x) / ∫ y, exp (t * s y) ∂μ))) :
@condExp Ω ℝ m m₀ _ _ (μ.withDensity fun x => ofReal
(exp (t * s x) / ∫ y, exp (t * s y) ∂μ)) f =ᵐ[μ]
fun x =>
μ[fun y => f y * (exp (t * s y) / ∫ z, exp (t * s z) ∂μ) | m] x /
μ[fun y => exp (t * s y) / ∫ z, exp (t * s z) ∂μ | m] x := by
rcases hs_bound with ⟨C, hs_bound⟩
let e : Ω → ℝ := fun x => exp (t * s x)
let c : ℝ := ∫ x, e x ∂μ
let w : Ω → ℝ := fun x => e x / c
have he_meas : @Measurable Ω ℝ m₀ _ e := by
dsimp [e]
fun_prop
have he_int : Integrable e μ := by
apply Integrable.of_bound (μ := μ) he_meas.aestronglyMeasurable (exp (|t| * C))
filter_upwards with x
rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
apply Real.exp_le_exp.mpr
exact (le_abs_self _).trans (by
rw [abs_mul]
exact mul_le_mul_of_nonneg_left (hs_bound x) (abs_nonneg t))
have hc_pos : 0 < c := by
have hlower : ∀ x, exp (-|t| * C) ≤ e x := by
intro x
apply Real.exp_le_exp.mpr
calc
-|t| * C = -(|t| * C) := by ring
_ ≤ -|t * s x| := neg_le_neg (by
rw [abs_mul]
exact mul_le_mul_of_nonneg_left (hs_bound x) (abs_nonneg t))
_ ≤ t * s x := neg_abs_le _
calc
0 < exp (-|t| * C) := Real.exp_pos _
_ = ∫ _ : Ω, exp (-|t| * C) ∂μ := by
rw [integral_const, probReal_univ, one_smul]
_ ≤ c := by
dsimp [c]
exact integral_mono (integrable_const _) he_int hlower
have hw_meas : @Measurable Ω ℝ m₀ _ w := by
dsimp [w]
fun_prop
have hw_pos : ∀ x, 0 < w x := fun x => div_pos (Real.exp_pos _) hc_pos
have hw_nonneg : ∀ x, 0 ≤ w x := fun x => (hw_pos x).le
have hw_norm : ∫ x, w x ∂μ = 1 := by
dsimp [w, c]
rw [integral_div]
exact div_self hc_pos.ne'
have hbayes := condExp_withDensity_ae_eq_div hm hw_meas hw_nonneg hw_norm hf
have hdens_meas : @Measurable Ω ENNReal m₀ _ (fun x => ofReal (w x)) :=
hw_meas.ennreal_ofReal
have hbase : @condExp Ω ℝ m m₀ _ _
(μ.withDensity fun x => ofReal (w x)) f =ᵐ[μ]
fun x => μ[fun y => f y * w y | m] x / μ[w | m] x := by
have htilt := (ae_withDensity_iff hdens_meas).mp hbayes
filter_upwards [htilt] with x hx
exact hx (ENNReal.ofReal_ne_zero_iff.mpr (hw_pos x))
simpa [w, e, c] using hbase
1 supporting declaration (lemmas, instances)
-
condExp_density_pos_aetheorem — If a measurable density is nonnegative, normalized to have integral one, and the conditioning σ-algebra is contained in the ambient one, then its conditional expectation is strictly positive almost everywhere under the probability measure having that density.hypothesesm :hm :m ≤ m₀w :Ω → ℝhw_meas :@Measurable Ω ℝ m₀ _ whw_nonneg :∀ x, 0 ≤ w xhw_norm :∫ x, w x ∂μ = 1conclusion∀ᵐ x ∂(μ.withDensity fun x => ofReal (w x)), 0 < μ[w | m] xProof (Lean source)
theorem condExp_density_pos_ae [IsProbabilityMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ m₀) {w : Ω → ℝ} (hw_meas : @Measurable Ω ℝ m₀ _ w) (hw_nonneg : ∀ x, 0 ≤ w x) (hw_norm : ∫ x, w x ∂μ = 1) : ∀ᵐ x ∂(μ.withDensity fun x => ofReal (w x)), 0 < μ[w | m] x := by have hw_int : Integrable w μ := by by_contra h have hzero := integral_undef h rw [hw_norm] at hzero norm_num at hzero have hden_nonneg : 0 ≤ᵐ[μ] μ[w | m] := condExp_nonneg (Eventually.of_forall hw_nonneg) let z : Set Ω := {x | μ[w | m] x = 0} have hz_m : MeasurableSet[m] z := by exact (stronglyMeasurable_condExp (μ := μ) (m := m) (f := w)).measurable (measurableSet_singleton 0) have hz : @MeasurableSet Ω m₀ z := hm z hz_m have hw_zero_on_z : w =ᵐ[μ.restrict z] 0 := by apply (setIntegral_eq_zero_iff_of_nonneg_ae ((Eventually.of_forall hw_nonneg).filter_mono ae_restrict_le) hw_int.integrableOn).mp rw [← setIntegral_condExp hm hw_int hz_m] exact setIntegral_eq_zero_of_ae_eq_zero (Eventually.of_forall fun x hx => hx) rw [ae_withDensity_iff (hw_meas.ennreal_ofReal)] filter_upwards [hden_nonneg, (ae_restrict_iff' hz).mp hw_zero_on_z] with x hden hx hweight rcases lt_or_eq_of_le hden with hpos | hzero · exact hpos · exfalso have hw0 : w x = 0 := hx (by simpa [z] using hzero.symm) exact hweight (by simp [hw0])
ConditionalExpectationTransport 2 core · 6 supporting This file proves preservation of deterministic almost-everywhere bounds by conditional expectation, a real-valued Doob--Dynkin factorization, and transport of almost-everywhere properties, integrability, integrals, and a ★ exists_measurable_real_comp_of_stronglyMeasurable_comap★ condExp_comp_eq_one_of_map_eq
Conditional-expectation bounds and law transport
This file proves preservation of deterministic almost-everywhere bounds by conditional expectation, a real-valued Doob--Dynkin factorization, and transport of almost-everywhere properties, integrability, integrals, and a conditional-mean identity across equality of pushforward measures.
theorem exists_measurable_real_comp_of_stronglyMeasurable_comap reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
A real function strongly measurable for the pullback σ-algebra factors exactly through the generating map by a measurable real function.
Formal statement
hypotheses
X Y :
hg :
@StronglyMeasurable X ℝ _ (comap f mY) g
Proof (Lean source)
theorem exists_measurable_real_comp_of_stronglyMeasurable_comap
{X Y : Type*} [mY : MeasurableSpace Y] {f : X → Y} {g : X → ℝ}
(hg : @StronglyMeasurable X ℝ _ (comap f mY) g) :
∃ h : Y → ℝ, Measurable h ∧ g = h ∘ f := by
obtain ⟨h, hh, hcomp⟩ := hg.exists_eq_measurable_comp
exact ⟨h, hh.measurable, hcomp⟩
theorem condExp_comp_eq_one_of_map_eq reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
A conditional-mean-one identity transfers between two representations with the same pushforward measure. This holds for two measurable maps, a measurable conditioning map, a measurable weighting function whose first composition is integrable, the common pushforward law, and the identity in the first representation.
Formal statement
hypotheses
Ω Ω' R D :
φ :
Ω → R
ψ :
Ω' → R
hφ :
hψ :
design :
R → D
hdesign :
Measurable design
weight :
R → ℝ
hweight :
Measurable weight
hmap :
μ.map φ = ν.map ψ
hint :
Integrable (weight ∘ φ) μ
hcond :
μ[weight ∘ φ | comap (design ∘ φ) inferInstance] =ᵐ[μ] (fun _ => 1)
conclusion
ν[weight ∘ ψ | comap (design ∘ ψ) inferInstance] =ᵐ[ν] (fun _ => 1)
Proof (Lean source)
theorem condExp_comp_eq_one_of_map_eq
{Ω Ω' R D : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω']
[MeasurableSpace R] [MeasurableSpace D]
{μ : Measure Ω} {ν : Measure Ω'} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
{φ : Ω → R} {ψ : Ω' → R} (hφ : Measurable φ) (hψ : Measurable ψ)
(design : R → D) (hdesign : Measurable design)
(weight : R → ℝ) (hweight : Measurable weight)
(hmap : μ.map φ = ν.map ψ) (hint : Integrable (weight ∘ φ) μ)
(hcond : μ[weight ∘ φ |
comap (design ∘ φ) inferInstance] =ᵐ[μ] (fun _ => 1)) :
ν[weight ∘ ψ | comap (design ∘ ψ) inferInstance] =ᵐ[ν]
(fun _ => 1) := by
have hint' : Integrable (weight ∘ ψ) ν :=
(integrable_comp_iff_of_map_eq hφ hψ weight hweight hmap).mp hint
apply condExp_eq_of_integral_preimage_eq ν (design ∘ ψ)
(hdesign.comp hψ) (weight ∘ ψ) (fun _ => 1)
hint' (integrable_const 1)
(stronglyMeasurable_const.aestronglyMeasurable)
intro B hB
let k : R → ℝ := (design ⁻¹' B).indicator weight
have hk : Measurable k :=
hweight.indicator (hdesign hB)
have htransport := integral_comp_eq_of_map_eq hφ hψ k hk hmap
have hmodel :
∫ ω in (design ∘ φ) ⁻¹' B, weight (φ ω) ∂μ =
∫ ω in (design ∘ φ) ⁻¹' B, (1 : ℝ) ∂μ := by
calc
∫ ω in (design ∘ φ) ⁻¹' B, weight (φ ω) ∂μ =
∫ ω in (design ∘ φ) ⁻¹' B,
μ[weight ∘ φ | comap (design ∘ φ) inferInstance] ω ∂μ :=
(setIntegral_condExp
(comap_le (hdesign.comp hφ)) hint
⟨B, hB, rfl⟩).symm
_ = ∫ ω in (design ∘ φ) ⁻¹' B, (1 : ℝ) ∂μ :=
setIntegral_congr_ae ((hdesign.comp hφ) hB)
(hcond.mono fun _ h _ => h)
calc
∫ ω in (design ∘ ψ) ⁻¹' B, (weight ∘ ψ) ω ∂ν = ∫ ω, k (ψ ω) ∂ν := by
rw [← integral_indicator ((hdesign.comp hψ) hB)]
rfl
_ = ∫ ω, k (φ ω) ∂μ := htransport.symm
_ = ∫ ω in (design ∘ φ) ⁻¹' B, weight (φ ω) ∂μ := by
rw [← integral_indicator ((hdesign.comp hφ) hB)]
rfl
_ = ∫ ω in (design ∘ φ) ⁻¹' B, (1 : ℝ) ∂μ := hmodel
_ = ∫ ω, ((design ∘ φ) ⁻¹' B).indicator (fun _ => (1 : ℝ)) ω ∂μ := by
rw [integral_indicator ((hdesign.comp hφ) hB)]
_ = ∫ ω, (design ⁻¹' B).indicator (fun _ => (1 : ℝ)) (φ ω) ∂μ := by
rfl
_ = ∫ ω, (design ⁻¹' B).indicator (fun _ => (1 : ℝ)) (ψ ω) ∂ν := by
apply integral_comp_eq_of_map_eq hφ hψ
((design ⁻¹' B).indicator (fun _ => (1 : ℝ)))
· exact measurable_const.indicator (hdesign hB)
· exact hmap
_ = ∫ ω, ((design ∘ ψ) ⁻¹' B).indicator (fun _ => (1 : ℝ)) ω ∂ν := by
rfl
_ = ∫ ω in (design ∘ ψ) ⁻¹' B, (1 : ℝ) ∂ν := by
rw [integral_indicator ((hdesign.comp hψ) hB)]
6 supporting declarations (lemmas, instances)
-
condExp_ae_mem_Icc_of_stronglyMeasurabletheorem — If the conditioning σ-algebra is contained in the ambient σ-algebra and three integrable real functions satisfy almost-everywhere lower and upper bounds, and both bounding functions are measurable for the conditioning σ-algebra, then the conditional expectation satisfies the same pointwise functional bounds almost everywhere.hypothesesΩ :hm :m ≤ mΩa f b :Ω → ℝha :Integrable a μhf :Integrable f μhb :Integrable b μha_meas :StronglyMeasurable[m] ahb_meas :StronglyMeasurable[m] bhlo :a ≤ᵐ[μ] fhhi :f ≤ᵐ[μ] bconclusion∀ᵐ ω ∂μ, a ω ≤ μ[f | m] ω ∧ μ[f | m] ω ≤ b ωProof (Lean source)
theorem condExp_ae_mem_Icc_of_stronglyMeasurable {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] (hm : m ≤ mΩ) {a f b : Ω → ℝ} (ha : Integrable a μ) (hf : Integrable f μ) (hb : Integrable b μ) (ha_meas : StronglyMeasurable[m] a) (hb_meas : StronglyMeasurable[m] b) (hlo : a ≤ᵐ[μ] f) (hhi : f ≤ᵐ[μ] b) : ∀ᵐ ω ∂μ, a ω ≤ μ[f | m] ω ∧ μ[f | m] ω ≤ b ω := by have hlo' := condExp_mono (μ := μ) (m := m) ha hf hlo have hhi' := condExp_mono (μ := μ) (m := m) hf hb hhi rw [condExp_of_stronglyMeasurable hm ha_meas ha] at hlo' rw [condExp_of_stronglyMeasurable hm hb_meas hb] at hhi' filter_upwards [hlo', hhi'] with ω hωlo hωhi exact ⟨hωlo, hωhi⟩ -
condExp_ae_mem_Icctheorem — If the conditioning σ-algebra is contained in the ambient σ-algebra and an integrable real function lies between two constants almost everywhere, then its conditional expectation lies between the same constants almost everywhere.hypothesesΩ :hm :m ≤ mΩf :Ω → ℝa b :ℝhf :Integrable f μhlo :(fun _ : Ω => a) ≤ᵐ[μ] fhhi :f ≤ᵐ[μ] (fun _ : Ω => b)conclusion∀ᵐ ω ∂μ, a ≤ μ[f | m] ω ∧ μ[f | m] ω ≤ bProof (Lean source)
theorem condExp_ae_mem_Icc {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] (hm : m ≤ mΩ) {f : Ω → ℝ} {a b : ℝ} (hf : Integrable f μ) (hlo : (fun _ : Ω => a) ≤ᵐ[μ] f) (hhi : f ≤ᵐ[μ] (fun _ : Ω => b)) : ∀ᵐ ω ∂μ, a ≤ μ[f | m] ω ∧ μ[f | m] ω ≤ b := by have hlo' := condExp_mono (μ := μ) (m := m) (integrable_const a) hf hlo have hhi' := condExp_mono (μ := μ) (m := m) hf (integrable_const b) hhi rw [condExp_const hm] at hlo' hhi' filter_upwards [hlo', hhi'] with ω hωlo hωhi exact ⟨hωlo, hωhi⟩ -
ae_pos_condExp_of_pos_const_letheorem — If the conditioning σ-algebra is contained in the ambient σ-algebra and an integrable real function is bounded below by a strictly positive constant, then its conditional expectation is strictly positive almost everywhere.hypothesesconclusion∀ᵐ ω ∂μ, 0 < μ[f | m] ωProof (Lean source)
theorem ae_pos_condExp_of_pos_const_le {Ω : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] (hm : m ≤ mΩ) {f : Ω → ℝ} {ε : ℝ} (hf : Integrable f μ) (hε : 0 < ε) (hlo : (fun _ : Ω => ε) ≤ᵐ[μ] f) : ∀ᵐ ω ∂μ, 0 < μ[f | m] ω := by have hbound := condExp_mono (μ := μ) (m := m) (integrable_const ε) hf hlo rw [condExp_const hm] at hbound filter_upwards [hbound] with ω hω exact hε.trans_le hω -
ae_comp_iff_of_map_eqtheorem — A measurable predicate holds almost everywhere after either of two maps under exactly the same conditions when the maps are measurable, the predicate and its truth set are measurable, and their pushforward measures coincide.hypothesesconclusion(∀ᵐ ω ∂μ, p (φ ω)) ↔ ∀ᵐ ω' ∂ν, p (ψ ω')Proof (Lean source)
theorem ae_comp_iff_of_map_eq {Ω Ω' R : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω'] [MeasurableSpace R] {μ : Measure Ω} {ν : Measure Ω'} {φ : Ω → R} {ψ : Ω' → R} (hφ : Measurable φ) (hψ : Measurable ψ) (p : R → Prop) (hp : MeasurableSet {r | p r}) (hmap : μ.map φ = ν.map ψ) : (∀ᵐ ω ∂μ, p (φ ω)) ↔ ∀ᵐ ω' ∂ν, p (ψ ω') := by rw [← ae_map_iff hφ.aemeasurable hp, hmap, ae_map_iff hψ.aemeasurable hp] -
integrable_comp_iff_of_map_eqtheorem — A real function is integrable after composition with one map exactly when it is integrable after composition with the other when both maps are measurable, the real function is measurable, and their pushforward measures coincide.hypothesesΩ Ω' R :hφ :hψ :k :R → ℝhk :hmap :μ.map φ = ν.map ψconclusionIntegrable (k ∘ φ) μ ↔ Integrable (k ∘ ψ) νProof (Lean source)
theorem integrable_comp_iff_of_map_eq {Ω Ω' R : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω'] [MeasurableSpace R] {μ : Measure Ω} {ν : Measure Ω'} {φ : Ω → R} {ψ : Ω' → R} (hφ : Measurable φ) (hψ : Measurable ψ) (k : R → ℝ) (hk : Measurable k) (hmap : μ.map φ = ν.map ψ) : Integrable (k ∘ φ) μ ↔ Integrable (k ∘ ψ) ν := by rw [← integrable_map_measure hk.aestronglyMeasurable hφ.aemeasurable, hmap, integrable_map_measure hk.aestronglyMeasurable hψ.aemeasurable] -
integral_comp_eq_of_map_eqtheorem — Integrating a real function after either of two maps gives the same value when both maps are measurable, the real function is measurable, and their pushforward measures coincide.hypothesesΩ Ω' R :hφ :hψ :k :R → ℝhk :hmap :μ.map φ = ν.map ψconclusion∫ ω, k (φ ω) ∂μ = ∫ ω', k (ψ ω') ∂νProof (Lean source)
theorem integral_comp_eq_of_map_eq {Ω Ω' R : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω'] [MeasurableSpace R] {μ : Measure Ω} {ν : Measure Ω'} {φ : Ω → R} {ψ : Ω' → R} (hφ : Measurable φ) (hψ : Measurable ψ) (k : R → ℝ) (hk : Measurable k) (hmap : μ.map φ = ν.map ψ) : ∫ ω, k (φ ω) ∂μ = ∫ ω', k (ψ ω') ∂ν := by calc ∫ ω, k (φ ω) ∂μ = ∫ r, k r ∂μ.map φ := (integral_map hφ.aemeasurable hk.aestronglyMeasurable).symm _ = ∫ r, k r ∂ν.map ψ := by rw [hmap] _ = ∫ ω', k (ψ ω') ∂ν := integral_map hψ.aemeasurable hk.aestronglyMeasurable
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 2 core · 3 supporting This file provides decomposition, pointwise recovery, and integrability facts for finite measures concentrated on a finite family of measurable atoms. ★ pairwise_singular_card_le_positive_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 pairwise_singular_card_le_positive_atoms reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a finite subset of indices, an indexed family of probability measures, a dominating measure, absolute continuity on the selected indices, and pairwise mutual singularity on distinct selected indices, the number of selected measures is at most the number of singletons having nonzero mass under the dominating measure.
Formal statement
hypotheses
I Z :
A :
Finset I
μ :
I → Measure Z
∀ s, IsProbabilityMeasure (μ s)
ν :
Measure Z
hac :
∀ s ∈ A, μ s ≪ ν
hsing :
∀ s ∈ A, ∀ u ∈ A, s ≠ u → μ s ⟂ₘ μ u
conclusion
(A.card : ℕ∞) ≤ encard {z : Z | ν {z} ≠ 0}
Proof (Lean source)
lemma pairwise_singular_card_le_positive_atoms
{I Z : Type*} [MeasurableSpace Z] [Finite Z]
(A : Finset I) (μ : I → Measure Z)
[∀ s, IsProbabilityMeasure (μ s)] (ν : Measure Z)
(hac : ∀ s ∈ A, μ s ≪ ν)
(hsing : ∀ s ∈ A, ∀ u ∈ A, s ≠ u → μ s ⟂ₘ μ u) :
(A.card : ℕ∞) ≤ encard {z : Z | ν {z} ≠ 0} := by
classical
let z : {s // s ∈ A} → Z := fun s ↦
choose (exists_singleton_ne_zero_of_probability_finite (μ s))
have hz (s : {s // s ∈ A}) : μ s {z s} ≠ 0 :=
Classical.choose_spec (exists_singleton_ne_zero_of_probability_finite (μ s))
have hzν (s : {s // s ∈ A}) : ν {z s} ≠ 0 := by
intro hzero
exact hz s (hac s s.property hzero)
have hinj : Injective z := by
intro s u hzu
by_contra hsu
have hms := hsing s s.property u u.property (Subtype.coe_ne_coe.mpr hsu)
by_cases hm : z s ∈ hms.nullSet
· have hzero : μ s {z s} = 0 :=
nonpos_iff_eq_zero.mp
((measure_mono (Set.singleton_subset_iff.mpr hm)).trans_eq
hms.measure_nullSet)
exact hz s hzero
· have hmem : z u ∈ hms.nullSetᶜ := by simpa [hzu] using hm
have hzero : μ u {z u} = 0 :=
nonpos_iff_eq_zero.mp
((measure_mono (Set.singleton_subset_iff.mpr hmem)).trans_eq
hms.measure_compl_nullSet)
exact hz u hzero
let B : Finset Z := A.attach.image z
have hcard : B.card = A.card := by
rw [Finset.card_image_iff.mpr hinj.injOn]
simp
have hsub : (B : Set Z) ⊆ {w : Z | ν {w} ≠ 0} := by
intro w hw
simp only [B, Finset.mem_coe, mem_image] at hw
obtain ⟨s, _, rfl⟩ := hw
exact hzν s
rw [← hcard, ← Set.encard_coe_eq_coe_finsetCard]
exact Set.encard_le_encard hsub
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
3 supporting declarations (lemmas, instances)
-
exists_singleton_ne_zero_of_probability_finitelemma — Given a probability measure on a finite measurable space, some singleton has nonzero probability.hypothesesZ :μ :conclusion∃ z : Z, μ {z} ≠ 0Proof (Lean source)
lemma exists_singleton_ne_zero_of_probability_finite {Z : Type*} [MeasurableSpace Z] [Finite Z] (μ : Measure Z) [IsProbabilityMeasure μ] : ∃ z : Z, μ {z} ≠ 0 := by letI := Fintype.ofFinite Z by_contra h push Not at h have hu : (Set.univ : Set Z) = ⋃ z ∈ (Finset.univ : Finset Z), ({z} : Set Z) := by ext z simp have hle := measure_biUnion_finset_le (μ := μ) (Finset.univ : Finset Z) (fun z ↦ ({z} : Set Z)) rw [← hu] at hle simp [h] at hle -
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 · 8 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).
abbrev 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.
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]
8 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) := fun _ _ hxy ↦ hxy i (by simp) -
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 have hi' : i ∈ S := 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 (μ := ν)
FiniteIntervalPartition 2 core · 1 supporting This file defines measurable finite partitions of a closed interval and constructs one from an ordered sequence of cut points. ★ orderedIntervalCells_partition
Finite partitions by ordered intervals
This file defines measurable finite partitions of a closed interval and constructs one from an ordered sequence of cut points. All cells except the last are left closed and right open; the last cell is closed at both ends.
def IsIntervalPartition reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
A family of k sets is a measurable partition of the closed interval from a to b when its cells are measurable, pairwise disjoint, and cover that interval.
Definition (Lean source)
lemma orderedIntervalCells_partition reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a positive number k of cells and ordered cut points f through index k, the consecutive half-open cells, with a closed final cell, measurably partition the closed interval from the first to the last cut point.
Formal statement
hypotheses
α :
f :
ℕ → α
k :
ℕ
hk :
0 < k
hf :
∀ i j
if
i ≤ j
and
j ≤ k
then
f i ≤ f j
conclusion
IsIntervalPartition (f 0) (f k) k (fun j : Fin k => if j.val + 1 = k then Icc (f j.val) (f (j.val + 1)) else Ico (f j.val) (f (j.val + 1)))
Proof (Lean source)
lemma orderedIntervalCells_partition {α : Type*} [TopologicalSpace α] [MeasurableSpace α]
[LinearOrder α] [BorelSpace α] [OrderClosedTopology α]
(f : ℕ → α) (k : ℕ) (hk : 0 < k)
(hf : ∀ i j, i ≤ j → j ≤ k → f i ≤ f j) :
IsIntervalPartition (f 0) (f k) k
(fun j : Fin k => if j.val + 1 = k then
Icc (f j.val) (f (j.val + 1))
else Ico (f j.val) (f (j.val + 1))) := by
classical
refine ⟨?_, ?_, ?_⟩
· intro j
change MeasurableSet (if j.val + 1 = k then
Icc (f j.val) (f (j.val + 1)) else
Ico (f j.val) (f (j.val + 1)))
split_ifs
· exact measurableSet_Icc
· exact measurableSet_Ico
· intro i j hij
apply Set.disjoint_left.mpr
intro x hxi hxj
have hji : i.val ≠ j.val := Fin.val_ne_of_ne hij
rcases lt_or_gt_of_ne hji with hlt | hgt
· have hi : i.val + 1 ≠ k := by omega
simp only [hi, ↓reduceIte, Set.mem_Ico] at hxi
have hlow : f j.val ≤ x := by
change x ∈ (if j.val + 1 = k then Icc (f j.val) (f (j.val + 1))
else Ico (f j.val) (f (j.val + 1))) at hxj
split_ifs at hxj <;> exact hxj.1
have horder : f (i.val + 1) ≤ f j.val :=
hf _ _ (by omega) (le_of_lt j.isLt)
exact (not_lt_of_ge (horder.trans hlow) hxi.2).elim
· have hj : j.val + 1 ≠ k := by omega
simp only [hj, ↓reduceIte, Set.mem_Ico] at hxj
have hlow : f i.val ≤ x := by
change x ∈ (if i.val + 1 = k then Icc (f i.val) (f (i.val + 1))
else Ico (f i.val) (f (i.val + 1))) at hxi
split_ifs at hxi <;> exact hxi.1
have horder : f (j.val + 1) ≤ f i.val :=
hf _ _ (by omega) (le_of_lt i.isLt)
exact (not_lt_of_ge (horder.trans hlow) hxj.2).elim
· let n := k - 1
have hn : n + 1 = k := by dsimp [n]; omega
have hnlt : n < k := by omega
have hcover := orderedHalfOpenIntervals_cover f n
(fun i j hij hj => hf i j hij (by omega))
have hchain : Ico (f 0) (f n) ∪ Icc (f n) (f k) =
Icc (f 0) (f k) :=
Set.Ico_union_Icc_eq_Icc (hf 0 n (zero_le n) (by omega))
(hf n k (by omega) le_rfl)
rw [← hchain, ← hcover]
ext x
constructor
· intro hx
obtain ⟨j, hjx⟩ := Set.mem_iUnion.mp hx
by_cases hj : j.val + 1 = k
· right
have hval : j.val = n := by omega
simpa [hval, hn] using hjx
· left
have hjn : j.val < n := by omega
refine Set.mem_iUnion.mpr ⟨j.val, Set.mem_iUnion.mpr ⟨Finset.mem_range.mpr hjn, ?_⟩⟩
simpa [hj] using hjx
· rintro (hx | hx)
· obtain ⟨j, hjx⟩ := Set.mem_iUnion.mp hx
obtain ⟨hj, hjx⟩ := Set.mem_iUnion.mp hjx
have hjlt : j < k := by have := Finset.mem_range.mp hj; omega
let q : Fin k := ⟨j, hjlt⟩
refine Set.mem_iUnion.mpr ⟨q, ?_⟩
have hne : j + 1 ≠ k := by have := Finset.mem_range.mp hj; omega
simpa [q, hne] using hjx
· let q : Fin k := ⟨n, hnlt⟩
refine Set.mem_iUnion.mpr ⟨q, ?_⟩
simpa [q, hn] using hx
1 supporting declaration (lemmas, instances)
-
orderedHalfOpenIntervals_coverlemma — For ordered cut points f through index n, the union of their consecutive left-closed, right-open cells is the interval from the first through the last cut point.hypothesesProof (Lean source)
lemma orderedHalfOpenIntervals_cover {α : Type*} [LinearOrder α] (f : ℕ → α) (n : ℕ) (hf : ∀ i j, i ≤ j → j ≤ n → f i ≤ f j) : (⋃ j ∈ range n, Ico (f j) (f (j + 1))) = Ico (f 0) (f n) := by induction n with | zero => simp | succ n ih => have ih' := ih (fun i j hij hj => hf i j hij (hj.trans (le_succ n))) simp only [Finset.range_add_one, Finset.mem_insert, Set.iUnion_or] rw [Set.iUnion_union_distrib] simp only [Set.iUnion_iUnion_eq_left, ih'] simpa [Set.union_comm] using (Set.Ico_union_Ico_eq_Ico (hf 0 n (zero_le n) (le_succ n)) (hf n (n + 1) (le_succ n) le_rfl))
FiniteMaximizer 3 core · 1 supporting This file gives a deterministic, measurably tie-broken maximizer for a nonempty finite family of real-valued measurable functions. ★ measurable_finiteClassMaximizer
Measurable Maximizers for Finite Real-Valued Classes
This file gives a deterministic, measurably tie-broken maximizer for a nonempty finite family of real-valued measurable functions. The construction is generic measurable-selection infrastructure and does not depend on concentration theory.
def listMaximizerPair reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a score family score, an initial index a, and a list of remaining indices, the finite maximizer fold returns its selected-index function and selected-score function: an empty list retains the initial index, while a nonempty list compares the initial score with the recursively selected tail score.
Definition (Lean source)
parameters
Omega :
Type u
I :
Type v
score :
I → Omega → ℝ
a :
I
def
given by
clause 1
| [] => (fun _ => a, score a)
clause 2
| b :: rest
=> let tail := listMaximizerPair score b rest (fun omega => if score a omega < tail.2 omega then tail.1 omega else a, fun omega => if score a omega < tail.2 omega then tail.2 omega else score a omega)
def finiteClassMaximizer reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a nonempty finite index type I and a real-valued score family score, the finite-class maximizer is the index selected by a fixed fold through the finite enumeration, retaining the earlier index when scores tie.
Definition (Lean source)
parameters
def
finiteClassMaximizer I score :
Omega → I
given by
(listMaximizerPair score (choice ‹Nonempty I›) Finset.univ.toList).1
theorem measurable_finiteClassMaximizer reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
If every score in a nonempty finite family is measurable, then its selected finite-class maximizer is measurable into the discrete measurable index space.
Formal statement
hypotheses
Omega :
Type u
I :
Type v
MeasurableSpace Omega
Fintype I
Nonempty I
score :
I → Omega → ℝ
hscore :
∀ i, Measurable (score i)
conclusion
@Measurable Omega I _ ⊤ (finiteClassMaximizer I score)
Proof (Lean source)
@[fun_prop]
theorem measurable_finiteClassMaximizer
{Omega : Type u} {I : Type v} [MeasurableSpace Omega] [Fintype I] [Nonempty I]
{score : I → Omega → ℝ} (hscore : ∀ i, Measurable (score i)) :
@Measurable Omega I _ ⊤ (finiteClassMaximizer I score) := by
unfold finiteClassMaximizer
exact (measurable_listMaximizerPair score hscore
(choice ‹Nonempty I›) Finset.univ.toList).1
1 supporting declaration (lemmas, instances)
-
finiteClassMaximizer_spectheorem — For a nonempty finite score family score, every member's score is at most the score at the selected finite-class maximizer.hypothesesconclusionscore i omega ≤ score (finiteClassMaximizer I score omega) omegaProof (Lean source)
theorem finiteClassMaximizer_spec {Omega : Type u} {I : Type v} [Fintype I] [Nonempty I] (score : I → Omega → ℝ) (omega : Omega) (i : I) : score i omega ≤ score (finiteClassMaximizer I score omega) omega := by let a := choice ‹Nonempty I› have hspec := listMaximizerPair_spec score a Finset.univ.toList omega have hi : i ∈ a :: Finset.univ.toList := by simp change score i omega ≤ score ((listMaximizerPair score a Finset.univ.toList).1 omega) omega rw [← hspec.1] exact hspec.2 i hi
FinsetValues 12 core · 17 supporting This file provides dependent function spaces over finite index sets, measurable coordinate restrictions, canonical equivalences and product-measure transport for equal index sets, and assembly over unions. ★ measurable_valuesProjection★ comap_valuesProjection_le★ measurePreserving_valuesEquivOfEq★ valuesUnionMk_comm★ valuesOn_heq_of_coord
Dependent functions over finite index sets
This file provides dependent function spaces over finite index sets, measurable coordinate restrictions, canonical equivalences and product-measure transport for equal index sets, and assembly over unions.
The restriction map valuesProjection coincides definitionally with Mathlib's
Finset.restrict₂.
abbrev ValuesOn reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
The dependent function space over a finite coordinate set selects a finite subset of an index type and assigns each selected index a value in its associated coordinate type.
def valuesProjection reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
The coordinate-restriction map takes dependent functions over a finite set of indices in an index type with measurable coordinate types and retains only coordinates in a contained finite subset.
Definition (Lean source)
parameters
given by
fun ξ j => ξ ⟨j.val, hJI j.property⟩
theorem measurable_valuesProjection reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Restricting a dependent function to a contained finite set of coordinates is measurable for an index type, the original and retained finite sets, measurable coordinate types, and the stated containment.
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.Mathlib.MeasureTheory
Pulling back the product σ-algebra along coordinate restriction yields a sub-σ-algebra of the original product space for an index type, the original and retained finite sets, measurable coordinate types, and their containment.
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.Mathlib.MeasureTheory
Equal finite index sets determine a canonical measurable equivalence between their dependent function spaces. The construction uses an index type, the two finite sets, measurable coordinate types, and the equality identifying the sets.
Definition (Lean source)
parameters
given by
clause 1
toFun := valuesProjection (le_of_eq h.symm)
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.Mathlib.MeasureTheory
The canonical equivalence between equal finite index sets preserves their coordinatewise product measures. It uses an index type, the two finite sets, measurable coordinate types, their equality, and one measure for each coordinate of the first set.
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.Mathlib.MeasureTheory
The union assignment combines dependent functions on two finite index sets drawn from a decidable index type with measurable coordinate types; the first function supplies values on overlaps.
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⟩
lemma valuesUnionMk_comm reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For finite sets A and B, their disjointness, a decidable index type, measurable coordinate types, and dependent functions a and b, union commutativity swaps the inputs.
Formal statement
hypotheses
conclusion
Proof (Lean source)
lemma valuesUnionMk_comm {M : Type*} [DecidableEq M] {Ω : M → Type*}
[∀ m, MeasurableSpace (Ω m)] {A B : Finset M} (hAB : Disjoint A B)
(a : ValuesOn A Ω) (b : ValuesOn B Ω) :
valuesEquivOfEq (union_comm A B) (valuesUnionMk a b) =
valuesUnionMk b a := by
funext ⟨v, hv⟩
have hvAB : v ∈ A ∪ B := by rwa [union_comm]
change valuesUnionMk a b ⟨v, hvAB⟩ = valuesUnionMk b a ⟨v, hv⟩
by_cases hA : v ∈ A
· have hB : v ∉ B := fun h => Finset.disjoint_left.mp hAB hA h
simp only [valuesUnionMk, dif_pos hA, dif_neg hB]
· have hB : v ∈ B := (Finset.mem_union.mp hv).resolve_right hA
simp only [valuesUnionMk, dif_pos hB, dif_neg hA]
lemma valuesOn_heq_of_coord reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For finite sets I and J, their equality, an index type, measurable coordinate types, dependent functions f and g, and coordinatewise agreement, the functions are heterogeneously equal.
Formal statement
hypotheses
M :
Type*
M → Type*
∀ m, MeasurableSpace (Ω m)
I J :
Finset M
hIJ :
I = J
f :
ValuesOn I Ω
g :
ValuesOn J Ω
h :
∀ (v : M) (hI : v ∈ I) (hJ : v ∈ J), f ⟨v, hI⟩ = g ⟨v, hJ⟩
conclusion
HEq f g
Proof (Lean source)
lemma valuesOn_heq_of_coord {M : Type*} {Ω : M → Type*} [∀ m, MeasurableSpace (Ω m)]
{I J : Finset M} (hIJ : I = J) (f : ValuesOn I Ω) (g : ValuesOn J Ω)
(h : ∀ (v : M) (hI : v ∈ I) (hJ : v ∈ J), f ⟨v, hI⟩ = g ⟨v, hJ⟩) :
HEq f g := by
apply Function.hfunext (congrArg (fun S : Finset M => {i // i ∈ S}) hIJ)
rintro ⟨v, hvI⟩ ⟨v', hvJ⟩ hidx
have hv_eq : v = v' := (Subtype.heq_iff_coe_eq (by intro x; rw [hIJ])).mp hidx
subst hv_eq
exact heq_of_eq (h v hvI hvJ)
def singletonValue reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For an index type ι, coordinate types, an index v, and a singleton assignment x, the singleton-coordinate value is its value at v.
def singletonValues reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For an index type ι, coordinate types, an index v, and a value x, the singleton assignment assigns x to its sole coordinate.
def reindexSubtypeProj reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For finite sets S and P, a finite decidable index type, measurable coordinate types, and the inclusion S ⊆ P, the measurable equivalence removes the redundant nested subtype index.
Definition (Lean source)
parameters
def
reindexSubtypeProj S hS :
((i : {i // i ∈ (S.subtype (· ∈ P))}) → Ω' i.val.val) ≃ᵐ ((j : {j // j ∈ S}) → Ω' j.val)
given by
clause 1
toFun := fun f j
=> f ⟨⟨j.val, hS j.property⟩, by simp only [Finset.mem_subtype]; exact j.property⟩
clause 2
invFun := fun g i
=> g ⟨i.val.val, by have := i.property; rw [Finset.mem_subtype] at this; exact this⟩
clause 3
left_inv := fun _ => rfl
clause 4
right_inv := fun _ => rfl
clause 5
measurable_toFun := by apply measurable_pi_lambda; intro j; exact measurable_pi_apply _
clause 6
measurable_invFun := by apply measurable_pi_lambda; intro i; exact measurable_pi_apply _
17 supporting declarations (lemmas, instances)
-
valuesProjection_comptheorem — For finite sets K, J, and I, an index type, measurable coordinate types, the inclusion K ⊆ J, and the inclusion J ⊆ I, coordinate restriction composes.hypothesesconclusionProof (Lean source)
theorem valuesProjection_comp {M : Type*} {I J K : Finset M} {Ω' : M → Type*} [∀ n, MeasurableSpace (Ω' n)] (hKJ : K ⊆ J) (hJI : J ⊆ I) : valuesProjection (Ω := Ω') (hKJ.trans hJI) = valuesProjection hKJ ∘ valuesProjection hJI := by funext ξ ⟨k, hk⟩ simp only [Function.comp_apply, valuesProjection] -
comap_valuesProjection_monotheorem — For finite sets A, B, and I, an index type, measurable coordinate types, the inclusion A ⊆ B, and the inclusion B ⊆ I, the projection pullbacks are monotone.hypothesesconclusionProof (Lean source)
theorem comap_valuesProjection_mono {M : Type*} {I A B : Finset M} {Ω' : M → Type*} [∀ n, MeasurableSpace (Ω' n)] (hAB : A ⊆ B) (hBI : B ⊆ I) : comap (valuesProjection (Ω := Ω') (hAB.trans hBI)) inferInstance ≤ comap (valuesProjection (Ω := Ω') hBI) inferInstance := by have hcomp := valuesProjection_comp (Ω' := Ω') hAB hBI rw [hcomp] intro s ⟨t, ht, hts⟩ exact ⟨valuesProjection hAB ⁻¹' t, measurable_valuesProjection hAB ht, hts⟩ -
measurable_valuesProjection_union_suptheorem — For finite sets A, B, and I, a decidable index type, measurable coordinate types, and inclusions in I, union projection is measurable for the supremum pullback.hypothesesconclusion@Measurable (ValuesOn I Ω') (ValuesOn (A ∪ B) Ω') (comap (valuesProjection (Ω := Ω') hA) inferInstance ⊔ comap (valuesProjection (Ω := Ω') hB) inferInstance) inferInstance (valuesProjection (Ω := Ω') (union_subset hA hB))Proof (Lean source)
theorem measurable_valuesProjection_union_sup {M : Type*} [DecidableEq M] {I A B : Finset M} {Ω' : M → Type*} [∀ n, MeasurableSpace (Ω' n)] (hA : A ⊆ I) (hB : B ⊆ I) : @Measurable (ValuesOn I Ω') (ValuesOn (A ∪ B) Ω') (comap (valuesProjection (Ω := Ω') hA) inferInstance ⊔ comap (valuesProjection (Ω := Ω') hB) inferInstance) inferInstance (valuesProjection (Ω := Ω') (union_subset hA hB)) := by let hAB : A ∪ B ⊆ I := union_subset hA hB change @Measurable (ValuesOn I Ω') (∀ i : {i // i ∈ A ∪ B}, Ω' i.val) (comap (valuesProjection (Ω := Ω') hA) inferInstance ⊔ comap (valuesProjection (Ω := Ω') hB) inferInstance) inferInstance (fun ξ : ValuesOn I Ω' => fun i : {i // i ∈ A ∪ B} => ξ ⟨i.val, hAB i.property⟩) refine (@measurable_pi_iff (ValuesOn I Ω') {i // i ∈ A ∪ B} (fun i : {i // i ∈ A ∪ B} => Ω' i.val) (comap (valuesProjection (Ω := Ω') hA) inferInstance ⊔ comap (valuesProjection (Ω := Ω') hB) inferInstance) inferInstance (fun ξ : ValuesOn I Ω' => fun i : {i // i ∈ A ∪ B} => ξ ⟨i.val, hAB i.property⟩)).2 ?_ intro ⟨i, hiAB⟩ by_cases hiA : i ∈ A · have hπA : @Measurable (ValuesOn I Ω') (ValuesOn A Ω') (comap (valuesProjection (Ω := Ω') hA) inferInstance ⊔ comap (valuesProjection (Ω := Ω') hB) inferInstance) inferInstance (valuesProjection (Ω := Ω') hA) := Measurable.of_comap_le le_sup_left exact (measurable_pi_apply (⟨i, hiA⟩ : {j // j ∈ A})).comp hπA · have hiB : i ∈ B := (Finset.mem_union.mp hiAB).resolve_left hiA have hπB : @Measurable (ValuesOn I Ω') (ValuesOn B Ω') (comap (valuesProjection (Ω := Ω') hA) inferInstance ⊔ comap (valuesProjection (Ω := Ω') hB) inferInstance) inferInstance (valuesProjection (Ω := Ω') hB) := Measurable.of_comap_le le_sup_right exact (measurable_pi_apply (⟨i, hiB⟩ : {j // j ∈ B})).comp hπB -
comap_valuesProjection_union_eq_suptheorem — For finite sets A, B, and I, a decidable index type, measurable coordinate types, and inclusions in I, the union-projection pullback equals the supremum of the separate pullbacks.hypothesesconclusion= comap (valuesProjection (Ω := Ω') hA) inferInstance ⊔ comap (valuesProjection (Ω := Ω') hB) inferInstanceProof (Lean source)
theorem comap_valuesProjection_union_eq_sup {M : Type*} [DecidableEq M] {I A B : Finset M} {Ω' : M → Type*} [∀ n, MeasurableSpace (Ω' n)] (hA : A ⊆ I) (hB : B ⊆ I) : comap (valuesProjection (Ω := Ω') (union_subset hA hB)) inferInstance = comap (valuesProjection (Ω := Ω') hA) inferInstance ⊔ comap (valuesProjection (Ω := Ω') hB) inferInstance := by let hAB : A ∪ B ⊆ I := union_subset hA hB apply le_antisymm · exact comap_le (measurable_valuesProjection_union_sup (Ω' := Ω') hA hB) · exact sup_le (comap_valuesProjection_mono (Ω' := Ω') subset_union_left hAB) (comap_valuesProjection_mono (Ω' := Ω') subset_union_right hAB) -
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 dependent functions is measurable in the second input 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 dependent functions is jointly measurable in both inputs.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 -
valuesUnionMk_projection_comptheorem — For finite sets A, B, and I, a decidable index type, measurable coordinate types, and inclusions in I, assembling the projected blocks equals projection to their union.hypothesesconclusion= valuesProjection (union_subset hA hB)Proof (Lean source)
theorem valuesUnionMk_projection_comp {M : Type*} [DecidableEq M] {I A B : Finset M} {Ω' : M → Type*} [∀ n, MeasurableSpace (Ω' n)] (hA : A ⊆ I) (hB : B ⊆ I) : (fun ξ : ValuesOn I Ω' => valuesUnionMk (Ω := Ω') (valuesProjection hA ξ) (valuesProjection hB ξ)) = valuesProjection (union_subset hA hB) := by let hAB : A ∪ B ⊆ I := union_subset hA hB funext ξ ⟨i, hiAB⟩ by_cases hiA : i ∈ A · simp [valuesUnionMk, valuesProjection, hiA] · simp [valuesUnionMk, valuesProjection, hiA] -
valuesUnionMk_empty_rightlemma — For a finite set A, a decidable index type, measurable coordinate types, a dependent function a, and an empty-domain function e, right union with e recovers a.Proof (Lean source)
lemma valuesUnionMk_empty_right {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ m, MeasurableSpace (Ω m)] {A : Finset M} (a : ValuesOn A Ω) (e : ValuesOn (∅ : Finset M) Ω) : valuesEquivOfEq (union_empty A) (valuesUnionMk a e) = a := by funext ⟨v, hv⟩ have hvA : v ∈ A ∪ (∅ : Finset M) := by rwa [union_empty] change valuesUnionMk a e ⟨v, hvA⟩ = a ⟨v, hv⟩ simp only [valuesUnionMk, dif_pos hv] -
valuesEquivOfEq_heqlemma — For finite sets I and J, their equality, measurable coordinate types, a dependent function x, and an index type, canonical transport is heterogeneously equal to the original function.hypothesesconclusionHEq (valuesEquivOfEq h x) xProof (Lean source)
lemma valuesEquivOfEq_heq {M : Type*} {Ω : M → Type*} [∀ m, MeasurableSpace (Ω m)] {I J : Finset M} (h : I = J) (x : ValuesOn I Ω) : HEq (valuesEquivOfEq h x) x := by subst h exact heq_of_eq rfl -
valuesUnionMk_comm_heqlemma — For finite sets A and B, their disjointness, a decidable index type, measurable coordinate types, and dependent functions a and b, the two union orders are heterogeneously equal.hypothesesconclusionProof (Lean source)
lemma valuesUnionMk_comm_heq {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ m, MeasurableSpace (Ω m)] {A B : Finset M} (hAB : Disjoint A B) (a : ValuesOn A Ω) (b : ValuesOn B Ω) : HEq (valuesUnionMk a b) (valuesUnionMk b a) := by rw [← valuesUnionMk_comm hAB a b] exact (valuesEquivOfEq_heq _ _).symm -
valuesUnionMk_empty_right_heqlemma — For a finite set A, a decidable index type, measurable coordinate types, a dependent function a, and an empty-domain function e, their union is heterogeneously equal to a.hypothesesconclusionHEq (valuesUnionMk a e) aProof (Lean source)
lemma valuesUnionMk_empty_right_heq {M : Type*} [DecidableEq M] {Ω : M → Type*} [∀ m, MeasurableSpace (Ω m)] {A : Finset M} (a : ValuesOn A Ω) (e : ValuesOn (∅ : Finset M) Ω) : HEq (valuesUnionMk a e) a := by have h : valuesEquivOfEq (union_empty A) (valuesUnionMk a e) = a := valuesUnionMk_empty_right a e have hx : HEq (valuesUnionMk a e) (valuesEquivOfEq (union_empty A) (valuesUnionMk a e)) := (valuesEquivOfEq_heq (union_empty A) (valuesUnionMk a e)).symm rw [h] at hx exact hx -
measurable_singletonValuelemma — For an index type ι, measurable coordinate types, and an index v, reading a singleton assignment is measurable.hypothesesconclusionMeasurable (singletonValue (α := α) (v := v))Proof (Lean source)
@[fun_prop] lemma measurable_singletonValue {ι : Type*} {α : ι → Type*} [∀ i, MeasurableSpace (α i)] {v : ι} : Measurable (singletonValue (α := α) (v := v)) := by unfold singletonValue exact measurable_pi_apply (⟨v, by simp⟩ : {w // w ∈ ({v} : Finset ι)}) -
measurable_singletonValueslemma — For an index type ι, measurable coordinate types, and an index v, building a singleton assignment is measurable.hypothesesconclusionMeasurable (singletonValues (α := α) (v := v))Proof (Lean source)
@[fun_prop] lemma measurable_singletonValues {ι : Type*} {α : ι → Type*} [∀ i, MeasurableSpace (α i)] {v : ι} : Measurable (singletonValues (α := α) (v := v)) := by refine measurable_pi_iff.mpr ?_ rintro ⟨w, hw⟩ have h : w = v := by simpa using hw subst w change Measurable (id : α v → α v) exact measurable_id -
singletonValue_singletonValueslemma — For an index type ι, coordinate types, an index v, and a value x, reading its singleton assignment returns x.hypothesesι :Type*ι → Type*ιx :α vconclusionsingletonValue (α := α) (v := v) (singletonValues (α := α) (v := v) x) = xProof (Lean source)
@[simp] lemma singletonValue_singletonValues {ι : Type*} {α : ι → Type*} {v : ι} (x : α v) : singletonValue (α := α) (v := v) (singletonValues (α := α) (v := v) x) = x := by rfl -
singletonValues_singletonValuelemma — For an index type ι, coordinate types, an index v, and a singleton assignment x, rebuilding from its value returns x.hypothesesconclusionsingletonValues (α := α) (v := v) (singletonValue (α := α) (v := v) x) = xProof (Lean source)
@[simp] lemma singletonValues_singletonValue {ι : Type*} {α : ι → Type*} {v : ι} (x : ValuesOn ({v} : Finset ι) α) : singletonValues (α := α) (v := v) (singletonValue (α := α) (v := v) x) = x := by ext ⟨w, hw⟩ have hwv : w = v := by simpa using hw subst w rfl
IntegralBind 3 core · 3 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
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
3 supporting declarations (lemmas, instances)
-
integral_bind_of_ae_eq_consttheorem — 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.hypothesesα β E :hκ :hp :∀ a, IsProbabilityMeasure (κ a)hconst :∀ a, ∀ᵐ y ∂κ a, f y = f' ahf :Integrable f (m.bind κ)conclusion∫ y, f y ∂m.bind κ = ∫ a, f' a ∂mProof (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] -
map_bind_bind_map_projtheorem — 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.hypotheseshp₁ :∀ 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) = aProof (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] -
integral_bind_bind_map_projtheorem — 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).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) = ahf' :Integrable f mProof (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
Matrix 2 core · 0 supporting This module proves entrywise measurability of determinants and nonsingular inverses for finite real matrices whose entries vary measurably. ★ measurable_matrix_det★ measurable_matrix_inv_apply
Measurability of finite real matrix operations
This module proves entrywise measurability of determinants and nonsingular inverses for finite real matrices whose entries vary measurably.
theorem measurable_matrix_det reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a measurable source and finite index type, if every entry of a finite real matrix-valued function is measurable, then its determinant is measurable.
Formal statement
hypotheses
conclusion
Measurable (fun ω => (A ω).det)
Proof (Lean source)
@[fun_prop]
theorem measurable_matrix_det {Ω ι : Type*} [MeasurableSpace Ω]
[Fintype ι] [DecidableEq ι] (A : Ω → Matrix ι ι ℝ)
(hA : ∀ i j, Measurable (fun ω => A ω i j)) :
Measurable (fun ω => (A ω).det) := by
simp only [Matrix.det_apply]
apply Finset.measurable_fun_sum
intro σ _
apply measurable_const.smul
apply Finset.measurable_fun_prod
intro i _
exact hA (σ i) i
theorem measurable_matrix_inv_apply reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a measurable source and finite index type, if every entry of a finite real matrix-valued function is measurable, then the entry at the specified row and column of its nonsingular inverse is measurable.
Formal statement
hypotheses
conclusion
Measurable (fun ω => (A ω)⁻¹ i j)
Proof (Lean source)
@[fun_prop]
theorem measurable_matrix_inv_apply {Ω ι : Type*} [MeasurableSpace Ω]
[Fintype ι] [DecidableEq ι]
(A : Ω → Matrix ι ι ℝ)
(hA : ∀ i j, Measurable (fun ω => A ω i j)) (i j : ι) :
Measurable (fun ω => (A ω)⁻¹ i j) := by
rw [show (fun ω => (A ω)⁻¹ i j) =
fun ω => Ring.inverse (A ω).det * (A ω).adjugate i j by
funext ω
simp [Matrix.inv_def]]
simp_rw [Ring.inverse_eq_inv]
apply (measurable_matrix_det A hA).inv.mul
rw [show (fun ω => (A ω).adjugate i j) =
fun ω => ((A ω).updateRow j (single i 1)).det by
funext ω
exact Matrix.adjugate_apply _ _ _]
apply measurable_matrix_det
intro a b
by_cases ha : a = j
· subst a
simp [Matrix.updateRow_self]
· simp [Matrix.updateRow_apply, ha]
exact hA a b
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' 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' 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' 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 := Finset.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 := 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 measurable fibres of a finite-valued map and proves that weights constant on each fibre can be pulled outside the corresponding fibre integral. ★ integral_eq_sum_setIntegral_fiber★ integral_cellConst_mul
Finite-partition integral algebra
This file decomposes integrals over the measurable fibres of a finite-valued map and proves that weights constant on each fibre can be pulled outside the corresponding fibre integral.
The public lemmas are integral_eq_sum_setIntegral_fiber, integral_cellConst_mul, and
integral_cellConst, which turn a finite partition into finite sums of set integrals or fibre
weights.
theorem integral_eq_sum_setIntegral_fiber reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
The integral of a function is the sum of its integrals over the fibres of a finite-valued map when every fibre is measurable and the function is integrable.
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
A function weighted by a constant on each fibre integrates as the sum of the fibre integrals with their corresponding weights when every fibre is measurable, the weighting assigns a real number to each fibre, and the function is integrable.
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 — The integral of a function constant on each fibre is the sum of each constant times the measure of its fibre for a finite measure, provided every fibre is measurable and a real weight is assigned to each fibre. This is the constant-function case of integral_cellConst_mul.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 Finset.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 1 core · 1 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
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
1 supporting declaration (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 := 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
RadonNikodymSqrt 3 core · 2 supporting This module packages the square root of a finite measure's Radon--Nikodym derivative as an L² element. ★ rnSqrtDensityLp_self
Square-root Radon--Nikodym densities in L²
This module packages the square root of a finite measure's Radon--Nikodym
derivative as an L² element. For probability measures it also identifies the
base law's square-root density with the constant-one vector. These are the
measure-theoretic primitives used to state differentiability in quadratic mean.
def rnSqrtDensity reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a finite measure Q and a reference measure P, the square-root Radon--Nikodym density of Q relative to P is sqrt((dQ/dP).toReal).
Definition (Lean source)
parameters
Z :
Type u_1
P Q :
def
rnSqrtDensity P Q :
Z → ℝ
def rnSqrtDensityLp reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a finite measure Q and a reference measure P, the L² square-root Radon--Nikodym density is the equivalence class of sqrt(dQ/dP).
Definition (Lean source)
parameters
Z :
Type u_1
P Q :
def
given by
(rnSqrtDensity_memLp P Q).toLp (rnSqrtDensity P Q)
theorem rnSqrtDensityLp_self reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a probability measure P, its square-root density relative to itself is the constant-one L² vector.
Formal statement
Proof (Lean source)
@[simp] theorem rnSqrtDensityLp_self (P : Measure Z) [IsProbabilityMeasure P] :
rnSqrtDensityLp P P = lpOne P := by
apply Lp.ext
filter_upwards [(rnSqrtDensity_memLp P P).coeFn_toLp,
(memLp_const (1 : ℝ)).coeFn_toLp (p := 2) (μ := P),
Measure.rnDeriv_self P] with z hs h1 hrn
rw [show rnSqrtDensityLp P P z = rnSqrtDensity P P z from hs]
rw [show lpOne P z = (1 : ℝ) from h1]
simp [rnSqrtDensity, hrn]
2 supporting declarations (lemmas, instances)
-
lpNorm_sq_eq_integral_sqtheorem — For a real L² element f, its squared Hilbert norm is the integral of the square of any canonical representative.Proof (Lean source)
theorem lpNorm_sq_eq_integral_sq {P : Measure Z} (f : Lp ℝ 2 P) : ‖f‖ ^ 2 = ∫ z, f z ^ 2 ∂P := by rw [← real_inner_self_eq_norm_sq, L2.inner_def] apply integral_congr_ae filter_upwards with z simp only [real_inner_self_eq_norm_sq, Real.norm_eq_abs, sq_abs] -
rnSqrtDensity_memLptheorem — For a finite measure Q and a reference measure P, its square-root Radon--Nikodym density is square-integrable under P.Proof (Lean source)
theorem rnSqrtDensity_memLp (P Q : Measure Z) [IsFiniteMeasure Q] : MemLp (rnSqrtDensity P Q) 2 P := by have hmeas : Measurable (rnSqrtDensity P Q) := Real.continuous_sqrt.measurable.comp (ENNReal.measurable_toReal.comp (Measure.measurable_rnDeriv Q P)) apply (memLp_two_iff_integrable_sq_norm hmeas.aestronglyMeasurable).2 refine (Measure.integrable_toReal_rnDeriv (μ := Q) (ν := P)).congr ?_ filter_upwards [] with z simp only [rnSqrtDensity, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _), Real.sq_sqrt ENNReal.toReal_nonneg]
RnDerivBounds 1 core · 0 supporting This module converts almost-everywhere lower bounds on Radon--Nikodym derivatives into lower bounds on the real-valued masses of arbitrary sets. ★ measureReal_lower_of_rnDeriv_lower
Setwise bounds from Radon--Nikodym derivative bounds
This module converts almost-everywhere lower bounds on Radon--Nikodym derivatives into lower bounds on the real-valued masses of arbitrary sets.
theorem measureReal_lower_of_rnDeriv_lower reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
Given a measurable sample type, two finite measures, absolute continuity of the first with respect to the second, a real lower bound, an almost-everywhere lower bound on the real-valued Radon--Nikodym derivative, and a set, the first measure of that set is at least the lower bound times the second measure of the set.
Formal statement
Proof (Lean source)
theorem measureReal_lower_of_rnDeriv_lower {α : Type*} [MeasurableSpace α]
(μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
(hAC : μ ≪ ν) (c : ℝ)
(hden : ∀ᵐ x ∂ν, c ≤ (μ.rnDeriv ν x).toReal)
(E : Set α) :
c * ν.real E ≤ μ.real E := by
have hconst : IntegrableOn (fun _ : α => c) E ν := by
exact (integrable_const c).integrableOn
have hrn : IntegrableOn (fun x => (μ.rnDeriv ν x).toReal) E ν :=
(Measure.integrable_toReal_rnDeriv).integrableOn
have hbound : (fun _ : α => c) ≤ᵐ[ν.restrict E]
(fun x => (μ.rnDeriv ν x).toReal) :=
ae_restrict_of_ae hden
have hle := setIntegral_mono_ae_restrict hconst hrn hbound
simpa [Measure.setIntegral_toReal_rnDeriv hAC E, mul_comm] using hle
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, Nat.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, Nat.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 This file proves measurability and integrability of pointwise suprema over arbitrary index sets by reducing them to uniformly bounded families on countable dense skeletons. ★ integrable_sSup_image_of_countable_dense
Integrability of suprema over a countable-dense-skeletoned index class
This file proves measurability and integrability of pointwise suprema over arbitrary index sets by reducing them to uniformly bounded families on countable dense skeletons.
The API works on an arbitrary measurable space and reduces measurability and Bochner-integrability side conditions to countable suprema.
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
The pointwise supremum of a real-valued family is integrable under a finite measure when the family and its full and skeleton index sets have a nonnegative uniform bound, the skeleton is countable, each skeleton coordinate is measurable, the full and skeleton suprema agree pointwise, and the family is uniformly bounded in absolute value, with integration against the given measure.
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 — A supremum over an index set equals the supremum over a dense skeleton when the real functional is bounded above on the full set, the skeleton lies inside that set, and every full-set value is approached along a skeleton-valued sequence.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 of a real-valued family over an index set is measurable when the family and its full and skeleton index sets satisfy countability of the skeleton, measurability at each skeleton index, and pointwise equality of the full and skeleton suprema.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 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]
(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 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 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 :S :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] (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
TorusConvolution 2 core · 8 supporting Finite measures on a torus are determined by their integer Fourier coefficients, and a channel with no vanishing coefficient is injective under convolution. ★ markedConv_injective_right
Fourier uniqueness and marked convolution on the torus
Finite measures on a torus are determined by their integer Fourier coefficients, and a channel with no vanishing coefficient is injective under convolution. The same result holds when convolution changes only a torus coordinate of a marked measure. The module also supplies product-law factorizations after conditioning an independent channel on a record-based event.
def markedConv reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
The marked convolution of a marked torus measure and a torus channel is the pushforward that adds the channel only to the torus coordinate.
theorem markedConv_injective_right reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
A finite torus channel with no zero integer Fourier coefficient maps two finite marked torus measures with equal marked convolutions to the same marked measure.
Formal statement
hypotheses
T :
ℝ
β :
Type u_3
Fact (0 < T)
hκ :
∀ n : ℤ, (∫ x, fourier n x ∂κ) ≠ 0
hconv :
markedConv ρ κ = markedConv σ κ
conclusion
ρ = σ
Proof (Lean source)
theorem markedConv_injective_right [Fact (0 < T)]
(κ : Measure (AddCircle T)) (ρ σ : Measure (AddCircle T × β))
[IsFiniteMeasure κ] [IsFiniteMeasure ρ] [IsFiniteMeasure σ]
(hκ : ∀ n : ℤ, (∫ x, fourier n x ∂κ) ≠ 0)
(hconv : markedConv ρ κ = markedConv σ κ) : ρ = σ := by
apply Measure.ext_prod
intro A B hA hB
have hmark : MeasurableSet (Prod.snd ⁻¹' B : Set (AddCircle T × β)) :=
measurable_snd hB
have hrestricted :
(markedConv (ρ.restrict (Prod.snd ⁻¹' B)) κ) =
markedConv (σ.restrict (Prod.snd ⁻¹' B)) κ := by
rw [← markedConv_restrict_mark ρ κ B hB,
← markedConv_restrict_mark σ κ B hB, hconv]
have hmarg :
Measure.map fst (ρ.restrict (Prod.snd ⁻¹' B)) =
Measure.map fst (σ.restrict (Prod.snd ⁻¹' B)) := by
apply torus_conv_injective_right κ _ _ hκ
rw [← markedConv_map_fst, ← markedConv_map_fst, hrestricted]
have hAρ := congrArg (fun μ : Measure (AddCircle T) => μ A) hmarg
rw [Measure.map_apply measurable_fst hA,
Measure.map_apply measurable_fst hA,
Measure.restrict_apply' hmark,
Measure.restrict_apply' hmark] at hAρ
simpa only [preimage, Set.prod_eq] using hAρ
8 supporting declarations (lemmas, instances)
-
torus_measure_ext_of_fourier_eqtheorem — Two finite torus measures whose integer-character integrals agree are the same measure.hypothesesμ ν :h :∀ n : ℤ, (∫ x, fourier n x ∂μ) = ∫ x, fourier n x ∂νconclusionμ = νProof (Lean source)
theorem torus_measure_ext_of_fourier_eq [Fact (0 < T)] (μ ν : Measure (AddCircle T)) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : ∀ n : ℤ, (∫ x, fourier n x ∂μ) = ∫ x, fourier n x ∂ν) : μ = ν := by let A : StarSubalgebra ℂ (AddCircle T →ᵇ ℂ) := (fourierSubalgebra (T := T)).comap (BoundedContinuousFunction.toContinuousMapStarₐ ℂ) have hA : A.map (BoundedContinuousFunction.toContinuousMapStarₐ ℂ) = fourierSubalgebra (T := T) := by apply le_antisymm · rintro f ⟨g, hg, rfl⟩ exact hg · intro f hf exact ⟨BoundedContinuousFunction.mkOfCompact f, hf, rfl⟩ apply ext_of_forall_mem_subalgebra_integral_eq_of_polish (A := A) (by simpa [hA] using (fourierSubalgebra_separatesPoints (T := T))) intro g hg have hg' : (g.toContinuousMap : C(AddCircle T, ℂ)) ∈ span ℂ (range (fourier (T := T))) := by rw [← fourierSubalgebra_coe] exact hg have hspan : ∀ f : C(AddCircle T, ℂ), f ∈ span ℂ (range (fourier (T := T))) → (∫ x, f x ∂μ) = ∫ x, f x ∂ν := by intro f hf induction hf using Submodule.span_induction with | mem f hf => obtain ⟨n, rfl⟩ := hf exact h n | zero => simp | add f g hf hg ihf ihg => have hfμ : Integrable (fun x => f x) μ := (BoundedContinuousFunction.mkOfCompact f).integrable μ have hgμ : Integrable (fun x => g x) μ := (BoundedContinuousFunction.mkOfCompact g).integrable μ have hfν : Integrable (fun x => f x) ν := (BoundedContinuousFunction.mkOfCompact f).integrable ν have hgν : Integrable (fun x => g x) ν := (BoundedContinuousFunction.mkOfCompact g).integrable ν simp only [ContinuousMap.add_apply, integral_add hfμ hgμ, integral_add hfν hgν, ihf, ihg] | smul c f hf ih => simp only [ContinuousMap.smul_apply, smul_eq_mul, integral_const_mul, ih] exact hspan g.toContinuousMap hg' -
torus_integral_fourier_convtheorem — The integer index Fourier coefficient of the convolution of two finite torus measures is the product of their coefficients.hypothesesconclusion(∫ x, fourier n x ∂(μ ∗ ν)) = (∫ x, fourier n x ∂μ) * (∫ x, fourier n x ∂ν)Proof (Lean source)
theorem torus_integral_fourier_conv [Fact (0 < T)] (μ ν : Measure (AddCircle T)) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (n : ℤ) : (∫ x, fourier n x ∂(μ ∗ ν)) = (∫ x, fourier n x ∂μ) * (∫ x, fourier n x ∂ν) := by have hf : Integrable (fun x : AddCircle T => fourier n x) (μ ∗ ν) := by exact (BoundedContinuousFunction.mkOfCompact (fourier n)).integrable _ rw [integral_conv hf] simp_rw [fourier_apply, zsmul_add, toCircle_add, Circle.coe_mul] simp only [integral_const_mul, integral_mul_const] -
torus_conv_injective_righttheorem — A finite torus channel with no zero integer Fourier coefficient maps two finite torus measures with equal convolution outputs to the same input measure.hypothesesκ μ ν :hκ :∀ n : ℤ, (∫ x, fourier n x ∂κ) ≠ 0hconv :μ ∗ κ = ν ∗ κconclusionμ = νProof (Lean source)
theorem torus_conv_injective_right [Fact (0 < T)] (κ μ ν : Measure (AddCircle T)) [IsFiniteMeasure κ] [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hκ : ∀ n : ℤ, (∫ x, fourier n x ∂κ) ≠ 0) (hconv : μ ∗ κ = ν ∗ κ) : μ = ν := by apply torus_measure_ext_of_fourier_eq μ ν intro n have heq := congrArg (fun ρ : Measure (AddCircle T) => ∫ x, fourier n x ∂ρ) hconv rw [torus_integral_fourier_conv, torus_integral_fourier_conv] at heq exact mul_right_cancel₀ (hκ n) heq -
markedConv_restrict_marktheorem — Restricting a marked torus measure convolved with a torus channel to a measurable mark set commutes with marked convolution.Proof (Lean source)
theorem markedConv_restrict_mark (ρ : Measure (AddCircle T × β)) (κ : Measure (AddCircle T)) [SFinite ρ] [SFinite κ] (B : Set β) (hB : MeasurableSet B) : (markedConv ρ κ).restrict (Prod.snd ⁻¹' B) = markedConv (ρ.restrict (Prod.snd ⁻¹' B)) κ := by have hmarked : Measurable (fun p : (AddCircle T × β) × AddCircle T => (p.1.1 + p.2, p.1.2)) := by fun_prop have hmark : MeasurableSet (Prod.snd ⁻¹' B : Set (AddCircle T × β)) := measurable_snd hB have hpre : (fun p : (AddCircle T × β) × AddCircle T => (p.1.1 + p.2, p.1.2)) ⁻¹' (Prod.snd ⁻¹' B) = (Prod.snd ⁻¹' B) ×ˢ univ := by ext p simp rw [markedConv, Measure.restrict_map hmarked hmark, hpre, ← Measure.restrict_prod_eq_prod_univ] rfl -
markedConv_map_fsttheorem — The torus marginal of a marked torus measure after convolution with a torus channel is the convolution of its original marginal and that channel.Proof (Lean source)
theorem markedConv_map_fst (ρ : Measure (AddCircle T × β)) (κ : Measure (AddCircle T)) [SFinite ρ] [SFinite κ] : Measure.map Prod.fst (markedConv ρ κ) = (Measure.map Prod.fst ρ) ∗ κ := by have hmarked : Measurable (fun p : (AddCircle T × β) × AddCircle T => (p.1.1 + p.2, p.1.2)) := by fun_prop have hsum : Measurable (fun p : AddCircle T × AddCircle T => p.1 + p.2) := by fun_prop have hpair : Measurable (Prod.map Prod.fst id : (AddCircle T × β) × AddCircle T → AddCircle T × AddCircle T) := measurable_fst.prodMap measurable_id have hprod : (Measure.map Prod.fst ρ).prod κ = Measure.map (Prod.map Prod.fst id) (ρ.prod κ) := by simpa only [Measure.map_id] using (Measure.map_prod_map ρ κ measurable_fst measurable_id) calc Measure.map Prod.fst (markedConv ρ κ) = Measure.map (fun p : (AddCircle T × β) × AddCircle T => p.1.1 + p.2) (ρ.prod κ) := by rw [markedConv, Measure.map_map measurable_fst hmarked] rfl _ = Measure.map (fun p : AddCircle T × AddCircle T => p.1 + p.2) ((Measure.map Prod.fst ρ).prod κ) := by rw [hprod, Measure.map_map hsum hpair] rfl _ = (Measure.map Prod.fst ρ) ∗ κ := rfl -
independent_channel_map_condtheorem — Under a probability law, a measurable torus channel and a measurable record that are independent, conditioning on a measurable record event with positive probability leaves the channel marginal unchanged.hypothesesProof (Lean source)
theorem independent_channel_map_cond (P : Measure Ω) [IsProbabilityMeasure P] (U : Ω → AddCircle T) (R : Ω → L) (hU : Measurable U) (hR : Measurable R) (hind : IndepFun U R P) (A : Set L) (hA : MeasurableSet A) (hpos : P (R ⁻¹' A) ≠ 0) : (cond P (R ⁻¹' A)).map U = P.map U := by have hEA : MeasurableSet (R ⁻¹' A) := hR hA have htop : P (R ⁻¹' A) ≠ (⊤ : ENNReal) := measure_ne_top P _ ext S hS rw [Measure.map_apply hU hS, ProbabilityTheory.cond_apply hEA, Measure.map_apply hU hS] rw [Set.inter_comm, hind.measure_inter_preimage_eq_mul S A hS hA] rw [mul_comm (P (U ⁻¹' S)) (P (R ⁻¹' A)), ← mul_assoc, ENNReal.inv_mul_cancel hpos htop, one_mul] -
independent_channel_record_map_condtheorem — Under a probability law, a measurable torus channel and a measurable record that are independent, conditioning on a measurable record event with positive probability makes the joint law the product of the unchanged channel law and the conditioned record law.hypothesesProof (Lean source)
theorem independent_channel_record_map_cond (P : Measure Ω) [IsProbabilityMeasure P] (U : Ω → AddCircle T) (R : Ω → L) (hU : Measurable U) (hR : Measurable R) (hind : IndepFun U R P) (A : Set L) (hA : MeasurableSet A) (hpos : P (R ⁻¹' A) ≠ 0) : (cond P (R ⁻¹' A)).map (fun ω => (U ω, R ω)) = (P.map U).prod ((cond P (R ⁻¹' A)).map R) := by have _hpos : P (R ⁻¹' A) ≠ 0 := hpos let F : Ω → AddCircle T × L := fun ω => (U ω, R ω) have hF : Measurable F := hU.prodMk hR have hEA : MeasurableSet (R ⁻¹' A) := hR hA have hbase : P.map F = (P.map U).prod (P.map R) := hind.map_prod_eq_prod_map_map hU.aemeasurable hR.aemeasurable have hpre : F ⁻¹' (univ ×ˢ A) = R ⁻¹' A := by ext ω; simp [F] have hrest : (P.restrict (R ⁻¹' A)).map F = (P.map U).prod ((P.restrict (R ⁻¹' A)).map R) := by calc (P.restrict (R ⁻¹' A)).map F = (P.map F).restrict (univ ×ˢ A) := by rw [Measure.restrict_map hF (MeasurableSet.univ.prod hA), hpre] _ = (P.map U).prod ((P.restrict (R ⁻¹' A)).map R) := by rw [hbase, ← Measure.prod_restrict, Measure.restrict_univ, Measure.restrict_map hR hA] simp only [cond, Measure.map_smul] rw [hrest, Measure.prod_smul_right] -
independent_channel_mark_restrict_condtheorem — Under a probability law, a measurable torus channel and a measurable record with a measurable mark map that are independent, conditioning on a measurable record event with positive probability and then restricting to a measurable mark set preserves the channel-product factorization.hypothesesProof (Lean source)
theorem independent_channel_mark_restrict_cond (P : Measure Ω) [IsProbabilityMeasure P] (U : Ω → AddCircle T) (R : Ω → L) (M : L → β) (hU : Measurable U) (hR : Measurable R) (hM : Measurable M) (hind : IndepFun U R P) (A : Set L) (hA : MeasurableSet A) (hpos : P (R ⁻¹' A) ≠ 0) (B : Set β) (hB : MeasurableSet B) : ((cond P (R ⁻¹' A)).map (fun ω => (U ω, M (R ω)))).restrict (snd ⁻¹' B) = (P.map U).prod (((cond P (R ⁻¹' A)).map (M ∘ R)).restrict B) := by have _hB : MeasurableSet B := hB have hpair : Measurable (fun ω : Ω => (U ω, R ω)) := hU.prodMk hR have hmap : Measurable (Prod.map id M : AddCircle T × L → AddCircle T × β) := measurable_id.prodMap hM have hcomp : (fun ω : Ω => (U ω, M (R ω))) = (Prod.map id M) ∘ (fun ω : Ω => (U ω, R ω)) := rfl rw [hcomp, ← Measure.map_map hmap hpair, independent_channel_record_map_cond P U R hU hR hind A hA hpos, ← Measure.map_prod_map (P.map U) ((cond P (R ⁻¹' A)).map R) measurable_id hM] simp only [Measure.map_id] have hBprod : snd ⁻¹' B = (Set.univ ×ˢ B : Set (AddCircle T × β)) := by ext p; simp rw [hBprod, ← Measure.prod_restrict, Measure.restrict_univ] congr 1 rw [Measure.map_map hM hR]
WithDensityInverse 1 core · 0 supporting This file supplies a real-valued form of density cancellation: weighting a measure by the nonnegative density 1 / h and then by h recovers the original measure whenever h is positive almost everywhere. ★ withDensity_one_div_ofReal_cancel
Cancellation for reciprocal real densities
This file supplies a real-valued form of density cancellation: weighting a
measure by the nonnegative density 1 / h and then by h recovers the
original measure whenever h is positive almost everywhere.
theorem withDensity_one_div_ofReal_cancel reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
For a measure, a measurable real function, and the assumption that the function is positive almost everywhere, weighting the measure first by max(1/h,0) and then by max(h,0) recovers the original measure.
Formal statement
hypotheses
Proof (Lean source)
theorem withDensity_one_div_ofReal_cancel
{α : Type*} [MeasurableSpace α] (μ : Measure α) (h : α → ℝ)
(hh : Measurable h) (hpos : ∀ᵐ a ∂μ, 0 < h a) :
(μ.withDensity (fun a => ofReal (1 / h a))).withDensity
(fun a => ofReal (h a)) = μ := by
rw [← withDensity_mul μ (by fun_prop) (by fun_prop)]
rw [withDensity_congr_ae]
· exact withDensity_one
filter_upwards [hpos] with a ha
simp only [Pi.mul_apply, Pi.one_apply]
rw [← ENNReal.ofReal_mul (by positivity : 0 ≤ 1 / h a)]
convert ENNReal.ofReal_one using 1
field_simp
WithDensityTransport 1 core · 0 supporting This module shows that weighting a source measure by a density pulled back along a measure-preserving measurable equivalence commutes with pushing that measure forward. ★ map_withDensity_comp_measurableEquiv
Weighted-measure transport under measurable equivalences
This module shows that weighting a source measure by a density pulled back along a measure-preserving measurable equivalence commutes with pushing that measure forward.
theorem map_withDensity_comp_measurableEquiv reviewed
⚑ flagged
Causalean.Mathlib.MeasureTheory
With a measurable equivalence, a certificate that it preserves the two measures, and a target-domain density, pushing forward the source measure weighted by the pulled-back density yields the target measure weighted by that density.
Formal statement
hypotheses
conclusion
Measure.map e (μ.withDensity (d ∘ e)) = μ'.withDensity d
Proof (Lean source)
theorem map_withDensity_comp_measurableEquiv
{Ω Ω' : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω']
(e : Ω ≃ᵐ Ω') {μ : Measure Ω} {μ' : Measure Ω'}
(he : MeasurePreserving e μ μ') (d : Ω' → ℝ≥0∞) :
Measure.map e (μ.withDensity (d ∘ e)) = μ'.withDensity d := by
ext s hs
rw [Measure.map_apply e.measurable hs,
withDensity_apply _ (e.measurable hs), withDensity_apply _ hs]
rw [← lintegral_indicator (e.measurable hs), ← lintegral_indicator hs]
rw [he.lintegral_map_equiv (s.indicator d) e]
congr 1