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) [Field K] (f : NumberField.InfinitePlace K → NNReal) : Set (({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // 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.

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

theorem NumberField.mixedEmbedding.convexBodyLT_neg_mem (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) (hx : x ∈ NumberField.mixedEmbedding.convexBodyLT K f) : -x ∈ NumberField.mixedEmbedding.convexBodyLT K f

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

instance NumberField.mixedEmbedding.instIsAddHaarMeasureProdForallSubtypeInfinitePlaceIsRealRealForallIsComplexComplexVolume (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.volume.IsAddHaarMeasure

Equations

• ⋯ = ⋯

instance NumberField.mixedEmbedding.instNoAtomsProdForallSubtypeInfinitePlaceIsRealRealForallIsComplexComplexVolume (K : Type u_1) [Field K] [NumberField K] : MeasureTheory.NoAtoms MeasureTheory.volume

Equations

• ⋯ = ⋯

@[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.

Equations

• NumberField.mixedEmbedding.convexBodyLTFactor K = 2 ^ NumberField.InfinitePlace.NrRealPlaces K * NNReal.pi ^ NumberField.InfinitePlace.NrComplexPlaces K

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

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

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

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

theorem NumberField.mixedEmbedding.convexBodyLT'_convex (K : Type u_1) [Field K] (f : NumberField.InfinitePlace K → NNReal) (w₀ : { w : NumberField.InfinitePlace K // w.IsComplex }) : Convex ℝ (NumberField.mixedEmbedding.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'.

Equations

• NumberField.mixedEmbedding.convexBodyLT'Factor K = 2 ^ (NumberField.InfinitePlace.NrRealPlaces K + 2) * NNReal.pi ^ (NumberField.InfinitePlace.NrComplexPlaces K - 1)

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

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

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

@[reducible, inline]

noncomputable abbrev NumberField.mixedEmbedding.convexBodySumFun {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // 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

• One or more equations did not get rendered due to their size.

theorem NumberField.mixedEmbedding.convexBodySumFun_nonneg {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : 0 ≤ NumberField.mixedEmbedding.convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_neg {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : NumberField.mixedEmbedding.convexBodySumFun (-x) = NumberField.mixedEmbedding.convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_add_le {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) (y : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : NumberField.mixedEmbedding.convexBodySumFun (x + y) ≤ NumberField.mixedEmbedding.convexBodySumFun x + NumberField.mixedEmbedding.convexBodySumFun y

theorem NumberField.mixedEmbedding.convexBodySumFun_smul {K : Type u_1} [Field K] [NumberField K] (c : ℝ) (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : NumberField.mixedEmbedding.convexBodySumFun (c • x) = |c| * NumberField.mixedEmbedding.convexBodySumFun x

theorem NumberField.mixedEmbedding.convexBodySumFun_eq_zero_iff {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : NumberField.mixedEmbedding.convexBodySumFun x = 0 ↔ x = 0

theorem NumberField.mixedEmbedding.norm_le_convexBodySumFun {K : Type u_1} [Field K] [NumberField K] (x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)) : ‖x‖ ≤ NumberField.mixedEmbedding.convexBodySumFun x

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

@[reducible, inline]

abbrev NumberField.mixedEmbedding.convexBodySum (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Set (({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // 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.

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

theorem NumberField.mixedEmbedding.convexBodySum_mem (K : Type u_1) [Field K] [NumberField K] (B : ℝ) {x : K} : (NumberField.mixedEmbedding K) x ∈ NumberField.mixedEmbedding.convexBodySum K B ↔ (Finset.univ.sum fun (w : NumberField.InfinitePlace K) => ↑w.mult * ↑w x) ≤ B

theorem NumberField.mixedEmbedding.convexBodySum_neg_mem (K : Type u_1) [Field K] [NumberField K] (B : ℝ) {x : ({ w : NumberField.InfinitePlace K // w.IsReal } → ℝ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ)} (hx : x ∈ NumberField.mixedEmbedding.convexBodySum K B) : -x ∈ NumberField.mixedEmbedding.convexBodySum K B

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

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

theorem NumberField.mixedEmbedding.convexBodySum_compact (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : IsCompact (NumberField.mixedEmbedding.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.

Equations

• One or more equations did not get rendered due to their size.

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

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

noncomputable def NumberField.mixedEmbedding.minkowskiBound (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.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)).

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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

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 : NumberField.InfinitePlace K → NNReal} (w₀ : { w : NumberField.InfinitePlace K // w.IsComplex }) (h : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑↑MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT' K f w₀)) : ∃ (a : NumberField.RingOfIntegers K), a ≠ 0 ∧ (∀ (w : NumberField.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₀ : NumberField.InfinitePlace K} (hw₀ : w₀.IsReal) {B : NNReal} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B) : ∃ (a : NumberField.RingOfIntegers K), ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : NumberField.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₀ : NumberField.InfinitePlace K} (hw₀ : w₀.IsComplex) {B : NNReal} (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLT'Factor K) * ↑B) : ∃ (a : NumberField.RingOfIntegers K), ℚ⟮↑a⟯ = ⊤ ∧ ∀ (w : NumberField.InfinitePlace K), w ↑a < (1 + ↑B ^ 2).sqrt

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