← Mathematical handbook

noncomputable def Verification.maximaWeight (n : ℕ) : ↑unitInterval

Equations

• Verification.maximaWeight n = ⟨(↑n + 1) / (↑n + 2), ⋯⟩

noncomputable def Verification.normalizedMaxima {d : ℕ} (C : ProbabilityTheory.Copula d) : ℕ → ProbabilityTheory.Copula d

The normalized maximum of n+1 independent copies of a copula.

Equations

• Verification.normalizedMaxima C 0 = C
• Verification.normalizedMaxima C n.succ = (Verification.normalizedMaxima C n).maxProduct C fun (x : Fin d) => Verification.maximaWeight n

theorem Verification.normalizedMaxima_cdf {d : ℕ} (C : ProbabilityTheory.Copula d) (n : ℕ) (u : Fin d → ↑unitInterval) : (normalizedMaxima C n).cdf u = (C.cdf fun (i : Fin d) => ProbabilityTheory.Copula.unitPower (u i) (↑n + 1)⁻¹ ⋯) ^ (n + 1)

theorem Verification.exists_copula_of_pointwise_cdf_limit (C : ℕ → ProbabilityTheory.Copula 2) (F : (Fin 2 → ↑unitInterval) → ℝ) (hF : ∀ (u : Fin 2 → ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => (C n).cdf u) Filter.atTop (nhds (F u))) : ∃ (D : ProbabilityTheory.Copula 2), D.cdf = F