def
definition
Delta_0_entry
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.PDG.Fits on GitHub at line 123.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
120@[simp] def n_entry : SpeciesEntry := { name := "n", mass_obs := 0.9395654133, sigma := 1e-6, mass_pred := 0.9395654133 }
121@[simp] def Delta_pp_entry : SpeciesEntry := { name := "Delta_pp", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
122@[simp] def Delta_p_entry : SpeciesEntry := { name := "Delta_p", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
123@[simp] def Delta_0_entry : SpeciesEntry := { name := "Delta_0", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
124@[simp] def Delta_m_entry : SpeciesEntry := { name := "Delta_m", mass_obs := 1.232, sigma := 0.005, mass_pred := 1.232 }
125
126@[simp] def baryonsWitness : List SpeciesEntry :=
127 [p_entry, n_entry, Delta_pp_entry, Delta_p_entry, Delta_0_entry, Delta_m_entry]
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. -/