← Mathematical handbook

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

Equations

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

theorem Verification.normalScaleMixtureMarginal_cdf (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (a : ℝ) : ↑(ProbabilityTheory.cdf (normalScaleMixtureMarginal μ s)) a = ∫ (t : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a / s t) ∂↑μ

theorem Verification.integrable_normalScaleMixture_cdf (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (a : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (a / s t)) ↑μ

theorem Verification.normalScaleMixtureMarginal_cdf_strictMono (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : StrictMono ↑(ProbabilityTheory.cdf (normalScaleMixtureMarginal μ s))

theorem Verification.normalScaleMixtureMarginal_cdf_neg (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (a : ℝ) : ↑(ProbabilityTheory.cdf (normalScaleMixtureMarginal μ s)) (-a) = 1 - ↑(ProbabilityTheory.cdf (normalScaleMixtureMarginal μ s)) a