← Mathematical handbook

Continuous costs attain their extrema over all copulas

Uniform-marginal probability measures form a closed subset of the compact space of probability measures on the unit cube, in the weak topology.

noncomputable def Verification.uniformMarginalMeasures (d : ℕ) : Set (MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval))

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.isCompact_uniformMarginalMeasures (d : ℕ) : IsCompact (uniformMarginalMeasures d)

theorem Verification.measure_mem_uniformMarginalMeasures {d : ℕ} (C : ProbabilityTheory.Copula d) : C.measure ∈ uniformMarginalMeasures d

theorem Verification.exists_copula_maximizer {d : ℕ} {f : (Fin d → ↑unitInterval) → ℝ} (hf : Continuous f) : ∃ (C : ProbabilityTheory.Copula d), ∀ (D : ProbabilityTheory.Copula d), ∫ (x : Fin d → ↑unitInterval), f x ∂D.toMeasure ≤ ∫ (x : Fin d → ↑unitInterval), f x ∂C.toMeasure

A maximum exists for every continuous real cost, in every finite dimension.

theorem Verification.exists_copula_minimizer {d : ℕ} {f : (Fin d → ↑unitInterval) → ℝ} (hf : Continuous f) : ∃ (C : ProbabilityTheory.Copula d), ∀ (D : ProbabilityTheory.Copula d), ∫ (x : Fin d → ↑unitInterval), f x ∂C.toMeasure ≤ ∫ (x : Fin d → ↑unitInterval), f x ∂D.toMeasure

theorem Verification.isCompact_copula_integral_pair {f g : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) (hg : Continuous g) : IsCompact (Set.range fun (C : ProbabilityTheory.Copula 2) => (∫ (x : Fin 2 → ↑unitInterval), f x ∂C.toMeasure, ∫ (x : Fin 2 → ↑unitInterval), g x ∂C.toMeasure))

Any finite pair of continuous costs has a compact attainable set.