Documentation

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

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 #

Tags #

number field, infinite places

@[reducible, inline]
abbrev NumberField.mixedEmbedding.convexBodyLT (K : Type u_1) [Field K] (f : NumberField.InfinitePlace KNNReal) :
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.
Instances For
    @[reducible, inline]

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

    Equations
    Instances For

      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 KNNReal} [NumberField K] {w₁ : NumberField.InfinitePlace K} (B : NNReal) (hf : ∀ (w : NumberField.InfinitePlace K), w w₁f w 0) :
      ∃ (g : NumberField.InfinitePlace KNNReal), (∀ (w : NumberField.InfinitePlace K), w w₁g w = f w) 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 KNNReal) (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.
      Instances For
        theorem NumberField.mixedEmbedding.convexBodyLT'_mem (K : Type u_1) [Field K] (f : NumberField.InfinitePlace KNNReal) (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 KNNReal) (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₀) :
        @[reducible, inline]

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

        Equations
        Instances For
          @[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
          Instances For
            theorem NumberField.mixedEmbedding.convexBodySumFun_apply' {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 = w : { w : NumberField.InfinitePlace K // w.IsReal }, x.1 w + 2 * w : { w : NumberField.InfinitePlace K // w.IsComplex }, x.2 w
            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.
            Instances For
              @[reducible, inline]

              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

                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

                  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 KNNReal} (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₀)) :
                  aI, 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 KNNReal} (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.

                  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.