AutoSamplingTheory.TechnicalLemmas.Measure.CouplingAEMarginals

- Pull an arbitrary first-marginal almost-everywhere proposition back to the joint coupling. No measurability assumption on the proposition is required; `ae_of_ae_map` works directly at the filter level.

theorem ae_fst_of_isCoupling
    {gamma : Measure (α × β)} {mu : Measure α} {nu : Measure β}
    (hgamma : IsCoupling gamma mu nu)
    {P : α → Prop}
    (hP : ∀ᵐ x ∂mu, P x) :
    ∀ᵐ z ∂gamma, P z.1 := by
  have hP' : ∀ᵐ x ∂gamma.fst, P x := by
    simpa [hgamma.1] using hP
  apply ae_of_ae_map measurable_fst.aemeasurable
  simpa [Measure.fst] using hP'

/-- Pull an arbitrary second-marginal almost-everywhere proposition back to the
joint coupling. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CouplingAEMarginals.lean:29published source at 0e31a3cda412

- Pull an arbitrary second-marginal almost-everywhere proposition back to the joint coupling.

theorem ae_snd_of_isCoupling
    {gamma : Measure (α × β)} {mu : Measure α} {nu : Measure β}
    (hgamma : IsCoupling gamma mu nu)
    {P : β → Prop}
    (hP : ∀ᵐ y ∂nu, P y) :
    ∀ᵐ z ∂gamma, P z.2 := by
  have hP' : ∀ᵐ y ∂gamma.snd, P y := by
    simpa [hgamma.2] using hP
  apply ae_of_ae_map measurable_snd.aemeasurable
  simpa [Measure.snd] using hP'

end CouplingAEMarginals
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/CouplingAEMarginals.lean:42published source at 0e31a3cda412