Dataset

formal source

 157  chi2Max : ℝ
 158  deriving Repr
 159
 160structure Dataset where
 161  leptons : List SpeciesEntry
 162  quarks  : List SpeciesEntry
 163  bosons  : List SpeciesEntry
 164  baryons : List SpeciesEntry
 165  deriving Repr
 166
 167@[simp] def defaultDataset : Dataset :=
 168  { leptons := leptonsWitness
 169  , quarks  := quarksWitness
 170  , bosons  := bosonsWitness
 171  , baryons := baryonsWitness
 172  }
 173
 174/-- All-species acceptability at given thresholds. -/
 175def acceptable_all (D : Dataset) (T : Thresholds) : Prop :=
 176  acceptable D.leptons T.zMax T.chi2Max ∧
 177  acceptable D.quarks  T.zMax T.chi2Max ∧
 178  acceptable D.bosons  T.zMax T.chi2Max ∧
 179  acceptable D.baryons T.zMax T.chi2Max
 180
 181/-- Monotonicity of single-list acceptability in the thresholds. -/
 182lemma acceptable_mono {L : List SpeciesEntry}
 183  {z₁ z₂ χ₁ χ₂ : ℝ}
 184  (hz : z₁ ≤ z₂) (hχ : χ₁ ≤ χ₂) :
 185  acceptable L z₁ χ₁ → acceptable L z₂ χ₂ := by
 186  intro h
 187  rcases h with ⟨hzs, hchi⟩
 188  refine And.intro ?hzs' ?hchi'
 189  · intro e he; exact le_trans (hzs e he) hz
 190  · exact le_trans hchi hχ