OAI/NumberTheory/JointDickman/Amplification/CellAverageProfile.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lipschitz control of normalized cell integrals

  1. theorem OAI.JointDickman.cellAverage_profile_error line 12
  2. theorem OAI.JointDickman.normalizedCell_profile_error line 37

    Source documentation

    Normalize the probability error by the actual cell mass, then add only the Lipschitz oscillation across that cell.

    theorem normalizedCell_profile_error {f : ℝ → ℝ} {L : ℝ≥0} (hLip : LipschitzWith L f)
    {a b P φ ε : ℝ} (hab : a < b) (hφ : 0 < φ) (t : ℝ)
    (hlocal : |P - (∫ x in a..b, f (x - t)) / φ| ≤ ε) :
    |P / ((b - a) / φ) - f (a - t)| ≤ ε / ((b - a) / φ) + L * (b - a) := by
…