← Mathematical handbook

theorem Verification.tawn_tendsto_atTop {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hθ : ∀ (a : A), 1 ≤ θ a) (ht : Filter.Tendsto θ l Filter.atTop) (α β : ↑unitInterval) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : A) => (ProbabilityTheory.Copula.tawn (θ a) ⋯ α β).cdf u) l (nhds ((ProbabilityTheory.Copula.marshallOlkin α β).cdf u))

theorem Verification.tawn_lowerOrthant_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) (α β : ↑unitInterval) : (ProbabilityTheory.Copula.tawn θ hθ α β).LowerOrthantLE (ProbabilityTheory.Copula.tawn η ⋯ α β)

theorem Verification.tawn_tendsto_parameter {A : Type u_1} {l : Filter A} (θ : A → ℝ) (hθ : ∀ (a : A), 1 ≤ θ a) {η : ℝ} (hη : 1 ≤ η) (ht : Filter.Tendsto θ l (nhds η)) (α β u v : ↑unitInterval) : Filter.Tendsto (fun (a : A) => (ProbabilityTheory.Copula.tawn (θ a) ⋯ α β).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.tawn η hη α β).cdf ![u, v]))

theorem Verification.tawn_one_one_density_tp2 (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.tawn θ hθ 1 1).HasMTP2Density

theorem Verification.tawn_one_one_not_independence {θ : ℝ} (hθ : 1 < θ) : ProbabilityTheory.Copula.tawn θ ⋯ 1 1 ≠ ProbabilityTheory.Copula.independence 2

theorem Verification.tawn_printed_tp2_exclusion_false : ¬∀ (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval), ProbabilityTheory.Copula.tawn θ hθ α β ≠ ProbabilityTheory.Copula.independence 2 → ¬(ProbabilityTheory.Copula.tawn θ hθ α β).HasMTP2Density