Existence #
Supporting results for bicausal optimal transport and measurable selection.
theorem
optimal_kernel_exists_pointwise
{X₀ : Type u_1}
{X₁ : Type u_2}
{Y₀ : Type u_3}
{Y₁ : Type u_4}
[MeasurableSpace X₁]
[MeasurableSpace Y₁]
(c₁ : (X₀ × Y₀) × X₁ × Y₁ → ENNReal)
[TopologicalSpace (MeasureTheory.Measure (X₁ × Y₁))]
(κ_μ : X₀ → MeasureTheory.Measure X₁)
(κ_ν : Y₀ → MeasureTheory.Measure Y₁)
(z₀ : X₀ × Y₀)
(h_ne : (FeasibleSet₀ κ_μ κ_ν z₀).Nonempty)
(h_compact : IsCompact (FeasibleSet₀ κ_μ κ_ν z₀))
(h_lsc :
LowerSemicontinuousOn (fun (γ : MeasureTheory.Measure (X₁ × Y₁)) => ∫⁻ (z₁ : X₁ × Y₁), c₁ (z₀, z₁) ∂γ)
(FeasibleSet₀ κ_μ κ_ν z₀))
: