Documentation

Verification.Nelsen13Integrals

← Mathematical handbook

noncomputable def Verification.n13DensityReal (θ u v : ℝ) :

Equations

Verification.n13DensityReal θ u v = Verification.n13Second θ⁻¹ (Verification.n13Inv θ u + Verification.n13Inv θ v) * Verification.n13Weight θ u * Verification.n13Weight θ v

Instances For

noncomputable def Verification.n13RealCDF (θ u v : ℝ) :

Equations

Verification.n13RealCDF θ u v = Verification.n13Psi θ⁻¹ (Verification.n13Inv θ u + Verification.n13Inv θ v)

Instances For

theorem Verification.n13Inv_continuousAt {θ u : ℝ} (hu : 0 < u) (ha : 0 < 1 - Real.log u) :

ContinuousAt (n13Inv θ) u

theorem Verification.n13Weight_continuousAt {θ u : ℝ} (hu : 0 < u) (ha : 0 < 1 - Real.log u) :

ContinuousAt (n13Weight θ) u

theorem Verification.n13Second_continuousAt (p t : ℝ) (ht : 0 < 1 + t) :

ContinuousAt (n13Second p) t

theorem Verification.n13Inv_nonneg_real {θ u : ℝ} (hθ : 0 ≤ θ) (hu : u ∈ Set.Icc 0 1) :

0 ≤ n13Inv θ u

theorem Verification.n13RealCDF_eq {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) :

n13RealCDF θ ↑u ↑v = (nelsen13 θ ⋯).cdf ![u, v]

theorem Verification.n13Partial_continuous_first {θ u v : ℝ} (hθ : 0 ≤ θ) (hu : u ∈ Set.Ioc 0 1) (hv : v ∈ Set.Icc 0 1) :

ContinuousAt (fun (x : ℝ) => n13Partial θ x v) u

theorem Verification.n13DensityReal_continuous_second {θ u v : ℝ} (hθ : 0 ≤ θ) (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Ioc 0 1) :

ContinuousAt (n13DensityReal θ u) v

theorem Verification.integral_n13DensityReal_second {θ u a b : ℝ} (hθ : 0 ≤ θ) (hu : u ∈ Set.Icc 0 1) (ha : 0 < a) (hab : a ≤ b) (hb : b ≤ 1) :

∫ (v : ℝ) in a..b, n13DensityReal θ u v = n13Partial θ u b - n13Partial θ u a

theorem Verification.integral_n13Partial_first {θ v a b : ℝ} (hθ : 0 ≤ θ) (hv : v ∈ Set.Icc 0 1) (ha : 0 < a) (hab : a ≤ b) (hb : b ≤ 1) :

∫ (u : ℝ) in a..b, n13Partial θ u v = n13RealCDF θ b v - n13RealCDF θ a v

theorem Verification.n13Density_continuousAt {θ : ℝ} (hθ : 0 ≤ θ) (x : Fin 2 → ↑unitInterval) (hx0 : 0 < ↑(x 0)) (hx1 : 0 < ↑(x 1)) :

ContinuousAt (n13Density θ) x

theorem Verification.n13Density_integrable_rectangle {θ : ℝ} (hθ : 0 ≤ θ) (a b c d : ↑unitInterval) (ha : 0 < ↑a) (hc : 0 < ↑c) :

MeasureTheory.IntegrableOn (n13Density θ) (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i)) MeasureTheory.volume

theorem Verification.integral_n13Density_rectangle {θ a b c d : ℝ} (hθ : 0 ≤ θ) (ha : 0 < a) (hab : a ≤ b) (hb : b ≤ 1) (hc : 0 < c) (hcd : c ≤ d) (hd : d ≤ 1) :

∫ (u : ℝ) in a..b, ∫ (v : ℝ) in c..d, n13DensityReal θ u v = n13RealCDF θ b d - n13RealCDF θ a d - n13RealCDF θ b c + n13RealCDF θ a c

theorem Verification.n13Density_rectangle_eq_measure {θ : ℝ} (hθ : 0 < θ) (a b c d : ↑unitInterval) (ha : 0 < ↑a) (hab : a ≤ b) (hc : 0 < ↑c) (hcd : c ≤ d) :

∫ (x : Fin 2 → ↑unitInterval) in Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i), n13Density θ x = (nelsen13 θ ⋯).toMeasure.real (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i))