Error Thread for defining special type of gauss sums

Stream: new members

[Suryansh Shrivastava]

If I had to define a coercion instance from F^x to F , where F is a field, how do I go about doing it?

[Yaël Dillies]

There is docs#units.has_coe if you want inspiration.

[Kevin Buzzard]

Isn't that more than inspiration, isn't that the claim that the instance is already there?

[Yaël Dillies]

Well, I don't know if Suryansh is working with our units or a hand-rolled version!

[Suryansh Shrivastava]

Yeah, I have to define coercion between C^x to C, so maybe that will work.

[Suryansh Shrivastava]

Also, is there a way to convert n: \N to n : \Z in the following code :-

import number_theory.legendre_symbol.add_character
import number_theory.legendre_symbol.zmod_char
import algebra.char_p.char_and_card
import field_theory.finite.trace
import number_theory.cyclotomic.basic
import data.zmod.basic
import data.complex.basic
import ring_theory.roots_of_unity
import algebra.group_power.basic
import data.complex.basic
noncomputable theory
open add_char
open_locale big_operators
open_locale classical
open_locale complex_conjugate
universes u v w
variables {F : Type u} [field F] [fintype F] (ζ_p : ℂˣ) [ fact (is_primitive_root ζ_p (ring_char F)) ]


lemma ζ_p_pow_eq_one(n : ℕ ): ζ_p^((n % (ring_char F)) ) = ζ_p^(n) := by
begin

end

lemma ζ_p_helper (n : ℤ ): ζ_p^((n % (ring_char F)) ) = ζ_p^(n) := by
begin
  rw ←  mul_inv_eq_one,
  rw ← zpow_neg ζ_p n,
  rw ← zpow_add ζ_p,
  rw  is_primitive_root.zpow_eq_one_iff_dvd (fact.out (is_primitive_root ζ_p (ring_char F))) ,
  rw ← int.modeq_zero_iff_dvd,
  have h1 : 0 = n + -n := by ring,
  rw h1,
  apply int.modeq.add_right,
  apply int.mod_modeq,
end

[Suryansh Shrivastava]

I have proved the second one but how do I prove the first one?

[Alex J. Best]

Can you post the imports too to make a #mwe? I'd guess something like simpa using ζ_p_helper n but have no idea as I can't run the code

[Suryansh Shrivastava]

import number_theory.legendre_symbol.add_character
import number_theory.legendre_symbol.zmod_char
import algebra.char_p.char_and_card
import field_theory.finite.trace
import number_theory.cyclotomic.basic
import data.zmod.basic
import data.complex.basic
import ring_theory.roots_of_unity
import algebra.group_power.basic
import data.complex.basic
noncomputable theory
open add_char
open_locale big_operators
open_locale classical
open_locale complex_conjugate
universes u v w
variables {F : Type u} [field F] [fintype F] (ζ_p : ℂˣ) [ fact (is_primitive_root ζ_p (ring_char F)) ]

[Alex J. Best]

So yeah simpa using ζ_p_helper ζ_p n, works, this is basically a short way of doing something like

  have := ζ_p_helper ζ_p n,
  simp at this,
  assumption,
  apply_instance,
  apply_instance,

[Suryansh Shrivastava]

okay so simp seems pretty nice in tying up these things,

[Suryansh Shrivastava]

Say, I have a summation

def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x))


