← Mathematical handbook

noncomputable def Verification.positivePower (ν z : ℝ) : ℝ

Equations

• Verification.positivePower ν z = max z 0 ^ ν

theorem Verification.positivePower_nonneg (ν z : ℝ) : 0 ≤ positivePower ν z

theorem Verification.positivePower_continuous (ν : ℝ) (hν : 0 < ν) : Continuous (positivePower ν)

theorem Verification.positivePower_integrable (ν : ℝ) (hν : 0 < ν) : MeasureTheory.Integrable (positivePower ν) (ProbabilityTheory.gaussianReal 0 1)

noncomputable def Verification.gaussianPositiveMoment (ν : ℝ) : ℝ

Equations

• Verification.gaussianPositiveMoment ν = ∫ (z : ℝ), Verification.positivePower ν z ∂ProbabilityTheory.gaussianReal 0 1

theorem Verification.gaussianPositiveMoment_pos (ν : ℝ) (hν : 0 < ν) : 0 < gaussianPositiveMoment ν

noncomputable def Verification.gaussianPositiveWeight (ν z : ℝ) : ℝ

Equations

• Verification.gaussianPositiveWeight ν z = Verification.positivePower ν z / Verification.gaussianPositiveMoment ν

theorem Verification.gaussianPositiveWeight_integrable (ν : ℝ) (hν : 0 < ν) : MeasureTheory.Integrable (gaussianPositiveWeight ν) (ProbabilityTheory.gaussianReal 0 1)

theorem Verification.gaussianPositiveWeight_nonneg (ν : ℝ) (hν : 0 < ν) (z : ℝ) : 0 ≤ gaussianPositiveWeight ν z

theorem Verification.gaussianPositiveWeight_mean (ν : ℝ) (hν : 0 < ν) : ∫ (z : ℝ), gaussianPositiveWeight ν z ∂ProbabilityTheory.gaussianReal 0 1 = 1