Convex Bodies

The file contains the definitions of several convex bodies lying in the mixed 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) [Field K] (f : InfinitePlace K → NNReal) : Set (mixedSpace K)

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

theorem NumberField.mixedEmbedding.convexBodyLT_mem (K : Type u_1) [Field K] (f : InfinitePlace K → NNReal) {x : K} : (mixedEmbedding K) x ∈ convexBodyLT K f ↔ ∀ (w : InfinitePlace K), w x < ↑(f w)

theorem NumberField.mixedEmbedding.convexBodyLT_neg_mem (K : Type u_1) [Field K] (f : InfinitePlace K → NNReal) (x : mixedSpace K) (hx : x ∈ convexBodyLT K f) : -x ∈ convexBodyLT K f

theorem NumberField.mixedEmbedding.convexBodyLT_convex (K : Type u_1) [Field K] (f : InfinitePlace K → NNReal) : Convex ℝ (convexBodyLT K f)

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.convexBodyLTFactor (K : Type u_1) [Field K] [NumberField K] : NNReal

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

theorem NumberField.mixedEmbedding.convexBodyLTFactor_ne_zero (K : Type u_1) [Field K] [NumberField K] : convexBodyLTFactor K ≠ 0

theorem NumberField.mixedEmbedding.one_le_convexBodyLTFactor (K : Type u_1) [Field K] [NumberField K] : 1 ≤ convexBodyLTFactor K

