feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero…

…_mem_ringOfIntegers_lt (#5650)

This PR proves the following result: 
```lean
theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowski_bound K < volume (convex_body_lt K f)) :
     ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w 
```
where `f : InfinitePlace K → ℝ≥0` and `convex_body_lt K f` is the set of points `x` such that `‖x w‖ < f w` for all infinite places `w`. This is a key result in the proof of Dirichlet's unit theorem #5960

Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

@@ -3,6 +3,9 @@ Copyright (c) 2022 Xavier Roblot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
+import Mathlib.Algebra.Module.Zlattice
+import Mathlib.MeasureTheory.Group.GeometryOfNumbers
+import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
 import Mathlib.NumberTheory.NumberField.Embeddings
 import Mathlib.RingTheory.Discriminant
 
@@ -25,6 +28,16 @@ the vector `(φ x)` indexed by `φ : K →+* ℂ`.
 image of the ring of integers by the canonical embedding and any ball centered at `0` of finite
 radius is finite.
 
+* `mixedEmbedding`: the ring homomorphism from `K →+* ({ w // IsReal w } → ℝ) ×
+({ w // IsComplex w } → ℂ)` that sends `x ∈ K` to `(φ_w x)_w` where `φ_w` is the embedding
+associated to the infinite place `w`. In particular, if `w` is real then `φ_w : K →+* ℝ` and, if
+`w` is complex, `φ_w` is an arbitrary choice between the two complex embeddings defining the place
+`w`.
+
+* `exists_ne_zero_mem_ringOfIntegers_lt`: let `f : InfinitePlace K → ℝ≥0`, if the product
+`∏ w, f w` is large enough, then there exists a nonzero algebraic integer `a` in `K` such that
+`w a < f w` for all infinite places `w`.
+
 ## Tags
 
 number field, infinite places
@@ -145,3 +158,275 @@ theorem mem_span_latticeBasis [NumberField K] (x : (K →+* ℂ) → ℂ) :
   rfl
 
 end NumberField.canonicalEmbedding
+
+namespace NumberField.mixedEmbedding
+
+open NumberField NumberField.InfinitePlace NumberField.ComplexEmbedding FiniteDimensional
+
+/-- The space `ℝ^r₁ × ℂ^r₂` with `(r₁, r₂)` the signature of `K`. -/
+local notation "E" K =>
+  ({w : InfinitePlace K // IsReal w} → ℝ) × ({w : InfinitePlace K // IsComplex w} → ℂ)
+
+/-- The mixed embedding of a number field `K` of signature `(r₁, r₂)` into `ℝ^r₁ × ℂ^r₂`. -/
+noncomputable def _root_.NumberField.mixedEmbedding : K →+* (E K) :=
+  RingHom.prod (Pi.ringHom fun w => embedding_of_isReal w.prop)
+    (Pi.ringHom fun w => w.val.embedding)
+
+instance [NumberField K] :  Nontrivial (E K) := by
+  obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
+  obtain hw | hw := w.isReal_or_isComplex
+  · have : Nonempty {w : InfinitePlace K // IsReal w} := ⟨⟨w, hw⟩⟩
+    exact nontrivial_prod_left
+  · have : Nonempty {w : InfinitePlace K // IsComplex w} := ⟨⟨w, hw⟩⟩
+    exact nontrivial_prod_right
+
+protected theorem finrank [NumberField K] : finrank ℝ (E K) = finrank ℚ K := by
+  classical
+  rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const,
+    Finset.card_univ, ← card_real_embeddings, Algebra.id.smul_eq_mul, mul_comm,
+    ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
+    Nat.add_sub_of_le (Fintype.card_subtype_le _)]
+
+theorem _root_.NumberField.mixedEmbedding_injective [NumberField K] :
+    Function.Injective (NumberField.mixedEmbedding K) := by
+  exact RingHom.injective _
+
+section commMap
+
+/-- The linear map that makes `canonicalEmbedding` and `mixedEmbedding` commute, see
+`commMap_canonical_eq_mixed`. -/
+noncomputable def commMap : ((K →+* ℂ) → ℂ) →ₗ[ℝ] (E K) :=
+{ toFun := fun x => ⟨fun w => (x w.val.embedding).re, fun w => x w.val.embedding⟩
+  map_add' := by
+    simp only [Pi.add_apply, Complex.add_re, Prod.mk_add_mk, Prod.mk.injEq]
+    exact fun _ _ => ⟨rfl, rfl⟩
+  map_smul' := by
+    simp only [Pi.smul_apply, Complex.real_smul, Complex.mul_re, Complex.ofReal_re,
+      Complex.ofReal_im, zero_mul, sub_zero, RingHom.id_apply, Prod.smul_mk, Prod.mk.injEq]
+    exact fun _ _ => ⟨rfl, rfl⟩ }
+
+theorem commMap_apply_of_isReal (x : (K →+* ℂ) → ℂ) {w : InfinitePlace K} (hw : IsReal w) :
+  (commMap K x).1 ⟨w, hw⟩ = (x w.embedding).re := rfl
+
+theorem commMap_apply_of_isComplex (x : (K →+* ℂ) → ℂ) {w : InfinitePlace K} (hw : IsComplex w) :
+  (commMap K x).2 ⟨w, hw⟩ = x w.embedding := rfl
+
+@[simp]
+theorem commMap_canonical_eq_mixed (x : K) :
+    commMap K (canonicalEmbedding K x) = mixedEmbedding K x := by
+  simp only [canonicalEmbedding, commMap, LinearMap.coe_mk, AddHom.coe_mk, Pi.ringHom_apply,
+    mixedEmbedding, RingHom.prod_apply, Prod.mk.injEq]
+  exact ⟨rfl, rfl⟩
+
+/-- This is a technical result to ensure that the image of the `ℂ`-basis of `ℂ^n` defined in
+`canonicalEmbedding.latticeBasis` is a `ℝ`-basis of `ℝ^r₁ × ℂ^r₂`,
+see `mixedEmbedding.latticeBasis`. -/
+theorem disjoint_span_commMap_ker [NumberField K]:
+    Disjoint (Submodule.span ℝ (Set.range (canonicalEmbedding.latticeBasis K)))
+      (LinearMap.ker (commMap K)) := by
+  refine LinearMap.disjoint_ker.mpr (fun x h_mem h_zero => ?_)
+  replace h_mem : x ∈ Submodule.span ℝ (Set.range (canonicalEmbedding K)) := by
+    refine (Submodule.span_mono ?_) h_mem
+    rintro _ ⟨i, rfl⟩
+    exact ⟨integralBasis K i, (canonicalEmbedding.latticeBasis_apply K i).symm⟩
+  ext1 φ
+  rw [Pi.zero_apply]
+  by_cases hφ : IsReal φ
+  · rw [show x φ = (x φ).re by
+      rw [eq_comm, ← Complex.conj_eq_iff_re, canonicalEmbedding.conj_apply _ h_mem,
+        ComplexEmbedding.isReal_iff.mp hφ], ← Complex.ofReal_zero]
+    congr
+    rw [← embedding_mk_eq_of_isReal hφ, ← commMap_apply_of_isReal K x ⟨φ, hφ, rfl⟩]
+    exact congrFun (congrArg (fun x => x.1) h_zero) ⟨InfinitePlace.mk φ, _⟩
+  · have := congrFun (congrArg (fun x => x.2) h_zero) ⟨InfinitePlace.mk φ, ⟨φ, hφ, rfl⟩⟩
+    cases embedding_mk_eq φ with
+    | inl h => rwa [← h, ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
+    | inr h =>
+        apply RingHom.injective (starRingEnd ℂ)
+        rwa [canonicalEmbedding.conj_apply _ h_mem, ← h, map_zero,
+          ← commMap_apply_of_isComplex K x ⟨φ, hφ, rfl⟩]
+
+end commMap
+
+section integerLattice
+
+open Module FiniteDimensional
+
+/-- A `ℝ`-basis of `ℝ^r₁ × ℂ^r₂` that is also a `ℤ`-basis of the image of `𝓞 K`. -/
+noncomputable def latticeBasis [NumberField K] :
+    Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℝ (E K) := by
+  classical
+    -- We construct an `ℝ`-linear independent family from the image of
+    -- `canonicalEmbedding.lattice_basis` by `comm_map`
+    have := LinearIndependent.map (LinearIndependent.restrict_scalars
+      (by { simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective })
+      (canonicalEmbedding.latticeBasis K).linearIndependent)
+      (disjoint_span_commMap_ker K)
+    -- and it's a basis since it has the right cardinality
+    refine basisOfLinearIndependentOfCardEqFinrank this ?_
+    rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_prod, finrank_pi,
+      finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, Finset.card_univ,
+      ← card_real_embeddings, Algebra.id.smul_eq_mul, mul_comm, ← card_complex_embeddings,
+      ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
+      Nat.add_sub_of_le (Fintype.card_subtype_le _)]
+
+@[simp]
+theorem latticeBasis_apply [NumberField K] (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
+    latticeBasis K i = (mixedEmbedding K) (integralBasis K i) := by
+  simp only [latticeBasis, coe_basisOfLinearIndependentOfCardEqFinrank, Function.comp_apply,
+    canonicalEmbedding.latticeBasis_apply, integralBasis_apply, commMap_canonical_eq_mixed]
+
+theorem mem_span_latticeBasis [NumberField K] (x : (E K)) :
+    x ∈ Submodule.span ℤ (Set.range (latticeBasis K)) ↔ x ∈ mixedEmbedding K '' (𝓞 K) := by
+  rw [show Set.range (latticeBasis K) =
+      (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (integralBasis K)) by
+    rw [← Set.range_comp]; exact congrArg Set.range (funext (fun i => latticeBasis_apply K i))]
+  rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
+  rw [show (Submodule.span ℤ (Set.range (integralBasis K)) : Set K) = 𝓞 K by
+    ext; exact mem_span_integralBasis K]
+  rfl
+
+end integerLattice
+
+section convexBodyLt
+
+open Metric ENNReal NNReal
+
+variable (f : InfinitePlace K → ℝ≥0)
+
+/-- The convex body defined by `f`: the set of points `x : E` such that `‖x w‖ < f w` for all
+infinite places `w`. -/
+abbrev convexBodyLt : Set (E K) :=
+  (Set.univ.pi (fun w : { w : InfinitePlace K // IsReal w } => ball 0 (f w))) ×ˢ
+  (Set.univ.pi (fun w : { w : InfinitePlace K // IsComplex w } => ball 0 (f w)))
+
+theorem convexBodyLt_mem {x : K} :
+    mixedEmbedding K x ∈ (convexBodyLt K f) ↔ ∀ w : InfinitePlace K, w x < f w := by
+  simp_rw [mixedEmbedding, RingHom.prod_apply, Set.mem_prod, Set.mem_pi, Set.mem_univ,
+    forall_true_left, mem_ball_zero_iff, Pi.ringHom_apply, ← Complex.norm_real,
+    embedding_of_isReal_apply, Subtype.forall, ← ball_or_left, ← not_isReal_iff_isComplex, em,
+    forall_true_left, norm_embedding_eq]
+
+theorem convexBodyLt_symmetric (x : E K) (hx : x ∈ (convexBodyLt K f)) :
+    -x ∈ (convexBodyLt K f) := by
+  simp only [Set.mem_prod, Prod.fst_neg, Set.mem_pi, Set.mem_univ, Pi.neg_apply,
+    mem_ball_zero_iff, norm_neg, Real.norm_eq_abs, forall_true_left, Subtype.forall,
+    Prod.snd_neg, Complex.norm_eq_abs, hx] at hx ⊢
+  exact hx
+
+theorem convexBodyLt_convex : Convex ℝ (convexBodyLt K f) :=
+  Convex.prod (convex_pi (fun _ _ => convex_ball _ _)) (convex_pi (fun _ _ => convex_ball _ _))
+
+open Classical Fintype MeasureTheory MeasureTheory.Measure BigOperators
+
+-- See: https://github.com/leanprover/lean4/issues/2220
+local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)
+
+variable [NumberField K]
+
+/-- The fudge factor that appears in the formula for the volume of `convexBodyLt`. -/
+noncomputable abbrev convexBodyLtFactor : ℝ≥0∞ :=
+  (2 : ℝ≥0∞) ^ card {w : InfinitePlace K // IsReal w} *
+    volume (ball (0 : ℂ) 1) ^ card {w : InfinitePlace K // IsComplex w}
+
+theorem convexBodyLtFactor_lt_pos : 0 < (convexBodyLtFactor K) := by
+  refine mul_pos (NeZero.ne _) ?_
+  exact ENNReal.pow_ne_zero (ne_of_gt (measure_ball_pos _ _ (by norm_num))) _
+
+theorem convexBodyLtFactor_lt_top : (convexBodyLtFactor K) < ⊤ := by
+  refine mul_lt_top ?_ ?_
+  · exact ne_of_lt (pow_lt_top (lt_top_iff_ne_top.mpr two_ne_top) _)
+  · exact ne_of_lt (pow_lt_top measure_ball_lt_top _)
+
+/-- 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 convexBodyLt_volume :
+    volume (convexBodyLt K f) = (convexBodyLtFactor K) * ∏ w, (f w) ^ (mult w) := by
+  calc
+    _ = (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (2 * (f x.val))) *
+          ∏ x : {w // InfinitePlace.IsComplex w}, volume (ball (0 : ℂ) 1) *
+            ENNReal.ofReal (f x.val) ^ 2 := by
+      simp_rw [volume_eq_prod, prod_prod, volume_pi, pi_pi, Real.volume_ball]
+      conv_lhs =>
+        congr; next => skip
+        congr; next => skip
+        ext i; rw [addHaar_ball _ _ (by exact (f i).prop), Complex.finrank_real_complex, mul_comm,
+          ENNReal.ofReal_pow (by exact (f i).prop)]
+    _ = (↑2 ^ card {w : InfinitePlace K // InfinitePlace.IsReal w} *
+          (∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val))) *
+          (volume (ball (0 : ℂ) 1) ^ card {w : InfinitePlace K // IsComplex w} *
+          (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by
+      simp_rw [ofReal_mul (by norm_num : 0 ≤ (2 : ℝ)), Finset.prod_mul_distrib, Finset.prod_const,
+        Finset.card_univ, ofReal_ofNat]
+    _ = (convexBodyLtFactor K) * ((∏ x : {w // InfinitePlace.IsReal w}, ENNReal.ofReal (f x.val)) *
+        (∏ x : {w // IsComplex w}, ENNReal.ofReal (f x.val) ^ 2)) := by ring
+    _ = (convexBodyLtFactor K) * ∏ w, (f w) ^ (mult w) := by
+      simp_rw [mult, pow_ite, pow_one, Finset.prod_ite, ofReal_coe_nnreal, not_isReal_iff_isComplex,
+        coe_mul, coe_finset_prod, ENNReal.coe_pow]
+      congr 2
+      · refine (Finset.prod_subtype (Finset.univ.filter _) ?_ (fun w => (f w : ℝ≥0∞))).symm
+        exact fun _ => by simp only [Finset.mem_univ, forall_true_left, Finset.mem_filter, true_and]
+      · refine (Finset.prod_subtype (Finset.univ.filter _) ?_ (fun w => (f w : ℝ≥0∞) ^ 2)).symm
+        exact fun _ => by simp only [Finset.mem_univ, forall_true_left, Finset.mem_filter, true_and]
+
+variable {f}
+
+/-- 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`. -/
+theorem adjust_f {w₁ : InfinitePlace K} (B : ℝ≥0) (hf : ∀ w, w ≠ w₁→ f w ≠ 0) :
+    ∃ g : InfinitePlace K → ℝ≥0, (∀ w, w ≠ w₁ → g w = f w) ∧ ∏ w, (g w) ^ mult w = B := by
+  let S := ∏ w in Finset.univ.erase w₁, (f w) ^ mult w
+  refine ⟨Function.update f w₁ ((B * S⁻¹) ^ (mult w₁ : ℝ)⁻¹), ?_, ?_⟩
+  · exact fun w hw => Function.update_noteq hw _ f
+  · rw [← Finset.mul_prod_erase Finset.univ _ (Finset.mem_univ w₁), Function.update_same,
+      Finset.prod_congr rfl fun w hw => by rw [Function.update_noteq (Finset.ne_of_mem_erase hw)],
+      ← NNReal.rpow_nat_cast, ← NNReal.rpow_mul, inv_mul_cancel, NNReal.rpow_one, mul_assoc,
+      inv_mul_cancel, mul_one]
+    · rw [Finset.prod_ne_zero_iff]
+      exact fun w hw => pow_ne_zero _ (hf w (Finset.ne_of_mem_erase hw))
+    · rw [mult]; split_ifs <;> norm_num
+
+end convexBodyLt
+
+section minkowski
+
+open MeasureTheory MeasureTheory.Measure Classical NNReal ENNReal FiniteDimensional Zspan
+
+variable [NumberField K]
+
+/-- The bound that appears in Minkowski Convex Body theorem, see
+`MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure`. -/
+noncomputable def minkowskiBound : ℝ≥0∞ :=
+  volume (fundamentalDomain (latticeBasis K)) * 2 ^ (finrank ℝ (E K))
+
+theorem minkowskiBound_lt_top : minkowskiBound K < ⊤ := by
+  refine mul_lt_top ?_ ?_
+  · exact ne_of_lt (fundamentalDomain_isBounded (latticeBasis K)).measure_lt_top
+  · exact ne_of_lt (pow_lt_top (lt_top_iff_ne_top.mpr two_ne_top) _)
+
+variable {f : InfinitePlace K → ℝ≥0}
+
+/-- Assume that `f : InfinitePlace K → ℝ≥0` is such that
+`minkowskiBound K < 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 integer `a` in `𝓞 K` such
+that `w a < f w` for all infinite places `w`. -/
+theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowskiBound K < volume (convexBodyLt K f)) :
+    ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w := by
+  have : @IsAddHaarMeasure (E K) _ _ _ volume := prod.instIsAddHaarMeasure volume volume
+  have h_fund := Zspan.isAddFundamentalDomain (latticeBasis K) volume
+  have : Countable (Submodule.span ℤ (Set.range (latticeBasis K))).toAddSubgroup := by
+    change Countable (Submodule.span ℤ (Set.range (latticeBasis K)): Set (E K))
+    infer_instance
+  obtain ⟨⟨x, hx⟩, h_nzr, h_mem⟩ := exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure
+    h_fund h (convexBodyLt_symmetric K f) (convexBodyLt_convex K f)
+  rw [Submodule.mem_toAddSubgroup, mem_span_latticeBasis] at hx
+  obtain ⟨a, ha, rfl⟩ := hx
+  refine ⟨⟨a, ha⟩, ?_, (convexBodyLt_mem K f).mp h_mem⟩
+  rw [ne_eq, AddSubgroup.mk_eq_zero_iff, map_eq_zero, ← ne_eq] at h_nzr
+  exact Subtype.ne_of_val_ne h_nzr
+
+end minkowski
+
+end NumberField.mixedEmbedding