Additive content built from a projective family of measures #
Let P be a projective family of measures on a family of measurable spaces indexed by ι.
That is, for each finite set I of indices, P I is a measure on Π j : I, α j, and for J ⊆ I,
the projection from Π i : I, α i to Π i : J, α i maps P I to P J.
We build an additive content projectiveFamilyContent on the measurable cylinders, by setting
projectiveFamilyContent s = P I S for s = cylinder I S, where I is a finite set of indices
and S is a measurable set in Π i : I, α i.
This content will be used to define the projective limit of the family of measures P.
For a countable index set and a projective family given by a sequence of kernels,
the projective limit is given by the Ionescu-Tulcea theorem.
For an arbitrary index set but under topological conditions on the spaces, this is the result of
the Kolmogorov extension theorem.
(both results are not yet in Mathlib)
Main definitions #
projectiveFamilyContent: additive content on the measurable cylinders, defined from a projective family of measures.
theorem
MeasureTheory.isSetAlgebra_measurableCylinders
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
:
theorem
MeasureTheory.isSetRing_measurableCylinders
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
:
theorem
MeasureTheory.isSetSemiring_measurableCylinders
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
:
noncomputable def
MeasureTheory.projectiveFamilyFun
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
(P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j))
(s : Set ((i : ι) → α i))
:
For P a family of measures, with P J a measure on Π j : J, α j, we define a function
projectiveFamilyFun P s by setting it to P I S if s = cylinder I S for a measurable S and
to 0 if s is not a measurable cylinder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.projectiveFamilyFun_congr
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s : Set ((i : ι) → α i)}
{I : Finset ι}
{S : Set ((i : ↥I) → α ↑i)}
(hP : IsProjectiveMeasureFamily P)
(hs : s ∈ measurableCylinders α)
(hs_eq : s = cylinder I S)
(hS : MeasurableSet S)
:
theorem
MeasureTheory.projectiveFamilyFun_empty
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
(hP : IsProjectiveMeasureFamily P)
:
theorem
MeasureTheory.projectiveFamilyFun_union
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s t : Set ((i : ι) → α i)}
(hP : IsProjectiveMeasureFamily P)
(hs : s ∈ measurableCylinders α)
(ht : t ∈ measurableCylinders α)
(hst : Disjoint s t)
:
noncomputable def
MeasureTheory.projectiveFamilyContent
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
(hP : IsProjectiveMeasureFamily P)
:
For P a projective family of measures, we define an additive content on the measurable
cylinders, by setting projectiveFamilyContent s = P I S for s = cylinder I S, where I is
a finite set of indices and S is a measurable set in Π i : I, α i.
Equations
Instances For
theorem
MeasureTheory.projectiveFamilyContent_eq
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s : Set ((i : ι) → α i)}
(hP : IsProjectiveMeasureFamily P)
:
theorem
MeasureTheory.projectiveFamilyContent_congr
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{I : Finset ι}
{S : Set ((i : ↥I) → α ↑i)}
(hP : IsProjectiveMeasureFamily P)
(s : Set ((i : ι) → α i))
(hs_eq : s = cylinder I S)
(hS : MeasurableSet S)
:
theorem
MeasureTheory.projectiveFamilyContent_cylinder
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{I : Finset ι}
{S : Set ((i : ↥I) → α ↑i)}
(hP : IsProjectiveMeasureFamily P)
(hS : MeasurableSet S)
:
theorem
MeasureTheory.projectiveFamilyContent_mono
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s t : Set ((i : ι) → α i)}
(hP : IsProjectiveMeasureFamily P)
(hs : s ∈ measurableCylinders α)
(ht : t ∈ measurableCylinders α)
(hst : s ⊆ t)
:
theorem
MeasureTheory.projectiveFamilyContent_iUnion_le
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
(hP : IsProjectiveMeasureFamily P)
{s : ℕ → Set ((i : ι) → α i)}
(hs : ∀ (n : ℕ), s n ∈ measurableCylinders α)
(n : ℕ)
:
(projectiveFamilyContent hP) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i) ≤ ∑ i ∈ Finset.range (n + 1), (projectiveFamilyContent hP) (s i)
theorem
MeasureTheory.projectiveFamilyContent_ne_top
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s : Set ((i : ι) → α i)}
[∀ (J : Finset ι), IsFiniteMeasure (P J)]
(hP : IsProjectiveMeasureFamily P)
:
theorem
MeasureTheory.projectiveFamilyContent_sdiff
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s t : Set ((i : ι) → α i)}
(hP : IsProjectiveMeasureFamily P)
(hs : s ∈ measurableCylinders α)
(ht : t ∈ measurableCylinders α)
:
(projectiveFamilyContent hP) s - (projectiveFamilyContent hP) t ≤ (projectiveFamilyContent hP) (s \ t)
@[deprecated MeasureTheory.projectiveFamilyContent_sdiff (since := "2026-06-03")]
theorem
MeasureTheory.projectiveFamilyContent_diff
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s t : Set ((i : ι) → α i)}
(hP : IsProjectiveMeasureFamily P)
(hs : s ∈ measurableCylinders α)
(ht : t ∈ measurableCylinders α)
:
(projectiveFamilyContent hP) s - (projectiveFamilyContent hP) t ≤ (projectiveFamilyContent hP) (s \ t)
theorem
MeasureTheory.projectiveFamilyContent_sdiff_of_subset
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s t : Set ((i : ι) → α i)}
[∀ (J : Finset ι), IsFiniteMeasure (P J)]
(hP : IsProjectiveMeasureFamily P)
(hs : s ∈ measurableCylinders α)
(ht : t ∈ measurableCylinders α)
(hts : t ⊆ s)
:
(projectiveFamilyContent hP) (s \ t) = (projectiveFamilyContent hP) s - (projectiveFamilyContent hP) t
@[deprecated MeasureTheory.projectiveFamilyContent_sdiff_of_subset (since := "2026-06-03")]
theorem
MeasureTheory.projectiveFamilyContent_diff_of_subset
{ι : Type u_1}
{α : ι → Type u_2}
{mα : (i : ι) → MeasurableSpace (α i)}
{P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)}
{s t : Set ((i : ι) → α i)}
[∀ (J : Finset ι), IsFiniteMeasure (P J)]
(hP : IsProjectiveMeasureFamily P)
(hs : s ∈ measurableCylinders α)
(ht : t ∈ measurableCylinders α)
(hts : t ⊆ s)
:
(projectiveFamilyContent hP) (s \ t) = (projectiveFamilyContent hP) s - (projectiveFamilyContent hP) t
Alias of MeasureTheory.projectiveFamilyContent_sdiff_of_subset.