OAI/Combinatorics/SphericalRamsey/DerivationCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GrahamSpherical.derivation_rotation_coordinates line 13

   Source documentation

   Only the algebraic quotient rule is used; no continuity or differentiation of the infinite series defining the parameter is involved.

   theorem derivation_rotation_coordinates (D : Derivation ℤ ℝ ℝ) (t : ℝ)
       (ht : D t = (1 + t ^ 2) / 2) :
       D ((1 - t ^ 2) / (1 + t ^ 2)) = -(2 * t / (1 + t ^ 2)) ∧
         D (2 * t / (1 + t ^ 2)) = (1 - t ^ 2) / (1 + t ^ 2) := by
   …