← Copula mathematical handbook

Uniform ranks from a uniform magnitude and a fair sign

The sign selector may depend on the magnitude and on arbitrary other data. Symmetrizing it with its opposite still produces the uniform rank law.

noncomputable def ProbabilityTheory.Copula.RankRegion.positiveRank (a : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.positiveRank a = ProbabilityTheory.Copula.OrdinalSum.upperEmbed ProbabilityTheory.Copula.unitHalf a

noncomputable def ProbabilityTheory.Copula.RankRegion.negativeRank (a : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.negativeRank a = ProbabilityTheory.Copula.OrdinalSum.lowerEmbed ProbabilityTheory.Copula.unitHalf (unitInterval.symm a)

theorem ProbabilityTheory.Copula.RankRegion.continuous_positiveRank : Continuous positiveRank

theorem ProbabilityTheory.Copula.RankRegion.continuous_negativeRank : Continuous negativeRank

theorem ProbabilityTheory.Copula.RankRegion.measurable_positiveRank : Measurable positiveRank

theorem ProbabilityTheory.Copula.RankRegion.measurable_negativeRank : Measurable negativeRank

theorem ProbabilityTheory.Copula.RankRegion.coe_positiveRank (a : ↑unitInterval) : ↑(positiveRank a) = (1 + ↑a) / 2

theorem ProbabilityTheory.Copula.RankRegion.coe_negativeRank (a : ↑unitInterval) : ↑(negativeRank a) = (1 - ↑a) / 2

noncomputable def ProbabilityTheory.Copula.RankRegion.fairMeasure {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [MeasurableSpace X] (μ : MeasureTheory.Measure Ω) (f g : Ω → X) : MeasureTheory.Measure X

Equations

• ProbabilityTheory.Copula.RankRegion.fairMeasure μ f g = ENNReal.ofReal (1 / 2) • MeasureTheory.Measure.map f μ + ENNReal.ofReal (1 / 2) • MeasureTheory.Measure.map g μ

theorem ProbabilityTheory.Copula.RankRegion.fairMeasure_probability {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [MeasurableSpace X] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {f g : Ω → X} (hf : Measurable f) (hg : Measurable g) : MeasureTheory.IsProbabilityMeasure (fairMeasure μ f g)

theorem ProbabilityTheory.Copula.RankRegion.integral_fairMeasure {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [MeasurableSpace X] (μ : MeasureTheory.Measure Ω) {f g : Ω → X} {h : X → ℝ} (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) (hi : MeasureTheory.Integrable h (MeasureTheory.Measure.map f μ)) (hj : MeasureTheory.Integrable h (MeasureTheory.Measure.map g μ)) : ∫ (x : X), h x ∂fairMeasure μ f g = 1 / 2 * ∫ (x : Ω), h (f x) ∂μ + 1 / 2 * ∫ (x : Ω), h (g x) ∂μ

theorem ProbabilityTheory.Copula.RankRegion.fairMeasure_map {Ω : Type u_1} {X : Type u_2} {Y : Type u_3} [MeasurableSpace Ω] [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure Ω) {f g : Ω → X} {h : X → Y} (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) : MeasureTheory.Measure.map h (fairMeasure μ f g) = fairMeasure μ (h ∘ f) (h ∘ g)

theorem ProbabilityTheory.Copula.RankRegion.fair_ranks_uniform : fairMeasure MeasureTheory.volume positiveRank negativeRank = MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.RankRegion.signedRank (s : Bool) (a : ↑unitInterval) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.signedRank s a = if s = true then ProbabilityTheory.Copula.RankRegion.positiveRank a else ProbabilityTheory.Copula.RankRegion.negativeRank a

theorem ProbabilityTheory.Copula.RankRegion.measurable_signedRank {Ω : Type u_1} [MeasurableSpace Ω] {A : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hS : Measurable S) : Measurable fun (w : Ω) => signedRank (S w) (A w)

theorem ProbabilityTheory.Copula.RankRegion.fair_signed_rank_uniform {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {A : Ω → ↑unitInterval} {S : Ω → Bool} (hA : Measurable A) (hS : Measurable S) (hU : MeasureTheory.Measure.map A μ = MeasureTheory.volume) : (fairMeasure μ (fun (w : Ω) => signedRank (S w) (A w)) fun (w : Ω) => signedRank (!S w) (A w)) = MeasureTheory.volume