F distribution

noncomputable def FDistributionNumerator (d₁ d₂ : ℝ) : ℝ → ℝ

Equations

• FDistributionNumerator d₁ d₂ x = √(d₁ ^ d₁ * d₂ ^ d₂ * x ^ d₁ / (d₁ * x + d₂) ^ (d₁ + d₂))

noncomputable def Real.Beta (d₁ d₂ : ℝ) : ℝ

Equations

• d₁.Beta d₂ = Real.Gamma d₁ * Real.Gamma d₂ / Real.Gamma (d₁ + d₂)

noncomputable def FDistribution (d₁ d₂ : ℝ) : ℝ → ℝ

Equations

• FDistribution d₁ d₂ = (fun (x : ℝ) => FDistributionNumerator d₁ d₂ x) / fun (x : ℝ) => x * (d₁ / 2).Beta (d₂ / 2)

theorem deriv_FdistributionNumerator (a d₁ d₂ x : ℝ) (hd₁ : 0 < d₁) (hd₂ : 0 < d₂) (hx : 0 < x) : deriv (FDistributionNumerator d₁ d₂) x = (d₁ ^ d₁ * d₂ ^ d₂ * (d₁ * x ^ (d₁ - 1)) * (d₁ * x + d₂) ^ (d₁ + d₂) - d₁ ^ d₁ * d₂ ^ d₂ * x ^ d₁ * ((d₁ + d₂) * (d₁ * x + d₂) ^ (d₁ + d₂ - 1) * d₁)) / ((d₁ * x + d₂) ^ (d₁ + d₂)) ^ 2 / (2 * √(d₁ ^ d₁ * d₂ ^ d₂ * x ^ d₁ / (d₁ * x + d₂) ^ (d₁ + d₂)))

theorem deriv_Fdistribution (a d₁ d₂ x : ℝ) (hd₁ : 0 < d₁) (hd₂ : 0 < d₂) (hx : 0 < x) : deriv (FDistribution d₁ d₂) x = (d₁ ^ d₁ * d₂ ^ d₂ * d₁ * (x ^ (d₁ - 1) * (d₁ * x + d₂) ^ (d₁ + d₂) - x ^ d₁ * ((d₁ + d₂) * (d₁ * x + d₂) ^ (d₁ + d₂ - 1))) / ((d₁ * x + d₂) ^ (d₁ + d₂)) ^ 2 / (2 * √(d₁ ^ d₁ * d₂ ^ d₂ * x ^ d₁ / (d₁ * x + d₂) ^ (d₁ + d₂))) * (x * (d₁ / 2).Beta (d₂ / 2)) - √(d₁ ^ d₁ * d₂ ^ d₂ * x ^ d₁ / (d₁ * x + d₂) ^ (d₁ + d₂)) * (d₁ / 2).Beta (d₂ / 2)) / (x * (d₁ / 2).Beta (d₂ / 2)) ^ 2

theorem simplify (a d₁ d₂ x target : ℝ) (hd₁ : 0 < d₁) (hd₂ : 0 < d₂) (hx : 0 < x) : (d₁ ^ d₁ * d₂ ^ d₂ * d₁ * (x ^ (d₁ - 1) * (d₁ * x + d₂) ^ (d₁ + d₂) - x ^ d₁ * ((d₁ + d₂) * (d₁ * x + d₂) ^ (d₁ + d₂ - 1))) / ((d₁ * x + d₂) ^ (d₁ + d₂)) ^ 2 / (2 * √(d₁ ^ d₁ * d₂ ^ d₂ * x ^ d₁ / (d₁ * x + d₂) ^ (d₁ + d₂))) * (x * (d₁ / 2).Beta (d₂ / 2)) - √(d₁ ^ d₁ * d₂ ^ d₂ * x ^ d₁ / (d₁ * x + d₂) ^ (d₁ + d₂)) * (d₁ / 2).Beta (d₂ / 2)) / (x * (d₁ / 2).Beta (d₂ / 2)) ^ 2 = -(d₂ ^ (d₂ / 2) * d₁ ^ (d₁ / 2) * x ^ (d₁ / 2 - 2) * (d₂ * (d₁ * (x - 1) + 2) + 2 * d₁ * x) * (d₂ + d₁ * x) ^ (1 / 2 * (-d₂ - d₁ - 2))) / (2 * (d₁ / 2).Beta (d₂ / 2))