def gauss_sum' (χ : mul_char F ℂ ) : ℂ := ∑' x : F,  -(add_char' ζ_p x)* (χ x)

We know that additive inverses exist in our field, so how will we substitute x by -x in our sum?

[Suryansh Shrivastava]

like If I want to show equivalence between the above statement and

def gauss_sum' (χ : mul_char F ℂ ) : ℂ := ∑' x : F,  -(add_char' ζ_p (-x))* (χ (-x))

How do I go about doing that?

[Eric Wieser]

Can you make a mwe?

[Suryansh Shrivastava]

What's a MWE?

[Martin Dvořák]

#mwe

[Suryansh Shrivastava]

import number_theory.legendre_symbol.add_character
import number_theory.legendre_symbol.zmod_char
import algebra.char_p.char_and_card
import field_theory.finite.trace
import number_theory.cyclotomic.basic
import data.zmod.basic
import data.complex.basic
import ring_theory.roots_of_unity
import algebra.group_power.basic
import data.complex.basic
import analysis.normed.field.basic
import data.pnat.defs
noncomputable theory
/-!
# Modified Gauss sums

We define the Gauss sum associated to a multiplicative and an additive
character of a finite field and prove some results about them.

## Main definition


Here, let 𝔽 = 𝔽_q be a finite field with q elements(q = p^f ) and let χ ζ_p be a fixed primitive root of unity and let T be the trace from 𝔽 to
ℤ/pℤ. Define
 ψ : 𝔽 → ℂ^× , ψ(x) = ζ_p^T(x)
 and now we define χ as a multiplicative character with these domains.
 𝔽^× → ℂ^×
We extend χ to all of 𝔽 by setting χ(0) = 0(even if χ is a trivial character).
-/
open add_char
open_locale big_operators
open_locale classical
open_locale complex_conjugate
universes u v w
-- variables (f : ℕ)
variables {F : Type u} [field F] [fintype F] (ζ_p : ℂˣ) [ fact (is_primitive_root ζ_p (ring_char F)) ]

def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x))


