indep_of_indep_of_le for iIndep

Stream: Is there code for X?

[Joris van Winden]

Is there a version of ProbabilityTheory.indep_of_indep_of_le_left (or right) which applies to iIndep? Given a family A n of independent sigma-algebras, and a family B n which satisfies ∀ n, B n ≤ A n, I would like to conclude that the family B n is also independent.

The closest could find is ProbabilityTheory.iIndepFun.comp, which is the analogous statement for function composition, but this is not quite satisfactory for my purpose.

[Etienne Marion]

@loogle ProbabilityTheory.iIndep, _ ≤ _

[loogle]

:search: ProbabilityTheory.iIndepSets.iIndep, ProbabilityTheory.indep_iSup_of_disjoint, and 10 more

[Etienne Marion]

I don't think it exists.

[Joris van Winden]

I eventually managed to prove the following:

theorem iIndep_of_iIndep_of_le {m₀ : ι → MeasurableSpace Ω} {m₁ : ι → MeasurableSpace Ω}
    {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} (h_indep : iIndep m₁ κ μ)
    (h_le : ∀ i, m₀ i ≤ m₁ i) : iIndep m₀ κ μ :=
  fun a b c ↦ h_indep a (f := b) <| fun _ e ↦ (h_le _) _ (c _ e)

[Etienne Marion]

This would be a useful addition to Mathlib, please open a PR!

[Joris van Winden]

#34542