Finite real-cutoff carriers for Northcott functions

This file packages the finite carrier selected by a real cutoff for a natural-valued Northcott function, together with generic summatory functions over that carrier. The carrier depends only on the integer part of the cutoff, and for a nonnegative cutoff it agrees with the one selected by its natural floor.

theorem TauCeti.finite_setOf_natCast_le {ι : Type u_1} (N : ι → ℕ) [Northcott N] (x : ℝ) : {i : ι | ↑(N i) ≤ x}.Finite

Only finitely many indices have N-value at most a fixed real number, because the N-value is a natural number and N is Northcott.

noncomputable def TauCeti.normLE {ι : Type u_1} (N : ι → ℕ) [Northcott N] (x : ℝ) : Finset ι

The finite set of indices whose N-value is at most the real cutoff x. The cutoff is inclusive: an index with N i = x belongs to normLE N x.

Equations

• TauCeti.normLE N x = ⋯.toFinset

@[simp]

theorem TauCeti.mem_normLE {ι : Type u_1} (N : ι → ℕ) [Northcott N] {i : ι} {x : ℝ} : i ∈ normLE N x ↔ ↑(N i) ≤ x

An index belongs to normLE N x exactly when its N-value is at most the inclusive real cutoff x.

@[simp]

theorem TauCeti.coe_normLE {ι : Type u_1} (N : ι → ℕ) [Northcott N] (x : ℝ) : ↑(normLE N x) = {i : ι | ↑(N i) ≤ x}

