Printed statistics: schema

The primitive values of Data/Statistics/<Paper>.lean, the per-paper modules that scripts/gen_statistics.py generates from Data/Statistics/<Paper>.json. A paper's own coding labels (its factors, response types, predictors) become generated enums, and each table it prints becomes a generated structure with one row per printed line; this file holds only what every paper shares.

This is data: it imports nothing from Linglib/ and states no theorems about theories. A statistic is kept as printed, Decimal recording the digits so that 75 and 75.0 differ, and a study reads it through Decimal.toRat. A p-value is a PValue, kept with the relation it is printed with, so that p < .05 and p = .05 differ, and read at a level through PValue.Significant. What a study concludes from the numbers (a prototype, a preference, the effects it counts as found) is a definition in the study, not a stored label.

structure Data.Statistics.Decimal : Type

A decimal as printed: the value mantissa / 10 ^ exponent, with exponent the place of the last printed digit, the number of decimal places or the k of a printed power of ten 10^-k.

• mantissa : ℤ
• exponent : ℕ

def Data.Statistics.instDecidableEqDecimal.decEq (x✝ x✝¹ : Decimal) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Data.Statistics.instDecidableEqDecimal : DecidableEq Decimal

Equations

• Data.Statistics.instDecidableEqDecimal = Data.Statistics.instDecidableEqDecimal.decEq

@[instance_reducible]

instance Data.Statistics.instReprDecimal : Repr Decimal

Equations

• Data.Statistics.instReprDecimal = { reprPrec := Data.Statistics.instReprDecimal.repr }

def Data.Statistics.instReprDecimal.repr : Decimal → ℕ → Std.Format

Equations

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

def Data.Statistics.Decimal.toRat (d : Decimal) : ℚ

The printed value.

Equations

• d.toRat = ↑d.mantissa / 10 ^ d.exponent

@[simp]

theorem Data.Statistics.Decimal.toRat_pos (d : Decimal) : 0 < d.toRat ↔ 0 < d.mantissa

@[simp]

theorem Data.Statistics.Decimal.toRat_neg (d : Decimal) : d.toRat < 0 ↔ d.mantissa < 0

@[instance_reducible]

instance Data.Statistics.Decimal.instDecidableLtRatOfNatToRat (d : Decimal) : Decidable (0 < d.toRat)

Equations

• d.instDecidableLtRatOfNatToRat = decidable_of_iff' (0 < d.mantissa) ⋯

@[instance_reducible]

instance Data.Statistics.Decimal.instDecidableLtRatToRatOfNat (d : Decimal) : Decidable (d.toRat < 0)

Equations

• d.instDecidableLtRatToRatOfNat = decidable_of_iff' (d.mantissa < 0) ⋯

def Data.Statistics.Decimal.hundredths (d : Decimal) : ℤ

The printed value in hundredths, exact when at most two places are printed: a proportion printed to two places, in percent.

Equations

• d.hundredths = d.mantissa * 100 / 10 ^ d.exponent

def Data.Statistics.Decimal.Rounds (d : Decimal) (k n : ℕ) : Prop

The printed value is the proportion k / n rounded to the printed places: the two differ by at most half a unit in the last printed place.

Equations

• d.Rounds k n = (2 * |10 ^ d.exponent * ↑k - d.mantissa * ↑n| ≤ ↑n)

@[instance_reducible]

instance Data.Statistics.Decimal.instDecidableRounds (d : Decimal) (k n : ℕ) : Decidable (d.Rounds k n)

Equations

• d.instDecidableRounds k n = Data.Statistics.Decimal.instDecidableRounds._aux_1 d k n

theorem Data.Statistics.Decimal.rounds_iff {d : Decimal} {k n : ℕ} (hn : 0 < n) : d.Rounds k n ↔ |↑k / ↑n - d.toRat| ≤ 1 / (2 * 10 ^ d.exponent)

def Data.Statistics.Decimal.RoundsPercent (d : Decimal) (k n : ℕ) : Prop

The printed value is the percentage 100 * k / n rounded to the printed places.

Equations

• d.RoundsPercent k n = d.Rounds (100 * k) n

