← Mathematical handbook

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

Equations

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

theorem Verification.map_gaussianWeightedDifference (r a b : ℝ) (hp : 0 < a ^ 2 + b ^ 2) : have μ := ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r); MeasureTheory.Measure.map (⇑(gaussianWeightedDifference a b)) (μ.prod μ) = μ

theorem Verification.gaussian_scaled_comparison_probability (r a b : ℝ) (hp : 0 < a ^ 2 + b ^ 2) : have μ := ProbabilityTheory.multivariateGaussian 0 (bivariateCorrelation r); (μ.prod μ).real {p : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) | a * p.1.ofLp 0 ≤ b * p.2.ofLp 0 ∧ a * p.1.ofLp 1 ≤ b * p.2.ofLp 1} = μ.real {x : EuclideanSpace ℝ (Fin 2) | x.ofLp 0 ≤ 0 ∧ x.ofLp 1 ≤ 0}