theorem TauCeti.Nat.card_coe_normLE {ι : Type u_1} (N : ι → ℕ) [Northcott N] (x : ℝ) : Nat.card { i : ι // ↑(N i) ≤ x } = (normLE N x).card

The cardinality of the cutoff subtype agrees with that of its finite carrier.

theorem TauCeti.normLE_mono {ι : Type u_1} (N : ι → ℕ) [Northcott N] : Monotone (normLE N)

Increasing the real cutoff can only enlarge the finite carrier.

theorem TauCeti.tendsto_normLE_atTop {ι : Type u_1} (N : ι → ℕ) [Northcott N] : Filter.Tendsto (normLE N) Filter.atTop Filter.atTop

The finite carriers exhaust the index type as the cutoff grows: every finite set of indices is eventually contained in normLE N x.

theorem TauCeti.mem_normLE_natCast {ι : Type u_1} (N : ι → ℕ) [Northcott N] {i : ι} {n : ℕ} : i ∈ normLE N ↑n ↔ N i ≤ n

Membership in a carrier with natural cutoff is the plain inequality of natural numbers.

theorem TauCeti.normLE_eq_normLE_natFloor {ι : Type u_1} (N : ι → ℕ) [Northcott N] {x : ℝ} (hx : 0 ≤ x) : normLE N x = normLE N ↑⌊x⌋₊

A nonnegative real cutoff and its floor select the same indices; this is the promised conversion between the real and the natural cutoff conventions. Nonnegativity is needed: for x < 0 the floor is 0, which still admits an index of N-value 0.

theorem TauCeti.normLE_eq_normLE_of_floor_eq {ι : Type u_1} (N : ι → ℕ) [Northcott N] {x y : ℝ} (h : ⌊x⌋ = ⌊y⌋) : normLE N x = normLE N y

The inclusive carrier cut off at x depends only on the integer part of x.

theorem TauCeti.normLE_eq_empty_of_lt {ι : Type u_1} (N : ι → ℕ) [Northcott N] {b x : ℝ} (hb : ∀ (i : ι), b ≤ ↑(N i)) (hx : x < b) : normLE N x = ∅

Below a uniform lower bound for the N-values the carrier is empty.

Generic summatory functions

noncomputable def TauCeti.summatory {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommMonoid M] (w : ι → M) (x : ℝ) : M

The inclusive summatory function of a weight w: the sum of w over all indices of N-value at most x.

Equations

• TauCeti.summatory N w x = ∑ i ∈ TauCeti.normLE N x, w i

theorem TauCeti.summatory_apply {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommMonoid M] (w : ι → M) (x : ℝ) : summatory N w x = ∑ i ∈ normLE N x, w i

Evaluating summatory N w at x gives the finite sum of w over normLE N x.

@[simp]

theorem TauCeti.summatory_zero {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommMonoid M] (x : ℝ) : summatory N 0 x = 0

theorem TauCeti.summatory_add {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommMonoid M] (w₁ w₂ : ι → M) (x : ℝ) : summatory N (w₁ + w₂) x = summatory N w₁ x + summatory N w₂ x

Summation distributes over pointwise addition of weights.

theorem TauCeti.summatory_sub {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [SubtractionCommMonoid M] (w₁ w₂ : ι → M) (x : ℝ) : summatory N (w₁ - w₂) x = summatory N w₁ x - summatory N w₂ x

Summation distributes over pointwise subtraction of weights.

theorem TauCeti.summatory_const_mul {ι : Type u_1} (N : ι → ℕ) [Northcott N] (c : ℝ) (w : ι → ℝ) (x : ℝ) : summatory N (fun (i : ι) => c * w i) x = c * summatory N w x

A real scalar can be pulled out of a summatory function.

theorem TauCeti.summatory_eq_zero_of_lt {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommMonoid M] {b x : ℝ} (hb : ∀ (i : ι), b ≤ ↑(N i)) (hx : x < b) (w : ι → M) : summatory N w x = 0

Below a uniform lower bound for the N-values every summatory function vanishes.

theorem TauCeti.summatory_eq_summatory_natFloor {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommMonoid M] (w : ι → M) {x : ℝ} (hx : 0 ≤ x) : summatory N w x = summatory N w ↑⌊x⌋₊

For a nonnegative cutoff, a summatory function has the same value at the cutoff and at its natural floor.

theorem TauCeti.summatory_sub_summatory_eq_sum_filter {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommGroup M] (w : ι → M) {a b : ℝ} (hab : a ≤ b) : summatory N w b - summatory N w a = ∑ i ∈ normLE N b with a < ↑(N i), w i

Between two cutoffs a ≤ b, the difference of the values of a summatory function is the total weight of the indices of N-value in (a, b].

theorem TauCeti.summatory_nonneg {ι : Type u_1} (N : ι → ℕ) [Northcott N] {w : ι → ℝ} (hw : ∀ (i : ι), 0 ≤ w i) (x : ℝ) : 0 ≤ summatory N w x

The summatory function of a pointwise nonnegative real weight is nonnegative.

theorem TauCeti.summatory_le_summatory {ι : Type u_1} (N : ι → ℕ) [Northcott N] {w₁ w₂ : ι → ℝ} (h : ∀ (i : ι), w₁ i ≤ w₂ i) (x : ℝ) : summatory N w₁ x ≤ summatory N w₂ x

Pointwise comparison of real weights gives the same comparison of their summatory functions.

theorem TauCeti.summatory_mono {ι : Type u_1} (N : ι → ℕ) [Northcott N] {w : ι → ℝ} (hw : ∀ (i : ι), 0 ≤ w i) : Monotone (summatory N w)

A summatory function with nonnegative real weight is monotone in the cutoff.

theorem TauCeti.continuousWithinAt_summatory_Ici {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] (w : ι → M) (x : ℝ) : ContinuousWithinAt (summatory N w) (Set.Ici x) x

A summatory function is continuous from the right: it is constant on each interval [n, n + 1) with n an integer, because the cutoff is inclusive.

theorem TauCeti.eventually_summatory_sub_eq {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommGroup M] (w₁ w₂ : ι → M) (u : Finset ι) (h : ∀ i ∉ u, w₁ i = w₂ i) : ∀ᶠ (x : ℝ) in Filter.atTop, summatory N w₁ x - summatory N w₂ x = ∑ i ∈ u, (w₁ i - w₂ i)

Changing a weight on a finite set of indices changes the summatory function, for all large cutoffs, by the constant total discrepancy over that set.

theorem TauCeti.eventually_summatory_eq_sum {ι : Type u_1} (N : ι → ℕ) [Northcott N] {M : Type u_2} [AddCommMonoid M] (w : ι → M) (u : Finset ι) (h : ∀ i ∉ u, w i = 0) : ∀ᶠ (x : ℝ) in Filter.atTop, summatory N w x = ∑ i ∈ u, w i

A weight vanishing outside a finite set has eventually constant summatory function, equal to its total sum.

theorem TauCeti.eventually_summatory_indicator_sub_eq {ι : Type u_1} (N : ι → ℕ) [Northcott N] (w : ι → ℝ) {S T : Set ι} (hST : (symmDiff S T).Finite) : ∀ᶠ (x : ℝ) in Filter.atTop, summatory N (S.indicator w) x - summatory N (T.indicator w) x = ∑ i ∈ hST.toFinset, (S.indicator w i - T.indicator w i)

If two sets have finite symmetric difference, their indicator-weighted summatory functions have eventually constant difference.