Hypothesis testing

noncomputable def one_sided_pval (a : ℝ) (p : MeasureTheory.Measure ℝ) : ENNReal

Equations

• One or more equations did not get rendered due to their size.

noncomputable def one_sided_pvalPMF (a : ℝ) (p : PMF ℝ) : ENNReal

Equations

• One or more equations did not get rendered due to their size.

noncomputable def one_sided_pval' (a : ℝ) (p : MeasureTheory.Measure ℝ) : ENNReal

Equations

• one_sided_pval' a p = if a > ProbabilityTheory.moment id 1 p then p (Set.Ici a) else if a < ProbabilityTheory.moment id 1 p then p (Set.Iic a) else 1

noncomputable def two_sided_pval' (a : ℝ) (p : MeasureTheory.Measure ℝ) : ENNReal

Equations

• One or more equations did not get rendered due to their size.

noncomputable def two_sided_pval (a : ℝ) (p : MeasureTheory.Measure ℝ) : ENNReal

Equations

• two_sided_pval a p = p {x : ℝ | |x - ProbabilityTheory.moment id 1 p| ≥ |a - ProbabilityTheory.moment id 1 p|}

def twoSidedRejectionRegion (p : MeasureTheory.Measure ℝ) (threshold : ENNReal) : Set ℝ

Equations

• twoSidedRejectionRegion p threshold = {observed : ℝ | two_sided_pval observed p < threshold}

def power (threshold : ENNReal) (p₀ p : MeasureTheory.Measure ℝ) : ENNReal

Equations

• power threshold p₀ p = p (twoSidedRejectionRegion p₀ threshold)

def type1err (f : ℝ → MeasureTheory.Measure ℝ) (hypθ realθ observed : ℝ) (threshold : ENNReal) : Prop

Type 1 error when testing H₀ : θ = hypθ Incorrectly reject H₀.

Equations

• type1err f hypθ realθ observed threshold = (observed ∈ twoSidedRejectionRegion (f hypθ) threshold ∧ hypθ = realθ)

def type2err (f : ℝ → MeasureTheory.Measure ℝ) (hypθ realθ observed : ℝ) (threshold : ENNReal) : Prop

Type 2 error: incorrectly fail to reject H₀.

Equations

• type2err f hypθ realθ observed threshold = (observed ∉ twoSidedRejectionRegion (f hypθ) threshold ∧ hypθ ≠ realθ)

def correct_fail_to_reject (f : ℝ → MeasureTheory.Measure ℝ) (hypθ realθ observed : ℝ) (threshold : ENNReal) : Prop

Equations

• correct_fail_to_reject f hypθ realθ observed threshold = (observed ∉ twoSidedRejectionRegion (f hypθ) threshold ∧ hypθ = realθ)

def correct_reject (f : ℝ → MeasureTheory.Measure ℝ) (hypθ realθ observed : ℝ) (threshold : ENNReal) : Prop

Equations

• correct_reject f hypθ realθ observed threshold = (observed ∈ twoSidedRejectionRegion (f hypθ) threshold ∧ hypθ ≠ realθ)

theorem two_sided_p_val_eq_two_sided_p_val' (a : ℝ) (p : MeasureTheory.Measure ℝ) : two_sided_pval a p = two_sided_pval' a p

theorem one_sided_p_val_eq_one_sided_p_val' (a : ℝ) (p : MeasureTheory.Measure ℝ) : one_sided_pval a p = one_sided_pval' a p

theorem one_sided_p_val_le_two_sided_p_val (a : ℝ) (p : MeasureTheory.Measure ℝ) : one_sided_pval a p ≤ two_sided_pval a p