← Mathematical handbook

noncomputable def Verification.normalScaleMixtureDensity (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (x : ℝ) : ENNReal

Equations

• Verification.normalScaleMixtureDensity μ s x = ∫⁻ (t : ℝ), ProbabilityTheory.gaussianPDF 0 (NNReal.mk (s t ^ 2) ⋯) x ∂↑μ

theorem Verification.measurable_normalScaleMixtureDensity (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) : Measurable (normalScaleMixtureDensity μ s)

theorem Verification.normalScaleMixtureMarginal_withDensity (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : normalScaleMixtureMarginal μ s = MeasureTheory.volume.withDensity (normalScaleMixtureDensity μ s)

theorem Verification.normalScaleMixtureDensity_pos (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (x : ℝ) : 0 < normalScaleMixtureDensity μ s x

theorem Verification.normalScaleMixtureMarginal_equivalent_volume (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (normalScaleMixtureMarginal μ s).AbsolutelyContinuous MeasureTheory.volume ∧ MeasureTheory.volume.AbsolutelyContinuous (normalScaleMixtureMarginal μ s)