Documentation

Formalizations.NumberTheory.WeightedCharacterSums.SubsetSumsAndRows

Intervals of subset sums and the parity of a signed half sum #

Two small statements on weighted sums of a sign sequence: how an interval of subset sums grows when an element is adjoined, and the parity of ∑_{c ≤ m} c ε(c) for a sequence of signs.

Main results #

References #

lem:intervalos (a) #

source
@[reducible, inline]
abbrev IntervalosFilas.SS (A : Finset ℕ) :
Finset ℕ

Σ(A): the set of subset sums of a finite set A ⊆ ℕ.

Equations
Instances For
    source
    theorem IntervalosFilas.mem_SS {A : Finset ℕ} {y : ℕ} :
    y ∈ SS A ↔ ∃ B ⊆ A, ∑ b ∈ B, b = y
    source
    theorem IntervalosFilas.SS_mono {A A' : Finset ℕ} (h : A ⊆ A') {y : ℕ} (hy : y ∈ SS A) :
    y ∈ SS A'
    source
    theorem IntervalosFilas.intervalos_a {A : Finset ℕ} {α β x : ℕ} (hA : ∀ y ∈ Finset.Icc α β, y ∈ SS A) (hx : x ∉ A) (_hx0 : 0 < x) (hxb : x + α ≤ β + 1) (y : ℕ) :
    y ∈ Finset.Icc α (β + x) → y ∈ SS (insert x A)

    lem:intervalos (a), first sentence. If Σ(A) ⊇ [α, β], x ∉ A and 0 < x ≤ β − α + 1, then Σ(A ∪ {x}) ⊇ [α, β + x].

    source
    theorem IntervalosFilas.SS_symm {A : Finset ℕ} {y : ℕ} (hy : y ∈ SS A) :
    y ≤ ∑ a ∈ A, a ∧ ∑ a ∈ A, a - y ∈ SS A

    lem:intervalos (a): "Σ(A) is symmetric under x ↦ P_A − x", P_A = ∑_{a∈A} a.

    source
    theorem IntervalosFilas.intervalos_a_sym {A : Finset ℕ} {α β : ℕ} (hA : ∀ y ∈ Finset.Icc α β, y ∈ SS A) (hβ : ∑ a ∈ A, a ≤ 2 * β) (y : ℕ) :
    y ∈ Finset.Icc α (∑ a ∈ A, a - α) → y ∈ SS A

    lem:intervalos (a), second sentence. Σ(A) ⊇ [α, β] with β ≥ P_A/2 implies Σ(A) ⊇ [α, P_A − α].

    prop:filas #

    source
    theorem IntervalosFilas.two_mul_sum_id (m : ℕ) :
    2 * ∑ c ∈ Finset.Icc 1 m, ↑c = ↑m * (↑m + 1)

    ∑_{c=1}^{m} c = m(m+1)/2, in the form 2 ∑ c = m(m+1).

    source
    theorem IntervalosFilas.eighth (m : ℕ) :
    (↑(2 * m + 1) ^ 2 - 1) / 8 = ∑ c ∈ Finset.Icc 1 m, ↑c

    (n² − 1)/8 = m(m+1)/2 for n = 2m+1.

    source
    theorem IntervalosFilas.filas_parity (m : ℕ) (ε : ℕ → ℤ) (hε : ∀ c ∈ Finset.Icc 1 m, ε c = 1 ∨ ε c = -1) :
    ∑ c ∈ Finset.Icc 1 m, ↑c * ε c ≡ (↑(2 * m + 1) ^ 2 - 1) / 8 [ZMOD 2]

    prop:filas, the congruence. For n = 2m+1 and any ε with values ±1 on 1, …, m, ∑_{c=1}^{m} c ε(c) ≡ (n² − 1)/8 (mod 2).

    source
    theorem IntervalosFilas.even_eighth_iff (m : ℕ) :
    2 ∣ ∑ c ∈ Finset.Icc 1 m, ↑c ↔ (2 * m + 1) % 8 = 1 ∨ (2 * m + 1) % 8 = 7

    (n² − 1)/8 even, for n = 2m+1, iff n ≡ ±1 (mod 8).

    source
    theorem IntervalosFilas.filas_vanish (m : ℕ) (ε : ℕ → ℤ) (hε : ∀ c ∈ Finset.Icc 1 m, ε c = 1 ∨ ε c = -1) (h0 : ∑ c ∈ Finset.Icc 1 m, ↑c * ε c = 0) :
    jacobiSym 2 (2 * m + 1) = 1

    prop:filas, "so it can vanish only if (2/n) = 1" (Jacobi symbol, n = 2m+1), through the second supplementary law J(2 | n) = χ₈(n) (jacobiSym.at_two).

    source
    def IntervalosFilas.T {f : ℕ} (m : ℕ) (χ : MulChar (ZMod f) ℤ) :
    ℤ

    T(m, χ) = ∑_{c=1}^{m} c χ(c) for a character χ modulo f.

    Equations
    Instances For
      source
      theorem IntervalosFilas.quad_unit {f c : ℕ} (χ : MulChar (ZMod f) ℤ) (hχ : χ.IsQuadratic) (hc : c.Coprime f) :
      χ ↑c = 1 ∨ χ ↑c = -1

      A quadratic character takes the values ±1 at the residues prime to its modulus.

      source
      theorem IntervalosFilas.filas_char {f m : ℕ} (χ : MulChar (ZMod f) ℤ) (hχ : χ.IsQuadratic) (hf : f.Coprime m.factorial) (h0 : T m χ = 0) :
      jacobiSym 2 (2 * m + 1) = 1

      prop:filas, "In particular". If χ is a quadratic character modulo f with gcd(f, m!) = 1, then T(m, χ) = 0 forces (2/n) = 1, n = 2m+1. (Primitivity is not used.)

      Controls #