Student t distribution

noncomputable def t_pdf (ν : ℝ) : ℝ → ℝ

The probability density function for the Student t distribution with ν degrees of freedom.

Equations

• t_pdf ν x = Real.Gamma ((ν + 1) / 2) / (√(Real.pi * ν) * Real.Gamma (ν / 2)) * (1 + x ^ 2 / ν) ^ (-((ν + 1) / 2))

noncomputable def logNormalPdf (μ σ : ℝ) : ℝ → ℝ

The probability density function for lognormal distribution with parameters μ and σ.

Equations

• logNormalPdf μ σ x = 1 / (σ * √(2 * Real.pi)) * (x ^ (-1) * Real.exp (-1 / (2 * σ ^ 2) * (Real.log x - μ) ^ 2))

noncomputable def logNormalPdf' (μ σ : ℝ) : ℝ → ℝ

Equations

• logNormalPdf' μ σ x = (σ * √(2 * Real.pi))⁻¹ * x⁻¹ * Real.exp (-(2 * σ ^ 2)⁻¹ * (Real.log x - μ) ^ 2)

theorem logNormalPdf_eq_logNormalPdf' (μ σ : ℝ) : logNormalPdf μ σ = logNormalPdf' μ σ

theorem rpow_neg_one_int {x : ℝ} (hx : x ≠ 0) (s e : ℝ) : e * (x ^ (-1)) ^ 2 * s * x ^ 2 = e * s

theorem rpow_neg_one_int' {x : ℝ} (hx : x ≠ 0) (s e : ℝ) : e * x⁻¹ ^ 2 * s * x ^ 2 = e * s

theorem derivLogNormal (μ σ : ℝ) {x : ℝ} (hx : x ≠ 0) : deriv (logNormalPdf μ σ) x = 1 / (σ * √(2 * Real.pi)) * Real.exp (-1 / (2 * σ ^ 2) * (Real.log x - μ) ^ 2) * x ^ (-2) * (-1 + -1 / σ ^ 2 * (Real.log x - μ))

A bit surprising that σ does not need to be positive here.

theorem mode_lognormal_equation {σ μ x : ℝ} (hσ : σ ≠ 0) (hx : 0 < x) (h : -1 + -1 / σ ^ 2 * (Real.log x - μ) = 0) : x = Real.exp (μ - σ ^ 2)

Auxiliary for the mode of the lognormal distribution.

theorem mode_lognormal (σ μ x : ℝ) (hσ : σ ≠ 0) (hx : 0 < x) (h : deriv (logNormalPdf μ σ) x = 0) : x = Real.exp (μ - σ ^ 2)

The mode of the lognormal distribution.

theorem derivStudent.extracted_1_1 {d e g h : ℝ} (f : ℝ) (this : d * e = g * h) : d * -f * e = -(f * g * h)

theorem tHelper {ν : ℝ} (hν : 0 ≤ ν) (x : ℝ) : 0 < 1 + x ^ 2 / ν

theorem derivStudent {ν : ℝ} (hν : 0 ≤ ν) : deriv (t_pdf ν) = fun (x : ℝ) => Real.Gamma ((ν + 1) / 2) / (√(Real.pi * ν) * Real.Gamma (ν / 2)) * (-((ν + 1) / 2) * (1 + x ^ 2 / ν) ^ (-((ν + 3) / 2)) * (2 * x / ν))

The messy formula for the derivative of Student's t.

theorem derivStudent' (x ν : ℝ) (hν : 0 < ν) : deriv (t_pdf ν) x = 0 ↔ x = 0

The only place the derivative of Student's t is 0 is 0.

theorem t_pdf_one (x : ℝ) : t_pdf 1 x = 1 / (Real.pi * (1 + x ^ 2))

The Student t distribution with one df is the Cauchy distribution.

theorem t_pdf_pos (x ν : ℝ) (hν : ν > 0) : t_pdf ν x > 0

The t distribution pdf has an everywhere-positive pdf.

theorem studentT2Pdf (x : ℝ) : t_pdf 2 x = 1 / (2 * √2) * (1 + x ^ 2 / 2) ^ (-3 / 2)

