OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingTwoAnnuli.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform positive displacement at one of two annular returns

The normalized profile is the actual matrix profile. Consequently the two-scale cancellation estimate gives a positive lower bound independent of the return matrix, while the scale bound controls every intervening shearing parameter.

  1. theorem OAI.DukePrimeDegree.rootShearSize_two_scales_lower line 21
  2. theorem OAI.DukePrimeDegree.rootShearSize_bound_on_symmetric_interval line 47