Limiting probability measures

Irfan Alam

concerns integrals. Here we merely 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