English
A general Dirichlet-type statement: in a normed additive group that is compact and connected, for any ξ and any positive n, there exists j in [1,n] with norm j·ξ ≤ δ whenever δ is large enough to cover the total mass; this is a finite-multiplicity approximation result for Haar measure.
Русский
Обобщённая версия теоремы Дирихле в нормированной абелевой группе: в компактном связном нормированном аддитивном группе для данного ξ и положительного n существует j в [1,n] такое, что ∥j·ξ∥ ≤ δ, где δ выбирается так, чтобы мера охватывала всю массу.
LaTeX
$$$$ \\exists j \\in [1,n],\\; \\|j\\cdot \\xi\\| \\le \\delta. $$$$
Lean4
/-- **Gallagher's ergodic theorem** on Diophantine approximation. -/
theorem addWellApproximable_ae_empty_or_univ (δ : ℕ → ℝ) (hδ : Tendsto δ atTop (𝓝 0)) :
(∀ᵐ x, ¬addWellApproximable 𝕊 δ x) ∨ ∀ᵐ x, addWellApproximable 𝕊 δ x := by
/- Sketch of proof:
Let `E := addWellApproximable 𝕊 δ`. For each prime `p : ℕ`, we can partition `E` into three
pieces `E = (A p) ∪ (B p) ∪ (C p)` where:
`A p = blimsup (approxAddOrderOf 𝕊 n (δ n)) atTop (fun n => 0 < n ∧ (p ∤ n))`
`B p = blimsup (approxAddOrderOf 𝕊 n (δ n)) atTop (fun n => 0 < n ∧ (p ∣∣ n))`
`C p = blimsup (approxAddOrderOf 𝕊 n (δ n)) atTop (fun n => 0 < n ∧ (p*p ∣ n))`.
In other words, `A p` is the set of points `x` for which there exist infinitely-many `n` such
that `x` is within a distance `δ n` of a point of order `n` and `p ∤ n`. Similarly for `B`, `C`.
These sets have the following key properties:
1. `A p` is almost invariant under the ergodic map `y ↦ p • y`
2. `B p` is almost invariant under the ergodic map `y ↦ p • y + 1/p`
3. `C p` is invariant under the map `y ↦ y + 1/p`
To prove 1 and 2 we need the key result `blimsup_thickening_mul_ae_eq` but 3 is elementary.
It follows from `AddCircle.ergodic_nsmul_add` and `Ergodic.ae_empty_or_univ_of_image_ae_le` that
if either `A p` or `B p` is not almost empty for any `p`, then it is almost full and thus so is
`E`. We may therefore assume that `A p` and `B p` are almost empty for all `p`. We thus have
`E` is almost equal to `C p` for every prime. Combining this with 3 we find that `E` is almost
invariant under the map `y ↦ y + 1/p` for every prime `p`. The required result then follows from
`AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self`. -/
letI : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup _
set μ : Measure 𝕊 := volume
set u : Nat.Primes → 𝕊 := fun p => ↑((↑(1 : ℕ) : ℝ) / ((p : ℕ) : ℝ) * T)
have hu₀ : ∀ p : Nat.Primes, addOrderOf (u p) = (p : ℕ) := by rintro ⟨p, hp⟩;
exact addOrderOf_div_of_gcd_eq_one hp.pos (gcd_one_left p)
have hu : Tendsto (addOrderOf ∘ u) atTop atTop :=
by
rw [(funext hu₀ : addOrderOf ∘ u = (↑))]
have h_mono : Monotone ((↑) : Nat.Primes → ℕ) := fun p q hpq => hpq
refine h_mono.tendsto_atTop_atTop fun n => ?_
obtain ⟨p, hp, hp'⟩ := n.exists_infinite_primes
exact ⟨⟨p, hp'⟩, hp⟩
set E := addWellApproximable 𝕊 δ
set X : ℕ → Set 𝕊 := fun n => approxAddOrderOf 𝕊 n (δ n)
set A : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p∤n
set B : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p∣∣n
set C : ℕ → Set 𝕊 := fun p => blimsup X atTop fun n => 0 < n ∧ p ^ 2 ∣ n
have hA₀ : ∀ p, MeasurableSet (A p) := fun p =>
MeasurableSet.measurableSet_blimsup fun n _ => isOpen_thickening.measurableSet
have hB₀ : ∀ p, MeasurableSet (B p) := fun p =>
MeasurableSet.measurableSet_blimsup fun n _ => isOpen_thickening.measurableSet
have hE₀ : NullMeasurableSet E μ :=
by
refine (MeasurableSet.measurableSet_blimsup fun n hn => IsOpen.measurableSet ?_).nullMeasurableSet
exact isOpen_thickening
have hE₁ : ∀ p, E = A p ∪ B p ∪ C p := by
intro p
simp only [E, A, B, C, addWellApproximable, ← blimsup_or_eq_sup, ← and_or_left, ← sup_eq_union, sq]
congr
ext n
tauto
have hE₂ : ∀ p : Nat.Primes, A p =ᵐ[μ] (∅ : Set 𝕊) ∧ B p =ᵐ[μ] (∅ : Set 𝕊) → E =ᵐ[μ] C p :=
by
rintro p ⟨hA, hB⟩
rw [hE₁ p]
exact union_ae_eq_right_of_ae_eq_empty ((union_ae_eq_right_of_ae_eq_empty hA).trans hB)
have hA : ∀ p : Nat.Primes, A p =ᵐ[μ] (∅ : Set 𝕊) ∨ A p =ᵐ[μ] univ :=
by
rintro ⟨p, hp⟩
let f : 𝕊 → 𝕊 := fun y => (p : ℕ) • y
suffices f '' A p ⊆ blimsup (fun n => approxAddOrderOf 𝕊 n (p * δ n)) atTop fun n => 0 < n ∧ p∤n
by
apply (ergodic_nsmul hp.one_lt).ae_empty_or_univ_of_image_ae_le (hA₀ p).nullMeasurableSet
apply (HasSubset.Subset.eventuallyLE this).congr EventuallyEq.rfl
exact
blimsup_thickening_mul_ae_eq μ (fun n => 0 < n ∧ p∤n) (fun n => {y | addOrderOf y = n})
(Nat.cast_pos.mpr hp.pos) _ hδ
refine (sSupHom.setImage f).apply_blimsup_le.trans (mono_blimsup fun n hn => ?_)
replace hn := Nat.coprime_comm.mp (hp.coprime_iff_not_dvd.2 hn.2)
exact approxAddOrderOf.image_nsmul_subset_of_coprime (δ n) hp.pos hn
have hB : ∀ p : Nat.Primes, B p =ᵐ[μ] (∅ : Set 𝕊) ∨ B p =ᵐ[μ] univ :=
by
rintro ⟨p, hp⟩
let x := u ⟨p, hp⟩
let f : 𝕊 → 𝕊 := fun y => p • y + x
suffices f '' B p ⊆ blimsup (fun n => approxAddOrderOf 𝕊 n (p * δ n)) atTop fun n => 0 < n ∧ p∣∣n
by
apply (ergodic_nsmul_add x hp.one_lt).ae_empty_or_univ_of_image_ae_le (hB₀ p).nullMeasurableSet
apply (HasSubset.Subset.eventuallyLE this).congr EventuallyEq.rfl
exact
blimsup_thickening_mul_ae_eq μ (fun n => 0 < n ∧ p∣∣n) (fun n => {y | addOrderOf y = n})
(Nat.cast_pos.mpr hp.pos) _ hδ
refine (sSupHom.setImage f).apply_blimsup_le.trans (mono_blimsup ?_)
rintro n ⟨hn, h_div, h_ndiv⟩
have h_cop : (addOrderOf x).Coprime (n / p) :=
by
obtain ⟨q, rfl⟩ := h_div
rw [hu₀, Subtype.coe_mk, hp.coprime_iff_not_dvd, q.mul_div_cancel_left hp.pos]
exact fun contra => h_ndiv (mul_dvd_mul_left p contra)
replace h_div : n / p * p = n := Nat.div_mul_cancel h_div
have hf : f = (fun y => x + y) ∘ fun y => p • y := by ext; simp [f, add_comm x]
simp_rw [Function.comp_apply, le_eq_subset]
rw [sSupHom.setImage_toFun, hf, image_comp]
have := @monotone_image 𝕊 𝕊 fun y => x + y
specialize this (approxAddOrderOf.image_nsmul_subset (δ n) (n / p) hp.pos)
simp only [h_div] at this ⊢
refine this.trans ?_
convert approxAddOrderOf.vadd_subset_of_coprime (p * δ n) h_cop
rw [hu₀, Subtype.coe_mk, mul_comm p, h_div]
change (∀ᵐ x, x ∉ E) ∨ E ∈ ae volume
rw [← eventuallyEq_empty, ← eventuallyEq_univ]
have hC : ∀ p : Nat.Primes, u p +ᵥ C p = C p := by
intro p
let e := (AddAction.toPerm (u p) : Equiv.Perm 𝕊).toOrderIsoSet
change e (C p) = C p
rw [OrderIso.apply_blimsup e, ← hu₀ p]
exact blimsup_congr (Eventually.of_forall fun n hn => approxAddOrderOf.vadd_eq_of_mul_dvd (δ n) hn.1 hn.2)
by_cases h : ∀ p : Nat.Primes, A p =ᵐ[μ] (∅ : Set 𝕊) ∧ B p =ᵐ[μ] (∅ : Set 𝕊)
· replace h : ∀ p : Nat.Primes, (u p +ᵥ E : Set _) =ᵐ[μ] E :=
by
intro p
replace hE₂ : E =ᵐ[μ] C p := hE₂ p (h p)
have h_qmp : Measure.QuasiMeasurePreserving (-u p +ᵥ ·) μ μ := (measurePreserving_vadd _ μ).quasiMeasurePreserving
refine (h_qmp.vadd_ae_eq_of_ae_eq (u p) hE₂).trans (ae_eq_trans ?_ hE₂.symm)
rw [hC]
exact ae_empty_or_univ_of_forall_vadd_ae_eq_self hE₀ h hu
· right
simp only [not_forall, not_and_or] at h
obtain ⟨p, hp⟩ := h
rw [hE₁ p]
cases hp
· rcases hA p with _ | h; · contradiction
simp only [μ, h, union_ae_eq_univ_of_ae_eq_univ_left]
· rcases hB p with _ | h; · contradiction
simp only [μ, h, union_ae_eq_univ_of_ae_eq_univ_left, union_ae_eq_univ_of_ae_eq_univ_right]
