Limiting probability measures

by Irfan Alam

concerns integrals. Here we compute some.

theorem int000 : ∫ (x : ℝ) in Set.Icc 0 0, 0 = 0

theorem int01xminus1 : (∫ (x : ℝ) in 0 ..2, x) - 1 = 1

theorem int02pisin : ∫ (x : ℝ) in 0 ..2 * Real.pi, Real.sin x = 0

theorem int02picos : ∫ (x : ℝ) in 0 ..2 * Real.pi, Real.cos x = 0

theorem int01cosSqAddSinSq : ∫ (x : ℝ) in 0 ..1, Real.cos x ^ 2 + Real.sin x ^ 2 = 1

theorem int011 : ∫ (x : ℝ) in 0 ..1, 1 = 1