Measurable section theorems

Let s be a subset of ℝ≥0 × Ω that is analytic for the paving of measurable sets (for example a measurable set) and let μ be an s-finite measure on Ω. We prove that there is a measurable τ : Ω → WithTop ℝ≥0 whose graph is contained in s where τ ≠ ⊤, and such that τ ω ≠ ⊤ for μ-almost every ω in the projection of s on Ω.

For a subset s of 𝓨 × Ω with 𝓨 a nonempty standard Borel space, we obtain a measurable τ : Ω → 𝓨 and a measurable set A, almost everywhere equal to the projection of s, such that (τ ω, ω) ∈ s for ω ∈ A.

Main statements

• MeasureTheory.IsPavingAnalytic.exists_measurable_section_left_nnreal: measurable section theorem for an analytic subset of ℝ≥0 × Ω.
• MeasureTheory.IsPavingAnalytic.exists_measurable_section_right_nnreal: the same for an analytic subset of Ω × ℝ≥0.
• MeasurableSet.exists_measurable_section_left_nnreal, MeasurableSet.exists_measurable_section_right_nnreal: the same for measurable sets.
• MeasureTheory.IsPavingAnalytic.exists_measurable_section_left, MeasureTheory.IsPavingAnalytic.exists_measurable_section_right, MeasurableSet.exists_measurable_section_left, MeasurableSet.exists_measurable_section_right: measurable section theorems for subsets of 𝓨 × Ω and Ω × 𝓨, with 𝓨 a nonempty standard Borel space.

Implementation notes

The section is obtained as the infimum of a sequence of measurable sections: at each step, we use Choquet's capacitability theorem to get a measurable section of the part of s above the set where the previous sections are ⊤, defined on a set of at least half the measure of the projection of that part.

For a standard Borel space 𝓨, we embed 𝓨 in ℝ≥0 and use the result for ℝ≥0. The section is a function Ω → 𝓨 together with the measurable set on which it is a section, rather than a function Ω → Option 𝓨, since Option 𝓨 has no measurable space structure in Mathlib.

References

• [S. He, J. Wang and J. Yan, Semimartingale theory and stochastic calculus][he2019semimartingale]

theorem MeasureTheory.exists_nullMeasurable_section_measure_ge {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] {s : Set (NNReal × Ω)} (hs : IsPavingAnalytic {t : Set (NNReal × Ω) | MeasurableSet t} s) (a : ENNReal) (ha : a < μ (Prod.snd '' s)) : ∃ (τ : Ω → WithTop NNReal), NullMeasurable τ μ ∧ (∀ (ω : Ω), τ ω ≠ ⊤ → ((τ ω).untopA, ω) ∈ s) ∧ a ≤ μ {ω : Ω | τ ω ≠ ⊤} ∧ debut s 0 ≤ τ

Let s be an analytic subset of ℝ≥0 × Ω and μ a finite measure. For every a smaller than the measure of the projection of s, there is a null-measurable τ : Ω → WithTop ℝ≥0 with graph contained in s (where τ ≠ ⊤), such that a ≤ μ {ω | τ ω ≠ ⊤} and debut s 0 ≤ τ.

theorem MeasureTheory.exists_measurable_section_measure_ge {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] {s : Set (NNReal × Ω)} (hs : IsPavingAnalytic {t : Set (NNReal × Ω) | MeasurableSet t} s) (a : ENNReal) (ha : a < μ (Prod.snd '' s)) : ∃ (τ : Ω → WithTop NNReal), Measurable τ ∧ (∀ (ω : Ω), τ ω ≠ ⊤ → ((τ ω).untopA, ω) ∈ s) ∧ a ≤ μ {ω : Ω | τ ω ≠ ⊤} ∧ debut s 0 ≤ τ

Let s be an analytic subset of ℝ≥0 × Ω and μ a finite measure. For every a smaller than the measure of the projection of s, there is a measurable τ : Ω → WithTop ℝ≥0 with graph contained in s (where τ ≠ ⊤), such that a ≤ μ {ω | τ ω ≠ ⊤} and debut s 0 ≤ τ.

