# Convex Bodies #

The file contains the definitions of several convex bodies lying in the space ℝ^r₁ × ℂ^r₂ associated to a number field of signature K and proves several existence theorems by applying Minkowski Convex Body Theorem to those.

## Main definitions and results #

• NumberField.mixedEmbedding.convexBodyLT: The set of points x such that ‖x w‖ < f w for all infinite places w with f : InfinitePlace K → ℝ≥0.

• NumberField.mixedEmbedding.convexBodySum: The set of points x such that ∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B

• NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt: Let I be a fractional ideal of K. Assume that f is such that minkowskiBound K I < volume (convexBodyLT K f), then there exists a nonzero algebraic number a in I such that w a < f w for all infinite places w.

• NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le: Let I be a fractional ideal of K. Assume that B is such that minkowskiBound K I < volume (convexBodySum K B) (see convexBodySum_volume for the computation of this volume), then there exists a nonzero algebraic number a in I such that |Norm a| < (B / d) ^ d where d is the degree of K.

## Tags #

number field, infinite places

@[reducible, inline]
abbrev NumberField.mixedEmbedding.convexBodyLT (K : Type u_1) [] (f : ) :
Set (({ w : // w.IsReal }) × ({ w : // w.IsComplex }))

The convex body defined by f: the set of points x : E such that ‖x w‖ < f w for all infinite places w.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem NumberField.mixedEmbedding.convexBodyLT_mem (K : Type u_1) [] (f : ) {x : K} :
∀ (w : ), w x < (f w)
theorem NumberField.mixedEmbedding.convexBodyLT_neg_mem (K : Type u_1) [] (f : ) (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) (hx : ) :
@[reducible, inline]
noncomputable abbrev NumberField.mixedEmbedding.convexBodyLTFactor (K : Type u_1) [] [] :

The fudge factor that appears in the formula for the volume of convexBodyLT.

Equations
Instances For
theorem NumberField.mixedEmbedding.convexBodyLT_volume (K : Type u_1) [] (f : ) [] :
MeasureTheory.volume = * (∏ w : , f w ^ w.mult)

The volume of (ConvexBodyLt K f) where convexBodyLT K f is the set of points x such that ‖x w‖ < f w for all infinite places w.

theorem NumberField.mixedEmbedding.adjust_f (K : Type u_1) [] {f : } [] {w₁ : } (B : NNReal) (hf : ∀ (w : ), w w₁f w 0) :
∃ (g : ), (∀ (w : ), w w₁g w = f w) w : , g w ^ w.mult = B

This is a technical result: quite often, we want to impose conditions at all infinite places but one and choose the value at the remaining place so that we can apply exists_ne_zero_mem_ringOfIntegers_lt.

@[reducible, inline]
abbrev NumberField.mixedEmbedding.convexBodyLT' (K : Type u_1) [] (f : ) (w₀ : { w : // w.IsComplex }) :
Set (({ w : // w.IsReal }) × ({ w : // w.IsComplex }))

A version of convexBodyLT with an additional condition at a fixed complex place. This is needed to ensure the element constructed is not real, see for example exists_primitive_element_lt_of_isComplex.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem NumberField.mixedEmbedding.convexBodyLT'_mem (K : Type u_1) [] (f : ) (w₀ : { w : // w.IsComplex }) {x : K} :
(∀ (w : ), w w₀w x < (f w)) |((↑w₀).embedding x).re| < 1 |((↑w₀).embedding x).im| < (f w₀) ^ 2
theorem NumberField.mixedEmbedding.convexBodyLT'_neg_mem (K : Type u_1) [] (f : ) (w₀ : { w : // w.IsComplex }) (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) (hx : ) :
theorem NumberField.mixedEmbedding.convexBodyLT'_convex (K : Type u_1) [] (f : ) (w₀ : { w : // w.IsComplex }) :
@[reducible, inline]
noncomputable abbrev NumberField.mixedEmbedding.convexBodyLT'Factor (K : Type u_1) [] [] :

The fudge factor that appears in the formula for the volume of convexBodyLT'.

Equations
Instances For
theorem NumberField.mixedEmbedding.convexBodyLT'_volume (K : Type u_1) [] (f : ) (w₀ : { w : // w.IsComplex }) [] :
MeasureTheory.volume = * (∏ w : , f w ^ w.mult)
@[reducible, inline]
noncomputable abbrev NumberField.mixedEmbedding.convexBodySumFun {K : Type u_1} [] [] (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :

The function that sends x : ({w // IsReal w} → ℝ) × ({w // IsComplex w} → ℂ) to ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖. It defines a norm and it used to define convexBodySum.

Equations
• = w : , w.mult *
Instances For
theorem NumberField.mixedEmbedding.convexBodySumFun_apply {K : Type u_1} [] [] (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :
= w : , w.mult *
theorem NumberField.mixedEmbedding.convexBodySumFun_apply' {K : Type u_1} [] [] (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :
= w : { w : // w.IsReal }, x.1 w + 2 * w : { w : // w.IsComplex }, x.2 w
theorem NumberField.mixedEmbedding.convexBodySumFun_nonneg {K : Type u_1} [] [] (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :
theorem NumberField.mixedEmbedding.convexBodySumFun_neg {K : Type u_1} [] [] (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :
theorem NumberField.mixedEmbedding.convexBodySumFun_add_le {K : Type u_1} [] [] (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) (y : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :
theorem NumberField.mixedEmbedding.convexBodySumFun_smul {K : Type u_1} [] [] (c : ) (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :
theorem NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff {K : Type u_1} [] [] (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :
theorem NumberField.mixedEmbedding.norm_le_convexBodySumFun {K : Type u_1} [] [] (x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })) :
theorem NumberField.mixedEmbedding.convexBodySumFun_continuous (K : Type u_1) [] [] :
Continuous NumberField.mixedEmbedding.convexBodySumFun
@[reducible, inline]
abbrev NumberField.mixedEmbedding.convexBodySum (K : Type u_1) [] [] (B : ) :
Set (({ w : // w.IsReal }) × ({ w : // w.IsComplex }))

The convex body equal to the set of points x : E such that ∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero (K : Type u_1) [] [] {B : } (hB : B 0) :
MeasureTheory.volume = 0
theorem NumberField.mixedEmbedding.convexBodySum_mem (K : Type u_1) [] [] (B : ) {x : K} :
w : , w.mult * w x B
theorem NumberField.mixedEmbedding.convexBodySum_neg_mem (K : Type u_1) [] [] (B : ) {x : ({ w : // w.IsReal }) × ({ w : // w.IsComplex })} (hx : ) :
@[reducible, inline]
noncomputable abbrev NumberField.mixedEmbedding.convexBodySumFactor (K : Type u_1) [] [] :

The fudge factor that appears in the formula for the volume of convexBodyLt.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem NumberField.mixedEmbedding.convexBodySum_volume (K : Type u_1) [] [] (B : ) :
MeasureTheory.volume =
noncomputable def NumberField.mixedEmbedding.minkowskiBound (K : Type u_1) [] [] (I : ) :

The bound that appears in Minkowski Convex Body theorem, see MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure. See NumberField.mixedEmbedding.volume_fundamentalDomain_idealLatticeBasis_eq and NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis for the computation of volume (fundamentalDomain (idealLatticeBasis K)).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis (K : Type u_1) [] [] (I : ) :
MeasureTheory.volume = ENNReal.ofReal (FractionalIdeal.absNorm I) * MeasureTheory.volume
theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt (K : Type u_1) [] [] {f : } (I : ) (h : < MeasureTheory.volume ) :
aI, a 0 ∀ (w : ), w a < (f w)

Let I be a fractional ideal of K. Assume that f : InfinitePlace K → ℝ≥0 is such that minkowskiBound K I < volume (convexBodyLT K f) where convexBodyLT K f is the set of points x such that ‖x w‖ < f w for all infinite places w (see convexBodyLT_volume for the computation of this volume), then there exists a nonzero algebraic number a in I such that w a < f w for all infinite places w.

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt' (K : Type u_1) [] [] {f : } (I : ) (w₀ : { w : // w.IsComplex }) (h : < MeasureTheory.volume ) :
aI, a 0 (∀ (w : ), w w₀w a < (f w)) |((↑w₀).embedding a).re| < 1 |((↑w₀).embedding a).im| < (f w₀) ^ 2

A version of exists_ne_zero_mem_ideal_lt where the absolute value of the real part of a is smaller than 1 at some fixed complex place. This is useful to ensure that a is not real.

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt (K : Type u_1) [] [] {f : } (h : < MeasureTheory.volume ) :
∃ (a : ), a 0 ∀ (w : ), w a < (f w)

A version of exists_ne_zero_mem_ideal_lt for the ring of integers of K.

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt' (K : Type u_1) [] [] {f : } (w₀ : { w : // w.IsComplex }) (h : < MeasureTheory.volume ) :
∃ (a : ), a 0 (∀ (w : ), w w₀w a < (f w)) |((↑w₀).embedding a).re| < 1 |((↑w₀).embedding a).im| < (f w₀) ^ 2

A version of exists_ne_zero_mem_ideal_lt' for the ring of integers of K.

theorem NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal (K : Type u_1) [] [] {w₀ : } (hw₀ : w₀.IsReal) {B : NNReal} :
∃ (a : ), a = ∀ (w : ), w a < (max B 1)
theorem NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex (K : Type u_1) [] [] {w₀ : } (hw₀ : w₀.IsComplex) {B : NNReal} :
∃ (a : ), a = ∀ (w : ), w a < (1 + B ^ 2)
theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le (K : Type u_1) [] [] (I : ) {B : } (h : MeasureTheory.volume ) :
aI, a 0 | a| (B / ) ^

Let I be a fractional ideal of K. Assume that B : ℝ is such that minkowskiBound K I < volume (convexBodySum K B) where convexBodySum K B is the set of points x such that ∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B (see convexBodySum_volume for the computation of this volume), then there exists a nonzero algebraic number a in I such that |Norm a| < (B / d) ^ d where d is the degree of K.

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le (K : Type u_1) [] [] {B : } (h : MeasureTheory.volume ) :
∃ (a : ), a 0 | a| (B / ) ^