← Copula mathematical handbook

Integration tools for population rank coefficients

theorem ProbabilityTheory.Copula.integrable_continuous_cube {d : ℕ} (μ : MeasureTheory.Measure (Fin d → ↑unitInterval)) [MeasureTheory.IsFiniteMeasure μ] {f : (Fin d → ↑unitInterval) → ℝ} (hf : Continuous f) : MeasureTheory.Integrable f μ

theorem ProbabilityTheory.Copula.integrable_continuous_unit (μ : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsFiniteMeasure μ] {f : ↑unitInterval → ℝ} (hf : Continuous f) : MeasureTheory.Integrable f μ

theorem ProbabilityTheory.Copula.integrable_cdf {d : ℕ} (C : Copula d) (μ : MeasureTheory.Measure (Fin d → ↑unitInterval)) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable C.cdf μ

theorem ProbabilityTheory.Copula.integral_unitInterval (f : ℝ → ℝ) : ∫ (u : ↑unitInterval), f ↑u = ∫ (t : ℝ) in 0..1, f t

Integrating a real function over the uniform unit interval.

@[simp]

theorem ProbabilityTheory.Copula.integral_unit_pow (n : ℕ) : ∫ (u : ↑unitInterval), ↑u ^ n = 1 / (↑n + 1)

@[simp]

theorem ProbabilityTheory.Copula.integral_unit_id : ∫ (u : ↑unitInterval), ↑u = 1 / 2

theorem ProbabilityTheory.Copula.integral_eval {d : ℕ} (C : Copula d) (i : Fin d) (f : ↑unitInterval → ℝ) (hf : Measurable f) : ∫ (x : Fin d → ↑unitInterval), f (x i) ∂C.toMeasure = ∫ (u : ↑unitInterval), f u

@[simp]

theorem ProbabilityTheory.Copula.integral_coe_eval {d : ℕ} (C : Copula d) (i : Fin d) : ∫ (x : Fin d → ↑unitInterval), ↑(x i) ∂C.toMeasure = 1 / 2

@[simp]

theorem ProbabilityTheory.Copula.integral_sq_eval {d : ℕ} (C : Copula d) (i : Fin d) : ∫ (x : Fin d → ↑unitInterval), ↑(x i) ^ 2 ∂C.toMeasure = 1 / 3

theorem ProbabilityTheory.Copula.integral_comonotonic {d : ℕ} (f : (Fin d → ↑unitInterval) → ℝ) (hf : Measurable f) : ∫ (x : Fin d → ↑unitInterval), f x ∂(comonotonic d).toMeasure = ∫ (u : ↑unitInterval), f fun (x : Fin d) => u

theorem ProbabilityTheory.Copula.integral_countermonotonic (f : (Fin 2 → ↑unitInterval) → ℝ) (hf : Measurable f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂countermonotonic.toMeasure = ∫ (u : ↑unitInterval), f ![u, unitInterval.symm u]

theorem ProbabilityTheory.Copula.integral_independence_mul (f g : ↑unitInterval → ℝ) : ∫ (x : Fin 2 → ↑unitInterval), f (x 0) * g (x 1) ∂(independence 2).toMeasure = (∫ (u : ↑unitInterval), f u) * ∫ (v : ↑unitInterval), g v

theorem ProbabilityTheory.Copula.cdf_comonotonic_two (u : Fin 2 → ↑unitInterval) : (comonotonic 2).cdf u = min ↑(u 0) ↑(u 1)

theorem ProbabilityTheory.Copula.cdf_countermonotonic_le (C : Copula 2) (u : Fin 2 → ↑unitInterval) : countermonotonic.cdf u ≤ C.cdf u

theorem ProbabilityTheory.Copula.cdf_le_comonotonic (C : Copula 2) (u : Fin 2 → ↑unitInterval) : C.cdf u ≤ (comonotonic 2).cdf u