Q_ident

lemma Q_ident (j j' : Fin p.m) : IdentDistrib (Q j) (Q j') ℙ ℙ := by  let f : (Fin p.m → G) → G := fun x ↦ ∑ i, x i  convert_to IdentDistrib (f ∘ (fun ω i ↦ Y (i,j) ω)) (f ∘ (fun ω i ↦ Y (i,j') ω)) ℙ ℙ  · ext ω; simp [f]  · ext ω; simp [f]  apply IdentDistrib.comp _ (by fun_prop)  exact {    aemeasurable_fst := by fun_prop    aemeasurable_snd := by fun_prop    map_eq := by      rw [(iIndepFun_iff_map_fun_eq_pi_map (by fun_prop)).mp,        (iIndepFun_iff_map_fun_eq_pi_map (by fun_prop)).mp]      · congr 1; ext1 i        exact ((hident i j).trans (hident i j').symm).map_eq      · exact indep_yj h_mes h_indep j'      exact indep_yj h_mes h_indep j      }