The pdf of the Student t distribution with 2 degrees of freedom.

theorem studentTDecreasing {x₁ x₂ ν : ℝ} (hν : 0 < ν) (h : x₁ ∈ Set.Ico 0 x₂) : t_pdf ν x₂ < t_pdf ν x₁

theorem studentTSymmetric (x ν : ℝ) : t_pdf ν x = t_pdf ν (-x)

theorem studentTIncreasing {x₁ x₂ ν : ℝ} (hν : 0 < ν) (h : x₂ ∈ Set.Ioc x₁ 0) : t_pdf ν x₁ < t_pdf ν x₂

theorem studentTMin (a ν : ℝ) (hν : 0 < ν) : ¬IsLocalMin (t_pdf ν) a

The Student t distribution pdf has no local minimum.

theorem studentTMode (x ν : ℝ) (hν : 0 ≤ ν) : t_pdf ν x ≤ t_pdf ν 0

theorem studentTMax (ν : ℝ) (hν : 0 ≤ ν) : IsLocalMax (t_pdf ν) 0

RANDOM VARIABLES

noncomputable def Bar {n : ℕ} : (Fin n → ℝ) → ℝ

The sample mean.

Equations

• Bar X = 1 / ↑n * ∑ i : Fin n, X i

noncomputable def S {n : ℕ} : (Fin n → ℝ) → ℝ

The sample standard deviation.

Equations

• S X = √(1 / (↑n - 1) * ∑ i : Fin n, (X i - Bar X) ^ 2)

noncomputable def T {μ : ℝ} {n : ℕ} : (Fin n → ℝ) → ℝ

The function underlying the t distribution. If X i are iid and N(μ, σ^2) then this T has the t distribution.

Equations

• T X = (Bar X - μ) / (S X / √↑n)

noncomputable def S₂ {m n : ℕ} : (Fin m → ℝ) → (Fin n → ℝ) → ℝ

Equations

• S₂ X Y = √(1 / (↑m - 1) * ∑ i : Fin m, (X i - Bar X) ^ 2 + 1 / (↑n - 1) * ∑ i : Fin n, (Y i - Bar Y) ^ 2)

noncomputable def BF {n : ℕ} : (Fin n → ℝ) → (Fin n → ℝ) → ℝ

Behrens-Fisher distribution.

Equations

• BF X Y = (Bar X - Bar Y) / S₂ X Y

theorem compute_sample_mean_example : Bar ![1, 1, 5] = 7 / 3

noncomputable def welch_df (s₁ s₂ n₁ n₂ ν₁ ν₂ : ℝ) : ℝ

Equations

• welch_df s₁ s₂ n₁ n₂ ν₁ ν₂ = (s₁ ^ 2 / n₁ + s₂ ^ 2 / n₂) ^ 2 / (s₁ ^ 4 / (n₁ ^ 2 * ν₁) + s₂ ^ 4 / (n₂ ^ 2 * ν₂))

theorem welch₀ {s₁ s₂ n₁ n₂ ν₁ ν₂ : ℝ} (hs₁ : 0 < s₁) (hs₂ : 0 < s₂) (hn₁ : 0 < n₁) (hn₂ : 0 < n₂) (hν₁ : 0 < ν₁) (hν₂ : 0 < ν₂) (h : ν₁ ≤ ν₂) : welch_df s₁ s₂ n₁ n₂ ν₁ ν₂ ≥ min ν₁ ν₂

theorem welch' {s₁ s₂ n₁ n₂ ν₁ ν₂ : ℝ} (hs₁ : 0 = s₁) (hs₂ : 0 < s₂) (hn₂ : 0 < n₂) : welch_df s₁ s₂ n₁ n₂ ν₁ ν₂ ≥ min ν₁ ν₂

The welch_df lower bound when s₁ or s₂ is 0.

