Beatty's theorem to Mahler's theorem

TheoremBeatty's theorem #

Mathlib records this with 2 declarations.

Irrational.beattySeq_symmDiff_beattySeq_pos: Rayleigh's theorem on Beatty sequences. Let r be an irrational number greater than 1, and 1/r + 1/s = 1. Then B⁺_r and B⁺_s partition the positive integers.

Irrational.beattySeq_symmDiff_beattySeq_pos {r s : ℝ} (hrs : r.HolderConjugate s)
  (hr : Irrational r) :
  symmDiff {x | ∃ k > 0, beattySeq r k = x} {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}

compl_beattySeq: Generalization of Rayleigh's theorem on Beatty sequences. Let r be a real number greater than 1, and 1/r + 1/s = 1. Then the complement of B_r is B'_s.

compl_beattySeq {r s : ℝ} (hrs : r.HolderConjugate s) :
  {x | ∃ k, beattySeq r k = x}ᶜ = {x | ∃ k, beattySeq' s k = x}

Sources

MathlibIrrational.beattySeq_symmDiff_beattySeq_pos · compl_beattySeq

Uses 3

Statement usesOrder

Proof usesField \(\R\) of real numbers · Ordered ring

TheoremDirichlet's approximation theorem #

Mathlib records this with 4 declarations.

AddCircle.exists_norm_nsmul_le: Dirichlet's approximation theorem

See also Real.exists_rat_abs_sub_le_and_den_le.

AddCircle.exists_norm_nsmul_le {T : ℝ} [hT : Fact (0 < T)] (ξ : AddCircle T) {n : ℕ} (hn : 0 < n) :
  ∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1)

Real.exists_int_int_abs_mul_sub_le: Dirichlet's approximation theorem: For any real number ξ and positive natural n, there are integers j and k, with 0 < k ≤ n and |k*ξ - j| ≤ 1/(n+1).

See also Real.exists_nat_abs_mul_sub_round_le.

Real.exists_int_int_abs_mul_sub_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
  ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)

Real.exists_nat_abs_mul_sub_round_le: Dirichlet's approximation theorem: For any real number ξ and positive natural n, there is a natural number k, with 0 < k ≤ n such that |k*ξ - round(k*ξ)| ≤ 1/(n+1).

Real.exists_nat_abs_mul_sub_round_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
  ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)

Real.exists_rat_abs_sub_le_and_den_le: Dirichlet's approximation theorem: For any real number ξ and positive natural n, there is a fraction q such that q.den ≤ n and |ξ - q| ≤ 1/((n+1)*q.den).

See also AddCircle.exists_norm_nsmul_le.

Real.exists_rat_abs_sub_le_and_den_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
  ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

Sources

MathlibAddCircle.exists_norm_nsmul_le · Real.exists_int_int_abs_mul_sub_le · Real.exists_nat_abs_mul_sub_round_le · Real.exists_rat_abs_sub_le_and_den_le

Uses 17 · Used by 1

Statement usesMetric space

Proof usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Characteristic zero · Closure · Compactness in terms of filters · Completeness of R · Connectedness · Continuous function · Euclidean affine space · Lebesgue measure (Measure theory) · Linear map · Measurable function · Metric structure · Ring structure \(\Z\)

Used bySolutions to Pell’s Equation (Freek Wiedijk's 100 theorems)

Dirichlet's theorem on arithmetic progressions

DefinitionDirichlet's unit theorem #

Mathlib records this with 2 declarations.

NumberField.Units.basisModTorsion: A basis of the quotient (𝓞 K)ˣ ⧸ (torsion K) seen as an additive ℤ-module.

NumberField.Units.basisModTorsion.{u_1} (K : Type u_1) [Field K] [NumberField K] :
  Module.Basis (Fin (NumberField.Units.rank K)) ℤ
    (Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K))

NumberField.Units.exist_unique_eq_mul_prod: Dirichlet Unit Theorem. Any unit x of 𝓞 K can be written uniquely as the product of a root of unity and powers of the units of the fundamental system fundSystem.

