← Mathematical handbook

noncomputable def Verification.n16RawDensity (θ : ℝ) (p : ↑unitInterval × ↑unitInterval) : ℝ

Equations

• Verification.n16RawDensity θ p = Verification.n16Second θ (Verification.n16Inv θ ↑p.1 + Verification.n16Inv θ ↑p.2) * Verification.n16Weight θ ↑p.1 * Verification.n16Weight θ ↑p.2

theorem Verification.n16RawDensity_continuousAt {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : ContinuousAt (n16RawDensity θ) (u, v)

theorem Verification.n16RawDensity_ae_minors {θ : ℝ} (hθ : 0 < θ) (hC : (nelsen16 θ ⋯).HasMTP2Density) : HasAEOrderedMinors 1 fun (u v : ↑unitInterval) => n16RawDensity θ (u, v)

theorem Verification.n16_second_midpoint_of_mtp2 {θ : ℝ} (hθ : 0 < θ) (hC : (nelsen16 θ ⋯).HasMTP2Density) (u : ↑unitInterval) (hu : 0 < ↑u) (hu1 : u < 1) : n16Second θ (n16Inv θ ↑u) ^ 2 ≤ n16Second θ (2 * n16Inv θ ↑u) * n16Second θ 0

theorem Verification.n16_rad_polynomial_of_second_midpoint {θ t : ℝ} (hθ : 0 < θ) (ht : 0 < t) (hh : n16Second θ t ^ 2 ≤ n16Second θ (2 * t) * n16Second θ 0) : 0 ≤ t ^ 2 - 4 * (1 - θ) * t + 2 * (1 - θ) ^ 2 - 8 * θ

theorem Verification.n16_density_necessary_polynomial {θ : ℝ} (hθ : 0 < θ) (hC : (nelsen16 θ ⋯).HasMTP2Density) : 4 * θ ≤ (θ - 1) ^ 2

theorem Verification.nelsen16_density_tp2_iff (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen16 θ hθ).HasMTP2Density ↔ 3 + 2 * √2 ≤ θ