Transport of independence through measure-preserving maps

import Mathlib.Probability.Independence.Basic

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Probability/Transport.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory
namespace LevyStochCalc
namespace Probability
variable {α β : Type*} [mα : MeasurableSpace α] [mβ : MeasurableSpace β]
  {μa : Measure α} {μb : Measure β} {h : α → β}
/-- Independence of two sub-σ-algebras of `β` transports to their comaps in `α`
along a measure-preserving map `h : α → β`. -/
theorem indep_comap_of_measurePreserving (hmp : MeasurePreserving h μa μb)
    {m₁ m₂ : MeasurableSpace β} (hm₁ : m₁ ≤ mβ) (hm₂ : m₂ ≤ mβ)
    (hindep : ProbabilityTheory.Indep m₁ m₂ μb) :
    ProbabilityTheory.Indep (m₁.comap h) (m₂.comap h) μa := by
  have h_aux : ∀ s : Set β, @MeasurableSet β mβ s → μa (h ⁻¹' s) = μb s := fun s hs =>
    @MeasurePreserving.measure_preimage α β mα mβ μa μb h hmp s
      (@MeasurableSet.nullMeasurableSet β mβ μb s hs)
  rw [ProbabilityTheory.Indep_iff]
  rintro _ _ ⟨u, hu, rfl⟩ ⟨v, hv, rfl⟩
  have hu' : @MeasurableSet β mβ u := hm₁ _ hu
  have hv' : @MeasurableSet β mβ v := hm₂ _ hv
  rw [show h ⁻¹' u ∩ h ⁻¹' v = h ⁻¹' (u ∩ v) from rfl,
    h_aux _ (@MeasurableSet.inter β mβ _ _ hu' hv'), h_aux _ hu', h_aux _ hv']
  exact (ProbabilityTheory.Indep_iff _ _ _).1 hindep u v hu hv
end Probability
end LevyStochCalc