Elementary facts about dslope

Divided-slope facts that need no differentiability, collected for the Schwarz-lemma consumers. Away from its base point dslope is the plain difference quotient, so these are statements about a normed field and its norm, with no calculus in them.

Main results

• TauCeti.norm_dslope_eq_one_of_norm_sub_map_eq: a map that moves two points exactly as far apart as they already are has unimodular difference quotient between them. This is the hypothesis the equality case of Schwarz's lemma (Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div) takes, and the two Tau Ceti consumers of that equality case — the Schwarz--Pick rigidity theorem and the classification of the disc rotations — reach it by exactly this route, at base point 0.

theorem TauCeti.norm_dslope_eq_one_of_norm_sub_map_eq {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {x y : 𝕜} (hxy : y ≠ x) (hnorm : ‖g y - g x‖ = ‖y - x‖) : ‖dslope g x y‖ = 1

A map preserving the distance between two points has unit difference quotient between them. For y ≠ x with ‖g y - g x‖ = ‖y - x‖, the difference quotient dslope g x y is unimodular.

No differentiability is involved: away from the base point dslope is the plain difference quotient.