← Copula mathematical handbook

Nonnegative real powers on the unit interval

noncomputable def ProbabilityTheory.Copula.unitPower (u : ↑unitInterval) (r : ℝ) (hr : 0 ≤ r) : ↑unitInterval

Real powers as maps of the closed unit interval. In particular 0^0 = 1.

Equations

• ProbabilityTheory.Copula.unitPower u r hr = ⟨↑u ^ r, ⋯⟩

@[simp]

theorem ProbabilityTheory.Copula.coe_unitPower (u : ↑unitInterval) (r : ℝ) (hr : 0 ≤ r) : ↑(unitPower u r hr) = ↑u ^ r

@[simp]

theorem ProbabilityTheory.Copula.unitPower_one (u : ↑unitInterval) : unitPower u 1 ⋯ = u

@[simp]

theorem ProbabilityTheory.Copula.unitPower_zero (u : ↑unitInterval) : unitPower u 0 ⋯ = 1

@[simp]

theorem ProbabilityTheory.Copula.unitPower_top (r : ℝ) (hr : 0 ≤ r) : unitPower 1 r hr = 1

theorem ProbabilityTheory.Copula.unitPower_mul (u : ↑unitInterval) (r t : ℝ) (hr : 0 ≤ r) (ht : 0 ≤ t) : unitPower (unitPower u r hr) t ht = unitPower u (r * t) ⋯

theorem ProbabilityTheory.Copula.measurable_unitPower (r : ℝ) (hr : 0 ≤ r) : Measurable fun (u : ↑unitInterval) => unitPower u r hr

noncomputable def ProbabilityTheory.Copula.powerSample (a u : ↑unitInterval) : ↑unitInterval

The sampling map for a power marginal; exponent zero gives a point mass at zero.

Equations

• ProbabilityTheory.Copula.powerSample a u = if a = 0 then 0 else ProbabilityTheory.Copula.unitPower u (↑a)⁻¹ ⋯

theorem ProbabilityTheory.Copula.measurable_powerSample (a : ↑unitInterval) : Measurable (powerSample a)

theorem ProbabilityTheory.Copula.powerSample_le_iff (a u v : ↑unitInterval) : powerSample a u ≤ v ↔ u ≤ unitPower v ↑a ⋯