OAI/NumberTheory/JointDickman/Amplification/MovingLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

From rational fixed thresholds to the manuscript's main limit

Rational approximation compares fixed-scale thresholds with moving thresholds and extends the counting limit to real endpoints.

  1. def OAI.JointDickman.fixedDensity line 21
  2. def OAI.JointDickman.RationalFixedScaleLaw line 25

    Source documentation

    The joint limit for rational fixed-scale thresholds.

    def RationalFixedScaleLaw : Prop :=
…
  3. theorem OAI.JointDickman.tendsto_of_approximating_bounds line 29
  4. theorem OAI.JointDickman.fixedDensity_le_moving_add line 48
  5. theorem OAI.JointDickman.movingDensity_le_fixed line 67
  6. theorem OAI.JointDickman.jointDickmanLaw_of_rational_fixedScale line 76

    Source documentation

    The rational fixed-scale law implies the moving-threshold joint law at every real counting endpoint.

    theorem jointDickmanLaw_of_rational_fixedScale (hfixed : RationalFixedScaleLaw) :
    JointDickmanLaw := by
…

    Mentions: OAI.JointDickman.RationalFixedScaleLaw, OAI.JointDickman.JointDickmanLaw