Documentation

LeanPool.Komlos.Tent

The discrete tent function #

Adapted for Lean Pool by changing module paths, selecting explicit imports, and simplifying the polynomial arithmetic in the tent-sum identities.

Komlos.tent M j = max (M - |j|) 0 is the tent of half-width M on ℤ. Its square, after normalisation, gives the one-dimensional probability weights used in Komlos.Grid.

The file computes ∑ j, tent M j ^ 2 and proves ∑ j ∈ s, (tent M j - tent M (j - m)) ^ 2 ≤ 2 * M * m ^ 2. The latter follows by expressing a shift as a sum of one-step differences and applying Cauchy–Schwarz.

source
noncomputable def Komlos.tent (M : ℕ) (j : ℤ) :
ℝ

The discrete tent function of half-width M.

Equations
Instances For
    source
    theorem Komlos.tent_nonneg (M : ℕ) (j : ℤ) :
    0 ≤ tent M j
    source
    @[simp]
    theorem Komlos.tent_neg (M : ℕ) (j : ℤ) :
    tent M (-j) = tent M j
    source
    @[simp]
    theorem Komlos.tent_zero (M : ℕ) :
    tent M 0 = ↑M
    source
    theorem Komlos.tent_eq_zero {M : ℕ} {j : ℤ} (h : ↑M ≤ |j|) :
    tent M j = 0
    source
    theorem Komlos.tent_of_abs_le {M : ℕ} {j : ℤ} (h : |j| ≤ ↑M) :
    tent M j = ↑M - |↑j|
    source
    theorem Komlos.support_tent_subset (M : ℕ) :
    Function.support (tent M) ⊆ ↑(Finset.Icc (-↑M) ↑M)
    source
    theorem Komlos.abs_tent_sub_le (M : ℕ) (j k : ℤ) :
    |tent M j - tent M k| ≤ |↑j - ↑k|

    The tent function is 1-Lipschitz.

    source
    theorem Komlos.tent_add_one {M : ℕ} {j : ℤ} (h : |j| ≤ ↑M) :
    tent (M + 1) j = tent M j + 1
    source
    theorem Komlos.card_Icc_neg (M : ℕ) :
    (Finset.Icc (-↑M) ↑M).card = 2 * M + 1
    source
    theorem Komlos.Icc_neg_add_one (M : ℕ) :
    Finset.Icc (-(↑M + 1)) (↑M + 1) = insert (-(↑M + 1)) (insert (↑M + 1) (Finset.Icc (-↑M) ↑M))
    source
    theorem Komlos.sum_Icc_comp_tent_add_one (M : ℕ) (f : ℝ → ℝ) (hf : f 0 = 0) :
    ∑ j ∈ Finset.Icc (-(↑M + 1)) (↑M + 1), f (tent (M + 1) j) = ∑ j ∈ Finset.Icc (-↑M) ↑M, f (tent M j + 1)

    Passing from half-width M to M + 1 raises the tent by 1 on [-M, M] and adds two zero endpoints.

    source
    theorem Komlos.sum_tent (M : ℕ) :
    ∑ j ∈ Finset.Icc (-↑M) ↑M, tent M j = ↑M ^ 2
    source
    theorem Komlos.sum_tent_sq (M : ℕ) :
    (∑ j ∈ Finset.Icc (-↑M) ↑M, tent M j ^ 2) * 3 = ↑M * (2 * ↑M ^ 2 + 1)

    The sum of the squared tent values is M * (2 * M ^ 2 + 1) / 3.

    source
    noncomputable def Komlos.step (M : ℕ) (j : ℤ) :
    ℝ

    The one-step difference of the tent.

    Equations
    Instances For
      source
      theorem Komlos.abs_step_le_one (M : ℕ) (j : ℤ) :
      |step M j| ≤ 1
      source
      theorem Komlos.step_eq_zero {M : ℕ} {j : ℤ} (h : j ∉ Finset.Icc (1 - ↑M) ↑M) :
      step M j = 0
      source
      theorem Komlos.sum_step_sq_le (M : ℕ) (s : Finset ℤ) :
      ∑ j ∈ s, step M j ^ 2 ≤ 2 * ↑M

      The steps of the tent are bounded by 1 and supported on 2 * M points.

      source
      theorem Komlos.tent_sub_tent_eq_sum_step (M k : ℕ) (j : ℤ) :
      tent M j - tent M (j - ↑k) = ∑ i ∈ Finset.range k, step M (j - ↑i)
      source
      theorem Komlos.sum_tent_sub_sq_le_nat (M k : ℕ) (s : Finset ℤ) :
      ∑ j ∈ s, (tent M j - tent M (j - ↑k)) ^ 2 ≤ 2 * ↑M * ↑k ^ 2

      The squared L² distance between the tent and its translate by k : ℕ is at most 2 * M * k ^ 2.

      source
      theorem Komlos.sum_tent_sub_sq_le (M : ℕ) (m : ℤ) (s : Finset ℤ) :
      ∑ j ∈ s, (tent M j - tent M (j - m)) ^ 2 ≤ 2 * ↑M * ↑m ^ 2

      The squared L² distance between the tent and its translate by m : ℤ is at most 2 * M * m ^ 2.