potential_min_at_one

formal source

  48noncomputable def inflatonPotential (φ : ℝ) (hφ : φ > 0) : ℝ := Jcost φ
  49
  50/-- **THEOREM**: The potential has a minimum at φ = 1. -/
  51theorem potential_min_at_one (φ : ℝ) (hφ : φ > 0) :
  52    inflatonPotential φ hφ ≥ inflatonPotential 1 (by norm_num : (1 : ℝ) > 0) := by
  53  unfold inflatonPotential
  54  have h1 : Jcost 1 = 0 := Cost.Jcost_unit0
  55  rw [h1]
  56  exact Cost.Jcost_nonneg hφ
  57
  58/-- **THEOREM**: The potential is positive (except at minimum). -/
  59theorem potential_positive (φ : ℝ) (hφ : φ > 0) (hne : φ ≠ 1) :
  60    inflatonPotential φ hφ > 0 := by
  61  unfold inflatonPotential
  62  exact Cost.Jcost_pos_of_ne_one φ hφ hne
  63
  64/-! ## Slow Roll Parameters -/
  65
  66/-- First slow-roll parameter ε = (V'/V)² / 2.
  67    Inflation requires ε < 1. -/
  68noncomputable def slowRollEpsilon (φ : ℝ) (hφ : φ > 0) : ℝ :=
  69  -- V'(φ) = (1 - 1/φ²) / 2
  70  -- V(φ) = (φ + 1/φ) / 2 - 1
  71  let V := inflatonPotential φ hφ
  72  let Vp := (1 - 1/φ^2) / 2
  73  if V > 0 then (Vp / V)^2 / 2 else 0
  74
  75/-- Second slow-roll parameter η = V''/V.
  76    Inflation requires |η| < 1. -/
  77noncomputable def slowRollEta (φ : ℝ) (hφ : φ > 0) : ℝ :=
  78  -- V''(φ) = 1/φ³
  79  let V := inflatonPotential φ hφ
  80  let Vpp := 1 / φ^3
  81  if V > 0 then Vpp / V else 0