z_Dpp_zero

formal source

 128
 129@[simp] lemma z_p_zero : z p_entry = 0 := by simp [z]
 130@[simp] lemma z_n_zero : z n_entry = 0 := by simp [z]
 131@[simp] lemma z_Dpp_zero : z Delta_pp_entry = 0 := by simp [z]
 132@[simp] lemma z_Dp_zero  : z Delta_p_entry  = 0 := by simp [z]
 133@[simp] lemma z_D0_zero  : z Delta_0_entry  = 0 := by simp [z]
 134@[simp] lemma z_Dm_zero  : z Delta_m_entry  = 0 := by simp [z]
 135
 136@[simp] lemma chi2_baryons_zero : chi2 baryonsWitness = 0 := by
 137  simp [chi2, baryonsWitness, z_p_zero, z_n_zero, z_Dpp_zero, z_Dp_zero, z_D0_zero, z_Dm_zero]
 138
 139@[simp] lemma acceptable_baryons : acceptable baryonsWitness 0 0 := by
 140  refine And.intro ?hzs ?hchi
 141  · intro e he
 142    have hcases : e = p_entry ∨ e = n_entry ∨ e = Delta_pp_entry ∨ e = Delta_p_entry ∨ e = Delta_0_entry ∨ e = Delta_m_entry := by
 143      simpa [baryonsWitness] using he
 144    rcases hcases with h | h | h | h | h | h
 145    · subst h; simp [z_p_zero]
 146    · subst h; simp [z_n_zero]
 147    · subst h; simp [z_Dpp_zero]
 148    · subst h; simp [z_Dp_zero]
 149    · subst h; simp [z_D0_zero]
 150    · subst h; simp [z_Dm_zero]
 151  · simpa using chi2_baryons_zero
 152
 153/-! Parameterized PDG fits: thresholds and dataset wrappers. -/
 154
 155structure Thresholds where
 156  zMax   : ℝ
 157  chi2Max : ℝ
 158  deriving Repr
 159
 160structure Dataset where
 161  leptons : List SpeciesEntry