pith. machine review for the scientific record. sign in
theorem proved tactic proof

V_reciprocal_symm

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  69theorem V_reciprocal_symm {phi_inf : ℝ} (h : -1 < phi_inf) :
  70    V phi_inf = V ((1 + phi_inf)⁻¹ - 1) := by

proof body

Tactic-mode proof.

  71  unfold V
  72  have h_arg_pos : (0 : ℝ) < 1 + phi_inf := by linarith
  73  have h_eq : 1 + ((1 + phi_inf)⁻¹ - 1) = (1 + phi_inf)⁻¹ := by ring
  74  rw [h_eq]
  75  exact Cost.Jcost_symm h_arg_pos
  76
  77/-- The squared-form expression for `V`:
  78`V(φ_inf) = φ_inf² / (2 (1 + φ_inf))`. Standard quadratic potential
  79near the vacuum, deviates at large displacement. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.