English
For finite index set ι, the piContent of a measurable set S equals the π-measure of S, i.e., content equals product-measure content on a cylinder.
Русский
Для конечного индекса ι содержимое π-меры на множества S совпадает с π-мерой на S.
LaTeX
$$$[Fintype\ ι] \to {s : Set (Π i, X i)} (hs : MeasurableSet s) :\ piContent μ s = Measure.pi μ s$$$
Lean4
/-- Let `μ (i + 1) : Measure (X (i + 1))` be a measure. Up to an equivalence,
`μ i = ⨂ j : Ioc i (i + 1), μ i`, where `⊗` denotes the product of measures. -/
theorem map_piSingleton (μ : (n : ℕ) → Measure (X n)) [∀ n, SigmaFinite (μ n)] (n : ℕ) :
(μ (n + 1)).map (piSingleton n) = Measure.pi (fun i : Ioc n (n + 1) ↦ μ i) :=
by
refine (Measure.pi_eq fun s hs ↦ ?_).symm
have : Subsingleton (Ioc n (n + 1)) := by rw [Nat.Ioc_succ_singleton]; infer_instance
rw [Fintype.prod_subsingleton _ ⟨n + 1, mem_Ioc.2 (by cutsat)⟩, Measure.map_apply (by fun_prop) (.univ_pi hs)]
congr 1 with x
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, forall_const, Subtype.forall, Nat.Ioc_succ_singleton,
mem_singleton]
exact ⟨fun h ↦ h (n + 1) rfl, fun h a b ↦ b.symm ▸ h⟩
