OAI/NumberTheory/JointDickman/Arithmetic/RpowTaylor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform power expansion for removing roughness

Taylor expansion is made on the fixed compact interval [0, 1/2]. Its coefficients are independent of the expansion order and of the moving logarithmic scale.

  1. def OAI.JointDickman.rpowShiftCoeff line 19
  2. theorem OAI.JointDickman.rpowShiftCoeff_zero line 23
  3. theorem OAI.JointDickman.rpowShift_contDiff line 26
  4. theorem OAI.JointDickman.rpowShift_taylor_eval line 33
  5. theorem OAI.JointDickman.rpowShift_remainder line 42
  6. theorem OAI.JointDickman.rpowShift_scaled_term line 53
  7. theorem OAI.JointDickman.rpow_scaled_remainder line 61

    Source documentation

    The power expansion with an error uniform throughout 0 ≤ v ≤ L/2. The exponent a is arbitrary; the application uses a = z - 1 - j.

    theorem rpow_scaled_remainder (a : ℝ) (H : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ L v : ℝ, 0 < L → 0 ≤ v → v ≤ L / 2 →
      |(L - v) ^ a - ∑ k ∈ range (H + 1),
        rpowShiftCoeff a k * v ^ k * L ^ (a - k)| ≤
          C * L ^ (a - (H + 1)) * v ^ (H + 1) := by
…

    Mentions: OAI.JointDickman.rpowShiftCoeff