← Copula mathematical handbook

Countable ordinal sums along an increasing partition

This constructor permits infinitely many adjacent positive-length blocks, starting at zero with endpoints tending to one. Its CDF is an absolutely convergent series. Arbitrary disjoint interval families with a residual comonotonic part are a different, more general construction.

structure ProbabilityTheory.Copula.CountableIntervalPartition : Type

An increasing sequence of partition endpoints exhausting the unit interval.

• point : ℕ → ↑unitInterval
• strictMono : StrictMono self.point
• zero : self.point 0 = 0
• tendsto_one : Filter.Tendsto (fun (k : ℕ) => ↑(self.point k)) Filter.atTop (nhds 1)

def ProbabilityTheory.Copula.CountableIntervalPartition.width (P : CountableIntervalPartition) (k : ℕ) : ℝ

Length of the kth block.

Equations

• P.width k = ↑(P.point (k + 1)) - ↑(P.point k)

theorem ProbabilityTheory.Copula.CountableIntervalPartition.width_pos (P : CountableIntervalPartition) (k : ℕ) : 0 < P.width k

noncomputable def ProbabilityTheory.Copula.CountableIntervalPartition.coord (P : CountableIntervalPartition) (k : ℕ) (u : ↑unitInterval) : ↑unitInterval

Clipped local coordinate on a countable partition block.

Equations

• P.coord k u = Set.projIcc 0 1 ProbabilityTheory.Copula.CountableIntervalPartition.coord._proof_1 ((↑u - ↑(P.point k)) / P.width k)

theorem ProbabilityTheory.Copula.CountableIntervalPartition.coord_mono (P : CountableIntervalPartition) (k : ℕ) : Monotone (P.coord k)

theorem ProbabilityTheory.Copula.CountableIntervalPartition.coord_of_le (P : CountableIntervalPartition) (k : ℕ) (u : ↑unitInterval) (hu : u ≤ P.point k) : P.coord k u = 0

theorem ProbabilityTheory.Copula.CountableIntervalPartition.coord_of_ge (P : CountableIntervalPartition) (k : ℕ) (u : ↑unitInterval) (hu : P.point (k + 1) ≤ u) : P.coord k u = 1

@[simp]

theorem ProbabilityTheory.Copula.CountableIntervalPartition.coord_zero (P : CountableIntervalPartition) (k : ℕ) : P.coord k 0 = 0

@[simp]

theorem ProbabilityTheory.Copula.CountableIntervalPartition.coord_one (P : CountableIntervalPartition) (k : ℕ) : P.coord k 1 = 1

theorem ProbabilityTheory.Copula.CountableIntervalPartition.width_mul_coord (P : CountableIntervalPartition) (k : ℕ) (u : ↑unitInterval) : P.width k * ↑(P.coord k u) = min ↑u ↑(P.point (k + 1)) - min ↑u ↑(P.point k)

theorem ProbabilityTheory.Copula.CountableIntervalPartition.hasSum_width_mul_coord (P : CountableIntervalPartition) (u : ↑unitInterval) : HasSum (fun (k : ℕ) => P.width k * ↑(P.coord k u)) ↑u

The weighted local coordinates have exactly the uniform marginal CDF.

theorem ProbabilityTheory.Copula.CountableIntervalPartition.hasSum_width (P : CountableIntervalPartition) : HasSum P.width 1

theorem ProbabilityTheory.Copula.CountableIntervalPartition.summable_cdf (P : CountableIntervalPartition) (C : ℕ → Copula 2) (u v : ↑unitInterval) : Summable fun (k : ℕ) => P.width k * (C k).cdf ![P.coord k u, P.coord k v]

Absolute convergence of the weighted local CDF series.

noncomputable def ProbabilityTheory.Copula.CountableIntervalPartition.cdf (P : CountableIntervalPartition) (C : ℕ → Copula 2) (u v : ↑unitInterval) : ℝ

The CDF series for the countable ordinal sum.

Equations

• P.cdf C u v = ∑' (k : ℕ), P.width k * (C k).cdf ![P.coord k u, P.coord k v]

theorem ProbabilityTheory.Copula.CountableIntervalPartition.isClassical (P : CountableIntervalPartition) (C : ℕ → Copula 2) : IsClassical fun (u : Fin 2 → ↑unitInterval) => P.cdf C (u 0) (u 1)

noncomputable def ProbabilityTheory.Copula.CountableIntervalPartition.dyadic : CountableIntervalPartition

The concrete countable partition with endpoints 1 - (1/2)^k.

Equations

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

noncomputable def ProbabilityTheory.Copula.countableOrdinalSum (P : CountableIntervalPartition) (C : ℕ → Copula 2) : Copula 2

Countable ordinal sum on adjacent blocks with endpoints tending to one.

Equations

• ProbabilityTheory.Copula.countableOrdinalSum P C = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => P.cdf C (u 0) (u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_countableOrdinalSum (P : CountableIntervalPartition) (C : ℕ → Copula 2) (u : Fin 2 → ↑unitInterval) : (countableOrdinalSum P C).cdf u = ∑' (k : ℕ), P.width k * (C k).cdf ![P.coord k (u 0), P.coord k (u 1)]

noncomputable def ProbabilityTheory.Copula.countableOrdinalSumPi (P : CountableIntervalPartition) : Copula 2

Countable ordinal sum of independent blocks.

Equations

• ProbabilityTheory.Copula.countableOrdinalSumPi P = ProbabilityTheory.Copula.countableOrdinalSum P fun (x : ℕ) => ProbabilityTheory.Copula.independence 2

theorem ProbabilityTheory.Copula.cdf_countableOrdinalSumPi (P : CountableIntervalPartition) (u v : ↑unitInterval) : (countableOrdinalSumPi P).cdf ![u, v] = ∑' (k : ℕ), P.width k * (↑(P.coord k u) * ↑(P.coord k v))

@[simp]

theorem ProbabilityTheory.Copula.countableOrdinalSum_comonotonic (P : CountableIntervalPartition) : (countableOrdinalSum P fun (x : ℕ) => comonotonic 2) = comonotonic 2