← 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 ProbabilityTheory.Copula.RankRegion.uniformMarginalMeasures (d : ℕ) : Set (MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval))

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.isCompact_uniformMarginalMeasures (d : ℕ) : IsCompact (uniformMarginalMeasures d)

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

theorem ProbabilityTheory.Copula.RankRegion.exists_copula_maximizer {d : ℕ} {f : (Fin d → ↑unitInterval) → ℝ} (hf : Continuous f) : ∃ (C : Copula d), ∀ (D : 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 ProbabilityTheory.Copula.RankRegion.exists_copula_minimizer {d : ℕ} {f : (Fin d → ↑unitInterval) → ℝ} (hf : Continuous f) : ∃ (C : Copula d), ∀ (D : Copula d), ∫ (x : Fin d → ↑unitInterval), f x ∂C.toMeasure ≤ ∫ (x : Fin d → ↑unitInterval), f x ∂D.toMeasure