NumberField.mixedEmbedding.convexBodyLT_volume
theorem NumberField.mixedEmbedding.convexBodyLT_volume :
∀ (K : Type u_1) [inst : Field K] (f : NumberField.InfinitePlace K → NNReal) [inst_1 : NumberField K],
↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) =
↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑(Finset.univ.prod fun w => f w ^ w.mult)
This theorem relates to the computation of the volume of a specific type of convex body in a Number Field. Specifically, in a given Number Field `K`, for a function `f` that maps infinite places of `K` to nonnegative real numbers, the theorem states that the volume of the convex body defined as the set of points `x` such that the norm of `x` at each infinite place `w` is less than `f(w)` is equal to the product of a factor related to the number of real and complex places in `K` and the product over all elements `w` in a universal finite set of the `f(w)` raised to the power `w.mult`. Here, 'volume' is measured using the MeasureTheory volume, and infinite places refer to places associated with complex embeddings.
More concisely: In a Number Field `K`, the volume of the convex body defined as the set of points `x` with norm at each infinite place `w` less than `f(w)` equals the product of a constant related to the number of real and complex places in `K` and the product over all infinite places `w` of `f(w)` raised to the power of `w.mult` (measured using the MeasureTheory volume).
|
NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt
theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt :
∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {f : NumberField.InfinitePlace K → NNReal},
NumberField.mixedEmbedding.minkowskiBound K 1 <
↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f) →
∃ a ∈ NumberField.ringOfIntegers K, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w a < ↑(f w)
This theorem, named `NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt`, asserts that for any number field `K`, given a function `f` that maps each infinite place of `K` to a nonnegative real number, if the Minkowski bound of the mixed embedding of `K` with respect to 1 is strictly less than the Lebesgue measure of the convex body defined by `f`, then there exists an element `a` from the ring of integers of `K` such that `a` is nonzero and for every infinite place `w` of `K`, `w(a)` is strictly less than `f(w)`. In simpler terms, it asserts that under certain conditions, there exists a nonzero integer in the number field that is bounded above by the function `f` at every infinite place.
More concisely: Given a number field `K` and a function `f` mapping infinite places to nonnegative reals with the Minkowski bound of the mixed embedding strictly less than the Lebesgue measure of the corresponding convex body, there exists a nonzero integer `a` in `K` such that `w(a) < f(w)` for all infinite places `w` of `K`.
|
NumberField.mixedEmbedding.adjust_f
theorem NumberField.mixedEmbedding.adjust_f :
∀ (K : Type u_1) [inst : Field K] {f : NumberField.InfinitePlace K → NNReal} [inst_1 : NumberField K]
{w₁ : NumberField.InfinitePlace K} (B : NNReal),
(∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → f w ≠ 0) →
∃ g, (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → g w = f w) ∧ (Finset.univ.prod fun w => g w ^ w.mult) = B
This theorem, `NumberField.mixedEmbedding.adjust_f`, presents a technical result in the context of number theory. For a given number field `K` and a non-negative real number `B`, given a function `f` from the infinite places of `K` to the non-negative reals, if `f` is non-zero at every infinite place except possibly one (`w₁`), the theorem asserts the existence of another function `g` that matches `f` at all the infinite places except possibly `w₁`, and the product of `g(w)` raised to the multiplicity of `w` over all elements `w` of the universal finite set is equal to `B`.
More concisely: For a number field `K` and a non-negative real number `B`, if `f` is a function from the infinite places of `K` to the non-negative reals, which is non-zero at all but one place `w₁`, then there exists a function `g` such that the product of `g(w)` raised to the multiplicity of `w` for all `w` in the universal finite set equals `B`, and `g(w) = f(w)` for all infinite places `w` except possibly `w₁`.
|