← Mathematical handbook

theorem Verification.standardNormal_scaled_joint_density (r a b : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => (a * p.1, r * (a * p.1) + b * p.2)) ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ProbabilityTheory.gaussianPDF 0 (NNReal.mk (a ^ 2) ⋯) p.1 * ProbabilityTheory.gaussianPDF (r * p.1) (NNReal.mk (b ^ 2) ⋯) p.2

theorem Verification.gaussian_scaled_pair_density {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (a : ℝ) (ha : a ≠ 0) : MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin 2)) => (a * x.ofLp 0, a * x.ofLp 1)) (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r)) = MeasureTheory.volume.withDensity fun (p : ℝ × ℝ) => ProbabilityTheory.gaussianPDF 0 (NNReal.mk (a ^ 2) ⋯) p.1 * ProbabilityTheory.gaussianPDF (r * p.1) (NNReal.mk ((a * √(1 - r ^ 2)) ^ 2) ⋯) p.2