vector and MOD

Stream: new members

[liu]

How to modify it?

import Mathlib
example(p:ℕ )(h1:p≥7∧ Nat.prime p):∑ i in Finset.range p-1 (i+1)⁻¹*(i+2)⁻¹%p≡2[MOD p] :=by sorry
example(u v w:Vector ℝ )(h1:u.norm=3)(h2:v.norm=4)(h3:w.norm=5)(h4:u+v+w=0):u·v+v·w+w·u=-25 :=by sorry

[Kevin Buzzard]

What's the problem? (I'm on mobile) If there's an error can you post the error?

[liu]

[
屏幕截图 2025-02-09 185118.png
屏幕截图 2025-02-09 185132.png

[Kevin Buzzard]

You probably need open scoped BigOperators or something to make the sum notation work. Just look in mathlib itself to see the syntax. My memory is that in changed to \in recently

[liu]

Then what about the second one?

[Ruben Van de Velde]

What's the dot supposed to mean?

[liu]

This is the operator for the dot product of vectors.

[Ruben Van de Velde]

Not in lean, but neither does Vector mean what you think it does, nor does u.norm. Are you just writing random code hoping that lean makes sense of it?

[Ruben Van de Velde]

In any case, for the first line, lean tells you it's looking for a comma. It's the comma after the set you're summing over that's missing

[liu]

Then how should I write it?

[Chris Wong]

Where did you get this code from?

[liu]

AI，haha

[Chris Wong]

I would avoid AI. There is not enough Lean code in the training data for AI to actually understand the language, so it gets many things wrong.

[liu]

I think so.

[Chris Wong]

You can read Mathematics in Lean to see how linear algebra works: https://leanprover-community.github.io/mathematics_in_lean/C09_Linear_Algebra.html

[liu]

I didn't see any content about the norm of vectors here.

[Aaron Liu]

What is the mathematical idea you are trying to express?

[liu]

I'm formalizing this problem description.I don't know how to represent the norm of this vector. I tried using \||, but it reported an error.

[liu]

屏幕截图 2025-02-09 212124.png

[Ruben Van de Velde]

Probably the question you need answered first is "how do I declare a vector"

[liu]

I don't know how to declare

[liu]

Are there any relevant tutorial links?

[Aaron Liu]

What kind of vector do you want?

[liu]

For example, vectors in the plane rectangular coordinate system.

[Aaron Liu]

This is my guess at what you want, does this work for you?

import Mathlib

example (u v w : EuclideanSpace ℝ (Fin 2)) (hu : ‖u‖ = 3) (hv : ‖v‖ = 4) (hw : ‖w‖ = 5)
    (huvw : u + v + w = 0) : u ⬝ᵥ v + v ⬝ᵥ w + w ⬝ᵥ u = -25 := by
  sorry

[liu]

It's really helpful. How did you learn this? The content about "mathematics in Lean" in existing materials isn't in - depth enough. For some problems, I often can't find the answers I want. Could you recommend some professional Lean tutorials? I'm in great need of them.

[Luigi Massacci]

liu said:

Are there any relevant tutorial links?

This is covered by #mil in the Linear Algebra section

[Luigi Massacci]

for norms, the part about normed spaces

[Chris Wong]

That's the same book I linked before...

[liu]

I have another question. I really don't understand why the := sign causes an error.

import Mathlib
example(p:ℕ )(h1:p≥7∧ Nat.prime p):∑ i ∈  Finset.range p-1 (i+1)⁻¹*(i+2)⁻¹%p≡2[MOD p]:=by sorry

[Aaron Liu]

liu said:

It's really helpful. How did you learn this?

Mostly just looking on loogle and moogle to find the things I want, and I have also spent some time reading the mathlib4 docs, and also working through Formalizing Mathematics was helpful to see a lot of different parts of mathlib.

[Aaron Liu]

liu said:

I have another question. I really don't understand why the := sign causes an error.

import Mathlib
example(p:ℕ )(h1:p≥7∧ Nat.prime p):∑ i ∈  Finset.range p-1 (i+1)⁻¹*(i+2)⁻¹%p≡2[MOD p]:=by sorry

You problem is that you started the ∑ notation but didn't separate the thing being summed over from the thing being summed up, so when the parser runs into := it gives up and throws an error.
The correct notation is ∑ i ∈ finset, value (note the comma).

[liu]

But I used the comma, and it still reported an error.

[Aaron Liu]

What was the error?

[liu]

屏幕截图 2025-02-09 222433.png

[Aaron Liu]

You have a different error now.
Nat.prime does not exist, you might have been thinking of docs#Nat.Prime.
Finset.range p-1 groups as (Finset.range p)-1, if you want Finset.range (p-1) then you need to add parentheses.
When taking the ⁻¹, you need to be in a number system that supports it, like ℚ or ℝ. Try adding some type annotations to force this.

[Chris Wong]

With the inverse, they might be thinking of the finite field mod p.

[Aaron Liu]

In that case, use ZMod.

import Mathlib

example (p : ℕ) (h : 7 ≤ p) (hp : Nat.Prime p) :
    ∑ i ∈ Finset.range (p - 1), (i + 1 : ZMod p)⁻¹ * (i + 2 : ZMod p)⁻¹ = 2 := by
  sorry

[liu]

Amazing! Where did you look up this information?

[Eric Wieser]

@liu , please read #backticks rather than posting screenshots

[liu]

@Eric Wieser I just want to show the error,so I post screenshots

[Eric Wieser]

liu said:

AI，haha

If you want to use AI, I recommend doing so only after you've learnt the basics first. Then you can use things like leansearch and moogle which use AI-based search to help you find theorems and functions.

[liu]

@Eric Wieser Can you give me the website URL of Moogle?

[Yaël Dillies]

Click here :point_right: #moogle

[Yaël Dillies]

liu said:

Eric Wieser I just want to show the error,so I post screenshots

It's great to want to show the errors, but it's much better if we can reproduce them. Click here :point_right: #mwe to see what we mean

[liu]

I've encountered a new problem. How can I formalize this problem description?
屏幕截图 2025-02-09 233630.png

[liu]

Why do I get an error when defining fun2, and why does Set1.ncard also cause an error?

import Mathlib
def fun1(x:ℝ):ℝ :=|x|
def fun2(x:ℝ ):ℝ :=-x*x+35/4
example(x:ℤ )(y:ℤ )(Set1:Finset ℤ )(h1:Set1={(x,y)|y≤ fun2 x ∧ y≥  fun1 x}):Set1.ncard=29:=by sorry

[Aaron Liu]

import Mathlib

def fun1 (x : ℝ) : ℝ := |x|

-- Division on the reals is noncomputable,
-- unless you want to start passing around proofs of nonzero (trust me, you don't).
noncomputable def fun2 (x : ℝ) : ℝ := -x * x + 35 / 4
-- def fun2 (x : ℝ) : ℝ := -x * x + (35 / 4 : ℚ)

example (x y : ℤ) (Set1 : Finset ℤ)
    -- This parses as `y ≤ (fun2 x ∧ y ≥ fun1 x)` for reasons I cannot explain.
    -- A more serious issue is that `Set1` is a `Finset ℤ` while `{(x, y) | ...}` is a `Set (_ × _)`,
    -- and integers are not the same as pairs of something.
    (h1 : Set1 = {(x, y) | y ≤ fun2 x ∧ y ≥ fun1 x}) :
    -- `Set1` is a `Finset ℤ`, so `Set1.ncard` is looking for `Finset.ncard`, which doesn't exist.
    -- Try `Set1.card` instead?
    Set1.ncard = 29 := by sorry

[liu]

I don't understang : A more serious issue is that Set1 is a Finset ℤ while {(x, y) | ...} is a Set (_ × _),

[Ruben Van de Velde]

A set of integers can not contain pairs

[Ruben Van de Velde]

Perhaps you meant Set1 : Finset (\Z \times \Z)

[liu]

Whether I follow the method in the comments or change 35/4 to 8.75, I still get an error.

def fun1 (x : ℝ) : ℝ := |x|
-- Division on the reals is noncomputable,
def fun2 (x : ℝ) : ℝ := -x * x + (35/4:ℚ)
-- def fun2 (x : ℝ) : ℝ := -x * x + (35 / 4 : ℚ)
example (x y : ℤ) (Set1 : Finset (ℤ×ℤ ))
    (h1 : Set1 = {(x, y) | y ≤ fun2 x ∧ y ≥ fun1 x}) :
    Set1.card = 29 := by sorry

[Aaron Liu]

The elaborator is struggling to add coercions here, you might need to help it a little.

example (x y : ℤ) (Set1 : Finset (ℤ × ℤ))
    (h1 : Set1.toSet = {(x, y) | (y : ℤ) ≤ fun2 (x : ℤ) ∧ y ≥ fun1 x}) :
    Set1.card = 29 := by sorry

[Chris Wong]

Why are we dealing with Real and Set at all?

[Chris Wong]

If we work within Rat and Finset, then the problem can be solved by decide.