def gauss_sum' (χ : mul_char F ℂ ) : ℂ := ∑' x : F,  -(add_char' ζ_p x)* (χ x)

[Kevin Buzzard]

Not answering your question, but your variables have no solution. If you have a finite field of characteristic p then you can't have an element of order p in its multiplicative group

[Alex J. Best]

It looks fine to me @Kevin Buzzard are you sure (or can you explain more)? zeta is a complex number

[Eric Wieser]

That's not a #mwe because it doesn't include the e; there's no sorry that is your question!

[Eric Wieser]

I also suspect you could improve on the m aspect; what's the essence of your question? Is it really about all of add_char, primitive roots, and infinite sums all at the same time? Or can you make a simpler mwe that only uses one of those things?

[Kevin Buzzard]

Alex J. Best said:

It looks fine to me Kevin Buzzard are you sure (or can you explain more)? zeta is a complex number

Oh sorry, I'm a fool, that'll teach me to not read properly. Objection retracted!

[Kevin Buzzard]

I'll try and say something more helpful this time. Suryansh -- the idea of a mwe is that you ask the question you want to ask, in Lean. For example instead of saying "how do I prove this lemma", you say "how do I fill in this sorry", and you write code containing the sorry which I can just cut and paste and which works at my end without any alterations. And the less code I have to copy, the better.

Often, when making good mwes, people find that they can answer their own question themselves. It's for this and other reasons that we encourage this way of asking questions on this site.

[Suryansh Shrivastava]

Oh my apologies, actually my code seemed a lot larger, for it to be contained in a single block, is it fine if I I write my code in more blocks.

[Suryansh Shrivastava]

instance char_p_non_zero : ne_zero (ring_char F) :=
{out :=  begin
  intro h,
  haveI : fact (ring_char F).prime := ⟨char_p.char_is_prime F _⟩,
  exact nat.prime.ne_zero (fact.out (ring_char F).prime) h,
end}

lemma ζ_p_helper_help (n : ℤ ): ζ_p^((n % (ring_char F)) ) = ζ_p^(n) := by
begin
  rw ←  mul_inv_eq_one,
  rw ← zpow_neg ζ_p n,
  rw ← zpow_add ζ_p,
  rw  is_primitive_root.zpow_eq_one_iff_dvd (fact.out (is_primitive_root ζ_p (ring_char F))) ,
  rw ← int.modeq_zero_iff_dvd,
  have h1 : 0 = n + -n := by ring,
  rw h1,
  apply int.modeq.add_right,
  apply int.mod_modeq,
end

lemma ζ_p_helper(n : ℕ ): ζ_p^((n % (ring_char F)) ) = ζ_p^(n) := by
begin
  simpa using ζ_p_helper_help ζ_p n,
end

lemma add_char'_mul_property (a : F) (x : F ): add_char' ζ_p (a + x) = add_char' ζ_p a * add_char' ζ_p x := by
begin
  unfold add_char',
  simp,
  haveI : fact (ring_char F).prime := ⟨char_p.char_is_prime F _⟩,
  rw [zmod.val_add ],
  rw[← pow_add],
  rw[← ζ_p_helper ζ_p ((algebra.trace (zmod (ring_char F)) F a).val + (algebra.trace (zmod (ring_char F)) F x).val)],
  assumption,
  assumption,
end


def conjugate (x : ℂˣ) : ℂ := conj (x.val)

[Suryansh Shrivastava]

lemma ζ_p_helper_add (n : ℤ )(x : F): conjugate (ζ_p^n) = (ζ_p^(-n)).val := by
begin
  unfold conjugate,
  simp[conj],
  have h1 : (ζ_p)^(ring_char F) = 1 := by
  {
    apply is_primitive_root.pow_eq_one,
    apply fact.out (is_primitive_root ζ_p (ring_char F)),
  },
  have h2 : ‖(ζ_p).val‖  = 1 := by
  {
    have h3 : ring_char F > 0 := by
    {
      haveI : fact (ring_char F).prime := ⟨char_p.char_is_prime F _⟩,
      exact nat.prime.pos (fact.out (ring_char F).prime),
    },
    set r := (ring_char F).to_pnat' with h4,
    have h5 : ((ζ_p).val)^(↑r) = 1 := by
    {
      rw  h4,
      simp,
      rw [nat.to_pnat',nat.succ_pnat],
      rw pnat.mk_coe,
      rw nat.succ_pred_eq_of_pos h3,
      rw [←units.coe_pow ζ_p (ring_char F),← units.coe_one ,units.eq_iff.mpr h1],
    },
    apply norm_one_of_pow_eq_one h5,
  },
  rw complex.inv_def,
  have h3 : ‖ ((ζ_p).val)^n ‖ = 1 := by
  {
    rw [norm_zpow , h2],
    simp,
  },
  simp at h3,
  rw ← complex.mul_self_abs,
  simp[h3],
end

lemma ζ_p_help_add' (n : ℕ  )(x : F): conjugate (ζ_p^n) = (ζ_p^(- int.of_nat (n) )).val := by
begin
  simpa using ζ_p_helper_add ζ_p n x,
end



lemma add_char'_conjugate (x : F ):  conjugate ( add_char' ζ_p x) = (add_char' ζ_p (-x)).val := by
begin
  unfold add_char',
  rw ζ_p_help_add' ζ_p (algebra.trace (zmod (ring_char F)) F x).val x,
  simp,
  sorry,
end


def conj_mul_char' (χ : mul_char F ℂ ) :mul_char F ℂ :=
{ to_fun := by {classical, exact λ x, conj (χ x) },
  map_nonunit' := by { classical, exact λ x hx, by simpa using χ.map_nonunit hx },
  map_one' := by {
    classical,
    rw[map_one],
    simp,
  },
  map_mul' := by {
    classical,
    intros x y,
    rw[map_mul],
    simp,
   }
}

[Suryansh Shrivastava]

