← Mathematical handbook

theorem Verification.nelsen13_toMeasure_density {θ : ℝ} (hθ : 1 ≤ θ) : (nelsen13 θ ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (n13Density θ x)

theorem Verification.nelsen13_hasMTP2Density {θ : ℝ} (hθ : 1 ≤ θ) : (nelsen13 θ ⋯).HasMTP2Density

theorem Verification.nelsen13_density_tp2_iff (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen13 θ hθ).HasMTP2Density ↔ 1 ≤ θ