← Mathematical handbook

noncomputable def Verification.gaussianSample (r : ℝ) (x : Fin 2 → ℝ) : Fin 2 → ↑unitInterval

Equations

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

theorem Verification.measurable_gaussianSample (r : ℝ) : Measurable (gaussianSample r)

theorem Verification.gaussianBivariate_cdf_sample {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (u : Fin 2 → ↑unitInterval) : (gaussianBivariate r hr).cdf u = ∫ (x : Fin 2 → ℝ), (Set.Iic u).indicator (fun (x : Fin 2 → ↑unitInterval) => 1) (gaussianSample r x) ∂MeasureTheory.Measure.pi fun (x : Fin 2) => ProbabilityTheory.gaussianReal 0 1

theorem Verification.gaussianBivariate_sample_integral_continuousAt {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (u : Fin 2 → ↑unitInterval) : ContinuousAt (fun (s : ℝ) => ∫ (x : Fin 2 → ℝ), (Set.Iic u).indicator (fun (x : Fin 2 → ↑unitInterval) => 1) (gaussianSample s x) ∂MeasureTheory.Measure.pi fun (x : Fin 2) => ProbabilityTheory.gaussianReal 0 1) r

theorem Verification.gaussianBivariate_cdf_continuous (u : Fin 2 → ↑unitInterval) : Continuous fun (r : ↑(Set.Icc (-1) 1)) => (gaussianBivariate ↑r ⋯).cdf u

theorem Verification.gaussianBivariate_cdf_tendsto_zero (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (gaussianBivariate ↑r ⋯).cdf u) (nhds ⟨0, ⋯⟩) (nhds ((ProbabilityTheory.Copula.independence 2).cdf u))

theorem Verification.gaussianBivariate_cdf_tendsto_one (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (gaussianBivariate ↑r ⋯).cdf u) (nhds ⟨1, ⋯⟩) (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))

theorem Verification.gaussianBivariate_cdf_tendsto_negative_one (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (r : ↑(Set.Icc (-1) 1)) => (gaussianBivariate ↑r ⋯).cdf u) (nhds ⟨-1, ⋯⟩) (nhds (ProbabilityTheory.Copula.countermonotonic.cdf u))