NormedAddCommGroup.exists_norm_nsmul_le
theorem NormedAddCommGroup.exists_norm_nsmul_le :
∀ {A : Type u_1} [inst : NormedAddCommGroup A] [inst_1 : CompactSpace A] [inst_2 : ConnectedSpace A]
[inst_3 : MeasurableSpace A] [inst_4 : BorelSpace A] {μ : MeasureTheory.Measure A} [inst_5 : μ.IsAddHaarMeasure]
(ξ : A) {n : ℕ},
0 < n → ∀ (δ : ℝ), ↑↑μ Set.univ ≤ (n + 1) • ↑↑μ (Metric.closedBall 0 (δ / 2)) → ∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ δ
This is a general version of the Dirichlet's approximation theorem for metric spaces. The theorem states that for any type `A` that can form a normed additive commutative group and is also a compact, connected, measurable, and Borel space with an additive Haar measure `μ`, given an element `ξ` of `A`, a positive natural number `n` and a real number `δ`, if the measure of the universal set is less than or equal to `(n + 1)` times the measure of the closed ball of radius `δ / 2` centered at 0, there exists a natural number `j` in the closed interval from 1 to `n` such that the norm of `j` times `ξ` is less than or equal to `δ`. This theorem is a direct generalization of the classical Dirichlet's approximation theorem and provides essential bounds on the approximation of elements in normed additive commutative groups.
More concisely: Given a compact, connected, measurable, and Borel space `A` with an additive Haar measure `μ` that is a normed additive commutative group, for any `ξ` in `A`, `n` in `ℕ`, and `δ` in `ℝ+`, if the measure of `A` is less than or equal to `(n + 1)` times the measure of the closed ball of radius `δ / 2` centered at 0, then there exists an integer `j` from 1 to `n` such that `‱(j * ξ) < δ`, where `‱` denotes the norm on `A`.
|
AddCircle.exists_norm_nsmul_le
theorem AddCircle.exists_norm_nsmul_le :
∀ {T : ℝ} [hT : Fact (0 < T)] (ξ : AddCircle T) {n : ℕ}, 0 < n → ∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1) := by
sorry
**Dirichlet's Approximation Theorem**
This theorem states that for any given positive real number `T`, and any element `ξ` in the additive circle defined with respect to `T`, and for any natural number `n` greater than 0, there exists an integer `j` within the closed interval from 1 to `n` inclusive, such that the norm of `j` times `ξ` is less than or equal to `T` divided by `(n + 1)`.
More concisely: For any positive real number T and any element ξ in the additive circle modulo 1 with respect to T, there exists an integer j between 1 and n inclusive such that |jξ| ≤ T / (n + 1).
|
AddCircle.addWellApproximable_ae_empty_or_univ
theorem AddCircle.addWellApproximable_ae_empty_or_univ :
∀ {T : ℝ} [hT : Fact (0 < T)] (δ : ℕ → ℝ),
Filter.Tendsto δ Filter.atTop (nhds 0) →
(∀ᵐ (x : AddCircle T), ¬addWellApproximable (AddCircle T) δ x) ∨
∀ᵐ (x : AddCircle T), addWellApproximable (AddCircle T) δ x
Gallagher's ergodic theorem on Diophantine approximation states the following: For a real number `T` greater than zero and a sequence of real numbers `δ` that converges to 0 as `n` approaches infinity (i.e., `Filter.Tendsto δ Filter.atTop (nhds 0)`), either almost every element `x` in the additive circle `AddCircle T` is not well-approximable in the sense of the `addWellApproximable` function with respect to the sequence `δ` (`∀ᵐ (x : AddCircle T), ¬addWellApproximable (AddCircle T) δ x`), or almost every element `x` in the additive circle `AddCircle T` is well-approximable in this sense (`∀ᵐ (x : AddCircle T), addWellApproximable (AddCircle T) δ x`). In other words, the set of well-approximable points in `AddCircle T` is either almost everywhere or almost nowhere.
More concisely: The set of real numbers `x` in the additive circle `AddCircle T` that are well-approximable with respect to a converging sequence `δ` of real numbers has full or zero measure.
|