Experimental results: schema

The primitive values of Data/Experiments/<Paper>.lean, the per-paper modules that scripts/gen_experiments.py generates from Data/Experiments/<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. What a study concludes from the numbers (a prototype, a preference, a significant difference) is a definition in the study, not a stored label.

structure Data.Experiments.Decimal : Type

A decimal as printed: the value mantissa / 10 ^ exponent, with exponent the number of printed decimal places.

• mantissa : ℤ
• exponent : ℕ

def Data.Experiments.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.Experiments.instDecidableEqDecimal : DecidableEq Decimal

Equations

• Data.Experiments.instDecidableEqDecimal = Data.Experiments.instDecidableEqDecimal.decEq

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

Equations

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

@[instance_reducible]

instance Data.Experiments.instReprDecimal : Repr Decimal

Equations

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

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

The printed value.

Equations

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

def Data.Experiments.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.Experiments.Decimal.RoundsPercent (d : Decimal) (k n : ℕ) : Prop

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

Equations

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

@[instance_reducible]

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

Equations

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

def Data.Experiments.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.Experiments.Decimal.instDecidableRounds (d : Decimal) (k n : ℕ) : Decidable (d.Rounds k n)

Equations

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

def Data.Experiments.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.Experiments.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 := ⋯ }

inductive Data.Experiments.Sign : Type

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

• plus : Sign
• minus : Sign

@[instance_reducible]

instance Data.Experiments.instDecidableEqSign : DecidableEq Sign

Equations

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

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

Equations

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

@[instance_reducible]

instance Data.Experiments.instReprSign : Repr Sign

Equations

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