← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.finiteWeight {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f : Ω → ι) (i : ι) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.finiteWeight μ f i = μ.real (f ⁻¹' {i})

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.finiteWeight_nonneg {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f : Ω → ι) (i : ι) : 0 ≤ finiteWeight μ f i

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.finiteWeight_sum {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f : Ω → ι} (hf : Measurable f) : ∑ i : ι, finiteWeight μ f i = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.integral_finite_map {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ι} (hf : Measurable f) (g : ι → ℝ) : ∫ (x : Ω), g (f x) ∂μ = ∑ i : ι, finiteWeight μ f i * g i

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.integral_finite_pair {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ι} (hf : Measurable f) (g : ι → ι → ℝ) : ∫ (x : Ω), ∫ (y : Ω), g (f x) (f y) ∂μ ∂μ = weighted2 (finiteWeight μ f) g