finite product measure on disjoint restrictions

Stream: Is there code for X?

[Bhavik Mehta]

Do we have any statement like the second of these in mathlib? I have a proof of the first, if that helps:

import Mathlib

open MeasureTheory ProbabilityTheory Classical

variable {ι Ω : Type*} [Fintype ι] [MeasurableSpace Ω] {P : ι → Measure Ω}
  [∀ i, IsProbabilityMeasure (P i)] {s : Set ι}

lemma map_pi_restrict :
    (Measure.pi P).map s.restrict = Measure.pi (fun i : s ↦ P i) := by
  sorry -- proved

example (s t : Set ι) (h : Disjoint s t) (A : Set (s → Ω)) (B : Set (t → Ω))
    (hA : MeasurableSet A) (hB : MeasurableSet B) :
    Measure.pi P (s.restrict ⁻¹' A ∩ t.restrict ⁻¹' B) =
      Measure.pi P (s.restrict ⁻¹' A) * Measure.pi P (t.restrict ⁻¹' B) := by
  sorry

[Bhavik Mehta]

Ah! I got there; the trick was to think about probability rather than measure:

lemma indepFun_restrict_restrict_pi (s t : Set ι) (hi : Disjoint s t) :
    IndepFun s.restrict t.restrict (Measure.pi P) := by
  lift s to Finset ι using s.toFinite
  lift t to Finset ι using t.toFinite
  simp only [disjoint_coe] at hi
  have : iIndepFun (fun i ω ↦ ω i) (Measure.pi P) := iIndepFun_pi  (X := fun i x ↦ x) (by fun_prop)
  have := iIndepFun.indepFun_finset s t hi this (by fun_prop)
  exact this

example (s t : Set ι) (hi : Disjoint s t)
    (A : Set (s → Ω)) (B : Set (t → Ω)) (hA : MeasurableSet A) (hB : MeasurableSet B) :
    Measure.pi P (s.restrict ⁻¹' A ∩ t.restrict ⁻¹' B) =
      Measure.pi P (s.restrict ⁻¹' A) * Measure.pi P (t.restrict ⁻¹' B) := by
  have := indepFun_restrict_restrict_pi s t hi (P := P)
  rw [indepFun_iff_measure_inter_preimage_eq_mul] at this
  exact this A B hA hB

[Etienne Marion]

Ah I was just about to suggest this approach!

[Bhavik Mehta]

It turns out what I actually needed was

lemma pi_inter_eq (s t : Set ι) (hst : Disjoint s t)
    (A B : Set (ι → Ω)) (hs : DependsOn (· ∈ A) s) (ht : DependsOn (· ∈ B) t)
    (hA : MeasurableSet A) (hB : MeasurableSet B) :
    Measure.pi P (A ∩ B) = Measure.pi P A * Measure.pi P B := by
  obtain ⟨A', rfl⟩ : ∃ A', A = s.restrict ⁻¹' A' := dependsOn_iff_exists_comp.1 hs
  obtain ⟨B', rfl⟩ : ∃ B', B = t.restrict ⁻¹' B' := dependsOn_iff_exists_comp.1 ht
  sorry

which seems to need some measurability assumptions that I can't find the right lemmas for to complete. Edit: solved by adding those lemmas, in particular constructing the inverse function to s.restrict assuming that A,B are nonempty (and it's trivial when they're empty)