English
traj κ a is the kernel whose action is given by the trajFun κ a; it is defined to have toFun equal to trajFun κ a and is measurable.
Русский
traj κ a — ядро, определяемое через trajFun κ a; оно имеет toFun равным trajFun κ a и является измеримым.
LaTeX
$$$\\text{traj}\\; a :=\\text{kernel with }\\text{toFun} = \\text{trajFun }\\kappa\\ a$$$
Lean4
theorem measurable_trajFun (a : ℕ) : Measurable (trajFun κ a) :=
by
apply Measure.measurable_of_measurable_coe
refine
MeasurableSpace.induction_on_inter (C := fun t ht ↦ Measurable (fun x₀ ↦ trajFun κ a x₀ t)) (s :=
measurableCylinders X) generateFrom_measurableCylinders.symm isPiSystem_measurableCylinders (by simp)
(fun t ht ↦ ?cylinder) (fun t mt ht ↦ ?compl) (fun f disf mf hf ↦ ?union)
· obtain ⟨N, S, mS, t_eq⟩ : ∃ N S, MeasurableSet S ∧ t = cylinder (Iic N) S := by
simpa [measurableCylinders_nat] using ht
simp_rw [trajFun, AddContent.measure_eq _ _ generateFrom_measurableCylinders.symm _ ht, trajContent,
projectiveFamilyContent_congr _ t t_eq mS, inducedFamily]
refine Measure.measurable_measure.1 ?_ _ mS
exact (Measure.measurable_map _ (measurable_restrict₂ _)).comp (measurable _)
· have := isProbabilityMeasure_trajFun κ a
simpa [measure_compl mt (measure_ne_top _ _)] using Measurable.const_sub ht _
· simpa [measure_iUnion disf mf] using Measurable.ennreal_tsum hf
