CountMaskDistance.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Upper distance cost of the reciprocal-count soft masks

theorem OAI.JointDickman.count_mask_distance_zero_le line 13

Source documentation

Softening finitely many prime values increases distance to the constant-one function by at most their reciprocal mass.

theorem count_mask_distance_zero_le (F : ℕ → ℂ) (hF : OneBounded F)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) {u : ℝ}
    (hu : 0 ≤ u) (hu1 : u ≤ 1) (N : ℕ) :
    squaredDistance (mrtCountMaskedCoefficient F P u) (mrtArchimedeanTwist 0) N ≤
      squaredDistance F (mrtArchimedeanTwist 0) N + ∑ p ∈ P, 1/(p:ℝ) := by
…