Measurable section theorems

instance MeasureTheory.instMeasurableInf₂WithTopNNReal_brownianMotion : MeasurableInf₂ (WithTop NNReal)

theorem MeasureTheory.infClosed_insert_empty_Icc {ι : Type} [LinearOrder ι] : InfClosed (insert ∅ {t : Set ι | ∃ (a : ι) (b : ι), Set.Icc a b = t})

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

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

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

theorem MeasureTheory.measure_debut_ne_top_mono {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {A B : Set (ι × Ω)} (hAB : A ⊆ B) (u : ι) : μ {ω : Ω | debut A u ω ≠ ⊤} ≤ μ {ω : Ω | debut B u ω ≠ ⊤}

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

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

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

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

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

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