← Mathematical handbook

noncomputable def Verification.gaussianRhoNoise (r a b c d : ℝ) : (ℝ × ℝ) × ℝ × ℝ →L[ℝ] EuclideanSpace ℝ (Fin 2)

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.map_gaussianRhoNoise {r a b c d : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hab : a ^ 2 + b ^ 2 = 1) (hcd : c ^ 2 + d ^ 2 = 1) : MeasureTheory.Measure.map (⇑(gaussianRhoNoise r a b c d)) (((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)).prod ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1))) = ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation (r * a * c))

noncomputable def Verification.gaussianRhoScaledNoise (r a b c : ℝ) : (ℝ × ℝ) × ℝ × ℝ →L[ℝ] EuclideanSpace ℝ (Fin 2)

Equations

• Verification.gaussianRhoScaledNoise r a b c = Verification.gaussianRhoNoise r (-a / √(a ^ 2 + b ^ 2)) (b / √(a ^ 2 + b ^ 2)) (-a / √(a ^ 2 + c ^ 2)) (c / √(a ^ 2 + c ^ 2))

theorem Verification.map_gaussianRhoScaledNoise {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b c : ℝ) (hab : 0 < a ^ 2 + b ^ 2) (hac : 0 < a ^ 2 + c ^ 2) : MeasureTheory.Measure.map (⇑(gaussianRhoScaledNoise r a b c)) (((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)).prod ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1))) = ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation (r * a ^ 2 / (√(a ^ 2 + b ^ 2) * √(a ^ 2 + c ^ 2))))

theorem Verification.gaussian_scaled_independent_comparison {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b c : ℝ) (hab : 0 < a ^ 2 + b ^ 2) (hac : 0 < a ^ 2 + c ^ 2) : (((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)).prod ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1))).real {p : (ℝ × ℝ) × ℝ × ℝ | b * p.1.2 ≤ a * p.1.1 ∧ c * p.2.2 ≤ a * (r * p.1.1 + √(1 - r ^ 2) * p.2.1)} = (ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation (r * a ^ 2 / (√(a ^ 2 + b ^ 2) * √(a ^ 2 + c ^ 2))))).real {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 0 ∧ x.ofLp 1 ≤ 0}

theorem Verification.scaledGaussianRhoCorrelation_mem {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b c : ℝ) (hab : 0 < a ^ 2 + b ^ 2) (hac : 0 < a ^ 2 + c ^ 2) : r * a ^ 2 / (√(a ^ 2 + b ^ 2) * √(a ^ 2 + c ^ 2)) ∈ Set.Icc (-1) 1

theorem Verification.gaussian_scaled_independent_comparison_arcsin {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b c : ℝ) (hab : 0 < a ^ 2 + b ^ 2) (hac : 0 < a ^ 2 + c ^ 2) : (((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1)).prod ((ProbabilityTheory.gaussianReal 0 1).prod (ProbabilityTheory.gaussianReal 0 1))).real {p : (ℝ × ℝ) × ℝ × ℝ | b * p.1.2 ≤ a * p.1.1 ∧ c * p.2.2 ≤ a * (r * p.1.1 + √(1 - r ^ 2) * p.2.1)} = 1 / 4 + Real.arcsin (r * a ^ 2 / (√(a ^ 2 + b ^ 2) * √(a ^ 2 + c ^ 2))) / (2 * Real.pi)