lemma gauss_sum_1 (χ : mul_char F ℂ ) : conj (gauss_sum' ζ_p χ) =  (χ(-1)) * (gauss_sum' ζ_p (conj_mul_char' (χ)) )  := by
begin
  unfold gauss_sum',
  simp,
  rw[is_R_or_C.conj_tsum],
  sorry,
end

I am trying to solve this problem and I think I might have all the machinery required except for the substitution that we need here

[Kevin Buzzard]

So the thing about a minimal working example is that you don't include all lemmas which you don't need, and you make it all fit into one code block so that the people who are going to help you can just cut and paste one code block.

[Kevin Buzzard]

I'm trying to explain to you how to ask an effective question.

[Suryansh Shrivastava]

Oh, my apologies. Maybe this code will work?

import number_theory.legendre_symbol.add_character
import number_theory.legendre_symbol.zmod_char
import algebra.char_p.char_and_card
import field_theory.finite.trace
import number_theory.cyclotomic.basic
import data.zmod.basic
import data.complex.basic
import ring_theory.roots_of_unity
import algebra.group_power.basic
import data.complex.basic
import analysis.normed.field.basic
import data.pnat.defs
noncomputable theory
open add_char
open zmod
open mul_char
open_locale big_operators
open_locale classical
open_locale complex_conjugate
universes u v w
variables {F : Type u} [field F] [fintype F] (ζ_p : ℂˣ) [ fact (is_primitive_root ζ_p (ring_char F)) ]
def add_char'(x : F) : ℂˣ  :=
  ζ_p^( zmod.val (algebra.trace (zmod (ring_char F)) F x))
lemma practice(χ : mul_char F ℂ ) : ∑' x : F,  -(add_char' ζ_p x).val* (χ x) = ∑' x : F,  -(add_char' ζ_p (-x))* ( χ (-x)) := by
begin
  sorry
end

[Eric Wieser]

Nice, that checks off "working" and "example"; can you see how you might make it more "minimal"?

[Kevin Buzzard]

yeah, I think those imports can be cut down a bit :-) But I can try to answer the question anyway! First you'll need some lemma saying chi(-x)=chi(-1)*chi(x). Then you'll need a lemma saying how add_char' zeta_p (-x) is related to add_char' zeta_p x. Then you simp_rw these lemmas because you want to apply them under a binder so rw won't work. And then it will hopefully be easy.

[Eric Wieser]

Isn't the argument just "reverse the direction of the sum"?

[Kevin Buzzard]

Oh! Sorry yes! That's a much better way to do it!

[Eric Wieser]

... which would be much more obvious once you remove all the irrelevant details

[Eric Wieser]

@Suryansh Shrivastava /@Suryansh Shrivastava, the reason I'm not answering your question exactly is that if you distill your question enough then library_search should be able to answer it for you

[Kevin Buzzard]

This is the question you want to ask.

import tactic
import analysis.complex.basic

open_locale big_operators

example {F : Type*} [field F] [fintype F] (f : F → ℂ) : ∑' x : F, f x = ∑' x : F, f (-x) := sorry

[Kevin Buzzard]

And you can check that this is the question you want to ask by changing example to lemma foo and then checking that you can use foo to solve your actual problem (and if you can't then you need to modify the example until it solves your problem)

[Kevin Buzzard]

Wait -- what? Why are you using ∑'?

[Kevin Buzzard]

Can you confirm that you are only doing finite sums? Life wil be much easier if you use ∑

[Eric Wieser]

I lied about library_search finding it; the tsum version can be proven as

import analysis.complex.basic

example {F : Type*} [field F] [fintype F] (f : F → ℂ) : ∑' x : F, f x = ∑' x : F, f (-x) :=
((equiv.neg _).tsum_eq _).symm

[Eric Wieser]

For ∑ instead of ∑'

The finite version is (fintype.sum_equiv (equiv.neg _) _ _ $ λ _, rfl).symm, see docs#fintype.sum_equiv

[Suryansh Shrivastava]

Kevin Buzzard said:

This is the question you want to ask.

import tactic
import analysis.complex.basic

open_locale big_operators

example {F : Type*} [field F] [fintype F] (f : F → ℂ) : ∑' x : F, f x = ∑' x : F, f (-x) := sorry

Yeah, I think that's the most succinct way to formalize my question.
Kevin Buzzard said:

Wait -- what? Why are you using ∑'?

Actually, later on, I had to use this , so how do I find a finite analog of this lemma? Or do I need to prove it?

[Kevin Buzzard]

Try formalising just the statement you want to know the proof of (i.e. make a minimal working example of precisely the abstract statement you need), and using library_search?

[Suryansh Shrivastava]

Oh, right, maybe I got it. I will update you guys with my progress