← Mathematical handbook

theorem Verification.lognormalSpectralWeight_pdf (s z : ℝ) : ProbabilityTheory.gaussianPDFReal 0 1 z * lognormalSpectralWeight s z = ProbabilityTheory.gaussianPDFReal s 1 z

theorem Verification.lognormalSpectralWeight_integral_Iic (s b : ℝ) : ∫ (z : ℝ) in Set.Iic b, lognormalSpectralWeight s z ∂ProbabilityTheory.gaussianReal 0 1 = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (b - s)

theorem Verification.lognormalSpectralWeight_integral_Ioi (s b : ℝ) : ∫ (z : ℝ) in Set.Ioi b, lognormalSpectralWeight s z ∂ProbabilityTheory.gaussianReal 0 1 = 1 - ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (b - s)

theorem Verification.lognormalSpectral_max_integral (s x y b : ℝ) (hs : 0 < s) (hx : 0 < x) (hb : x * lognormalSpectralWeight s b = y) : ∫ (z : ℝ), max (x * lognormalSpectralWeight s z) y ∂ProbabilityTheory.gaussianReal 0 1 = y * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) b + x * (1 - ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (b - s))