English
A function projectiveFamilyFun(P, s) returns P I S if s equals cylinder I S for some I, otherwise 0.
Русский
Функция projectiveFamilyFun(P, s) возвращает P I S, если s равен цилиндру I S, иначе 0.
LaTeX
$$$\text{projectiveFamilyFun}(P,s)=\begin{cases} P (\mathrm{measurableCylinders}.finset hs)(\mathrm{measurableCylinders}.set hs), & s\in\mathrm{measurableCylinders}(\alpha) \\ 0, & \text{otherwise} \end{cases}$$$
Lean4
/-- For `P` a family of measures, with `P J` a measure on `Π j : J, α j`, we define a function
`projectiveFamilyFun P s` by setting it to `P I S` if `s = cylinder I S` for a measurable `S` and
to 0 if `s` is not a measurable cylinder. -/
noncomputable def projectiveFamilyFun (P : ∀ J : Finset ι, Measure (Π j : J, α j)) (s : Set (Π i, α i)) : ℝ≥0∞ :=
if hs : s ∈ measurableCylinders α then P (measurableCylinders.finset hs) (measurableCylinders.set hs) else 0
