OAI/NumberTheory/JointDickman/Amplification/MinorArcApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reduced rational approximation outside the major arcs

  1. def OAI.JointDickman.InRationalArc line 12

    Source documentation

    Real representatives of the rational arcs; translating a numerator by an integer retains the corresponding arc on the unit circle.

    def InRationalArc (θ Q δ : ℝ) : Prop :=
…
  2. theorem OAI.JointDickman.minorArc_rational_approximation line 15