stronglyMeasurable_of_measurableSpace_le_on

English

If the restriction of one sigma-algebra m to a set s is contained in the restriction of another m2 on all intersections with s, and f is m-strongly measurable vanishing outside s, then f is m2-strongly measurable.

Русский

Если ограничение сигма-алгебры m к множеству s вложено в ограничение m2 на все пересечения с s и f на m-области сильно измеримо и ноль вне s, то f сильно измеримо и по m2.

LaTeX

$$$(\forall t\, MeasurableSet[m](s\cap t) \Rightarrow MeasurableSet[m2](s\cap t)) \land hs_m : MeasurableSet[m] s \to \text{функция } f \text{ сильнос-Measurable}_m2$$$

Lean4

/-- If the restriction to a set `s` of a σ-algebra `m` is included in the restriction to `s` of
another σ-algebra `m₂` (hypothesis `hs`), the set `s` is `m` measurable and a function `f` supported
on `s` is `m`-strongly-measurable, then `f` is also `m₂`-strongly-measurable. -/
theorem stronglyMeasurable_of_measurableSpace_le_on {α E} {m m₂ : MeasurableSpace α} [TopologicalSpace E] [Zero E]
    {s : Set α} {f : α → E} (hs_m : MeasurableSet[m] s) (hs : ∀ t, MeasurableSet[m] (s ∩ t) → MeasurableSet[m₂] (s ∩ t))
    (hf : StronglyMeasurable[m] f) (hf_zero : ∀ x ∉ s, f x = 0) : StronglyMeasurable[m₂] f :=
  by
  have hs_m₂ : MeasurableSet[m₂] s := by
    rw [← Set.inter_univ s]
    refine hs Set.univ ?_
    rwa [Set.inter_univ]
  obtain ⟨g_seq_s, hg_seq_tendsto, hg_seq_zero⟩ := stronglyMeasurable_in_set hs_m hf hf_zero
  let g_seq_s₂ : ℕ → @SimpleFunc α m₂ E := fun n =>
    { toFun := g_seq_s n
      measurableSet_fiber' := fun x =>
        by
        rw [← Set.inter_univ (g_seq_s n ⁻¹' { x }), ← Set.union_compl_self s, Set.inter_union_distrib_left,
          Set.inter_comm (g_seq_s n ⁻¹' { x })]
        refine MeasurableSet.union (hs _ (hs_m.inter ?_)) ?_
        · exact @SimpleFunc.measurableSet_fiber _ _ m _ _
        by_cases hx : x = 0
        · suffices g_seq_s n ⁻¹' { x } ∩ sᶜ = sᶜ by
            rw [this]
            exact hs_m₂.compl
          ext1 y
          rw [hx, Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff]
          exact ⟨fun h => h.2, fun h => ⟨hg_seq_zero y h n, h⟩⟩
        · suffices g_seq_s n ⁻¹' { x } ∩ sᶜ = ∅ by
            rw [this]
            exact MeasurableSet.empty
          ext1 y
          simp only [mem_inter_iff, mem_preimage, mem_singleton_iff, mem_compl_iff, mem_empty_iff_false, iff_false,
            not_and, not_notMem]
          refine Function.mtr fun hys => ?_
          rw [hg_seq_zero y hys n]
          exact Ne.symm hx
      finite_range' := @SimpleFunc.finite_range _ _ m (g_seq_s n) }
  exact ⟨g_seq_s₂, hg_seq_tendsto⟩

Похожие утверждения