NumberField.Units.dirichletUnitTheorem.seq_next
theorem NumberField.Units.dirichletUnitTheorem.seq_next :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (wβ : NumberField.InfinitePlace K) {B : β},
NumberField.mixedEmbedding.minkowskiBound K 1 < β(NumberField.mixedEmbedding.convexBodyLTFactor K) * βB β
β {x : β₯(NumberField.ringOfIntegers K)},
x β 0 β
β y, y β 0 β§ (β (w : NumberField.InfinitePlace K), w β wβ β w βy < w βx) β§ |(Algebra.norm β) βy| β€ βB
This theorem, `NumberField.Units.dirichletUnitTheorem.seq_next`, states that for any number field `K`, and given infinite place `wβ` of `K`, and a natural number `B` such that the Minkowski bound of `K` is less than the product of the "fudge factor" appearing in the volume formula for `convexBodyLT` and `B`, for any non-zero element `x` of the ring of integers of `K`, there always exists a non-zero element `y` such that for any infinite place `w` of `K` which is not equal to `wβ`, `w y` is less than `w x`, and the absolute value of the algebraic norm of `y` is less than or equal to `B`. This theorem essentially guarantees the existence of a next term in a certain sequence in the context of number theory and algebra.
More concisely: For any number field `K`, infinite place `wβ`, natural number `B` smaller than the Minkowski bound times the fudge factor, and non-zero element `x` in the ring of integers of `K`, there exists a non-zero `y` such that `|wy| < |wx|` for all infinite places `w β wβ` and `|N(y)| β€ B`, where `N` denotes the algebraic norm.
|
NumberField.Units.dirichletUnitTheorem.seq_norm_ne_zero
theorem NumberField.Units.dirichletUnitTheorem.seq_norm_ne_zero :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (wβ : NumberField.InfinitePlace K) {B : β}
(hB : NumberField.mixedEmbedding.minkowskiBound K 1 < β(NumberField.mixedEmbedding.convexBodyLTFactor K) * βB)
(n : β), (Algebra.norm β€) β(NumberField.Units.dirichletUnitTheorem.seq K wβ hB n) β 0
The theorem `NumberField.Units.dirichletUnitTheorem.seq_norm_ne_zero` states that for any number field `K`, any infinite place `wβ` of `K`, any natural number `B` for which the Minkowski bound of `K` with respect to 1 is less than the product of the fudge factor (`convexBodyLTFactor`) associated with `K` and `B`, and any natural number `n`, the norm of the `n`-th term in the sequence defined by the Dirichlet unit theorem for `K` and `wβ` is nonzero. In other words, none of the terms in this sequence can be an element of the zero norm in the ring of integers. This is an important result as it ensures that the sequence elements don't "vanish" under the norm operation.
More concisely: For any number field `K`, infinite place `wβ`, natural number `B`, and natural number `n`, the norm of the `n`-th term in the Dirichlet unit sequence of `K` and `wβ` is nonzero, provided the Minkowski bound is less than the product of the fudge factor and `B`.
|
NumberField.Units.dirichletUnitTheorem.seq_decreasing
theorem NumberField.Units.dirichletUnitTheorem.seq_decreasing :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (wβ : NumberField.InfinitePlace K) {B : β}
(hB : NumberField.mixedEmbedding.minkowskiBound K 1 < β(NumberField.mixedEmbedding.convexBodyLTFactor K) * βB)
{n m : β},
n < m β
β (w : NumberField.InfinitePlace K),
w β wβ β
w ββ(NumberField.Units.dirichletUnitTheorem.seq K wβ hB m) <
w ββ(NumberField.Units.dirichletUnitTheorem.seq K wβ hB n)
This theorem, named `NumberField.Units.dirichletUnitTheorem.seq_decreasing`, states a property about a sequence in the context of number fields. Specifically, for any number field `K`, and an infinite place `wβ` of the field `K` and a natural number `B` such that NumberField's Minkowski Bound `K` 1 is less than `convexBodyLTFactor K` times `B`, if `n` and `m` are natural numbers with `n` less than `m`, then for any other infinite place `w` distinct from `wβ`, the `m`th term of the Dirichlet unit theorem sequence at `w` is strictly less than the `n`th term at the same place. In other words, the sequence is strictly decreasing at all infinite places other than `wβ`.
More concisely: For any number field `K`, infinite place `wβ`, natural number `B`, and distinct infinite places `w`, if the Minkowski bound of `K` is less than `convexBodyLTFactor K` times `B`, then the sequence of Dirichlet units at `w` is strictly decreasing for `n < m`.
|
NumberField.Units.dirichletUnitTheorem.exists_unit
theorem NumberField.Units.dirichletUnitTheorem.exists_unit :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (wβ : NumberField.InfinitePlace K),
β u, β (w : NumberField.InfinitePlace K), w β wβ β (w ββu).log < 0
The theorem `NumberField.Units.dirichletUnitTheorem.exists_unit` states that for any type `K` with a field structure and a number field structure, and for any infinite place `wβ` in the number field, there exists a unit `u` such that for all other infinite places `w` that are different from `wβ`, the logarithm of the image of `u` under the place `w` is negative. In other words, there is a unique unit associated with each infinite place in the number field, and these units have the property that their logarithms are negative when mapped through any other infinite place. This forms part of the basis for the proof that this set of units is linearly independent over the real numbers.
More concisely: For any number field `K` with a given field and number field structure, and for each infinite place `wβ` in `K`, there exists a unit `u` such that the logarithm of `u` under all other infinite places `w` different from `wβ` is negative.
|
NumberField.Units.dirichletUnitTheorem.seq_ne_zero
theorem NumberField.Units.dirichletUnitTheorem.seq_ne_zero :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (wβ : NumberField.InfinitePlace K) {B : β}
(hB : NumberField.mixedEmbedding.minkowskiBound K 1 < β(NumberField.mixedEmbedding.convexBodyLTFactor K) * βB)
(n : β), ββ(NumberField.Units.dirichletUnitTheorem.seq K wβ hB n) β 0
This theorem states that for any number field `K`, any infinite place `wβ` of `K`, and any natural number `B` for which the Minkowski bound of `K` with respect to 1 is less than the product of the `convexBodyLTFactor` of `K` and `B` converted to a non-negative real number, the terms of the sequence defined by the Dirichlet unit theorem for `K`, `wβ`, and `hB` are all non-zero, regardless of the index `n` of the term in the sequence.
More concisely: For any number field `K`, infinite place `wβ`, and natural number `B` satisfying the Minkowski bound of `K` with respect to 1 being strictly less than the product of the convex body L-factor of `K` and `B`, all terms in the Dirichlet unit sequence for `K`, `wβ`, and `hB` are non-zero.
|
NumberField.Units.fun_eq_repr
theorem NumberField.Units.fun_eq_repr :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {x ΞΆ : (β₯(NumberField.ringOfIntegers K))Λ£}
{f : Fin (NumberField.Units.rank K) β β€},
ΞΆ β NumberField.Units.torsion K β
(x = ΞΆ * Finset.univ.prod fun i => NumberField.Units.fundSystem K i ^ f i) β
f = β((NumberField.Units.basisModTorsion K).repr (Additive.ofMul βx))
The theorem, `NumberField.Units.fun_eq_repr`, in Lean 4 states that for any number field `K`, any unit `x` and any root of unity `ΞΆ` in the ring of integers of `K`, and any function `f` from the finite set of the unit rank of `K` to the integers, if `ΞΆ` is in the torsion subgroup of the group of units and `x` can be expressed as the product of `ΞΆ` and the product over all elements of the universal set (under the assumption `Fintype Ξ±`) where each term is a unit from the fundamental system `fundSystem` raised to the power of the corresponding value in the function `f`, then `f` is equal to the representation of the unit `x` on `basisModTorsion` after being reinterpreted as an element of `Additive Ξ±`. In other words, the exponents that appear in the unique decomposition of a unit as the product of a root of unity and powers of the units in the fundamental system are given by the representation of the unit on `basisModTorsion`.
More concisely: For any number field `K`, unit `x`, root of unity `ΞΆ` in its ring of integers, and function `f` from the unit rank of `K`, if `ΞΆ` is a torsion unit and `x = ΞΆ β(u\_i^(f i))`, where `u\_i` are units from the fundamental system of `K`, then `f` is the representation of `x` on `basisModTorsion` as an element of `Additive Ξ±`.
|
NumberField.Units.dirichletUnitTheorem.seq_norm_le
theorem NumberField.Units.dirichletUnitTheorem.seq_norm_le :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (wβ : NumberField.InfinitePlace K) {B : β}
(hB : NumberField.mixedEmbedding.minkowskiBound K 1 < β(NumberField.mixedEmbedding.convexBodyLTFactor K) * βB)
(n : β), ((Algebra.norm β€) β(NumberField.Units.dirichletUnitTheorem.seq K wβ hB n)).natAbs β€ B
This theorem, `NumberField.Units.dirichletUnitTheorem.seq_norm_le`, states that for any number field `K`, any infinite place `wβ` of `K`, and any natural number `B`, if the Minkowski bound of `K` for `1` is less than the product of `B` and the fudge factor that appears in the formula for the volume of `convexBodyLT`, then for any natural number `n`, the absolute value of the determinant of the multiplication by the `n`-th term of the sequence associated with Dirichlet's Unit Theorem in `K`, `wβ`, and `hB` (where this sequence is viewed as an integer) is less or equal to `B`.
Mathematically, if we denote by `seq` the sequence associated with Dirichlet's Unit Theorem in `K`, `wβ`, and `hB`, and by `norm` the function that sends an element to its norm (the determinant of the matrix representation of multiplication by this element), it's saying that for all `n`, the absolute value of `norm(seq(n))` is at most `B`.
More concisely: For any number field `K`, infinite place `wβ`, natural number `B`, if the Minkowski bound of `K` for `1` is less than `B` times the fudge factor, then the absolute value of the determinant of the `n`-th term in the sequence associated with Dirichlet's Unit Theorem is less or equal to `B` for all natural numbers `n`.
|
NumberField.Units.exist_unique_eq_mul_prod
theorem NumberField.Units.exist_unique_eq_mul_prod :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (β₯(NumberField.ringOfIntegers K))Λ£),
β! ΞΆe, x = βΞΆe.1 * Finset.univ.prod fun i => NumberField.Units.fundSystem K i ^ ΞΆe.2 i
**Dirichlet's Unit Theorem** states that for any given number field `K` and any unit `x` of the ring of integers of `K`, there exists a unique pair `(ΞΆ, e)` such that `x` can be expressed as the product of a root of unity `ΞΆ` and the product of the powers of the units of a fundamental system (given by function `fundSystem`) of `K`. The powers are indexed by the universal finite set of the given type.
More concisely: For any number field `K` and unit `x` of its ring of integers, there exists a unique root of unity `ΞΆ` and a unique expression `x = ΞΆ β (u^n)_{n in finset.univ}`, where `u` is a fundamental system of units of `K`.
|
NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top
theorem NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top :
β (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
Submodule.span β β(NumberField.Units.unitLattice K) = β€
This theorem states that for any number field `K`, the span over the real numbers of the lattice formed by the image of the logarithmic embedding, referred as `NumberField.Units.unitLattice K`, is equal to the entire space, denoted by `β€`. In other words, this theorem is asserting that the mentioned lattice spans the entire real number space for any given number field `K`.
More concisely: For any number field `K`, the logarithmic embedding of `NumberField.Units.unitLattice K` spans the real numbers, i.e., their span equals the entire real number space.
|