Help with geom_sum ite lemma

Stream: new members

[Junyan Xu]

1st sorry: obtain ⟨m, rfl⟩ := h_1,
2nd sorry: rw if_pos h_1, (goals accomplished)

btw, import all doesn't work for me and I had to squeeze it to

import data.complex.exponential
import analysis.special_functions.trigonometric.basic

[Eric Wieser]

import all is likely to make things like library_search timeout because it brings in far too many lemmas

[Junyan Xu]

On my end it just shows

file 'all' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

invalid import: all
could not resolve import: all

[Mauricio Collares]

all.lean needs to be generated first (by leanproject mk-all)

[Mark Gerads]

Thanks for the help. I used '_target/deps/mathlib/scripts/mk_all.sh' for my mk_all, which creates an 'all' which imports all of mathlib.
'leanproject mk-all' actually only imports what is in the '/src' folder of the current lean project.

[Kevin Buzzard]

One problem I've noticed with mk-all is that you make it and then you forget about it and then you pull new stuff and then the file breaks. I avoid it for this reason and others (e.g. it sometimes essentially disables library_search)

[Mark Gerads]

How do I solve this? ring, ring_nf, squeeze_simp do nothing.
image.png

[Junyan Xu]

This works

example (m n : ℕ) (h : n > 0) : (n : ℂ)⁻¹ * m * n = m :=
by { field_simp, rw mul_div_cancel, exact_mod_cast h.lt.ne.symm }

[Mark Gerads]

Almost done, but stuck on this part where the root of unity must be shown not equal to 1:
image.png

[Junyan Xu]

first rewrite by docs#complex.exp_eq_one_iff

[Mark Gerads]

Nice.

[Mark Gerads]

Stuck again. I need to do something with h_1, but don't know what.
image.png

[Mark Gerads]

The problem is at line 274.
RootOfUnityExponentialSum.lean

[Junyan Xu]

At line 270 you can do

    intro eq1, apply h_1,
    obtain ⟨m, he⟩ := complex.exp_eq_one_iff.1 eq1,
    use m.to_nat,

and I think you'll need to use docs#int.to_nat_of_nonneg at some point.

[Junyan Xu]

Oh sorry, it's best to rw ← int.coe_nat_dvd, use m,

[Mark Gerads]

And that is almost the same as 'he'. Normally, when something like 'he' is a goal, I would use the 'congr' tactic, but that doesn't work when the congruence is not in the goal?
image.png

[Junyan Xu]

You need to cancel a factor, and you need to show the factor is nonzero, so it's not congr; congr doesn't give you the reverse direction.

[Junyan Xu]

you can rewrite he by some comm/assoc lemmas and apply https://leanprover-community.github.io/mathlib_docs/algebra/group_with_zero/defs.html#mul_right_cancel%E2%82%80 to it

[Mark Gerads]

How does one show the computer 2 * ↑real.pi * I ≠ 0?

[Junyan Xu]

apply mul_ne_zero,

[Mark Gerads]

Doing the twice breaks the goal into ⊢ 2 ≠ 0,⊢ ↑real.pi ≠ 0, ⊢ I ≠ 0. norm_num gets rid of 2 ≠ 0, but not the other 2 inequalities.
Edit: found I_ne_zero and real.pi_ne_zero; the second needed norm_cast.

[Mark Gerads]

I've run into a new problem. I have the exact equation I need (h8), except it is the wrong type of equation; I need eq ℤ and have type eq ℂ. RootOfUnityExponentialSum.lean line 294
image.png

[Violeta Hernández]

Have you tried exact_mod_cast h8?

[Mark Gerads]

Thank you all for helping complete this lemma. :smile: :heart: :+1: :tada: :octopus: It is something required to prove my next attempted lemma, ruesNEqExpSum. I already foresee questions about interchanging an arbitrarily sized finset sum with a tsum infinite sum.