@@ -87,7 +87,7 @@ lemma IndepFun.process_indepFun_process {T : Type*} {𝓧 : S → Type*} {𝓨 :
8787 exact IndepFun.indepFun_process (measurable_pi_lambda _ fun _ ↦ hX _) hY fun J ↦ h I J
8888
8989/-- Stochastic processes $((X^s_t)_{t \in T_s})_{s \in S}$ are mutually independent if
90- for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}^ the families
90+ for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}$ the families
9191$(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ...,
9292(X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent. -/
9393lemma iIndepFun.iIndepFun_process {T : S → Type *} {𝓧 : (i : S) → (j : T i) → Type *}
@@ -169,7 +169,7 @@ lemma IndepFun.process_indepFun_process {T : Type*} {𝓧 : S → Type*} {𝓨 :
169169 Kernel.IndepFun.process_indepFun_process hX hY h
170170
171171/-- Stochastic processes $((X^s_t)_{t \in T_s})_{s \in S}$ are mutually independent if
172- for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}^ the families
172+ for all $s_1, ..., s_n$ and all $t^{s_i}_1, ..., t^{s_i}_{p_i}$ the families
173173$(X^{s_1}_{t^{s_1}_1}, ..., X^{s_1}_{t^{s_1}_{p_1}}), ...,
174174(X^{s_n}_{t^{s_n}_1}, ..., X^{s_n}_{t^{s_n}_{p_n}})$ are mutually independent. -/
175175lemma iIndepFun.iIndepFun_process {T : S → Type *} {𝓧 : (i : S) → (j : T i) → Type *}
0 commit comments