OAI/NumberTheory/JointDickman/Arithmetic/SeparatedHarmonicKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Harmonic-decay kernels on separated samples

  1. lemma OAI.JointDickman.interval_sample_card line 11
  2. lemma OAI.JointDickman.absolute_sample_card line 23
  3. theorem OAI.JointDickman.separated_harmonic_kernel_sum line 42

    Source documentation

    Harmonic row sums grow only logarithmically with the diameter of the sample set. The proof uses at most two points in each absolute unit band.

    theorem separated_harmonic_kernel_sum (S : Finset ℝ)
    (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x-y|)
    (t T : ℝ) (hT : 0 ≤ T) (hdiam : ∀ u ∈ S, |t-u| ≤ T) :
    (∑ u ∈ S, 1/(1+|t-u|)) ≤ 2*(1+Real.log (T+1)) := by
…