theorem MeasureTheory.isPavingAnalytic_section_eq_top {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {τ : Ω → WithTop NNReal} (hτ_meas : Measurable τ) : IsPavingAnalytic {t : Set (NNReal × Ω) | MeasurableSet t} {(fst, ω) : NNReal × Ω | τ ω = ⊤}

theorem MeasureTheory.IsPavingAnalytic.exists_measurable_section_left_nnreal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {s : Set (NNReal × Ω)} (hs : IsPavingAnalytic {t : Set (NNReal × Ω) | MeasurableSet t} s) (μ : Measure Ω) [SFinite μ] : ∃ (τ : Ω → WithTop NNReal), Measurable τ ∧ (∀ (ω : Ω), τ ω ≠ ⊤ → ((τ ω).untopA, ω) ∈ s) ∧ ∀ᵐ (ω : Ω) ∂μ, ω ∈ Prod.snd '' s ↔ τ ω ≠ ⊤

Measurable section theorem: let s be an analytic subset of ℝ≥0 × Ω and μ an s-finite measure. There is a measurable τ : Ω → WithTop ℝ≥0 with graph contained in s where τ ≠ ⊤, and such that τ ω ≠ ⊤ for μ-almost every ω in the projection of s.

theorem MeasureTheory.IsPavingAnalytic.exists_measurable_section_right_nnreal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {s : Set (Ω × NNReal)} (hs : IsPavingAnalytic {t : Set (Ω × NNReal) | MeasurableSet t} s) (μ : Measure Ω) [SFinite μ] : ∃ (τ : Ω → WithTop NNReal), Measurable τ ∧ (∀ (ω : Ω), τ ω ≠ ⊤ → (ω, (τ ω).untopA) ∈ s) ∧ ∀ᵐ (ω : Ω) ∂μ, ω ∈ Prod.fst '' s ↔ τ ω ≠ ⊤

Measurable section theorem: let s be an analytic subset of Ω × ℝ≥0 and μ an s-finite measure. There is a measurable τ : Ω → WithTop ℝ≥0 with graph contained in s where τ ≠ ⊤, and such that τ ω ≠ ⊤ for μ-almost every ω in the projection of s.

theorem MeasureTheory.IsMeasurableAnalytic.exists_measurable_section_left_nnreal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {s : Set (NNReal × Ω)} (hs : IsMeasurableAnalytic s) (μ : Measure Ω) [SFinite μ] : ∃ (τ : Ω → WithTop NNReal), Measurable τ ∧ (∀ (ω : Ω), τ ω ≠ ⊤ → ((τ ω).untopA, ω) ∈ s) ∧ ∀ᵐ (ω : Ω) ∂μ, ω ∈ Prod.snd '' s ↔ τ ω ≠ ⊤

Measurable section theorem for a measurably analytic subset of ℝ≥0 × Ω.

theorem MeasureTheory.IsMeasurableAnalytic.exists_measurable_section_right_nnreal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {s : Set (Ω × NNReal)} (hs : IsMeasurableAnalytic s) (μ : Measure Ω) [SFinite μ] : ∃ (τ : Ω → WithTop NNReal), Measurable τ ∧ (∀ (ω : Ω), τ ω ≠ ⊤ → (ω, (τ ω).untopA) ∈ s) ∧ ∀ᵐ (ω : Ω) ∂μ, ω ∈ Prod.fst '' s ↔ τ ω ≠ ⊤

Measurable section theorem for a measurably analytic subset of Ω × ℝ≥0.

theorem MeasurableSet.exists_measurable_section_left_nnreal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {s : Set (NNReal × Ω)} (hs : MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] : ∃ (τ : Ω → WithTop NNReal), Measurable τ ∧ (∀ (ω : Ω), τ ω ≠ ⊤ → ((τ ω).untopA, ω) ∈ s) ∧ ∀ᵐ (ω : Ω) ∂μ, ω ∈ Prod.snd '' s ↔ τ ω ≠ ⊤

Measurable section theorem for a measurable subset of ℝ≥0 × Ω.

theorem MeasurableSet.exists_measurable_section_right_nnreal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {s : Set (Ω × NNReal)} (hs : MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] : ∃ (τ : Ω → WithTop NNReal), Measurable τ ∧ (∀ (ω : Ω), τ ω ≠ ⊤ → (ω, (τ ω).untopA) ∈ s) ∧ ∀ᵐ (ω : Ω) ∂μ, ω ∈ Prod.fst '' s ↔ τ ω ≠ ⊤

Measurable section theorem for a measurable subset of Ω × ℝ≥0.

Measurable section theorem for a standard Borel space

theorem MeasureTheory.exists_measurableEmbedding_nnreal (𝓨 : Type u_2) [MeasurableSpace 𝓨] [StandardBorelSpace 𝓨] : ∃ (e : 𝓨 → NNReal), MeasurableEmbedding e

A standard Borel space admits a measurable embedding into ℝ≥0.

theorem MeasureTheory.IsPavingAnalytic.exists_measurable_section_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] {s : Set (𝓨 × Ω)} (hs : IsPavingAnalytic {t : Set (𝓨 × Ω) | MeasurableSet t} s) (μ : Measure Ω) [SFinite μ] : ∃ (τ : Ω → 𝓨) (A : Set Ω), Measurable τ ∧ MeasurableSet A ∧ (∀ ω ∈ A, (τ ω, ω) ∈ s) ∧ A =ᵐ[μ] Prod.snd '' s

