comap_eval_le_generateFrom_squareCylinders_singleton

English

For each i, the comap of the i-th projection’s σ-algebra is contained in the σ-algebra generated by fixing the i-th coordinate to a measurable set and varying the others.

Русский

Для каждого i прообраз σ-алгебры по i-й проекции вложен в σ-алгебру, порождаемую фиксацией i-й координаты к измеримому множеству и варьированием остальных координат.

LaTeX

$$$$\\mathcal{M}_{i}^{\\mathrm{comap}} \\le \\mathrm{generateFrom}\\big( (\\{ i \\} : \\mathrm{Set}\\,\\iota) \\ pi t \\big) '' (\\mathrm{univ} \\ pi (\\lambda i, \\{s: \\mathrm{Set}(\\alpha_i) \\mid \\mathrm{MeasurableSet}(s)\\})) $$$$

Lean4

theorem comap_eval_le_generateFrom_squareCylinders_singleton (α : ι → Type*) [m : ∀ i, MeasurableSpace (α i)] (i : ι) :
    MeasurableSpace.comap (Function.eval i) (m i) ≤
      MeasurableSpace.generateFrom
        ((fun t ↦ ({ i } : Set ι).pi t) '' univ.pi fun i ↦ {s : Set (α i) | MeasurableSet s}) :=
  by
  simp only [singleton_pi]
  rw [MeasurableSpace.comap_eq_generateFrom]
  refine MeasurableSpace.generateFrom_mono fun S ↦ ?_
  simp only [mem_setOf_eq, mem_image, mem_univ_pi, forall_exists_index, and_imp]
  intro t ht h
  classical
  refine ⟨fun j ↦ if hji : j = i then by convert t else univ, fun j ↦ ?_, ?_⟩
  · by_cases hji : j = i
    · simp only [hji, eq_mpr_eq_cast, dif_pos]
      convert ht
      simp only [cast_heq]
    · simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]
  · grind

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