crossSectionRatio

formal source

  28noncomputable section
  29
  30/-- The RS-predicted dark-matter cross-section ratio. -/
  31def crossSectionRatio : ℝ := Cost.Jcost phi
  32
  33/-- The cross-section ratio is strictly positive. -/
  34theorem crossSectionRatio_pos : 0 < crossSectionRatio := by
  35  unfold crossSectionRatio
  36  have hphi_ne_one : phi ≠ 1 := by
  37    intro h
  38    have hphi_gt : (1 : ℝ) < phi := by
  39      have := Constants.phi_gt_onePointFive; linarith
  40    rw [h] at hphi_gt
  41    exact lt_irrefl _ hphi_gt
  42  exact Cost.Jcost_pos_of_ne_one phi Constants.phi_pos hphi_ne_one
  43
  44/-- The cross-section ratio sits in the canonical band. -/
  45theorem crossSectionRatio_band :
  46    0.11 < crossSectionRatio ∧ crossSectionRatio < 0.13 := by
  47  unfold crossSectionRatio
  48  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  49  rw [Cost.Jcost_eq_sq hphi_ne]
  50  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  51  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  52  have hpos : (0 : ℝ) < 2 * phi := by
  53    have : (0 : ℝ) < phi := Constants.phi_pos
  54    linarith
  55  refine ⟨?lo, ?hi⟩
  56  · rw [lt_div_iff₀ hpos]
  57    nlinarith [h_lo, h_hi]
  58  · rw [div_lt_iff₀ hpos]
  59    nlinarith [h_lo, h_hi]
  60
  61/-- Detection within the predicted band of cross-section is consistent. -/