structure
definition
Dataset
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.PDG.Fits on GitHub at line 160.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
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χ