← Mathematical handbook

noncomputable def Verification.normalScaleMixtureAffineLaw (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (m : ℝ) : MeasureTheory.Measure ℝ

Equations

• Verification.normalScaleMixtureAffineLaw μ s m = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => m + s p.2 * p.1) ((ProbabilityTheory.gaussianReal 0 1).prod ↑μ)

theorem Verification.normalScaleMixtureAffineLaw_withDensity (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (m : ℝ) : normalScaleMixtureAffineLaw μ s m = MeasureTheory.volume.withDensity fun (x : ℝ) => ∫⁻ (t : ℝ), ProbabilityTheory.gaussianPDF m (NNReal.mk (s t ^ 2) ⋯) x ∂↑μ

theorem Verification.normalScaleMixtureAffineLaw_cdf (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (m y : ℝ) : ↑(ProbabilityTheory.cdf (normalScaleMixtureAffineLaw μ s m)) y = ∫ (t : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((y - m) / s t) ∂↑μ