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

recoverEps_conformal

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)

  78theorem recoverEps_conformal {n : ℕ} (a : ℝ) (ha : 0 < a)
  79    (ε : LogPotential n) (i : Fin n) :
  80    recoverEps (conformal_edge_length_field a ha ε) i = ε i := by

proof body

Tactic-mode proof.

  81  unfold recoverEps conformal_edge_length_field
  82  simp only
  83  have h_a_ne : a ≠ 0 := ne_of_gt ha
  84  have h_exp_arg : (ε i + ε i) / 2 = ε i := by ring
  85  rw [h_exp_arg]
  86  rw [mul_div_cancel_left₀ (Real.exp (ε i)) h_a_ne]
  87  exact Real.log_exp _
  88
  89/-! ## §2. A single-edge hinge datum -/
  90
  91/-- Build a hinge datum carrying a single ordered edge and its weight. -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.