phi_suppression_bounded

proof body

Tactic-mode proof.

  70  have heq : phi_suppression_ga = phi ^ (-4.5 : ℝ) := by
  71    unfold phi_suppression_ga gallium_rung
  72    norm_num
  73  rw [heq]
  74  have h1 : phi ^ (-4.5 : ℝ) > 0 := by
  75    apply Real.rpow_pos_of_pos
  76    exact phi_pos
  77  have h2 : phi ^ (-4.5 : ℝ) < 1 := by
  78    -- phi^(-4.5) = 1/phi^4.5 and phi^4.5 > 1, so phi^(-4.5) < 1
  79    have h3 : phi ^ (-4.5 : ℝ) = 1 / (phi ^ (4.5 : ℝ)) := by
  80      rw [show (-4.5 : ℝ) = - (4.5 : ℝ) by norm_num]
  81      rw [Real.rpow_neg]
  82      · ring
  83      · exact le_of_lt phi_pos
  84    have h4 : phi ^ (4.5 : ℝ) > 1 := by
  85      -- Use the fact that phi > 1.618 > 1, so phi^4.5 > 1^4.5 = 1
  86      have hphi_gt : phi > (1.618 : ℝ) := by
  87        have h1 : phi > (1.618 : ℝ) := by
  88          have hsqrt5 : Real.sqrt 5 > (2.236 : ℝ) := by
  89            rw [show (2.236 : ℝ) = Real.sqrt (2.236^2) by rw [Real.sqrt_sq (by norm_num)]]
  90            apply Real.sqrt_lt_sqrt
  91            · norm_num
  92            · norm_num
  93          unfold phi
  94          linarith
  95        linarith
  96      have h1_pow : (1.618 : ℝ) ^ (4.5 : ℝ) > 1 := by
  97        -- 1.618^4.5 > 1 since 1.618 > 1
  98        have hbase : (1.618 : ℝ) > 1 := by norm_num
  99        have hexp_pos : (4.5 : ℝ) > 0 := by norm_num
 100        have h1_lt : (1 : ℝ) < (1.618 : ℝ) ^ (4.5 : ℝ) := by
 101          rw [← Real.one_rpow (4.5 : ℝ)]
 102          apply Real.rpow_lt_rpow
 103          · norm_num
 104          · linarith
 105          · norm_num
 106        linarith
 107      have hphi_pow : phi ^ (4.5 : ℝ) > (1.618 : ℝ) ^ (4.5 : ℝ) := by
 108        apply Real.rpow_lt_rpow
 109        · linarith
 110        · linarith
 111        · norm_num
 112      linarith [h1_pow, hphi_pow]
 113    rw [h3]
 114    have h5 : phi ^ (4.5 : ℝ) > 0 := by positivity
 115    apply (div_lt_iff₀ h5).mpr
 116    nlinarith
 117  exact ⟨h1, h2⟩
 118
 119/-! ## III. The Cross-Section Correction -/
 120
 121/-- The RS cross-section for Ga(ν,e)Ge.
 122    σ_RS = σ_SM × (57.7 / 74.0) -/