NormSignDilation.lean

1 import PaperX.NormSignArithmetic
2 import PaperX.NormSignResidueCounting
3 
4 /-! Arithmetic sign on positive dilations of the actual sign regions. -/
5 set_option autoImplicit false
6 noncomputable section
7 
8 namespace PaperX.NormSignArithmetic
9 open Set NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
10 open NormSignGeometry
11 open scoped Classical Pointwise
12 variable (K : Type*) [Field K] [NumberField K]
13 
14 theorem realProduct_smul (t : ℝ) (x : mixedSpace K) :
15     realProduct K (t • x) =
16       t ^ Fintype.card {w : InfinitePlace K // IsReal w} * realProduct K x := by
17   simp only [realProduct, Prod.smul_fst, Pi.smul_apply, smul_eq_mul,
18     Finset.prod_mul_distrib, Finset.prod_const, Finset.card_univ]
19 
20 theorem realProduct_pos_of_mem_smul_signCone {t : ℝ} (ht : 0 < t)
21     {x : mixedSpace K} (hx : x ∈ t • signCone K true) : 0 < realProduct K x := by
22   rcases hx with ⟨y, hy, rfl⟩
23   rw [realProduct_smul]
24   exact mul_pos (pow_pos ht _) hy.2
25 
26 theorem realProduct_neg_of_mem_smul_signCone {t : ℝ} (ht : 0 < t)
27     {x : mixedSpace K} (hx : x ∈ t • signCone K false) : realProduct K x < 0 := by
28   rcases hx with ⟨y, hy, rfl⟩
29   rw [realProduct_smul]
30   exact mul_neg_of_pos_of_neg (pow_pos ht _) (neg_pos.mp hy.2)
31 
32 theorem ne_zero_of_mem_smul_signCone {t : ℝ} (ht : 0 < t) {x : K}
33     {positive : Bool} (hx : mixedEmbedding K x ∈ t • signCone K positive) : x ≠ 0 := by
34   intro hzero
35   rcases hx with ⟨y, hy, he⟩
36   have he0 : t • y = 0 := by simpa only [hzero, map_zero] using he
37   have hy0 : y = 0 := (smul_eq_zero.mp he0).resolve_left (ne_of_gt ht)
38   subst y
39   have hp := fundamentalCone.normAtPlace_pos_of_mem hy.1.1
40     (Classical.arbitrary (InfinitePlace K))
41   simp at hp
42 
43 theorem toMixed_mem_smul_signCone {t : ℝ} {positive : Bool}
44     {x : euclidean.mixedSpace K} (hx : x ∈ t • signRegion K positive) :
45     euclidean.toMixed K x ∈ t • signCone K positive := by
46   rcases hx with ⟨y, hy, he⟩
47   refine ⟨euclidean.toMixed K y, hy, ?_⟩
48   simpa only [map_smul] using congrArg (euclidean.toMixed K) he
49 
50 theorem integer_norm_pos_of_mem_smul_signRegion {t : ℝ} (ht : 0 < t)
51     {x : 𝓞 K}
52     (hx : (euclidean.toMixed K).symm (mixedEmbedding K (x : K)) ∈
53       t • signRegion K true) : 0 < Algebra.norm ℤ x := by
54   have hm : mixedEmbedding K (x : K) ∈ t • signCone K true := by
55     simpa only [ContinuousLinearEquiv.apply_symm_apply] using toMixed_mem_smul_signCone K hx
56   have hne : x ≠ 0 := by
57     intro hzero
58     exact ne_zero_of_mem_smul_signCone K ht hm (congrArg (fun z : 𝓞 K => (z : K)) hzero)
59   exact (integer_norm_pos_iff K hne).mpr (realProduct_pos_of_mem_smul_signCone K ht hm)
60 
61 theorem integer_norm_neg_of_mem_smul_signRegion {t : ℝ} (ht : 0 < t)
62     {x : 𝓞 K}
63     (hx : (euclidean.toMixed K).symm (mixedEmbedding K (x : K)) ∈
64       t • signRegion K false) : Algebra.norm ℤ x < 0 := by
65   have hm : mixedEmbedding K (x : K) ∈ t • signCone K false := by
66     simpa only [ContinuousLinearEquiv.apply_symm_apply] using toMixed_mem_smul_signCone K hx
67   have hne : x ≠ 0 := by
68     intro hzero
69     exact ne_zero_of_mem_smul_signCone K ht hm (congrArg (fun z : 𝓞 K => (z : K)) hzero)
70   exact (integer_norm_neg_iff K hne).mpr (realProduct_neg_of_mem_smul_signCone K ht hm)
71 
72 end PaperX.NormSignArithmetic

Back to source controls