← Copula mathematical handbook

Conditional moment bounds for stochastically increasing copulas

Concavity supplies an antitone version of every conditional CDF section. The construction changes only a null set and does not assume a density.

theorem ProbabilityTheory.Copula.RankRegion.Common.exists_antitone_version {f : ↑unitInterval → ℝ} {s : Set ↑unitInterval} (hs : ∀ᵐ (u : ↑unitInterval), u ∈ s) (hf : ∀ (u : ↑unitInterval), f u ∈ Set.Icc 0 1) (hm : AntitoneOn f s) : ∃ (g : ↑unitInterval → ℝ), Antitone g ∧ (∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) ∧ f =ᵐ[MeasureTheory.volume] g

theorem ProbabilityTheory.Copula.RankRegion.Common.conditionalCDF_antitone_version (C : Copula 2) (hC : C.IsSI) (v : ↑unitInterval) : ∃ (g : ↑unitInterval → ℝ), Antitone g ∧ (∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) ∧ (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] g

theorem ProbabilityTheory.Copula.RankRegion.Common.integrable_unit_bounded {f : ↑unitInterval → ℝ} (hf : Measurable f) (hb : ∀ (u : ↑unitInterval), f u ∈ Set.Icc 0 1) : MeasureTheory.Integrable f MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.Common.integral_sq_le_lower_at_mean {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (v : ↑unitInterval) (hv : ∫ (u : ↑unitInterval), g u = ↑v) : ∫ (u : ↑unitInterval), g u ^ 2 ≤ ∫ (u : ↑unitInterval) in Set.Iic v, g u

A decreasing function in [0,1] has its second moment below its lower-interval integral at its mean.

theorem ProbabilityTheory.Copula.RankRegion.Common.conditionalCDF_sq_le_diagonal (C : Copula 2) (hC : C.IsSI) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 ≤ C.cdf ![v, v]

theorem ProbabilityTheory.Copula.RankRegion.Common.xi_le_footrule_of_isSI (C : Copula 2) (hC : C.IsSI) : C.chatterjeeXi ≤ C.spearmanFootrule