NumberField.Units.exist_unique_eq_mul_prod.{u_1} (K : Type u_1) [Field K] [NumberField K]
  (x : (NumberField.RingOfIntegers K)ˣ) :
  ∃! ζe, x = ↑ζe.1 * ∏ i, NumberField.Units.fundSystem K i ^ ζe.2 i

Sources

MathlibNumberField.Units.basisModTorsion · NumberField.Units.exist_unique_eq_mul_prod

Uses 12

Statement usesAssociative algebra over a commutative ring · Basis · Characteristic zero · Complex number · Finite-dimensionality · Metric space · Orbit · Periodic points · Polynomial in one indeterminate · Ring structure \(\Z\) · Subgroup

Proof usesQuotient group

TheoremFermat's little theorem #

Fermat's Little Theorem: for all nonzero a : ZMod p, we have a ^ (p - 1) = 1.

ZMod.pow_card_sub_one_eq_one {p : ℕ} [Fact (Nat.Prime p)] {a : ZMod p} (ha : a ≠ 0) :
  a ^ (p - 1) = 1

Sources

MathlibZMod.pow_card_sub_one_eq_one

Uses 4 · Used by 3

Statement usesField · Irreducible element · Rational number

Proof usesFinite set

Used byErdős–Ginzburg–Ziv theorem · Chevalley-Warning theorem (Number theory) · Quadratic reciprocity

TheoremGlaisher's theorem #

Mathlib states this as Nat.Partition.card_restricted_eq_card_countRestricted.

Nat.Partition.card_restricted_eq_card_countRestricted (n : ℕ) {m : ℕ} (hm : 0 < m) :
  (Nat.Partition.restricted n fun x => ¬m ∣ x).card = (Nat.Partition.countRestricted n m).card

Sources

MathlibNat.Partition.card_restricted_eq_card_countRestricted

Uses 12 · Used by 1

Statement usesFinite set · Natural number

Proof usesAssociative algebra over a commutative ring · Characteristic zero · Closure · Hausdorff space · Infinite sum · Linear map · Ordered ring · Power series · Ring structure \(\Z\) · Topological ring

Used byThe Partition Theorem

Lagrange's four-square theorem

TheoremLucas's theorem #

Alias of Choose.choose_modEq_prod_range_choose.

Lucas's Theorem: For primes p, choose n k is congruent to the product of choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p) over i modulo p.

Choose.lucas_theorem {n k p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) :
  ↑(n.choose k) ≡ ∏ i ∈ Finset.range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Sources

MathlibChoose.lucas_theorem

Uses 4

Statement usesCongruence in \(\Z\) · Finite set · Irreducible element

Proof usesRing structure \(\Z\)

TheoremMahler's theorem #

Mahler's theorem: for any continuous function f from ℤ_[p] to a p-adic Banach space, the Mahler series with coefficients n ↦ Δ_[1]^[n] f 0 converges to the original function f.

PadicInt.hasSum_mahler.{u_1} {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [NormedAddCommGroup E]
  [_root_.Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E]
  (f : C(ℤ_[p], E)) : HasSum (fun n => PadicInt.mahlerTerm ((fwdDiff 1)^[n] (⇑f) 0) n) f

Sources

MathlibPadicInt.hasSum_mahler

Uses 18

Statement uses\(p\)-adic integer · Compact open topology · Completeness · Infinite sum · Irreducible element · Linear map · Polynomial in one indeterminate · Topological module

Proof usesBezout’s Theorem · Characteristic zero · Closure · Field \(\Q\) of rational numbers · Hausdorff space · Heine-Cantor theorem · Order topology · Ring structure \(\Z\) · Sequential space · Uniformly continuous function

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Beatty's theorem to Mahler's theorem

TheoremBeatty's theorem#

Sources

TheoremDirichlet's approximation theorem#

Sources

DefinitionDirichlet's unit theorem#

Sources

TheoremFermat's little theorem#

Sources

TheoremGlaisher's theorem#

Sources

TheoremLucas's theorem#

Sources

TheoremMahler's theorem#

Sources

TheoremBeatty's theorem #

TheoremDirichlet's approximation theorem #

DefinitionDirichlet's unit theorem #

TheoremFermat's little theorem #

TheoremGlaisher's theorem #

TheoremLucas's theorem #

TheoremMahler's theorem #