pi_map_piOptionEquivProd — Mathlib

English

A product over an index set with an extra coordinate (Option) is measure-theoretically equivalent to a product of the individual coordinates after applying a canonical pairing; the pushforward under this canonical equivalence preserves the product measure.

Русский

Произведение по индексу с дополнительной координатой (Option) эквивалентно произведению по каждому координатному множителю после применения канонического отображения; перенесение через это отображение сохраняет произведение меры.

LaTeX

$$$((\\mathrm{pi}\\; (\\lambda i.\\; \\mu(\\mathrm{some}\\ i))).prod (\\mu\\; \\mathrm{none})) \\,\\map (\\mathrm{MeasurableEquiv.piOptionEquivProd}\\; \\beta).\\mathrm{symm} = \\mathrm{Measure.pi}\\; \\mu$$$

Lean4

theorem pi_map_piOptionEquivProd {β : Option ι → Type*} [∀ i, MeasurableSpace (β i)]
    (μ : (i : Option ι) → Measure (β i)) [∀ (i : Option ι), SigmaFinite (μ i)] :
    ((Measure.pi fun i ↦ μ (some i)).prod (μ none)).map (MeasurableEquiv.piOptionEquivProd β).symm = Measure.pi μ :=
  by
  refine pi_eq (fun s _ ↦ ?_) |>.symm
  let e_meas : ((i : ι) → β (some i)) × β none ≃ᵐ ((i : Option ι) → β i) := MeasurableEquiv.piOptionEquivProd β |>.symm
  have me := MeasurableEquiv.measurableEmbedding e_meas
  have : e_meas ⁻¹' pi univ s = (pi univ (fun i ↦ s (some i))) ×ˢ (s none) :=
    by
    ext x
    simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, mem_prod]
    refine ⟨by tauto, fun _ i ↦ ?_⟩
    rcases i <;> tauto
  simp only [e_meas, me.map_apply, univ_option, Finset.prod_insertNone, this, prod_prod, pi_pi, mul_comm]

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