Q_indep

lemma Q_indep {j j' : Fin p.m} (h : j ≠ j') : IndepFun (Q j) (-Q j') ℙ := by  let T : Finset (Fin p.m × Fin p.m) := {q|q.2=j}  let T' : Finset (Fin p.m × Fin p.m) := {q|q.2=j'}  let φ : (T → G) → G := fun f ↦ ∑ i, f ⟨(i,j), by simp [T]⟩  let φ' : (T' → G) → G := fun f ↦ -∑ i, f ⟨(i,j'), by simp [T']⟩  convert iIndepFun.finsets_comp' _ h_indep (by fun_prop) (show Measurable φ by fun_prop)    (show Measurable φ' by fun_prop) with ω ω <;> try simp [φ,φ']  rw [Finset.disjoint_left]; rintro ⟨_, _⟩ h h'  simp [T,T'] at h h'; order