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

normalized_implies_G_zero

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)

 710theorem normalized_implies_G_zero (F : ℝ → ℝ) (hNorm : IsNormalized F) :
 711    G F 0 = 0 :=

proof body

Term-mode proof.

 712  G_zero_of_unit F hNorm
 713
 714/-- **Key Identity**: The composition law on F is equivalent to CoshAddIdentity on G.
 715
 716Specifically: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
 717becomes: G(s+t) + G(s-t) = 2G(s)G(t) + 2G(s) + 2G(t)
 718via the substitution x = e^s, y = e^t. -/

depends on (17)

Lean names referenced from this declaration's body.