theorem welch {s₁ s₂ n₁ n₂ ν₁ ν₂ : ℝ} (hs₁ : 0 ≤ s₁) (hs₂ : 0 < s₂) (hn₁ : 0 < n₁) (hn₂ : 0 < n₂) (hν₁ : 0 < ν₁) (hν₂ : 0 < ν₂) : welch_df s₁ s₂ n₁ n₂ ν₁ ν₂ ≥ min ν₁ ν₂

Slightly amusingly, if one of s₁, s₂ is zero the result still holds but if both are it does not.

theorem howell {s₁ s₂ n₁ n₂ ν₁ ν₂ : ℝ} (hs₁ : 0 < s₁) (hs₂ : 0 < s₂) (hn₁ : 0 < n₁ - 1) (hn₂ : 0 < n₂ - 1) (hνn₁ : ν₁ = n₁ - 1) (hνn₂ : ν₂ = n₂ - 1) : welch_df s₁ s₂ n₁ n₂ ν₁ ν₂ ≤ ν₁ + ν₂

A claim on the bottom of page 67: "We see that when n₁ = n₂, the difference between the Welch df and the conservative df is at most 1" That seems to be wrong.

But the claim at https://stats.stackexchange.com/questions/48636/are-the-degrees-of-freedom-for-welchs-test-always-less-than-the-df-of-the-poole is verified below.

theorem claimFromBook {s₁ s₂ n ν₁ ν₂ : ℝ} (hs₁ : 0 < s₁) (hs₂ : 0 < s₂) (hνn₁ : ν₁ = n - 1) (hνn₂ : ν₂ = n - 1) (h₂₀₂₅ : n = 2) : welch_df s₁ s₂ n n ν₁ ν₂ ≤ min ν₁ ν₂ + 1

I don't think this is true without the assumption n=2.

noncomputable def cχ (k : ℝ) : ℝ

Equations

• cχ k = (2 ^ (k / 2) * Real.Gamma (k / 2))⁻¹

noncomputable def χ2pdf (k : ℝ) : ℝ → ℝ

The probability density function of the χ² distribution with k degrees of freedom.

Equations

• χ2pdf k x = cχ k * (x ^ (k / 2 - 1) * Real.exp (-x / 2))

noncomputable def exponential_pdf (μ : ℝ) : ℝ → ℝ

The exponential distribution with parameter λ (written μ). We do not enforce x≥0 here.

Equations

• exponential_pdf μ x = μ * Real.exp (-μ * x)

theorem χ2_exponential (x : ℝ) : χ2pdf 2 x = exponential_pdf 2⁻¹ x

The χ² distribution with 2 degrees of freedom is the exponential distribution with parameter λ = 2⁻¹.

theorem auxχ (k x : ℝ) (hx : x ≠ 0) : DifferentiableAt ℝ (fun (x : ℝ) => x ^ (k / 2 - 1) * Real.exp (-x / 2)) x

theorem deriv_χ (k x : ℝ) (hx : x ≠ 0) : deriv (χ2pdf k) x = cχ k * Real.exp (-x / 2) * x ^ (k / 2 - 2) * (k / 2 - 1 - 2⁻¹ * x)

A formula for the derivative of the χ² pdf.

theorem cχ_ne_zero (k : ℝ) (hk : 0 < k) : cχ k ≠ 0

The multiplicative constant in the χ² pdf is nonzero.

theorem need₄ (x k : ℝ) (hk : k ≠ 4) (hx : 0 < x) (h : x ^ (k / 2 - 2) = 0) : x = k - 2

theorem deriv_χ_zero {x k : ℝ} (hk₀ : 0 < k) (hx : 0 < x) (h : deriv (χ2pdf k) x = 0) : x = k - 2

The only critical point of a χ²(k) pdf is k-2.

theorem no_deriv_χ_zero (x k : ℝ) (hk₀ : 0 < k) (hx : 0 < x) (h₀ : k ≤ 2) : deriv (χ2pdf k) x ≠ 0

The χ² distribution with 0 < k ≤ 2 df has no critical point.

theorem eventually_of_punctured {a b : ℝ} (hb : a ≠ b) {P : ℝ → Prop} (h₀ : ∀ (x : ℝ), x ≠ b → P x) : ∀ᶠ (x : ℝ) in nhds a, P x