theorem NumberField.mixedEmbedding.convexBodyLT_volume (K : Type u_1) [Field K] (f : InfinitePlace K → NNReal) [NumberField K] : MeasureTheory.volume (convexBodyLT K f) = ↑(convexBodyLTFactor K) * ↑(∏ w : InfinitePlace K, 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) [Field K] {f : InfinitePlace K → NNReal} [NumberField K] {w₁ : InfinitePlace K} (B : NNReal) (hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0) : ∃ (g : InfinitePlace K → NNReal), (∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w : InfinitePlace K, 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) [Field K] (f : InfinitePlace K → NNReal) (w₀ : { w : InfinitePlace K // w.IsComplex }) : Set (mixedSpace K)

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.

theorem NumberField.mixedEmbedding.convexBodyLT'_mem (K : Type u_1) [Field K] (f : InfinitePlace K → NNReal) (w₀ : { w : InfinitePlace K // w.IsComplex }) {x : K} : (mixedEmbedding K) x ∈ convexBodyLT' K f w₀ ↔ (∀ (w : InfinitePlace K), 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) [Field K] (f : InfinitePlace K → NNReal) (w₀ : { w : InfinitePlace K // w.IsComplex }) (x : mixedSpace K) (hx : x ∈ convexBodyLT' K f w₀) : -x ∈ convexBodyLT' K f w₀

theorem NumberField.mixedEmbedding.convexBodyLT'_convex (K : Type u_1) [Field K] (f : InfinitePlace K → NNReal) (w₀ : { w : InfinitePlace K // w.IsComplex }) : Convex ℝ (convexBodyLT' K f w₀)

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.convexBodyLT'Factor (K : Type u_1) [Field K] [NumberField K] : NNReal

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

theorem NumberField.mixedEmbedding.convexBodyLT'Factor_ne_zero (K : Type u_1) [Field K] [NumberField K] : convexBodyLT'Factor K ≠ 0

theorem NumberField.mixedEmbedding.one_le_convexBodyLT'Factor (K : Type u_1) [Field K] [NumberField K] : 1 ≤ convexBodyLT'Factor K

theorem NumberField.mixedEmbedding.convexBodyLT'_volume (K : Type u_1) [Field K] (f : InfinitePlace K → NNReal) (w₀ : { w : InfinitePlace K // w.IsComplex }) [NumberField K] : MeasureTheory.volume (convexBodyLT' K f w₀) = ↑(convexBodyLT'Factor K) * ↑(∏ w : InfinitePlace K, f w ^ w.mult)

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.convexBodySumFun {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : ℝ

The function that sends x : mixedSpace K to ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖. It defines a norm and it used to define convexBodySum.

theorem NumberField.mixedEmbedding.convexBodySumFun_apply {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : convexBodySumFun x = ∑ w : InfinitePlace K, ↑w.mult * (normAtPlace w) x

theorem NumberField.mixedEmbedding.convexBodySumFun_apply' {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : convexBodySumFun x = ∑ w : { w : InfinitePlace K // w.IsReal }, ‖x.1 w‖ + 2 * ∑ w : { w : InfinitePlace K // w.IsComplex }, ‖x.2 w‖

theorem NumberField.mixedEmbedding.convexBodySumFun_nonneg {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : 0 ≤ convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_neg {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : convexBodySumFun (-x) = convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_add_le {K : Type u_1} [Field K] [NumberField K] (x y : mixedSpace K) : convexBodySumFun (x + y) ≤ convexBodySumFun x + convexBodySumFun y

theorem NumberField.mixedEmbedding.convexBodySumFun_smul {K : Type u_1} [Field K] [NumberField K] (c : ℝ) (x : mixedSpace K) : convexBodySumFun (c • x) = |c| * convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : convexBodySumFun x = 0 ↔ x = 0

theorem NumberField.mixedEmbedding.norm_le_convexBodySumFun {K : Type u_1} [Field K] [NumberField K] (x : mixedSpace K) : ‖x‖ ≤ convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_continuous (K : Type u_1) [Field K] [NumberField K] : Continuous convexBodySumFun

@[reducible, inline]

abbrev NumberField.mixedEmbedding.convexBodySum (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Set (mixedSpace K)

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

theorem NumberField.mixedEmbedding.convexBodySum_volume_eq_zero_of_le_zero (K : Type u_1) [Field K] [NumberField K] {B : ℝ} (hB : B ≤ 0) : MeasureTheory.volume (convexBodySum K B) = 0

theorem NumberField.mixedEmbedding.convexBodySum_mem (K : Type u_1) [Field K] [NumberField K] (B : ℝ) {x : K} : (mixedEmbedding K) x ∈ convexBodySum K B ↔ ∑ w : InfinitePlace K, ↑w.mult * ↑w x ≤ B

theorem NumberField.mixedEmbedding.convexBodySum_neg_mem (K : Type u_1) [Field K] [NumberField K] (B : ℝ) {x : mixedSpace K} (hx : x ∈ convexBodySum K B) : -x ∈ convexBodySum K B

theorem NumberField.mixedEmbedding.convexBodySum_convex (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Convex ℝ (convexBodySum K B)

theorem NumberField.mixedEmbedding.convexBodySum_isBounded (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Bornology.IsBounded (convexBodySum K B)

theorem NumberField.mixedEmbedding.convexBodySum_compact (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : IsCompact (convexBodySum K B)

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.convexBodySumFactor (K : Type u_1) [Field K] [NumberField K] : NNReal

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

theorem NumberField.mixedEmbedding.convexBodySumFactor_ne_zero (K : Type u_1) [Field K] [NumberField K] : convexBodySumFactor K ≠ 0

theorem NumberField.mixedEmbedding.convexBodySum_volume (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : MeasureTheory.volume (convexBodySum K B) = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ Module.finrank ℚ K

noncomputable def NumberField.mixedEmbedding.minkowskiBound (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : ENNReal

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)).

theorem NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : MeasureTheory.volume (ZSpan.fundamentalDomain (fractionalIdealLatticeBasis K I)) = ENNReal.ofReal ↑(FractionalIdeal.absNorm ↑I) * MeasureTheory.volume (ZSpan.fundamentalDomain (latticeBasis K))

theorem NumberField.mixedEmbedding.minkowskiBound_lt_top (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : minkowskiBound K I < ⊤

theorem NumberField.mixedEmbedding.minkowskiBound_pos (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) : 0 < minkowskiBound K I

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt (K : Type u_1) [Field K] [NumberField K] {f : InfinitePlace K → NNReal} (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (h : minkowskiBound K I < MeasureTheory.volume (convexBodyLT K f)) : ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : InfinitePlace K), 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) [Field K] [NumberField K] {f : InfinitePlace K → NNReal} (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) (w₀ : { w : InfinitePlace K // w.IsComplex }) (h : minkowskiBound K I < MeasureTheory.volume (convexBodyLT' K f w₀)) : ∃ a ∈ ↑I, a ≠ 0 ∧ (∀ (w : InfinitePlace K), 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) [Field K] [NumberField K] {f : InfinitePlace K → NNReal} (h : minkowskiBound K 1 < MeasureTheory.volume (convexBodyLT K f)) : ∃ (a : RingOfIntegers K), a ≠ 0 ∧ ∀ (w : InfinitePlace K), 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) [Field K] [NumberField K] {f : InfinitePlace K → NNReal} (w₀ : { w : InfinitePlace K // w.IsComplex }) (h : minkowskiBound K 1 < MeasureTheory.volume (convexBodyLT' K f w₀)) : ∃ (a : RingOfIntegers K), a ≠ 0 ∧ (∀ (w : InfinitePlace K), 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) [Field K] [NumberField K] {w₀ : InfinitePlace K} (hw₀ : w₀.IsReal) {B : NNReal} (hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B) : ∃ (a : RingOfIntegers K), ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < ↑(max B 1)

theorem NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex (K : Type u_1) [Field K] [NumberField K] {w₀ : InfinitePlace K} (hw₀ : w₀.IsComplex) {B : NNReal} (hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B) : ∃ (a : RingOfIntegers K), ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : InfinitePlace K), w ↑a < √(1 + ↑B ^ 2)

theorem NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (RingOfIntegers K)) K)ˣ) {B : ℝ} (h : minkowskiBound K I ≤ MeasureTheory.volume (convexBodySum K B)) : ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ (B / ↑(Module.finrank ℚ K)) ^ Module.finrank ℚ K

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) [Field K] [NumberField K] {B : ℝ} (h : minkowskiBound K 1 ≤ MeasureTheory.volume (convexBodySum K B)) : ∃ (a : RingOfIntegers K), a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(Module.finrank ℚ K)) ^ Module.finrank ℚ K