lemma
proved
acceptable_mono
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.PDG.Fits on GitHub at line 182.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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χ
191
192/-- Monotonicity of all-species acceptability in the thresholds. -/
193lemma acceptable_all_mono (D : Dataset)
194 {T₁ T₂ : Thresholds}
195 (hZ : T₁.zMax ≤ T₂.zMax) (hC : T₁.chi2Max ≤ T₂.chi2Max) :
196 acceptable_all D T₁ → acceptable_all D T₂ := by
197 intro h; rcases h with ⟨hl, hq, hb, hB⟩
198 refine And.intro ?hl' (And.intro ?hq' (And.intro ?hb' ?hB'))
199 · exact acceptable_mono (L:=D.leptons) hZ hC hl
200 · exact acceptable_mono (L:=D.quarks) hZ hC hq
201 · exact acceptable_mono (L:=D.bosons) hZ hC hb
202 · exact acceptable_mono (L:=D.baryons) hZ hC hB
203
204/-- Baseline: default dataset satisfies thresholds (0,0). -/
205lemma acceptable_all_default_zero : acceptable_all defaultDataset { zMax := 0, chi2Max := 0 } := by
206 refine And.intro ?hl (And.intro ?hq (And.intro ?hb ?hB))
207 · simpa [defaultDataset] using acceptable_leptons
208 · simpa [defaultDataset] using acceptable_quarks
209 · simpa [defaultDataset] using acceptable_bosons
210 · simpa [defaultDataset] using acceptable_baryons
211
212namespace External