feat(NumberField/CanonicalEmbedding): define the plusPart of a set

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -237,6 +237,18 @@ instance : NoAtoms (volume : Measure (mixedSpace K)) := by
       pi_noAtoms ⟨w, not_isReal_iff_isComplex.mp hw⟩
     exact prod.instNoAtoms_snd
 
+variable {K} in
+open Classical in
+/-- The set of points in the mixedSpace that are equal to `0` at a fixed (real) place has
+volume zero. -/
+theorem volume_eq_zero (w : {w // IsReal w}) :
+    volume ({x : mixedSpace K | x.1 w = 0}) = 0 := by
+  let A : AffineSubspace ℝ (mixedSpace K) :=
+    Submodule.toAffineSubspace (Submodule.mk ⟨⟨{x | x.1 w = 0}, by aesop⟩, rfl⟩ (by aesop))
+  convert Measure.addHaar_affineSubspace volume A fun h ↦ ?_
+  have : 1 ∈ A := h ▸ Set.mem_univ _
+  simp [A] at this
+
 end Measure
 
 section commMap
@@ -771,30 +783,31 @@ end integerLattice
 
 noncomputable section plusPart
 
+open ContinuousLinearEquiv
+
 variable {K} (s : Set {w : InfinitePlace K // IsReal w})
 
 open Classical in
 /-- Let `s` be a set of real places, define the continuous linear equiv of the mixed space that
 swaps sign at places in `s` and leaves the rest unchanged. -/
 def negAt :
     (mixedSpace K) ≃L[ℝ] (mixedSpace K) :=
-  (ContinuousLinearEquiv.piCongrRight
-    fun w ↦ if w ∈ s then ContinuousLinearEquiv.neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prod
-      (ContinuousLinearEquiv.refl ℝ _)
+  (piCongrRight fun w ↦ if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ).prod
+    (ContinuousLinearEquiv.refl ℝ _)
 
 variable {s}
 
 @[simp]
 theorem negAt_apply_of_isReal_and_mem (x : mixedSpace K) {w : {w // IsReal w}} (hw : w ∈ s) :
     (negAt s x).1 w = - x.1 w := by
-  simp_rw [negAt, ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.piCongrRight_apply,
-    if_pos hw, ContinuousLinearEquiv.neg_apply]
+  simp_rw [negAt, ContinuousLinearEquiv.prod_apply, piCongrRight_apply, if_pos hw,
+    ContinuousLinearEquiv.neg_apply]
 
 @[simp]
 theorem negAt_apply_of_isReal_and_not_mem (x : mixedSpace K) {w : {w // IsReal w}} (hw : w ∉ s) :
     (negAt s x).1 w = x.1 w := by
-  simp_rw [negAt, ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.piCongrRight_apply,
-    if_neg hw, ContinuousLinearEquiv.refl_apply]
+  simp_rw [negAt, ContinuousLinearEquiv.prod_apply, piCongrRight_apply, if_neg hw,
+    ContinuousLinearEquiv.refl_apply]
 
 @[simp]
 theorem negAt_apply_of_isComplex (x : mixedSpace K) (w : {w // IsComplex w}) :
@@ -835,7 +848,6 @@ theorem norm_negAt [NumberField K] (x : mixedSpace K) :
     mixedEmbedding.norm (negAt s x) = mixedEmbedding.norm x :=
   norm_eq_of_normAtPlace_eq (fun w ↦ normAtPlace_negAt _ _ w)
 
-open ContinuousLinearEquiv in
 /-- `negAt` is its own inverse. -/
 @[simp]
 theorem negAt_symm :
@@ -862,6 +874,126 @@ theorem negAt_signSet_apply_of_isReal (x : mixedSpace K) (w : {w // IsReal w}) :
 theorem negAt_signSet_apply_of_isComplex (x : mixedSpace K) (w : {w // IsComplex w}) :
     (negAt (signSet x) x).2 w = x.2 w := rfl
 
+variable (A : Set (mixedSpace K))
+
+variable (s) in
+ /-- `negAt s A` is also equal to the preimage of `A` by `negAt s`. This fact is used to simplify
+ some proofs. -/
+ theorem negAt_preimage :
+    negAt s ⁻¹' A = negAt s '' A := by
+  rw [ContinuousLinearEquiv.image_eq_preimage, negAt_symm]
+
+/-- The `plusPart` of a subset `A` of the `mixedSpace` is the set of points in `A` that are
+positive at all real places. -/
+abbrev plusPart : Set (mixedSpace K) := A ∩ {x | ∀ w, 0 < x.1 w}
+
+theorem neg_of_mem_negA_plusPart {x : mixedSpace K} (hx : x ∈ negAt s '' (plusPart A))
+    {w : {w // IsReal w}} (hw : w ∈ s) :
+    x.1 w < 0 := by
+  obtain ⟨y, hy, rfl⟩ := hx
+  rw [negAt_apply_of_isReal_and_mem _ hw, neg_lt_zero]
+  exact hy.2 w
+
+ theorem pos_of_not_mem_negAt_plusPart {x : mixedSpace K} (hx : x ∈ negAt s '' (plusPart A))
+    {w : {w // IsReal w}} (hw : w ∉ s) :
+    0 < x.1 w := by
+  obtain ⟨y, hy, rfl⟩ := hx
+  rw [negAt_apply_of_isReal_and_not_mem _ hw]
+  exact hy.2 w
+
+ /-- The images of `plusPart` by `negAt` are pairwise disjoint. -/
+ theorem disjoint_negAt_plusPart : Pairwise (Disjoint on (fun s ↦ negAt s '' (plusPart A))) := by
+  classical
+  intro s t hst
+  refine Set.disjoint_left.mpr fun _ hx hx' ↦ ?_
+  obtain ⟨w, hw | hw⟩ : ∃ w, (w ∈ s ∧ w ∉ t) ∨ (w ∈ t ∧ w ∉ s) := by
+    exact Set.symmDiff_nonempty.mpr hst
+  · exact lt_irrefl _ <|
+      (neg_of_mem_negA_plusPart A hx hw.1).trans (pos_of_not_mem_negAt_plusPart A hx' hw.2)
+  · exact lt_irrefl _ <|
+      (neg_of_mem_negA_plusPart A hx' hw.1).trans (pos_of_not_mem_negAt_plusPart A hx hw.2)
+
+-- We will assume from now that `A` is symmetric at real places
+variable  (hA : ∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A)
+
+open Classical in
+include hA in
+theorem mem_negAt_plusPart_of_mem {x : mixedSpace K} (hx₁ : x ∈ A) (hx₂ : ∀ w, x.1 w ≠ 0) :
+    x ∈ negAt s '' (plusPart A) ↔ (∀ w, w ∈ s → x.1 w < 0) ∧ (∀ w, w ∉ s → x.1 w > 0) := by
+  refine ⟨fun hx ↦ ⟨fun _ hw ↦ neg_of_mem_negA_plusPart A hx hw,
+      fun _ hw ↦ pos_of_not_mem_negAt_plusPart A hx hw⟩,
+      fun ⟨h₁, h₂⟩ ↦ ⟨(fun w ↦ |x.1 w|, x.2), ⟨(hA x).mp hx₁, fun w ↦ abs_pos.mpr (hx₂ w)⟩, ?_⟩⟩
+  ext w
+  · by_cases hw : w ∈ s
+    · simp only [negAt_apply_of_isReal_and_mem _ hw, abs_of_neg (h₁ w hw), neg_neg]
+    · simp only [negAt_apply_of_isReal_and_not_mem _ hw, abs_of_pos (h₂ w hw)]
+  · rfl
+
+include hA in
+/-- Assume that `A`  is symmetric at real places then, the union of the images of `plusPart`
+by `negAt` and of the set of elements of `A` that are zero at at least one real place
+is equal to `A`. -/
+theorem iUnion_negAt_plusPart_union :
+    (⋃ s, negAt s '' (plusPart A)) ∪ (A ∩ (⋃ w, {x | x.1 w = 0})) = A := by
+  ext x
+  rw [Set.mem_union, Set.mem_inter_iff, Set.mem_iUnion, Set.mem_iUnion]
+  refine ⟨?_, fun h ↦ ?_⟩
+  · rintro (⟨s, ⟨x, ⟨hx, _⟩, rfl⟩⟩ | h)
+    · simp_rw (config := {singlePass := true}) [hA, negAt_apply_abs_of_isReal, negAt_apply_snd]
+      rwa [← hA]
+    · exact h.left
+  · obtain hx | hx := exists_or_forall_not (fun w ↦ x.1 w = 0)
+    · exact Or.inr ⟨h, hx⟩
+    · refine Or.inl ⟨signSet x,
+        (mem_negAt_plusPart_of_mem A hA h hx).mpr ⟨fun w hw ↦ ?_, fun w hw ↦ ?_⟩⟩
+      · exact lt_of_le_of_ne hw (hx w)
+      · exact lt_of_le_of_ne (lt_of_not_ge hw).le (Ne.symm (hx w))
+
+open MeasureTheory
+
+variable [NumberField K]
+
+include hA in
+open Classical in
+theorem iUnion_negAt_plusPart_ae :
+    ⋃ s, negAt s '' (plusPart A) =ᵐ[volume] A := by
+  nth_rewrite 2 [← iUnion_negAt_plusPart_union A hA]
+  refine (MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm
+  exact measure_mono_null Set.inter_subset_right
+    (measure_iUnion_null_iff.mpr fun _ ↦ volume_eq_zero _)
+
+variable {A} in
+theorem measurableSet_plusPart (hm : MeasurableSet A) :
+    MeasurableSet (plusPart A) := by
+  convert_to MeasurableSet (A ∩ (⋂ w, {x | 0 < x.1 w}))
+  · ext; simp
+  · refine hm.inter (MeasurableSet.iInter fun _ ↦ ?_)
+    exact measurableSet_lt measurable_const ((measurable_pi_apply _).comp' measurable_fst)
+
+variable (s) in
+theorem measurableSet_negAt_plusPart (hm : MeasurableSet A) :
+    MeasurableSet (negAt s '' (plusPart A)) := by
+  rw [← negAt_preimage]
+  exact (measurableSet_plusPart hm).preimage (negAt s).continuous.measurable
+
+open Classical in
+/-- The image of the `plusPart` of `A` by `negAt` have all the same volume as `plusPart A`. -/
+theorem volume_negAt_plusPart (hm : MeasurableSet A) :
+    volume (negAt s '' (plusPart A)) = volume (plusPart A) := by
+  rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
+    volume_preserving_negAt.measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]
+
+include hA in
+open Classical in
+/-- If a subset `A` of the `mixedSpace` is symmetric at real places, then its volume is
+`2^ nrRealPlaces K` times the volume of its `plusPart`. -/
+theorem volume_eq_two_pow_mul_volume_plusPart (hm : MeasurableSet A) :
+    volume A = 2 ^ nrRealPlaces K * volume (plusPart A) := by
+  simp only [← measure_congr (iUnion_negAt_plusPart_ae A hA),
+    measure_iUnion (disjoint_negAt_plusPart A) (fun _ ↦ measurableSet_negAt_plusPart _ A hm),
+    volume_negAt_plusPart _ hm, tsum_fintype, sum_const, card_univ, Fintype.card_set, nsmul_eq_mul,
+    Nat.cast_pow, Nat.cast_ofNat, nrRealPlaces]
+
 end plusPart
 
 end NumberField.mixedEmbedding