Theory Ergodic_Theory.Asymptotic_Density
section ‹Asymptotic densities›
theory Asymptotic_Density
imports SG_Library_Complement
begin
text ‹The upper asymptotic density of a subset $A$ of the integers is
$\limsup Card(A \cap [0,n)) / n \in [0,1]$. It measures how big a set of integers is,
at some times. In this paragraph, we establish the basic properties of this notion.
There is a corresponding notion of lower asymptotic density, with a liminf instead
of a limsup, measuring how big a set is at all times. The corresponding properties
are proved exactly in the same way.
›
subsection ‹Upper asymptotic densities›
text ‹As limsups are only defined for sequences taking values in a complete lattice
(here the extended reals), we define it in the extended reals and then go back to the reals.
This is a little bit artificial, but it is not a real problem as in the applications we
will never come back to this definition.›
definition upper_asymptotic_density::"nat set ⇒ real"
where "upper_asymptotic_density A = real_of_ereal(limsup (λn. card(A ∩ {..<n})/n))"
text ‹First basic property: the asymptotic density is between $0$ and $1$.›
lemma upper_asymptotic_density_in_01:
"ereal(upper_asymptotic_density A) = limsup (λn. card(A ∩ {..<n})/n)"
"upper_asymptotic_density A ≤ 1"
"upper_asymptotic_density A ≥ 0"
proof -
{
fix n::nat assume "n>0"
have "card(A ∩ {..<n}) ≤ n" by (metis card_lessThan Int_lower2 card_mono finite_lessThan)
then have "card(A ∩ {..<n}) / n ≤ ereal 1" using ‹n>0› by auto
}
then have "eventually (λn. card(A ∩ {..<n}) / n ≤ ereal 1) sequentially"
by (simp add: eventually_at_top_dense)
then have a: "limsup (λn. card(A ∩ {..<n})/n) ≤ 1" by (simp add: Limsup_const Limsup_bounded)
have "card(A ∩ {..<n}) / n ≥ ereal 0" for n by auto
then have "liminf (λn. card(A ∩ {..<n})/n) ≥ 0" by (simp add: le_Liminf_iff less_le_trans)
then have b: "limsup (λn. card(A ∩ {..<n})/n) ≥ 0" by (meson Liminf_le_Limsup order_trans sequentially_bot)
have "abs(limsup (λn. card(A ∩ {..<n})/n)) ≠ ∞" using a b by auto
then show "ereal(upper_asymptotic_density A) = limsup (λn. card(A ∩ {..<n})/n)"
unfolding upper_asymptotic_density_def by auto
show "upper_asymptotic_density A ≤ 1" "upper_asymptotic_density A ≥ 0" unfolding upper_asymptotic_density_def
using a b by (auto simp add: real_of_ereal_le_1 real_of_ereal_pos)
qed
text ‹The two next propositions give the usable characterization of the asymptotic density, in
terms of the eventual cardinality of $A \cap [0, n)$. Note that the inequality is strict for one
implication and large for the other.›
proposition upper_asymptotic_densityD:
fixes l::real
assumes "upper_asymptotic_density A < l"
shows "eventually (λn. card(A ∩ {..<n}) < l * n) sequentially"
proof -
have "limsup (λn. card(A ∩ {..<n})/n) < l"
using assms upper_asymptotic_density_in_01(1) ereal_less_ereal_Ex by auto
then have "eventually (λn. card(A ∩ {..<n})/n < ereal l) sequentially"
using Limsup_lessD by blast
then have "eventually (λn. card(A ∩ {..<n})/n < ereal l ∧ n > 0) sequentially"
using eventually_gt_at_top eventually_conj by blast
moreover have "card(A ∩ {..<n}) < l * n" if "card(A ∩ {..<n})/n < ereal l ∧ n > 0" for n
using that by (simp add: divide_less_eq)
ultimately show "eventually (λn. card(A ∩ {..<n}) < l * n) sequentially"
by (simp add: eventually_mono)
qed
proposition upper_asymptotic_densityI:
fixes l::real
assumes "eventually (λn. card(A ∩ {..<n}) ≤ l * n) sequentially"
shows "upper_asymptotic_density A ≤ l"
proof -
have "eventually (λn. card(A ∩ {..<n}) ≤ l * n ∧ n > 0) sequentially"
using assms eventually_gt_at_top eventually_conj by blast
moreover have "card(A ∩ {..<n})/n ≤ ereal l" if "card(A ∩ {..<n}) ≤ l * n ∧ n > 0" for n
using that by (simp add: divide_le_eq)
ultimately have "eventually (λn. card(A ∩ {..<n})/n ≤ ereal l) sequentially"
by (simp add: eventually_mono)
then have "limsup (λn. card(A ∩ {..<n})/n) ≤ ereal l"
by (simp add: Limsup_bounded)
then have "ereal(upper_asymptotic_density A) ≤ ereal l"
using upper_asymptotic_density_in_01(1) by auto
then show ?thesis by (simp del: upper_asymptotic_density_in_01)
qed
text ‹The following trivial lemma is useful to control the asymptotic density of unions.›
lemma lem_ge_sum:
fixes l x y::real
assumes "l>x+y"
shows "∃lx ly. l = lx + ly ∧ lx > x ∧ ly > y"
proof -
define lx ly where "lx = x + (l-(x+y))/2" and "ly = y + (l-(x+y))/2"
have "l = lx + ly ∧ lx > x ∧ ly > y" unfolding lx_def ly_def using assms by auto
then show ?thesis by auto
qed
text ‹The asymptotic density of a union is bounded by the sum of the asymptotic densities.›
lemma upper_asymptotic_density_union:
"upper_asymptotic_density (A ∪ B) ≤ upper_asymptotic_density A + upper_asymptotic_density B"
proof -
have "upper_asymptotic_density (A ∪ B) ≤ l" if H: "l > upper_asymptotic_density A + upper_asymptotic_density B" for l
proof -
obtain lA lB where l: "l = lA+lB" and lA: "lA > upper_asymptotic_density A" and lB: "lB > upper_asymptotic_density B"
using lem_ge_sum H by blast
{
fix n assume H: "card (A ∩ {..<n}) < lA * n ∧ card (B ∩ {..<n}) < lB * n"
have "card((A∪B) ∩ {..<n}) ≤ card(A ∩ {..<n}) + card(B ∩ {..<n})"
by (simp add: card_Un_le inf_sup_distrib2)
also have "... ≤ l * n" using l H by (simp add: ring_class.ring_distribs(2))
finally have "card ((A∪B) ∩ {..<n}) ≤ l * n" by simp
}
moreover have "eventually (λn. card (A ∩ {..<n}) < lA * n ∧ card (B ∩ {..<n}) < lB * n) sequentially"
using upper_asymptotic_densityD[OF lA] upper_asymptotic_densityD[OF lB] eventually_conj by blast
ultimately have "eventually (λn. card((A∪B) ∩ {..<n}) ≤ l * n) sequentially"
by (simp add: eventually_mono)
then show "upper_asymptotic_density (A ∪ B) ≤ l" using upper_asymptotic_densityI by auto
qed
then show ?thesis by (meson dense not_le)
qed
text ‹It follows that the asymptotic density is an increasing function for inclusion.›
lemma upper_asymptotic_density_subset:
assumes "A ⊆ B"
shows "upper_asymptotic_density A ≤ upper_asymptotic_density B"
proof -
have "upper_asymptotic_density A ≤ l" if l: "l > upper_asymptotic_density B" for l
proof -
have "card(A ∩ {..<n}) ≤ card(B ∩ {..<n})" for n
using assms by (metis Int_lower2 Int_mono card_mono finite_lessThan finite_subset inf.left_idem)
then have "card(A ∩ {..<n}) ≤ l * n" if "card(B ∩ {..<n}) < l * n" for n
using that by (meson lessThan_def less_imp_le of_nat_le_iff order_trans)
moreover have "eventually (λn. card(B ∩ {..<n}) < l * n) sequentially"
using upper_asymptotic_densityD l by simp
ultimately have "eventually (λn. card(A ∩ {..<n}) ≤ l * n) sequentially"
by (simp add: eventually_mono)
then show ?thesis using upper_asymptotic_densityI by auto
qed
then show ?thesis by (meson dense not_le)
qed
text ‹If a set has a density, then it is also its asymptotic density.›
lemma upper_asymptotic_density_lim:
assumes "(λn. card(A ∩ {..<n})/n) ⇢ l"
shows "upper_asymptotic_density A = l"
proof -
have "(λn. ereal(card(A ∩ {..<n})/n)) ⇢ l" using assms by auto
then have "limsup (λn. card(A ∩ {..<n})/n) = l"
using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
then show ?thesis unfolding upper_asymptotic_density_def by auto
qed
text ‹If two sets are equal up to something small, i.e. a set with zero upper density,
then they have the same upper density.›
lemma upper_asymptotic_density_0_diff:
assumes "A ⊆ B" "upper_asymptotic_density (B-A) = 0"
shows "upper_asymptotic_density A = upper_asymptotic_density B"
proof -
have "upper_asymptotic_density B ≤ upper_asymptotic_density A + upper_asymptotic_density (B-A)"
using upper_asymptotic_density_union[of A "B-A"] by (simp add: assms(1) sup.absorb2)
then have "upper_asymptotic_density B ≤ upper_asymptotic_density A"
using assms(2) by simp
then show ?thesis using upper_asymptotic_density_subset[OF assms(1)] by simp
qed
lemma upper_asymptotic_density_0_Delta:
assumes "upper_asymptotic_density (A Δ B) = 0"
shows "upper_asymptotic_density A = upper_asymptotic_density B"
proof -
have "A- (A∩B) ⊆ A Δ B" "B- (A∩B) ⊆ A Δ B"
using assms(1) by (auto simp add: Diff_Int Un_infinite)
then have "upper_asymptotic_density (A - (A∩B)) = 0"
"upper_asymptotic_density (B - (A∩B)) = 0"
using upper_asymptotic_density_subset assms(1) upper_asymptotic_density_in_01(3)
by (metis inf.absorb_iff2 inf.orderE)+
then have "upper_asymptotic_density (A∩B) = upper_asymptotic_density A"
"upper_asymptotic_density (A∩B) = upper_asymptotic_density B"
using upper_asymptotic_density_0_diff by auto
then show ?thesis by simp
qed
text ‹Finite sets have vanishing upper asymptotic density.›
lemma upper_asymptotic_density_finite:
assumes "finite A"
shows "upper_asymptotic_density A = 0"
proof -
have "(λn. card(A ∩ {..<n})/n) ⇢ 0"
proof (rule tendsto_sandwich[where ?f = "λn. 0" and ?h = "λ(n::nat). card A / n"])
have "card(A ∩ {..<n})/n ≤ card A / n" if "n>0" for n
using that ‹finite A› by (simp add: card_mono divide_right_mono)
then show "eventually (λn. card(A ∩ {..<n})/n ≤ card A / n) sequentially"
by (simp add: eventually_at_top_dense)
have "(λn. real (card A)* (1 / real n)) ⇢ real(card A) * 0"
by (intro tendsto_intros)
then show "(λn. real (card A) / real n) ⇢ 0" by auto
qed (auto)
then show "upper_asymptotic_density A = 0" using upper_asymptotic_density_lim by auto
qed
text ‹In particular, bounded intervals have zero upper density.›
lemma upper_asymptotic_density_bdd_interval [simp]:
"upper_asymptotic_density {} = 0"
"upper_asymptotic_density {..N} = 0"
"upper_asymptotic_density {..<N} = 0"
"upper_asymptotic_density {n..N} = 0"
"upper_asymptotic_density {n..<N} = 0"
"upper_asymptotic_density {n<..N} = 0"
"upper_asymptotic_density {n<..<N} = 0"
by (auto intro!: upper_asymptotic_density_finite)
text ‹The density of a finite union is bounded by the sum of the densities.›
lemma upper_asymptotic_density_finite_Union:
assumes "finite I"
shows "upper_asymptotic_density (⋃i∈I. A i) ≤ (∑i∈I. upper_asymptotic_density (A i))"
using assms apply (induction I rule: finite_induct)
using order_trans[OF upper_asymptotic_density_union] by auto
text ‹It is sometimes useful to compute the asymptotic density by shifting a little bit the set:
this only makes a finite difference that vanishes when divided by $n$.›
lemma upper_asymptotic_density_shift:
fixes k::nat and l::int
shows "ereal(upper_asymptotic_density A) = limsup (λn. card(A ∩ {k..nat(n+l)}) / n)"
proof -
define C where "C = k+2*nat(abs(l))+1"
have *: "(λn. C*(1/n)) ⇢ real C * 0"
by (intro tendsto_intros)
have l0: "limsup (λn. C/n) = 0"
apply (rule lim_imp_Limsup, simp) using * by (simp add: zero_ereal_def)
have "card(A ∩ {k..nat(n+l)}) / n ≤ card (A ∩ {..<n})/n + C/n" for n
proof -
have "card(A ∩ {k..nat(n+l)}) ≤ card (A ∩ {..<n} ∪ {n..n + nat(abs(l))})"
by (rule card_mono, auto)
also have "... ≤ card (A ∩ {..<n}) + card {n..n + nat(abs(l))}"
by (rule card_Un_le)
also have "... ≤ card (A ∩ {..<n}) + real C"
unfolding C_def by auto
finally have "card(A ∩ {k..nat(n+l)}) / n ≤ (card (A ∩ {..<n}) + real C) /n"
by (simp add: divide_right_mono)
also have "... = card (A ∩ {..<n})/n + C/n"
using add_divide_distrib by auto
finally show ?thesis
by auto
qed
then have "limsup (λn. card(A ∩ {k..nat(n+l)}) / n) ≤ limsup (λn. card (A ∩ {..<n})/n + ereal(C/n))"
by (simp add: Limsup_mono)
also have "... ≤ limsup (λn. card (A ∩ {..<n})/n) + limsup (λn. C/n)"
by (rule ereal_limsup_add_mono)
finally have a: "limsup (λn. card(A ∩ {k..nat(n+l)}) / n) ≤ limsup (λn. card (A ∩ {..<n})/n)"
using l0 by simp
have "card (A ∩ {..<n}) / n ≤ card (A ∩ {k..nat(n+l)})/n + C/n" for n
proof -
have "card ({..<k} ∪ {n-nat(abs(l))..n + nat(abs(l))}) ≤ card {..<k} + card {n-nat(abs(l))..n + nat(abs(l))}"
by (rule card_Un_le)
also have "... ≤ k + 2*nat(abs(l)) + 1" by auto
finally have *: "card ({..<k} ∪ {n-nat(abs(l))..n + nat(abs(l))}) ≤ C" unfolding C_def by blast
have "card(A ∩ {..<n}) ≤ card (A ∩ {k..nat(n+l)} ∪ ({..<k} ∪ {n-nat(abs(l))..n + nat(abs(l))}))"
by (rule card_mono, auto)
also have "... ≤ card (A ∩ {k..nat(n+l)}) + card ({..<k} ∪ {n-nat(abs(l))..n + nat(abs(l))})"
by (rule card_Un_le)
also have "... ≤ card (A ∩ {k..nat(n+l)}) + C"
using * by auto
finally have "card (A ∩ {..<n}) / n ≤ (card (A ∩ {k..nat(n+l)}) + real C)/n"
by (simp add: divide_right_mono)
also have "... = card (A ∩ {k..nat(n+l)})/n + C/n"
using add_divide_distrib by auto
finally show ?thesis
by auto
qed
then have "limsup (λn. card(A ∩ {..<n}) / n) ≤ limsup (λn. card (A ∩ {k..nat(n+l)})/n + ereal(C/n))"
by (simp add: Limsup_mono)
also have "... ≤ limsup (λn. card (A ∩ {k..nat(n+l)})/n) + limsup (λn. C/n)"
by (rule ereal_limsup_add_mono)
finally have "limsup (λn. card(A ∩ {..<n}) / n) ≤ limsup (λn. card (A ∩ {k..nat(n+l)})/n)"
using l0 by simp
then have "limsup (λn. card(A ∩ {..<n}) / n) = limsup (λn. card (A ∩ {k..nat(n+l)})/n)"
using a by auto
then show ?thesis using upper_asymptotic_density_in_01(1) by auto
qed
text ‹Upper asymptotic density is measurable.›
lemma upper_asymptotic_density_meas [measurable]:
assumes [measurable]: "⋀(n::nat). Measurable.pred M (P n)"
shows "(λx. upper_asymptotic_density {n. P n x}) ∈ borel_measurable M"
unfolding upper_asymptotic_density_def by auto
text ‹A finite union of sets with zero upper density still has zero upper density.›
lemma upper_asymptotic_density_zero_union:
assumes "upper_asymptotic_density A = 0" "upper_asymptotic_density B = 0"
shows "upper_asymptotic_density (A ∪ B) = 0"
using upper_asymptotic_density_in_01(3)[of "A ∪ B"] upper_asymptotic_density_union[of A B] unfolding assms by auto
lemma upper_asymptotic_density_zero_finite_Union:
assumes "finite I" "⋀i. i ∈ I ⟹ upper_asymptotic_density (A i) = 0"
shows "upper_asymptotic_density (⋃i∈I. A i) = 0"
using assms by (induction rule: finite_induct, auto intro!: upper_asymptotic_density_zero_union)
text ‹The union of sets with small asymptotic densities can have a large density: think
of $A_n = [0,n]$, it has density $0$, but the union of the $A_n$ has density $1$. However, if one
only wants a set which contains each $A_n$ eventually, then one can obtain a ``union'' that has
essentially the same density as each $A_n$. This is often used as a replacement for the diagonal
argument in density arguments: if for each $n$ one can find a set $A_n$ with good properties and
a controlled density, then their ``union'' will have the same properties (eventually) and a
controlled density.›
proposition upper_asymptotic_density_incseq_Union:
assumes "⋀(n::nat). upper_asymptotic_density (A n) ≤ l" "incseq A"
shows "∃B. upper_asymptotic_density B ≤ l ∧ (∀n. ∃N. A n ∩ {N..} ⊆ B)"
proof -
have A: "∃N. ∀j ≥ N. card (A k ∩ {..<j}) < (l + (1/2)^k) * j" for k
proof -
have *: "upper_asymptotic_density (A k) < l + (1/2)^k" using assms(1)[of k]
by (metis add.right_neutral add_mono_thms_linordered_field(4) less_divide_eq_numeral1(1) mult_zero_left zero_less_one zero_less_power)
show ?thesis
using upper_asymptotic_densityD[OF *] unfolding eventually_sequentially by auto
qed
have "∃N. ∀k. (∀j ≥ N k. card (A k ∩ {..<j}) ≤ (l+(1/2)^k) * j) ∧ N (Suc k) > N k"
proof (rule dependent_nat_choice)
fix x k::nat
obtain N where N: "∀j≥N. real (card (A (Suc k) ∩ {..<j})) ≤ (l + (1 / 2) ^ Suc k) * real j"
using A[of "Suc k"] less_imp_le by auto
show "∃y. (∀j≥y. real (card (A(Suc k) ∩ {..<j})) ≤ (l + (1 / 2) ^ Suc k) * real j) ∧ x < y"
apply (rule exI[of _ "max x N + 1"]) using N by auto
next
show "∃x. ∀j≥x. real (card ((A 0) ∩ {..<j})) ≤ (l + (1 / 2) ^ 0) * real j"
using A[of 0] less_imp_le by auto
qed
text ‹Here is the choice of the good waiting function $N$›
then obtain N where N: "⋀k j. j ≥ N k ⟹ card (A k ∩ {..<j}) ≤ (l + (1/2)^k) * j" "⋀k. N (Suc k) > N k"
by blast
then have "strict_mono N" by (simp add: strict_monoI_Suc)
have Nmono: "N k < N l" if "k < l" for k l
using N(2) by (simp add: lift_Suc_mono_less that)
text ‹We can now define the global bad set $B$.›
define B where "B = (⋃k. A k ∩ {N k..})"
text ‹We will now show that it also has density at most $l$.›
have Bcard: "card (B ∩ {..<n}) ≤ (l+(1/2)^k) * n" if "N k ≤ n" "n < N (Suc k)" for n k
proof -
have "{N j..<n} = {}" if "j ∈ {k<..}" for j
using ‹n < N (Suc k)› that by (auto, meson ‹strict_mono N› less_trans not_less_eq strict_mono_less)
then have *: "(⋃j∈{k<..}. A j ∩ {N j..<n}) = {}" by force
have "B ∩ {..<n} = (⋃j. A j ∩ {N j..<n})"
unfolding B_def by auto
also have "... = (⋃j ∈ {..k}. A j ∩ {N j..<n}) ∪ (⋃j∈{k<..}. A j ∩ {N j..<n})"
unfolding UN_Un [symmetric] by (rule arg_cong [of _ _ Union]) auto
also have "... = (⋃j ∈ {..k}. A j ∩ {N j..<n})"
unfolding * by simp
also have "... ⊆ (⋃j ∈ {..k}. A k ∩ {..<n})"
using ‹incseq A› unfolding incseq_def by (auto intro!: UN_mono)
also have "... = A k ∩ {..<n}"
by simp
finally have "card (B ∩ {..<n}) ≤ card (A k ∩ {..<n})"
by (rule card_mono[rotated], auto)
then show ?thesis
using N(1)[OF ‹n ≥ N k›] by simp
qed
have "eventually (λn. card (B ∩ {..<n}) ≤ a * n) sequentially" if "l < a" for a::real
proof -
have "eventually (λk. (l+(1/2)^k) < a) sequentially"
apply (rule order_tendstoD[of _ "l+0"], intro tendsto_intros) using that by auto
then obtain k where "l + (1/2)^k < a"
unfolding eventually_sequentially by auto
have "card (B ∩ {..<n}) ≤ a * n" if "n ≥ N k + 1"for n
proof -
have "n ≥ N k" "n ≥ 1" using that by auto
have "{p. n ≥ N p} ⊆ {..n}"
using ‹strict_mono N› dual_order.trans seq_suble by blast
then have *: "finite {p. n ≥ N p}" "{p. n ≥ N p} ≠ {}"
using ‹n ≥ N k› finite_subset by auto
define m where "m = Max {p. n ≥ N p}"
have "k ≤ m"
unfolding m_def using Max_ge[OF *(1), of k] that by auto
have "N m ≤ n"
unfolding m_def using Max_in[OF *] by auto
have "Suc m ∉ {p. n ≥ N p}"
unfolding m_def using * Max_ge Suc_n_not_le_n by blast
then have "n < N (Suc m)" by simp
have "card (B ∩ {..<n}) ≤ (l+(1/2)^m) * n"
using Bcard[OF ‹N m ≤ n› ‹n < N (Suc m)›] by simp
also have "... ≤ (l + (1/2)^k) * n"
apply (rule mult_right_mono) using ‹k ≤ m› by (auto simp add: power_decreasing)
also have "... ≤ a * n"
using ‹l + (1/2)^k < a› ‹n ≥ 1› by auto
finally show ?thesis by auto
qed
then show ?thesis unfolding eventually_sequentially by auto
qed
then have "upper_asymptotic_density B ≤ a" if "a > l" for a
using upper_asymptotic_densityI that by auto
then have "upper_asymptotic_density B ≤ l"
by (meson dense not_le)
moreover have "∃N. A n ∩ {N..} ⊆ B" for n
apply (rule exI[of _ "N n"]) unfolding B_def by auto
ultimately show ?thesis by auto
qed
text ‹When the sequence of sets is not increasing, one can only obtain a set whose density
is bounded by the sum of the densities.›
proposition upper_asymptotic_density_Union:
assumes "summable (λn. upper_asymptotic_density (A n))"
shows "∃B. upper_asymptotic_density B ≤ (∑n. upper_asymptotic_density (A n)) ∧ (∀n. ∃N. A n ∩ {N..} ⊆ B)"
proof -
define C where "C = (λn. (⋃i≤n. A i))"
have C1: "incseq C"
unfolding C_def incseq_def by fastforce
have C2: "upper_asymptotic_density (C k) ≤ (∑n. upper_asymptotic_density (A n))" for k
proof -
have "upper_asymptotic_density (C k) ≤ (∑i≤k. upper_asymptotic_density (A i))"
unfolding C_def by (rule upper_asymptotic_density_finite_Union, auto)
also have "... ≤ (∑i. upper_asymptotic_density (A i))"
apply (rule sum_le_suminf[OF assms]) using upper_asymptotic_density_in_01 by auto
finally show ?thesis by simp
qed
obtain B where B: "upper_asymptotic_density B ≤ (∑n. upper_asymptotic_density (A n))"
"⋀n. ∃N. C n ∩ {N..} ⊆ B"
using upper_asymptotic_density_incseq_Union[OF C2 C1] by blast
have "∃N. A n ∩ {N..} ⊆ B" for n
using B(2)[of n] unfolding C_def by auto
then show ?thesis using B(1) by blast
qed
text ‹A particular case of the previous proposition, often useful, is when all sets have density
zero.›
proposition upper_asymptotic_density_zero_Union:
assumes "⋀n::nat. upper_asymptotic_density (A n) = 0"
shows "∃B. upper_asymptotic_density B = 0 ∧ (∀n. ∃N. A n ∩ {N..} ⊆ B)"
proof -
have "∃B. upper_asymptotic_density B ≤ (∑n. upper_asymptotic_density (A n)) ∧ (∀n. ∃N. A n ∩ {N..} ⊆ B)"
apply (rule upper_asymptotic_density_Union) unfolding assms by auto
then obtain B where "upper_asymptotic_density B ≤ 0" "⋀n. ∃N. A n ∩ {N..} ⊆ B"
unfolding assms by auto
then show ?thesis
using upper_asymptotic_density_in_01(3)[of B] by auto
qed
subsection ‹Lower asymptotic densities›
text ‹The lower asymptotic density of a set of natural numbers is defined just as its
upper asymptotic density but using a liminf instead of a limsup. Its properties are proved
exactly in the same way.›
definition lower_asymptotic_density::"nat set ⇒ real"
where "lower_asymptotic_density A = real_of_ereal(liminf (λn. card(A ∩ {..<n})/n))"
lemma lower_asymptotic_density_in_01:
"ereal(lower_asymptotic_density A) = liminf (λn. card(A ∩ {..<n})/n)"
"lower_asymptotic_density A ≤ 1"
"lower_asymptotic_density A ≥ 0"
proof -
{
fix n::nat assume "n>0"
have "card(A ∩ {..<n}) ≤ n" by (metis card_lessThan Int_lower2 card_mono finite_lessThan)
then have "card(A ∩ {..<n}) / n ≤ ereal 1" using ‹n>0› by auto
}
then have "eventually (λn. card(A ∩ {..<n}) / n ≤ ereal 1) sequentially"
by (simp add: eventually_at_top_dense)
then have "limsup (λn. card(A ∩ {..<n})/n) ≤ 1" by (simp add: Limsup_const Limsup_bounded)
then have a: "liminf (λn. card(A ∩ {..<n})/n) ≤ 1"
by (meson Liminf_le_Limsup less_le_trans not_le sequentially_bot)
have "card(A ∩ {..<n}) / n ≥ ereal 0" for n by auto
then have b: "liminf (λn. card(A ∩ {..<n})/n) ≥ 0" by (simp add: le_Liminf_iff less_le_trans)
have "abs(liminf (λn. card(A ∩ {..<n})/n)) ≠ ∞" using a b by auto
then show "ereal(lower_asymptotic_density A) = liminf (λn. card(A ∩ {..<n})/n)"
unfolding lower_asymptotic_density_def by auto
show "lower_asymptotic_density A ≤ 1" "lower_asymptotic_density A ≥ 0" unfolding lower_asymptotic_density_def
using a b by (auto simp add: real_of_ereal_le_1 real_of_ereal_pos)
qed
text ‹The lower asymptotic density is bounded by the upper one. When they coincide,
$Card(A \cap [0,n))/n$ converges to this common value.›
lemma lower_asymptotic_density_le_upper:
"lower_asymptotic_density A ≤ upper_asymptotic_density A"
using lower_asymptotic_density_in_01(1) upper_asymptotic_density_in_01(1)
by (metis (mono_tags, lifting) Liminf_le_Limsup ereal_less_eq(3) sequentially_bot)
lemma lower_asymptotic_density_eq_upper:
assumes "lower_asymptotic_density A = l" "upper_asymptotic_density A = l"
shows "(λn. card(A ∩ {..<n})/n) ⇢ l"
apply (rule limsup_le_liminf_real)
using upper_asymptotic_density_in_01(1)[of A] lower_asymptotic_density_in_01(1)[of A] assms by auto
text ‹In particular, when a set has a zero upper density, or a lower density one, then this
implies the corresponding convergence of $Card(A \cap [0,n))/n$.›
lemma upper_asymptotic_density_zero_lim:
assumes "upper_asymptotic_density A = 0"
shows "(λn. card(A ∩ {..<n})/n) ⇢ 0"
apply (rule lower_asymptotic_density_eq_upper)
using assms lower_asymptotic_density_le_upper[of A] lower_asymptotic_density_in_01(3)[of A] by auto
lemma lower_asymptotic_density_one_lim:
assumes "lower_asymptotic_density A = 1"
shows "(λn. card(A ∩ {..<n})/n) ⇢ 1"
apply (rule lower_asymptotic_density_eq_upper)
using assms lower_asymptotic_density_le_upper[of A] upper_asymptotic_density_in_01(2)[of A] by auto
text ‹The lower asymptotic density of a set is $1$ minus the upper asymptotic density of its complement.
Hence, most statements about one of them follow from statements about the other one,
although we will rather give direct proofs as they are not more complicated.›
lemma lower_upper_asymptotic_density_complement:
"lower_asymptotic_density A = 1 - upper_asymptotic_density (UNIV - A)"
proof -
{
fix n assume "n>(0::nat)"
have "{..<n} ∩ UNIV - (UNIV - ({..<n} - (UNIV - A))) = {..<n} ∩ A"
by blast
moreover have "{..<n} ∩ UNIV ∩ (UNIV - ({..<n} - (UNIV - A))) = (UNIV - A) ∩ {..<n}"
by blast
ultimately have "card (A ∩ {..<n}) = n - card((UNIV-A) ∩ {..<n})"
by (metis (no_types) Int_commute card_Diff_subset_Int card_lessThan finite_Int finite_lessThan inf_top_right)
then have "card (A ∩ {..<n})/n = (real n - card((UNIV-A) ∩ {..<n})) / n"
by (metis Int_lower2 card_lessThan card_mono finite_lessThan of_nat_diff)
then have "card (A ∩ {..<n})/n = ereal 1 - card((UNIV-A) ∩ {..<n})/n"
using ‹n>0› by (simp add: diff_divide_distrib)
}
then have "eventually (λn. card (A ∩ {..<n})/n = ereal 1 - card((UNIV-A) ∩ {..<n})/n) sequentially"
by (simp add: eventually_at_top_dense)
then have "liminf (λn. card (A ∩ {..<n})/n) = liminf (λn. ereal 1 - card((UNIV-A) ∩ {..<n})/n)"
by (rule Liminf_eq)
also have "... = ereal 1 - limsup (λn. card((UNIV-A) ∩ {..<n})/n)"
by (rule liminf_ereal_cminus, simp)
finally show ?thesis unfolding lower_asymptotic_density_def
by (metis ereal_minus(1) real_of_ereal.simps(1) upper_asymptotic_density_in_01(1))
qed
proposition lower_asymptotic_densityD:
fixes l::real
assumes "lower_asymptotic_density A > l"
shows "eventually (λn. card(A ∩ {..<n}) > l * n) sequentially"
proof -
have "ereal(lower_asymptotic_density A) > l" using assms by auto
then have "liminf (λn. card(A ∩ {..<n})/n) > l"
using lower_asymptotic_density_in_01(1) by auto
then have "eventually (λn. card(A ∩ {..<n})/n > ereal l) sequentially"
using less_LiminfD by blast
then have "eventually (λn. card(A ∩ {..<n})/n > ereal l ∧ n > 0) sequentially"
using eventually_gt_at_top eventually_conj by blast
moreover have "card(A ∩ {..<n}) > l * n" if "card(A ∩ {..<n})/n > ereal l ∧ n > 0" for n
using that divide_le_eq ereal_less_eq(3) less_imp_of_nat_less not_less of_nat_eq_0_iff by fastforce
ultimately show "eventually (λn. card(A ∩ {..<n}) > l * n) sequentially"
by (simp add: eventually_mono)
qed
proposition lower_asymptotic_densityI:
fixes l::real
assumes "eventually (λn. card(A ∩ {..<n}) ≥ l * n) sequentially"
shows "lower_asymptotic_density A ≥ l"
proof -
have "eventually (λn. card(A ∩ {..<n}) ≥ l * n ∧ n > 0) sequentially"
using assms eventually_gt_at_top eventually_conj by blast
moreover have "card(A ∩ {..<n})/n ≥ ereal l" if "card(A ∩ {..<n}) ≥ l * n ∧ n > 0" for n
using that by (meson ereal_less_eq(3) not_less of_nat_0_less_iff pos_divide_less_eq)
ultimately have "eventually (λn. card(A ∩ {..<n})/n ≥ ereal l) sequentially"
by (simp add: eventually_mono)
then have "liminf (λn. card(A ∩ {..<n})/n) ≥ ereal l"
by (simp add: Liminf_bounded)
then have "ereal(lower_asymptotic_density A) ≥ ereal l"
using lower_asymptotic_density_in_01(1) by auto
then show ?thesis by auto
qed
text ‹One can control the asymptotic density of an intersection in terms of the asymptotic density
of each component›
lemma lower_asymptotic_density_intersection:
"lower_asymptotic_density A + lower_asymptotic_density B ≤ lower_asymptotic_density (A ∩ B) + 1"
using upper_asymptotic_density_union[of "UNIV - A" "UNIV - B"]
unfolding lower_upper_asymptotic_density_complement by (auto simp add: algebra_simps Diff_Int)
lemma lower_asymptotic_density_subset:
assumes "A ⊆ B"
shows "lower_asymptotic_density A ≤ lower_asymptotic_density B"
using upper_asymptotic_density_subset[of "UNIV-B" "UNIV-A"] assms
unfolding lower_upper_asymptotic_density_complement by auto
lemma lower_asymptotic_density_lim:
assumes "(λn. card(A ∩ {..<n})/n) ⇢ l"
shows "lower_asymptotic_density A = l"
proof -
have "(λn. ereal(card(A ∩ {..<n})/n)) ⇢ l" using assms by auto
then have "liminf (λn. card(A ∩ {..<n})/n) = l"
using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast
then show ?thesis unfolding lower_asymptotic_density_def by auto
qed
lemma lower_asymptotic_density_finite:
assumes "finite A"
shows "lower_asymptotic_density A = 0"
using lower_asymptotic_density_in_01(3) upper_asymptotic_density_finite[OF assms] lower_asymptotic_density_le_upper
by (metis antisym_conv)
text ‹In particular, bounded intervals have zero lower density.›
lemma lower_asymptotic_density_bdd_interval [simp]:
"lower_asymptotic_density {} = 0"
"lower_asymptotic_density {..N} = 0"
"lower_asymptotic_density {..<N} = 0"
"lower_asymptotic_density {n..N} = 0"
"lower_asymptotic_density {n..<N} = 0"
"lower_asymptotic_density {n<..N} = 0"
"lower_asymptotic_density {n<..<N} = 0"
by (auto intro!: lower_asymptotic_density_finite)
text ‹Conversely, unbounded intervals have density $1$.›
lemma lower_asymptotic_density_infinite_interval [simp]:
"lower_asymptotic_density {N..} = 1"
"lower_asymptotic_density {N<..} = 1"
"lower_asymptotic_density UNIV = 1"
proof -
have "UNIV - {N..} = {..<N}" by auto
then show "lower_asymptotic_density {N..} = 1"
by (auto simp add: lower_upper_asymptotic_density_complement)
have "UNIV - {N<..} = {..N}" by auto
then show "lower_asymptotic_density {N<..} = 1"
by (auto simp add: lower_upper_asymptotic_density_complement)
show "lower_asymptotic_density UNIV = 1"
by (auto simp add: lower_upper_asymptotic_density_complement)
qed
lemma upper_asymptotic_density_infinite_interval [simp]:
"upper_asymptotic_density {N..} = 1"
"upper_asymptotic_density {N<..} = 1"
"upper_asymptotic_density UNIV = 1"
by (metis antisym upper_asymptotic_density_in_01(2) lower_asymptotic_density_infinite_interval lower_asymptotic_density_le_upper)+
text ‹The intersection of sets with lower density one still has lower density one.›
lemma lower_asymptotic_density_one_intersection:
assumes "lower_asymptotic_density A = 1" "lower_asymptotic_density B = 1"
shows "lower_asymptotic_density (A ∩ B) = 1"
using lower_asymptotic_density_in_01(2)[of "A ∩ B"] lower_asymptotic_density_intersection[of A B] unfolding assms by auto
lemma lower_asymptotic_density_one_finite_Intersection:
assumes "finite I" "⋀i. i ∈ I ⟹ lower_asymptotic_density (A i) = 1"
shows "lower_asymptotic_density (⋂i∈I. A i) = 1"
using assms by (induction rule: finite_induct, auto intro!: lower_asymptotic_density_one_intersection)
text ‹As for the upper asymptotic density, there is a modification of the intersection, akin
to the diagonal argument in this context, for which the ``intersection'' of sets with large
lower density still has large lower density.›
proposition lower_asymptotic_density_decseq_Inter:
assumes "⋀(n::nat). lower_asymptotic_density (A n) ≥ l" "decseq A"
shows "∃B. lower_asymptotic_density B ≥ l ∧ (∀n. ∃N. B ∩ {N..} ⊆ A n)"
proof -
define C where "C = (λn. UNIV - A n)"
have *: "upper_asymptotic_density (C n) ≤ 1 - l" for n
using assms(1)[of n] unfolding C_def lower_upper_asymptotic_density_complement[of "A n"] by auto
have **: "incseq C"
using assms(2) unfolding C_def incseq_def decseq_def by auto
obtain D where D: "upper_asymptotic_density D ≤ 1 - l" "⋀n. ∃N. C n ∩ {N..} ⊆ D"
using upper_asymptotic_density_incseq_Union[OF * **] by blast
define B where "B = UNIV - D"
have "lower_asymptotic_density B ≥ l"
using D(1) lower_upper_asymptotic_density_complement[of B] by (simp add: double_diff B_def)
moreover have "∃N. B ∩ {N..} ⊆ A n" for n
using D(2)[of n] unfolding B_def C_def by auto
ultimately show ?thesis by auto
qed
text ‹In the same way, the modified intersection of sets of density $1$ still has density one,
and is eventually contained in each of them.›
proposition lower_asymptotic_density_one_Inter:
assumes "⋀n::nat. lower_asymptotic_density (A n) = 1"
shows "∃B. lower_asymptotic_density B = 1 ∧ (∀n. ∃N. B ∩ {N..} ⊆ A n)"
proof -
define C where "C = (λn. UNIV - A n)"
have *: "upper_asymptotic_density (C n) = 0" for n
using assms(1)[of n] unfolding C_def lower_upper_asymptotic_density_complement[of "A n"] by auto
obtain D where D: "upper_asymptotic_density D = 0" "⋀n. ∃N. C n ∩ {N..} ⊆ D"
using upper_asymptotic_density_zero_Union[OF *] by force
define B where "B = UNIV - D"
have "lower_asymptotic_density B = 1"
using D(1) lower_upper_asymptotic_density_complement[of B] by (simp add: double_diff B_def)
moreover have "∃N. B ∩ {N..} ⊆ A n" for n
using D(2)[of n] unfolding B_def C_def by auto
ultimately show ?thesis by auto
qed
text ‹Sets with density $1$ play an important role in relation to Cesaro convergence of nonnegative
bounded sequences: such a sequence converges to $0$ in Cesaro average if and only if it converges
to $0$ along a set of density $1$.
The proof is not hard. Since the Cesaro average tends to $0$, then given $\epsilon>0$ the
proportion of times where $u_n < \epsilon$ tends to $1$, i.e., the set $A_\epsilon$ of such good
times has density $1$. A modified intersection (as constructed in
Proposition~\verb+lower_asymptotic_density_one_Inter+) of these times has density $1$, and
$u_n$ tends to $0$ along this set.
›
theorem cesaro_imp_density_one:
assumes "⋀n. u n ≥ (0::real)" "(λn. (∑i<n. u i)/n) ⇢ 0"
shows "∃A. lower_asymptotic_density A = 1 ∧ (λn. u n * indicator A n) ⇢ 0"
proof -
define B where "B = (λe. {n. u n ≥ e})"
text ‹$B e$ is the set of bad times where $u_n \geq e$. It has density $0$ thanks to
the assumption of Cesaro convergence to $0$.›
have A: "upper_asymptotic_density (B e) = 0" if "e > 0" for e
proof -
have *: "card (B e ∩ {..<n}) / n ≤ (1/e) * ((∑i∈{..<n}. u i)/n)" if "n ≥ 1" for n
proof -
have "e * card (B e ∩ {..<n}) = (∑i∈B e ∩ {..<n}. e)" by auto
also have "... ≤ (∑i∈B e ∩ {..<n}. u i)"
apply (rule sum_mono) unfolding B_def by auto
also have "... ≤ (∑i∈{..<n}. u i)"
apply (rule sum_mono2) using assms by auto
finally show ?thesis
using ‹e > 0› ‹n ≥ 1› by (auto simp add: divide_simps algebra_simps)
qed
have "(λn. card (B e ∩ {..<n}) / n) ⇢ 0"
proof (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. (1/e) * ((∑i∈{..<n}. u i)/n)"])
have "(λn. (1/e) * ((∑i∈{..<n}. u i)/n)) ⇢ (1/e) * 0"
by (intro tendsto_intros assms)
then show "(λn. (1/e) * ((∑i∈{..<n}. u i)/n)) ⇢ 0" by simp
show "∀⇩F n in sequentially. real (card (B e ∩ {..<n})) / real n ≤ 1 / e * (sum u {..<n} / real n)"
using * unfolding eventually_sequentially by auto
qed (auto)
then show ?thesis
by (rule upper_asymptotic_density_lim)
qed
define C where "C = (λn::nat. UNIV - B (((1::real)/2)^n))"
have "lower_asymptotic_density (C n) = 1" for n
unfolding C_def lower_upper_asymptotic_density_complement by (simp add: A double_diff)
then obtain A where A: "lower_asymptotic_density A = 1" "⋀n. ∃N. A ∩ {N..} ⊆ C n"
using lower_asymptotic_density_one_Inter by blast
have E: "eventually (λn. u n * indicator A n < e) sequentially" if "e > 0" for e
proof -
have "eventually (λn. ((1::real)/2)^n < e) sequentially"
by (rule order_tendstoD[OF _ ‹e > 0›], intro tendsto_intros, auto)
then obtain n where n: "((1::real)/2)^n < e"
unfolding eventually_sequentially by auto
obtain N where N: "A ∩ {N..} ⊆ C n"
using A(2) by blast
have "u k * indicator A k < e" if "k ≥ N" for k
proof (cases "k ∈ A")
case True
then have "k ∈ C n" using N that by auto
then have "u k < ((1::real)/2)^n"
unfolding C_def B_def by auto
then have "u k < e"
using n by auto
then show ?thesis
unfolding indicator_def using True by auto
next
case False
then show ?thesis
unfolding indicator_def using ‹e > 0› by auto
qed
then show ?thesis
unfolding eventually_sequentially by auto
qed
have "(λn. u n * indicator A n) ⇢ 0"
apply (rule order_tendstoI[OF _ E])
unfolding indicator_def using ‹⋀n. u n ≥ 0› by (simp add: less_le_trans)
then show ?thesis
using ‹lower_asymptotic_density A = 1› by auto
qed
text ‹The proof of the reverse implication is more direct: in the Cesaro sum, just bound the
elements in $A$ by a small $\epsilon$, and the other ones by a uniform bound, to get a bound
which is $o(n)$.›
theorem density_one_imp_cesaro:
assumes "⋀n. u n ≥ (0::real)" "⋀n. u n ≤ C"
"lower_asymptotic_density A = 1"
"(λn. u n * indicator A n) ⇢ 0"
shows "(λn. (∑i<n. u i)/n) ⇢ 0"
proof (rule order_tendstoI)
fix e::real assume "e < 0"
have "(∑i<n. u i)/n ≥ 0" for n
using assms(1) by (simp add: sum_nonneg divide_simps)
then have "(∑i<n. u i)/n > e" for n
using ‹e < 0› less_le_trans by auto
then show "eventually (λn. (∑i<n. u i)/n > e) sequentially"
unfolding eventually_sequentially by auto
next
fix e::real assume "e > 0"
have "C ≥ 0" using ‹u 0 ≥ 0› ‹u 0 ≤ C› by auto
have "eventually (λn. u n * indicator A n < e/4) sequentially"
using order_tendstoD(2)[OF assms(4), of "e/4"] ‹e>0› by auto
then obtain N where N: "⋀k. k ≥ N ⟹ u k * indicator A k < e/4"
unfolding eventually_sequentially by auto
define B where "B = UNIV - A"
have *: "upper_asymptotic_density B = 0"
using assms unfolding B_def lower_upper_asymptotic_density_complement by auto
have "eventually (λn. card(B ∩ {..<n}) < (e/(4 * (C+1))) * n) sequentially"
apply (rule upper_asymptotic_densityD) using ‹e > 0› ‹C ≥ 0› * by auto
then obtain M where M: "⋀n. n ≥ M ⟹ card(B ∩ {..<n}) < (e/(4 * (C+1))) * n"
unfolding eventually_sequentially by auto
obtain P::nat where P: "P ≥ 4 * N * C/e"
using real_arch_simple by auto
define Q where "Q = N + M + 1 + P"
have "(∑i<n. u i)/n < e" if "n ≥ Q" for n
proof -
have n: "n ≥ N" "n ≥ M" "n ≥ P" "n ≥ 1"
using ‹n ≥ Q› unfolding Q_def by auto
then have n2: "n ≥ 4 * N * C/e" using P by auto
have "(∑i<n. u i) ≤ (∑i∈{..<N} ∪ ({N..<n} ∩ A) ∪ ({N..<n} - A). u i)"
by (rule sum_mono2, auto simp add: assms)
also have "... = (∑i∈{..<N}. u i) + (∑i∈{N..<n} ∩ A. u i) + (∑i∈{N..<n} - A. u i)"
by (subst sum.union_disjoint, auto)+
also have "... = (∑i∈{..<N}. u i) + (∑i∈{N..<n} ∩ A. u i * indicator A i) + (∑i∈{N..<n} - A. u i)"
unfolding indicator_def by auto
also have "... ≤ (∑i∈{..<N}. u i) + (∑i∈{N..<n}. u i * indicator A i) + (∑i∈ B ∩ {..<n}. u i)"
apply (intro add_mono sum_mono2) unfolding B_def using assms by auto
also have "... ≤ (∑i∈{..<N}. C) + (∑i∈{N..<n}. e/4) + (∑i∈B ∩ {..<n}. C)"
apply (intro add_mono sum_mono) using assms less_imp_le[OF N] by auto
also have "... = N * C + (n-N) * e/4 + card(B ∩ {..<n}) * C"
by auto
also have "... ≤ n * e/4 + n * e/4 + (e/(4 * (C+1))) * n * C"
apply (intro add_mono)
using n2 ‹e > 0› mult_right_mono[OF less_imp_le[OF M[OF ‹n ≥ M›]] ‹C ≥ 0›] by (auto simp add: divide_simps)
also have "... ≤ n * e * 3/4"
using ‹C ≥ 0› ‹e > 0› by (simp add: divide_simps algebra_simps)
also have "... < n * e"
using ‹n ≥ 1› ‹e > 0› by auto
finally show ?thesis
using ‹n ≥ 1› by (simp add: divide_simps algebra_simps)
qed
then show "eventually (λn. (∑i<n. u i)/n < e) sequentially"
unfolding eventually_sequentially by auto
qed
end