OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingProfile.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A positive displacement at one of two annuli

The normalized scale consists of a fixed linear coefficient, the square root of a quadratic coefficient, and the remaining linear coefficients. The latter already give a displacement; otherwise the quadratic pivot cannot cancel at both of the chosen scales.

  1. theorem OAI.DukePrimeDegree.quadratic_two_scales_quarter line 20
  2. theorem OAI.DukePrimeDegree.shearing_profile_two_scales line 54