← Mathematical handbook

theorem Verification.integral_Iic_le_of_affine_single_crossing {μ : MeasureTheory.Measure ℝ} {H : ℝ → ℝ} (hH : Monotone H) {p q r s : ℝ} (hqs : q ≤ s) (hf : MeasureTheory.Integrable (fun (x : ℝ) => H (p - q * x)) μ) (hg : MeasureTheory.Integrable (fun (x : ℝ) => H (r - s * x)) μ) (he : ∫ (x : ℝ), H (p - q * x) ∂μ = ∫ (x : ℝ), H (r - s * x) ∂μ) (a : ℝ) : ∫ (x : ℝ) in Set.Iic a, H (p - q * x) ∂μ ≤ ∫ (x : ℝ) in Set.Iic a, H (r - s * x) ∂μ

theorem Verification.gaussian_standardized_slope_monotone {r s : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (hs : s ∈ Set.Ioo (-1) 1) (hrs : r ≤ s) : r / √(1 - r ^ 2) ≤ s / √(1 - s ^ 2)

theorem Verification.gaussianConditional_normal_integral {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (b : ℝ) : ∫ (x : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((b - r * x) / √(1 - r ^ 2)) ∂ProbabilityTheory.gaussianReal 0 1 = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) b

theorem Verification.gaussianBivariate_cdf_normal_monotone {r s : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (hs : s ∈ Set.Ioo (-1) 1) (hrs : r ≤ s) (a b : ℝ) : (gaussianBivariate r ⋯).cdf ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b] ≤ (gaussianBivariate s ⋯).cdf ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) a, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) b]

theorem Verification.gaussianBivariate_lowerOrthant_monotone {r s : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hs : s ∈ Set.Icc (-1) 1) (hrs : r ≤ s) : (gaussianBivariate r hr).LowerOrthantLE (gaussianBivariate s hs)

theorem Verification.gaussianBivariate_lowerOrthant_iff {r s : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hs : s ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).LowerOrthantLE (gaussianBivariate s hs) ↔ r ≤ s

theorem Verification.gaussianBivariate_schur_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate (-r) ⋯).SchurLE (gaussianBivariate r hr) ∧ (gaussianBivariate r hr).SchurLE (gaussianBivariate (-r) ⋯)

theorem Verification.gaussianBivariate_schur_abs {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (gaussianBivariate |r| ⋯).SchurLE (gaussianBivariate r hr) ∧ (gaussianBivariate r hr).SchurLE (gaussianBivariate |r| ⋯)

theorem Verification.gaussianBivariate_schur_iff {r s : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hs : s ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).SchurLE (gaussianBivariate s hs) ↔ |r| ≤ |s|

theorem Verification.gaussianBivariate_schurBoth_iff {r s : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hs : s ∈ Set.Icc (-1) 1) : (gaussianBivariate r hr).SchurBothLE (gaussianBivariate s hs) ↔ |r| ≤ |s|