Theory Asymptotic_Density

theory Asymptotic_Density
imports SG_Library_Complement
(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

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"
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"
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"
then have "limsup (λn. card(A ∩ {..<n})/n) ≤ ereal l"
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})"
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"
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"
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"
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"
also have "... = card (A ∩ {..<n})/n + C/n"
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))"
also have "... ≤ limsup (λn. card (A ∩ {..<n})/n) + limsup (λn. C/n)"
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"
also have "... = card (A ∩ {k..nat(n+l)})/n + C/n"
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))"
also have "... ≤ limsup (λn. card (A ∩ {k..nat(n+l)})/n) + limsup (λn. C/n)"
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]
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"
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.
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"
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"
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"
then have "liminf (λn. card(A ∩ {..<n})/n) ≥ ereal l"
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"
have "UNIV - {N<..} = {..N}" by auto
then show "lower_asymptotic_density {N<..} = 1"
show "lower_asymptotic_density UNIV = 1"
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] unfolding B_def by auto
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] unfolding B_def by auto
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 (auto intro!: A)
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"
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 (*of Asymptotic_Density.thy*)