schnirelmannDensity_eq_zero_of_one_not_mem
theorem schnirelmannDensity_eq_zero_of_one_not_mem :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], 1 ∉ A → schnirelmannDensity A = 0
This theorem states that the Schnirelmann density of a set, which does not include the natural number `1`, is `0`. The Schnirelmann density is a concept in number theory, defined as the infimum of the ratio of the cardinality of intersection of set `A` and the set of natural numbers from `1` to `n`, to `n`, where `n` ranges over all positive natural numbers. In simpler terms, if a set of natural numbers doesn't include `1`, when we calculate the Schnirelmann density (which includes counting the number of elements shared with the set `{1, ..., n}` for each `n`), the result will always be `0`.
More concisely: The Schnirelmann density of a set without the natural number 1 is 0.
|
schnirelmannDensity_setOf_mod_eq_one
theorem schnirelmannDensity_setOf_mod_eq_one : ∀ {m : ℕ}, m ≠ 1 → schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹ := by
sorry
The theorem `schnirelmannDensity_setOf_mod_eq_one` states that for any natural number `m` not equal to 1, the Schnirelmann density of the set of natural numbers which are congruent to 1 modulo `m` is `1/m` (the reciprocal of `m`). It should be noted that if `m` is equal to 1, this set is empty. The Schnirelmann density here is computed as the infimum (greatest lower bound) of the ratio of the size of the intersection of set `A` and the set `{1, ..., n}` to `n`, as `n` ranges over the positive natural numbers.
More concisely: For any natural number `m` non-equal to 1, the Schnirelmann density of the set of numbers congruent to 1 modulo `m` is `1/m`.
|
schnirelmannDensity_finite
theorem schnirelmannDensity_finite :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], A.Finite → schnirelmannDensity A = 0
The theorem states that the Schnirelmann density of any finite set of natural numbers is `0`. In other words, for any finite set `A` of natural numbers, where it is decidable whether a given natural number `x` belongs to `A` or not, it is the case that the Schnirelmann density of `A` equals `0`. The Schnirelmann density is calculated as the infimum (greatest lower bound) of the ratio of the cardinality of the intersection of `A` with the set `{1, ..., n}` to `n`, as `n` ranges over the positive natural numbers.
More concisely: The Schnirelmann density of any finite set of natural numbers is 0.
|
schnirelmannDensity_mul_le_card_filter
theorem schnirelmannDensity_mul_le_card_filter :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {n : ℕ},
schnirelmannDensity A * ↑n ≤ ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card
The theorem `schnirelmannDensity_mul_le_card_filter` states that, for any set `A` of natural numbers and a given natural number `n`, the Schnirelmann density of the set `A` multiplied by `n` is less than or equal to the cardinality of the intersection of `A` and the interval `{1, ..., n}`. Notably, this property does not hold for the natural density. In other words, the Schnirelmann density, which quantifies the average presence of elements of a set `A` inside the initial segments of natural numbers, times `n`, is always bounded by the actual number of elements of `A` in the first `n` numbers.
More concisely: For any set A of natural numbers and natural number n, the Schnirelmann density of A multiplied by n is bounded above by the cardinality of A's intersection with {1, ..., n}.
|
schnirelmannDensity_insert_zero
theorem schnirelmannDensity_insert_zero :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] [inst_1 : DecidablePred fun x => x ∈ insert 0 A],
schnirelmannDensity (insert 0 A) = schnirelmannDensity A
This theorem states that the Schnirelmann density of a set of natural numbers is not changed by adding the element `0`. The Schnirelmann density, represented mathematically as the infimum of the ratio of the size of intersection of set `A` and the set `{1, ..., n}` to `n` over all positive natural numbers `n`, remains the same whether or not `0` is included in the set `A`. This is true for all sets `A` of natural numbers where it is decidable whether a given natural number is in `A` or in `A` with `0` added.
More concisely: The Schnirelmann density of a decidable subset of natural numbers is unchanged by adding or removing 0.
|
exists_of_schnirelmannDensity_eq_zero
theorem exists_of_schnirelmannDensity_eq_zero :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {ε : ℝ},
0 < ε →
schnirelmannDensity A = 0 → ∃ n, 0 < n ∧ ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card / ↑n < ε
The theorem `exists_of_schnirelmannDensity_eq_zero` states that if we have a set `A` of natural numbers and the Schnirelmann density of this set is `0`, then for any given positive real number `ε`, there exists a positive natural number `n` such that the proportion of elements in `A` which are less than or equal to `n` is less than `ε`. The Schnirelmann density is defined as the infimum over all natural numbers `n` of the proportion of elements in `A` that are less than or equal to `n`. Note that this statement cannot be strengthened to hold eventually for all `n` beyond some point, as can be illustrated by the counterexample where `A` is the complement of the set containing just `1`.
More concisely: Given a set of natural numbers `A` with Schnirelmann density 0, for any positive real `ε`, there exists a natural number `n` such that the proportion of elements in `A` less than or equal to `n` is less than `ε`.
|
schnirelmannDensity_eq_one_iff
theorem schnirelmannDensity_eq_one_iff :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A
The theorem `schnirelmannDensity_eq_one_iff` states that for any set `A` of natural numbers, the Schnirelmann density of `A` is equal to `1` if and only if `A` contains all positive natural numbers. In other words, it means that the Schnirelmann density of a set of natural numbers is `1` precisely when this set includes all numbers greater than `0`. The Schnirelmann density of a set is defined as the infimum of the ratio of the cardinality of the intersection of the set with the set of first `n` natural numbers to `n`, as `n` ranges over all positive natural numbers. The theorem sets a condition on this density measure to be `1`, signifying that the set is as large as the set of all positive natural numbers in terms of the Schnirelmann density.
More concisely: A set of natural numbers has Schnirelmann density equal to 1 if and only if it contains all positive natural numbers.
|
schnirelmannDensity_le_of_not_mem
theorem schnirelmannDensity_le_of_not_mem :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {k : ℕ}, k ∉ A → schnirelmannDensity A ≤ 1 - (↑k)⁻¹
The theorem `schnirelmannDensity_le_of_not_mem` states that for any set `A` of natural numbers, and any natural number `k` not in `A`, the Schnirelmann density of `A` is less than or equal to `1 - 1/k`. The Schnirelmann density is a measure of the size of a set of natural numbers, defined as the infimum over all positive integers `n` of the ratio of the size of the intersection of `A` and the set `{1, ..., n}` to `n`. The theorem asserts that if a natural number `k` is not in the set `A`, it imposes an upper bound on the Schnirelmann density of `A`, which is `1 - 1/k`.
More concisely: For any set of natural numbers `A` and any natural number `k not in A`, the Schnirelmann density of `A` is bounded above by `1 - 1/k`.
|
schnirelmannDensity_finset
theorem schnirelmannDensity_finset : ∀ (A : Finset ℕ), schnirelmannDensity ↑A = 0
The theorem states that the Schnirelmann density of any finite set of natural numbers (also known as finset) is `0`. In mathematical terms, the Schnirelmann density, which is calculated as the infimum of the ratio of the size of the intersection of set `A` with the set of natural numbers from `1` to `n`, to `n`, for all positive natural numbers `n`, always equals zero for any finite set of natural numbers.
More concisely: The Schnirelmann density of any finite set of natural numbers is 0.
|
schnirelmannDensity_congr'
theorem schnirelmannDensity_congr' :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {B : Set ℕ} [inst_1 : DecidablePred fun x => x ∈ B],
(∀ n > 0, n ∈ A ↔ n ∈ B) → schnirelmannDensity A = schnirelmannDensity B
This theorem states that if two sets of natural numbers, A and B, have the property that for every natural number greater than 0, that number is in A if and only if it is in B, then the Schnirelmann density of A is equal to the Schnirelmann density of B. The Schnirelmann density is defined as the infimum of the ratio of the size of the intersection of the set with the set of natural numbers from 1 through n and n itself, as n ranges over the positive naturals. Both sets, A and B, are assumed to have a decidable predicate, meaning it can be determined whether or not an element belongs to the set.
More concisely: If sets A and B of natural numbers have the same element-wise property that every number greater than 0 is in A if and only if it is in B, then they have equal Schnirelmann densities.
|
schnirelmannDensity_le_of_subset
theorem schnirelmannDensity_le_of_subset :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {B : Set ℕ} [inst_1 : DecidablePred fun x => x ∈ B],
A ⊆ B → schnirelmannDensity A ≤ schnirelmannDensity B
The theorem `schnirelmannDensity_le_of_subset` states that for any two sets of natural numbers `A` and `B`, given that the membership of elements in `A` and `B` is decidable, if `A` is a subset of `B` then the Schnirelmann density of `A` is less than or equal to the Schnirelmann density of `B`. The Schnirelmann density of a set `A` is defined as the infimum of the cardinality of the intersection of `A` and the set `{1, ..., n}` divided by `n`, as `n` ranges over the positive naturals.
More concisely: For decidably membership-testable sets `A` and `B` of natural numbers with `A` being a subset of `B`, the Schnirelmann density of `A` is less than or equal to that of `B`.
|
schnirelmannDensity_diff_singleton_zero
theorem schnirelmannDensity_diff_singleton_zero :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] [inst_1 : DecidablePred fun x => x ∈ A \ {0}],
schnirelmannDensity (A \ {0}) = schnirelmannDensity A
This theorem states that the Schnirelmann density of a set of natural numbers is unaffected by the removal of the element `0`. In other words, for any set `A` of natural numbers, the Schnirelmann density of `A` and the Schnirelmann density of `A` without `0` are equal. The Schnirelmann density, defined as the infimum of the ratio of the cardinality of the intersection of `A` with the set `{1, ..., n}` to `n` as `n` ranges over the positive natural numbers, remains the same even if `0` is removed from set `A`. The predicates for membership in `A` and `A` without `0` are assumed to be decidable.
More concisely: The Schnirelmann density of a set without the element 0 is equal to that of the original set.
|
schnirelmannDensity_le_of_le
theorem schnirelmannDensity_le_of_le :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {x : ℝ} (n : ℕ),
n ≠ 0 → ↑(Finset.filter (fun x => x ∈ A) (Finset.Ioc 0 n)).card / ↑n ≤ x → schnirelmannDensity A ≤ x
This theorem states that to prove the Schnirelmann density of a set of natural numbers `A` is less than or equal to a real number `x`, it is enough to demonstrate that the ratio of the cardinality of the intersection of `A` and the set of natural numbers from `1` to `n`, over `n`, is less than or equal to `x`, for any chosen positive natural number `n`. The theorem takes `n` as an explicit argument which makes it easier to use in `apply` or `refine`. This theorem is similar to `ciInf_le_of_le`.
More concisely: To prove the Schnirelmann density of a set of natural numbers is less than or equal to a real number, it suffices to show that the ratio of the set's intersection with the first `n` natural numbers to `n` is less than or equal to the real number, for any `n`.
|
schnirelmannDensity_eq_one_iff_of_zero_mem
theorem schnirelmannDensity_eq_one_iff_of_zero_mem :
∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A], 0 ∈ A → (schnirelmannDensity A = 1 ↔ A = Set.univ)
The theorem states that for any set `A` of natural numbers, with the property that `0` is an element of `A` and the membership of `A` is decidable, the Schnirelmann density of `A` is equal to `1` if and only if `A` consists of all natural numbers. In other words, the Schnirelmann density, which is the infimum of the ratio of the size of the intersection of `A` and the set `{1, ..., n}` to `n` as `n` ranges over the positive natural numbers, will only equal `1` if the set `A` is the set of all natural numbers i.e., the universal set.
More concisely: The Schnirelmann density of a decidably-membership set `A` containing `0` equals `1` if and only if `A` is the set of all natural numbers.
|