theorem second_deriv_χ (a k : ℝ) (ha : a ≠ 0) : deriv (deriv (χ2pdf k)) a = cχ k * Real.exp (-a / 2) * a ^ (k / 2 - 3) * 4⁻¹ * ((k - 4 - a) * (k - 2 - a) - 2 * a)

The second derivative of the χ² pdf.

theorem deriv_χ_inflexia (a k : ℝ) (hk : 2 < k) (h : (k - 4 - a) * (k - 2 - a) - 2 * a = 0) : a = k - 4 ∨ a = (k - 2) / 3

Inflexia of the χ² distribution are symmetric around the mode. If k>2 then the solutions are real.

def σ : Fin 2 → MeasurableSpace (Fin 2 → Bool)

Equations

• σ i = MeasurableSpace.comap (fun (v : Fin 2 → Bool) => v i) Bool.instMeasurableSpace

noncomputable def fairCoin : PMF Bool

Equations

• fairCoin = PMF.bernoulli (1 / 2) fairCoin._proof_1

noncomputable def μ : MeasureTheory.Measure Bool

Equations

• μ = fairCoin.toMeasure

noncomputable def μ' : MeasureTheory.Measure (Fin 2 → Bool)

Equations

• μ' = MeasureTheory.Measure.pi fun (x : Fin 2) => μ

noncomputable def μ'' : PMF (Fin 2 → Bool)

Maybe easier to work with than Measure.pi

Equations

• μ'' = PMF.ofFintype (fun (v : Fin 2 → Bool) => 1 / 4) μ''._proof_2

noncomputable def ν : MeasureTheory.Measure (Fin 2 → Bool)

Equations

• ν = μ''.toMeasure

theorem basic_ν (b c : Bool) : ν {![b, c]} = 1 / 2 * (1 / 2)

theorem basic_μ' (b c : Bool) : μ' {![b, c]} = 1 / 2 * (1 / 2)

Now we can do the independence example without the silly 1/4 construction.

theorem what_is_σ (A : Set (Fin 2 → Bool)) (i : Fin 2) (hA : MeasurableSpace.MeasurableSet' (σ i) A) : A = ∅ ∨ A = {x : Fin 2 → Bool | x i = true} ∨ A = {x : Fin 2 → Bool | x i = false} ∨ A = Set.univ

As a first steps towards understanding σ-algebras in Lean, and thereby indepdendence of random variables, we characterize the σ-algebra σ₀ above.

theorem prob_μ' : μ' Set.univ = 1

theorem prob_ν : ν Set.univ = 1

shows ν is a probability measure in fact

theorem true_ν₀ (a : Bool) : ν {x : Fin 2 → Bool | x 0 = a} = 1 / 2

theorem true_μ'₁ (a : Bool) : μ' {x : Fin 2 → Bool | x 1 = a} = 1 / 2

theorem true_μ'₀ (a : Bool) : μ' {x : Fin 2 → Bool | x 0 = a} = 1 / 2

theorem true_ν₁ (a : Bool) : ν {x : Fin 2 → Bool | x 1 = a} = 1 / 2

theorem what_is_σ₀_not (A : Set (Fin 2 → Bool)) (hA : MeasurableSpace.MeasurableSet' (σ 0) A) : A ≠ {![false, false]}

theorem realIndependenceGENERAL {n : ℕ} (m : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure m] : ProbabilityTheory.iIndepFun (fun (i : Fin n) (v : Fin n → ℝ) => v i) (MeasureTheory.Measure.pi fun (x : Fin n) => m)

August 21, 2025 Existenc eof n independent real variables, e.g., m = gaussianReal 0 1.

theorem realIndependence (m : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure m] : ProbabilityTheory.IndepFun (fun (v : Fin 2 → ℝ) => v 0) (fun (v : Fin 2 → ℝ) => v 1) (MeasureTheory.Measure.pi fun (x : Fin 2) => m)

Using this we can construct the t distribution with 1 df and state its Behrens-Fisher-like property.