@[instance_reducible]

instance Data.Statistics.Decimal.instDecidableRoundsPercent (d : Decimal) (k n : ℕ) : Decidable (d.RoundsPercent k n)

Equations

• d.instDecidableRoundsPercent k n = Data.Statistics.Decimal.instDecidableRoundsPercent._aux_1 d k n

def Data.Statistics.Decimal.AttainablePercent (d : Decimal) (n : ℕ) : Prop

Some count out of n rounds to the printed percentage.

Equations

• d.AttainablePercent n = ∃ (k : Fin (n + 1)), d.RoundsPercent (↑k) n

@[instance_reducible]

instance Data.Statistics.Decimal.instDecidableAttainablePercent (d : Decimal) (n : ℕ) : Decidable (d.AttainablePercent n)

Equations

• d.instDecidableAttainablePercent n = { decide := decide (∃ k < n + 1, ∀ (h : k < n + 1), (fun (x : Fin (n + 1)) => d.RoundsPercent (↑x) n) ⟨k, h⟩), reflects_decide := ⋯ }

structure Data.Statistics.PValue : Type

A p-value as printed: the relation compare p value it is printed with and the printed value, p < .001 as ⟨.lt, ⟨1, 3⟩⟩ and p = .03 as ⟨.eq, ⟨3, 2⟩⟩.

• relation : Ordering
• value : Decimal

def Data.Statistics.instDecidableEqPValue.decEq (x✝ x✝¹ : PValue) : Decidable (x✝ = x✝¹)

Equations

• Data.Statistics.instDecidableEqPValue.decEq { relation := a, value := a_1 } { relation := b, value := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.Statistics.instDecidableEqPValue : DecidableEq PValue

Equations

• Data.Statistics.instDecidableEqPValue = Data.Statistics.instDecidableEqPValue.decEq

@[instance_reducible]

instance Data.Statistics.instReprPValue : Repr PValue

Equations

• Data.Statistics.instReprPValue = { reprPrec := Data.Statistics.instReprPValue.repr }

def Data.Statistics.instReprPValue.repr : PValue → ℕ → Std.Format

Equations

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

def Data.Statistics.PValue.Significant (p : PValue) (α : ℚ) : Prop

A printed p-value is significant at level α when every p-value it allows is below α.

Equations

• p.Significant α = ∀ (q : ℚ), compare q p.value.toRat = p.relation → q < α

@[simp]

theorem Data.Statistics.PValue.significant_lt {v : Decimal} {α : ℚ} : { relation := Ordering.lt, value := v }.Significant α ↔ v.toRat ≤ α

@[simp]

theorem Data.Statistics.PValue.significant_eq {v : Decimal} {α : ℚ} : { relation := Ordering.eq, value := v }.Significant α ↔ v.toRat < α

@[simp]

theorem Data.Statistics.PValue.not_significant_gt {v : Decimal} {α : ℚ} : ¬{ relation := Ordering.gt, value := v }.Significant α

@[instance_reducible]

instance Data.Statistics.PValue.instDecidableSignificant (p : PValue) (α : ℚ) : Decidable (p.Significant α)

Equations

• { relation := Ordering.lt, value := value }.instDecidableSignificant α = decidable_of_iff' (value.toRat ≤ α) ⋯
• { relation := Ordering.eq, value := value }.instDecidableSignificant α = decidable_of_iff' (value.toRat < α) ⋯
• { relation := Ordering.gt, value := value }.instDecidableSignificant α = isFalse ⋯

inductive Data.Statistics.Sign : Type

The sign of a binary feature in the [+F] / [-F] notation.

• plus : Sign
• minus : Sign

@[instance_reducible]

instance Data.Statistics.instDecidableEqSign : DecidableEq Sign

Equations

• Data.Statistics.instDecidableEqSign x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Data.Statistics.instReprSign : Repr Sign

Equations

• Data.Statistics.instReprSign = { reprPrec := Data.Statistics.instReprSign.repr }

def Data.Statistics.instReprSign.repr : Sign → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Data.Statistics.instReprSign.repr Data.Statistics.Sign.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Data.Statistics.Sign.plus")).group prec✝