Measurable section theorem: let s be an analytic subset of 𝓨 × Ω, with 𝓨 a nonempty standard Borel space, and let μ be an s-finite measure. There is a measurable τ : Ω → 𝓨 and a measurable set A such that (τ ω, ω) ∈ s for ω ∈ A, and A is μ-almost everywhere equal to the projection of s.

theorem MeasureTheory.IsPavingAnalytic.exists_measurable_section_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] {s : Set (Ω × 𝓨)} (hs : IsPavingAnalytic {t : Set (Ω × 𝓨) | MeasurableSet t} s) (μ : Measure Ω) [SFinite μ] : ∃ (τ : Ω → 𝓨) (A : Set Ω), Measurable τ ∧ MeasurableSet A ∧ (∀ ω ∈ A, (ω, τ ω) ∈ s) ∧ A =ᵐ[μ] Prod.fst '' s

Measurable section theorem: let s be an analytic subset of Ω × 𝓨, with 𝓨 a nonempty standard Borel space, and let μ be an s-finite measure. There is a measurable τ : Ω → 𝓨 and a measurable set A such that (ω, τ ω) ∈ s for ω ∈ A, and A is μ-almost everywhere equal to the projection of s.

theorem MeasureTheory.IsMeasurableAnalytic.exists_measurable_section_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] {s : Set (𝓨 × Ω)} (hs : IsMeasurableAnalytic s) (μ : Measure Ω) [SFinite μ] : ∃ (τ : Ω → 𝓨) (A : Set Ω), Measurable τ ∧ MeasurableSet A ∧ (∀ ω ∈ A, (τ ω, ω) ∈ s) ∧ A =ᵐ[μ] Prod.snd '' s

Measurable section theorem for a measurably analytic subset of 𝓨 × Ω, with 𝓨 a nonempty standard Borel space.

theorem MeasureTheory.IsMeasurableAnalytic.exists_measurable_section_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] {s : Set (Ω × 𝓨)} (hs : IsMeasurableAnalytic s) (μ : Measure Ω) [SFinite μ] : ∃ (τ : Ω → 𝓨) (A : Set Ω), Measurable τ ∧ MeasurableSet A ∧ (∀ ω ∈ A, (ω, τ ω) ∈ s) ∧ A =ᵐ[μ] Prod.fst '' s

Measurable section theorem for a measurably analytic subset of Ω × 𝓨, with 𝓨 a nonempty standard Borel space.

theorem MeasurableSet.exists_measurable_section_left {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] {s : Set (𝓨 × Ω)} (hs : MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] : ∃ (τ : Ω → 𝓨) (A : Set Ω), Measurable τ ∧ MeasurableSet A ∧ (∀ ω ∈ A, (τ ω, ω) ∈ s) ∧ A =ᵐ[μ] Prod.snd '' s

Measurable section theorem for a measurable subset of 𝓨 × Ω, with 𝓨 a nonempty standard Borel space.

theorem MeasurableSet.exists_measurable_section_right {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] {s : Set (Ω × 𝓨)} (hs : MeasurableSet s) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SFinite μ] : ∃ (τ : Ω → 𝓨) (A : Set Ω), Measurable τ ∧ MeasurableSet A ∧ (∀ ω ∈ A, (ω, τ ω) ∈ s) ∧ A =ᵐ[μ] Prod.fst '' s

Measurable section theorem for a measurable subset of Ω × 𝓨, with 𝓨 a nonempty standard Borel space.