## Stream: maths

### Topic: sensitivity conjecture

#### Johan Commelin (Aug 02 2019 at 05:54):

The sensitivity conjecture was 30 years old, and recently resolved. Can we formalise this? https://www.scottaaronson.com/blog/?p=4229

#### Johan Commelin (Aug 02 2019 at 06:16):

@Chris Hughes You've been doing a lot with matrices lately. Did you do things like row/column rank?

#### Johan Commelin (Aug 02 2019 at 06:17):

And how far did you get with the inverse matrix?

#### Chris Hughes (Aug 02 2019 at 07:55):

I used a noncomputable inverse in the end. I didn't use row and column rank either, but used the predicates has_left_inverse and has_right_inverse as well. Both of these look good enough for the sensitivity proof.

#### Johan Commelin (Aug 02 2019 at 07:58):

But this isn't in mathlib yet, right?

No.

#### Chris Hughes (Aug 02 2019 at 08:24):

It's a bit unfinished, that's why. It would be nicer to have a pseudoinverse that worked on rectangular matrices.

#### Reid Barton (Aug 02 2019 at 11:54):

I thought about this also. How easy is it to do these block matrix calculations appearing in the proof that $A_n = nI$ (and in the definition of $A_n$)?
This is another example where it's natural to consider a matrix with rows and columns indexed by a general finite type (in this case, the hypercube).

#### Reid Barton (Aug 02 2019 at 11:55):

Given what we have at the moment it might be easier to formulate the Knuth proof in terms of linear maps everywhere instead of matrices

#### Kevin Buzzard (Aug 02 2019 at 11:56):

@Chris Hughes the matrices in Knuth's proof are indexed by {0,1}^n

#### Chris Hughes (Aug 02 2019 at 12:06):

My matrix pequiv thing might help with the block matrix computations. You can concatenate matrices algebraically using something like
$\begin{pmatrix} a & b \end{pmatrix} \begin{pmatrix} 1 & 0 \\0 & 0 \end{pmatrix} + \begin{pmatrix} c & d \end{pmatrix} \begin{pmatrix} 0 & 0 \\0 & 1 \end{pmatrix} = \begin{pmatrix} a & b \\c & d \end{pmatrix}$

#### Chris Hughes (Aug 02 2019 at 12:12):

In the proof you'll probably end up with some big ugly sum, but with some terms like $\begin{pmatrix} 1 & 0 \\0 & 0 \end{pmatrix} \begin{pmatrix} 0 & 0 \\0 & 1 \end{pmatrix}$, which cancel quite easily.

#### Reid Barton (Aug 02 2019 at 12:18):

I'm writing up a translation of Knuth's version into linear maps to compare

#### Reid Barton (Aug 02 2019 at 12:58):

https://gist.github.com/rwbarton/ed50d4340e2f654b9d778ccb3ec93442

#### Reid Barton (Aug 02 2019 at 13:00):

I haven't used the relevant parts of mathlib much but as far as I could tell while writing this everything ought to be fairly straightforward

#### Kevin Buzzard (Aug 02 2019 at 13:05):

rofl kids these days

One sec

sensitivity.pdf

#### Johan Commelin (Aug 02 2019 at 13:14):

That looks quite formalisable, I think.

#### Johan Commelin (Aug 02 2019 at 13:16):

After all, Kenny formalised the dimension formula, and Fabian did the dual basis.

#### Johan Commelin (Aug 02 2019 at 13:16):

Anything else that we need?

#### Johan Commelin (Aug 02 2019 at 13:18):

@Reid Barton How far are you with the Lean version?

Haven't started

#### Reid Barton (Aug 02 2019 at 13:18):

The only other general fact which gets used is the triangle inequality for summing over a finite set, do we have that?

#### Johan Commelin (Aug 02 2019 at 13:19):

If we do, it should be finset.abs_sum, right? I don't think I've seen it.

#### Reid Barton (Aug 02 2019 at 13:19):

Then there is going to be some possibly tricky business relating the hypercube graph to the matrix entries of the $f_n$, but that would also appear in the matrix version

#### Johan Commelin (Aug 02 2019 at 13:22):

Right, that final calc block seems the most tricky part.

#### Johan Commelin (Aug 02 2019 at 13:22):

The rest is straight-forward, I think.

#### Rob Lewis (Aug 02 2019 at 13:26):

This looks super doable. It's obviously a different kind of proof, but somehow it reminds me of the cap set proof in spirit.

#### Reid Barton (Aug 02 2019 at 13:32):

I guess I'll just start typing and see at what point I get stuck.

#### Johan Commelin (Aug 02 2019 at 14:30):

@Reid Barton How are things going so far? I finally have time to look at this

#### Reid Barton (Aug 02 2019 at 14:32):

So far I created a new repository and did other things while building mathlib :slight_smile:

#### Reid Barton (Aug 02 2019 at 14:33):

I was about to get started actually

#### Johan Commelin (Aug 02 2019 at 14:34):

Why do you build mathlib?

#### Johan Commelin (Aug 02 2019 at 14:34):

I haven't built mathlib in 3 months

#### Reid Barton (Aug 02 2019 at 14:34):

I haven't been indoctrinated in the new ways yet and I had other things to do anyways

#### Reid Barton (Aug 02 2019 at 14:48):

Does this look sensible so far?

import data.real.basic
import linear_algebra.dimension

noncomputable theory

/-- The free vector space on vertices of a hypercube, defined inductively. -/
def V : ℕ → Type
| 0 := ℝ
| (n+1) := V n × V n

instance : Π n, add_comm_group (V n) :=
begin
apply nat.rec,
{ dunfold V, apply_instance },
{ introsI n IH, dunfold V, apply_instance }
end

instance : Π n, vector_space ℝ (V n) :=
begin
apply nat.rec,
{ dunfold V, apply_instance },
{ introsI n IH, dunfold V, apply_instance }
end

lemma dim_V {n : ℕ} : vector_space.dim ℝ (V n) = 2^n :=
begin
induction n with n IH,
{ apply dim_of_field },
{ dunfold V,
rw [dim_prod, IH, pow_succ, two_mul] }
end

/-- The linear operator f_n corresponding to Huang's matrix A_n. -/
def f : Π n, V n →ₗ[ℝ] V n
| 0 := 0
| (n+1) := sorry


#### Reid Barton (Aug 02 2019 at 14:50):

And is there any special support for linear maps into/out of binary direct sums?

#### Rob Lewis (Aug 02 2019 at 14:52):

Heh, I just started playing around with this and got to exactly the same place. Not that I saw (at a quick glance).

#### Reid Barton (Aug 02 2019 at 14:52):

Ah yes, linear_map.fst/snd/prod

#### Reid Barton (Aug 02 2019 at 14:56):

/-- The linear operator f_n corresponding to Huang's matrix A_n. -/
noncomputable def f : Π n, V n →ₗ[ℝ] V n
| 0 := 0
| (n+1) :=
linear_map.pair
(linear_map.copair (f n) linear_map.id)
(linear_map.copair linear_map.id (-f n))


This definition needs an explicit noncomputable even though I have noncomputable theory at the top, is that supposed to happen?

#### Chris Hughes (Aug 02 2019 at 15:00):

Is noncomputable theory inside a section?

#### Rob Lewis (Aug 02 2019 at 15:00):

noncomputable theory doesn't always propogate to aux decls.

#### Reid Barton (Aug 02 2019 at 15:32):

/-- The linear operator f_n corresponding to Huang's matrix A_n. -/
noncomputable def f : Π n, V n →ₗ[ℝ] V n
| 0 := 0
| (n+1) :=
linear_map.pair
(linear_map.copair (f n) linear_map.id)
(linear_map.copair linear_map.id (-f n))

lemma f_squared {n : ℕ} : ∀ v, (f n) (f n v) = (n : ℝ) • v :=
-- The (n : ℝ) is necessary since n • v refers to the multiplication defined
-- using only the addition of V.
begin
induction n with n IH,
{ intro v, dunfold f, simp, refl },
{ rintro ⟨v, v'⟩,
ext,
{ dunfold f V,
conv_rhs { change ((n : ℝ) + 1) • v, rw add_smul },
simp [IH] },
{ dunfold f V,
conv_rhs { change ((n : ℝ) + 1) • v', rw add_smul },
have : Π (x y : V n), -x + (y + x) = y := by { intros, abel }, -- ugh
simp [IH, this] } }
end


#### Reid Barton (Aug 02 2019 at 15:32):

Maybe I'll put up a repository under leanprover-community?

#### Rob Lewis (Aug 02 2019 at 15:37):

This was weirdly hard to make it go through, I got caught on the (n : R) thing too for a bit.

lemma fn2 : ∀ n v, f n (f n v) = (n : ℝ) • v
| 0 v := by { rw (show f 0 = 0, from rfl), norm_cast, simp, refl }
| (k+1) ⟨v1, v2⟩ :=
begin
end


#### Reid Barton (Aug 02 2019 at 15:38):

Okay, I made https://github.com/leanprover-community/lean-sensitivity. I don't know how the permissions work by default, but anyone who can add collaborators should feel free to do so.

#### Floris van Doorn (Aug 02 2019 at 15:46):

My gut feeling says that defining V n := (fin n -> bool) -> real would be nicer to work with. Then V is defined directly instead of recursively. You can use the following to go between fin n and fin (n+1):

universe variable u
variables {α : Type u} {n : ℕ}
def tail (p : fin (n+1) → α) : fin n → α := λ i, p i.succ
def cons (x : α) (v : fin n → α) : fin (n+1) → α :=
λ j, fin.cases x v j


#### Reid Barton (Aug 02 2019 at 15:51):

I thought defining V recursively would be more convenient for defining and proving things about f and g--and it seems pretty convenient so far. I was thinking of defining the hypercube as fin n -> bool though (in part because it seems a bit cheating to define it recursively).

#### Rob Lewis (Aug 02 2019 at 15:52):

I've started with the hypercube as fin n -> bool but I'm not sure about the cleanest way to define the basis of e_ps.

#### Floris van Doorn (Aug 02 2019 at 15:53):

Ok. Maybe that's right. Why do you say it feels like cheating?

#### Johan Commelin (Aug 02 2019 at 15:53):

I thought defining V recursively would be more convenient for defining and proving things about f and g--and it seems pretty convenient so far. I was thinking of defining the hypercube as fin n -> bool though (in part because it seems a bit cheating to define it recursively).

Why would that be cheating?

#### Johan Commelin (Aug 02 2019 at 15:54):

I've started with the hypercube as fin n -> bool but I'm not sure about the cleanest way to define the basis of e_ps.

Dual basis is in mathlib

#### Reid Barton (Aug 02 2019 at 15:55):

Well just because it's part of the "interface" of the overall theorem and fin n -> bool feels a bit more canonical. For example if the hypercube is defined recursively then it's not obvious how to construct the action of the symmetric group.

#### Floris van Doorn (Aug 02 2019 at 15:55):

Isn't the basis e just

def V (n : ℕ) : Type := (fin n → bool) → ℝ
def e (p : fin n → bool) : V n := λ q, if q = p then 1 else 0


#### Reid Barton (Aug 02 2019 at 15:55):

I agree it's not cheating by much.

#### Johan Commelin (Aug 02 2019 at 15:57):

@Floris van Doorn But you changed the definition of V

#### Reid Barton (Aug 02 2019 at 15:58):

If you assume that the hypercube must be represented by fin n -> bool, then at some point you have to make a recursive decomposition of building something for n+1 out of two somethings for n. I suggest doing that when we define the basis e

#### Reid Barton (Aug 02 2019 at 15:58):

Which is I think what Rob was going to do

#### Floris van Doorn (Aug 02 2019 at 15:58):

I was responding to Rob, who said (as I understood it) that he was interested in the basis using this definition of V

#### Reid Barton (Aug 02 2019 at 15:59):

Probably it doesn't matter very much where you do it

#### Johan Commelin (Aug 02 2019 at 16:00):

Do we want to define e directly?

#### Johan Commelin (Aug 02 2019 at 16:00):

I don't really care.

#### Johan Commelin (Aug 02 2019 at 16:00):

I just thought that we would first define the basis for V.

#### Reid Barton (Aug 02 2019 at 16:01):

So something like e (n+1) p := if p 0 then prod.inr (e n p.tail) else prod.inl (e n p.tail)

#### Rob Lewis (Aug 02 2019 at 16:01):

@Floris van Doorn That looks way cleaner than what I was doing, I was using the other definition of V though.

#### Rob Lewis (Aug 02 2019 at 16:01):

def e : Π n : ℕ, Q n → V n
| 0 p := (1 : ℝ)
| (k+1) p :=
match p 0 with
| tt := (e k (drop p), 0)
| ff := (0, e k (drop p))
end


or something like that, I don't think it's gonna be convenient.

#### Floris van Doorn (Aug 02 2019 at 16:01):

The recursive decomposition is easy:

def tail (p : fin (n+1) → α) : fin n → α := λ i, p i.succ
def tuple (x : α) (v : α → (fin n → α) → β) : (fin (n+1) → α) → β :=
λ p, v (p 0) (tail p)


So if you have an element of bool -> V n you get an element of V (n+1)

#### Reid Barton (Aug 02 2019 at 16:04):

I'm just worried that you will end up with only a linear isomorphism (not a definitional equality) between V (n+1) and bool -> V n or V n x V n and that will make the computations involving f and g a lot more involved unless you can manage to cancel the isomorphisms automatically

#### Floris van Doorn (Aug 02 2019 at 16:05):

Ok, that might be a problem if we have to translate a lot between these two representations. I think it will be doable though.

#### Floris van Doorn (Aug 02 2019 at 16:06):

but maybe in that aspect the recursive definition is easier.

#### Johan Commelin (Aug 02 2019 at 16:06):

/-- The hypercube.-/
def Q (n) : Type := fin n → bool

/-- The basis of V indexed by the hypercube.-/
def b : Π n, Q n → V n
| 0     := λ _, (1:ℝ)
| (n+1) := λ v, if v n = tt
then (b n (v ∘ fin.succ), 0)
else (0, b n (v ∘ fin.succ))


#### Reid Barton (Aug 02 2019 at 16:07):

The alternative is to write down the basis and probably also the dual basis separately by this kind of recursive formula and then check that the dual basis is really dual and also the formula for $\varepsilon_q (f_n e_p)$, by induction

#### Rob Lewis (Aug 02 2019 at 16:09):

@Johan Commelin That's probably slightly more convenient than the match, yeah.

#### Johan Commelin (Aug 02 2019 at 16:12):

Ok, but now we need to prove that this is a basis...

#### Johan Commelin (Aug 02 2019 at 16:12):

It should suffice to prove linear independence

#### Reid Barton (Aug 02 2019 at 16:13):

something like

noncomputable def ε : Π {n : ℕ} (p : fin n → bool), V n →ₗ[ℝ] ℝ
| 0 _ := linear_map.id
| (n+1) p :=
match p 0 with
| ff := (ε (p ∘ fin.succ)).comp (linear_map.fst _ _ _)
| tt := (ε (p ∘ fin.succ)).comp (linear_map.snd _ _ _)
end


#### Reid Barton (Aug 02 2019 at 16:13):

Ok, but now we need to prove that this is a basis...

Yeah that's true

#### Johan Commelin (Aug 02 2019 at 16:14):

@Reid Barton Is there a reason you don't want to use mathlibs dual basis?

#### Reid Barton (Aug 02 2019 at 16:14):

I fear you might get stuck when you need to calculate the matrix entries but I don't really know

#### Reid Barton (Aug 02 2019 at 16:15):

because you won't have a formula for the dual basis like the one above

#### Reid Barton (Aug 02 2019 at 16:16):

Unless there are already theorems that say if we have bases of V and W, then we get a basis of V x W and the formula for the dual basis is the expected one

#### Johan Commelin (Aug 02 2019 at 16:17):

Aha, but wouldn't it be better/easier to prove those formulas?

#### Johan Commelin (Aug 02 2019 at 16:17):

Because otherwise you have to reprove that this thing is actually a dual basis.

#### Reid Barton (Aug 02 2019 at 16:18):

I guess we must already have a theorem about a basis of V x W so that we can compute its dimension

#### Reid Barton (Aug 02 2019 at 16:18):

You mean we should prove a mathlib theorem about the dual basis of V x W that comes from bases of V and W?

#### Reid Barton (Aug 02 2019 at 16:20):

I haven't seen the dual basis stuff in mathlib at all yet, let me take a look.

#### Reid Barton (Aug 02 2019 at 16:23):

So, there is

lemma is_basis_inl_union_inr {v : ι → β} {v' : ι' → γ}
(hv : is_basis α v) (hv' : is_basis α v') : is_basis α (sum.elim (inl α β γ ∘ v) (inr α β γ ∘ v')) :=


#### Johan Commelin (Aug 02 2019 at 16:23):

Also, more trivialities:

/-- The hypercube.-/
def Q (n) : Type := fin n → bool

instance Q.fintype (n) : fintype (Q n) := by delta Q; apply_instance

def Q.card (n) : fintype.card (Q n) = 2^n :=
calc _ = _ : fintype.card_fun
... = _ : by simp only [fintype.card_fin, fintype.card_bool]


#### Johan Commelin (Aug 02 2019 at 16:24):

Ooh, that def should be a simp-lemma

#### Reid Barton (Aug 02 2019 at 16:25):

Maybe the right way to do all this is to just define the hypercube recursively after all, and then tack a translation onto fin n -> bool at the end if we want to.

#### Reid Barton (Aug 02 2019 at 16:26):

Then we can use that is_basis_inl_union_inr and add a formula to linear_algebra.dual about its dual basis

#### Reid Barton (Aug 02 2019 at 16:27):

Q (n+1) := Q n ⊕ Q n and whatever definition of "adjacent" is the most convenient

#### Johan Commelin (Aug 02 2019 at 16:28):

Or should we just prove that Q n →₀ ℝ is linearly equivelent to V n?

#### Johan Commelin (Aug 02 2019 at 16:28):

Or maybe we should redefine V n to be that space?

#### Reid Barton (Aug 02 2019 at 16:29):

Or should we just prove that Q n →₀ ℝ is linearly equivelent to V n?

This one sounds good

#### Reid Barton (Aug 02 2019 at 16:32):

Maybe by first providing Q (n+1) ≃ Q n ⊕ Q n

#### Johan Commelin (Aug 02 2019 at 16:36):

Aha, that also sounds like a good idea. And then use is_basis.comp?

#### Johan Commelin (Aug 02 2019 at 16:38):

Need to feed some kids :children_crossing: brb

#### Johan Commelin (Aug 02 2019 at 16:54):

Huh, there is no has_xor typeclass??

#### Johan Commelin (Aug 02 2019 at 17:32):

namespace Q
variable (n : ℕ)

instance : fintype (Q n) := by delta Q; apply_instance

variable {n}

def xor (x y : Q n) : Q n :=
λ i, bxor (x i) (y i)

@[symm] lemma xor_comm (x y : Q n) : x.xor y = y.xor x :=
funext $λ i, bool.bxor_comm _ _ /-- The distance between two vertices of the hypercube.-/ def dist (x y : Q n) : ℕ := (finset.univ : finset (fin n)).sum$ λ i, cond (x.xor y i) 1  0

@[simp] lemma dist_self (x : Q n) : x.dist x = 0 :=
finset.sum_eq_zero $λ i hi, by simp only [xor, bxor_self, bool.cond_ff] @[symm] lemma dist_symm (x y : Q n) : x.dist y = y.dist x := congr_arg ((finset.univ : finset (fin n)).sum)$
by { funext i, simp [xor_comm] }

/-- Two vertices of the hypercube are adjacent if their distance is 1.-/
def adjacent (x y : Q n) : Prop := x.dist y = 1

/-- The set of n-/
def neighbours (x : Q n) : set (Q n) := {y | x.adjacent y}

variable (n)

/-- The cardinality of the hypercube.-/
@[simp] lemma card : fintype.card (Q n) = 2^n :=
calc _ = _ : fintype.card_fun
... = _ : by simp only [fintype.card_fin, fintype.card_bool]

theorem sensitivity (H : set (Q n)) (x) (h : x ∈ H) :
real.sqrt n ≤ fintype.card (H ∩ (neighbours x) : set (Q n)) :=
sorry

end Q


Lean isn't yet happy with the theorem statement

#### Johan Commelin (Aug 02 2019 at 17:54):

Voila: that's a statement that Lean likes:

theorem sensitivity (H : finset (Q n)) (x) (h : x ∈ H) :
real.sqrt n ≤ (H.filter (neighbours x)).card :=
sorry


#### Patrick Massot (Aug 02 2019 at 18:28):

Hi everybody. I'd like to play this game too. Can we somehow distribute efforts? Where are you now?

#### Reid Barton (Aug 02 2019 at 18:34):

Hi Patrick! I just got back to this, currently trying to add a recursive definition of the hypercube and associated basis.

#### Reid Barton (Aug 02 2019 at 18:35):

After that, I think there are some independent pieces to do

#### Patrick Massot (Aug 02 2019 at 18:35):

Do you think you could push something and give me lemmas to prove?

#### Johan Commelin (Aug 02 2019 at 18:36):

This is what I have now:

/-- The cardinality of the hypercube.-/
@[simp] lemma card : fintype.card (Q n) = 2^n :=
calc _ = _ : fintype.card_fun
... = _ : by simp only [fintype.card_fin, fintype.card_bool]

def equiv_sum : Q (n+1) ≃ Q n ⊕ Q n :=
{ to_fun := λ x, cond (x 0)
(sum.inl (x ∘ fin.succ))
(sum.inr (x ∘ fin.succ)),
inv_fun := λ x, sum.rec_on x
(λ y i, if h : i = 0 then tt else y (i.pred h))
(λ y i, if h : i = 0 then ff else y (i.pred h)),
left_inv :=
begin
intro x, dsimp only, cases h : x 0;
{ funext i, dsimp only [bool.cond_tt, bool.cond_ff], split_ifs with H,
{ rw [H, h] },
{ rw [function.comp_app, fin.succ_pred] } }
end,
right_inv :=
begin

end }


#### Patrick Massot (Aug 02 2019 at 18:36):

Johan, which definition of Q n is this using?

#### Patrick Massot (Aug 02 2019 at 18:36):

Did you agree on the definitions of Q n and V n?

#### Reid Barton (Aug 02 2019 at 18:37):

Maybe I will just push something using a lot of constant and axiom as a starting point

#### Reid Barton (Aug 02 2019 at 18:38):

then perhaps we can distribute the representation decisions

#### Patrick Massot (Aug 02 2019 at 18:39):

It seems hard to decide independently the representations of V n and Q n

#### Johan Commelin (Aug 02 2019 at 18:42):

This is with Q n := fin n → bool

#### Reid Barton (Aug 02 2019 at 18:43):

I think https://github.com/leanprover-community/lean-sensitivity/commit/c2d0b69cbe175f3125c2719f3b87f2f6f626f424 is enough to make the rest of the proof go through

#### Reid Barton (Aug 02 2019 at 18:44):

Except with a correct statement of f_matrix_nonadjacent

#### Johan Commelin (Aug 02 2019 at 18:49):

@Reid Barton @Patrick Massot Shall I fill in the Q and adjacent constants?

#### Reid Barton (Aug 02 2019 at 18:50):

Feel free, I'm going to try to continue to sketch out the rest of the proof

#### Johan Commelin (Aug 02 2019 at 18:51):

@Patrick Massot @Floris van Doorn I've given you write permissions on the repo

thanks!

#### Patrick Massot (Aug 02 2019 at 18:58):

Reid I see you defined epsilon as the dual basis, but I liked the recursive definition

#### Patrick Massot (Aug 02 2019 at 18:59):

I'd like to work on the fact about |epsilon_q f_n e_p|

#### Rob Lewis (Aug 02 2019 at 18:59):

@Johan Commelin mind giving me access too? I was looking at this for a bit before dinner, might try to do a bit more.

Sure!

#### Reid Barton (Aug 02 2019 at 19:00):

I was intending that we'd add a lemma to mathlib that says that the dual basis element on inl i is given by projecting to the first factor, then applying the dual basis of the original basis

#### Johan Commelin (Aug 02 2019 at 19:00):

With this definition:

/-- The basis of V indexed by the hypercube.-/
def e : Π n, Q n → V n
| 0     := λ _, (1:ℝ)
| (n+1) := λ v, cond (v 0) (e n (v ∘ fin.succ), 0) (0, e n (v ∘ fin.succ))


I can't make {n} implicit...

#### Johan Commelin (Aug 02 2019 at 19:01):

@Rob Lewis Done, although I guess you also have admin rights by default...

#### Johan Commelin (Aug 02 2019 at 19:01):

Since you are admin of leanprover-community, right?

#### Reid Barton (Aug 02 2019 at 19:02):

Gah, I keep running into "maximum class-instance resolution depth has been reached" issues, I think they are related to decidable_eq somehow...

#### Rob Lewis (Aug 02 2019 at 19:02):

Oh, maybe. But thanks anyway!

#### Rob Lewis (Aug 02 2019 at 19:05):

I can't make {n} implicit...

Why not?

def e : Π {n}, Q n → V n
| 0     := λ _, (1:ℝ)
| (n+1) := λ v, cond (v 0) (e (v ∘ fin.succ), 0) (0, e (v ∘ fin.succ))


#### Reid Barton (Aug 02 2019 at 19:05):

@Patrick Massot That proof will depend on the definition of Q and e, though

#### Reid Barton (Aug 02 2019 at 19:07):

I pushed another commit about g

#### Patrick Massot (Aug 02 2019 at 19:07):

I'm using the definition of e that Rob just pasted

#### Patrick Massot (Aug 02 2019 at 19:08):

(which I indeed modified from Johan's message)

#### Jesse Michael Han (Aug 02 2019 at 19:11):

i'm also happy to contribute

what needs to be done besides the two sorrys Reid just pushed?

#### Reid Barton (Aug 02 2019 at 19:11):

Oh dang, H is not a great name

#### Reid Barton (Aug 02 2019 at 19:13):

@Jesse Michael Han I'll be pushing a couple more sorrys soon to complete the proof outline

#### Johan Commelin (Aug 02 2019 at 19:17):

I'm inductively proving that e is a basis.

#### Johan Commelin (Aug 02 2019 at 19:18):

See the jmc branch

#### Patrick Massot (Aug 02 2019 at 19:22):

As I wrote earlier, I'm inductively calculating epsilon q e p

#### Patrick Massot (Aug 02 2019 at 19:22):

I guess it should prove that e is a basis right?

#### Reid Barton (Aug 02 2019 at 19:24):

Lean isn't yet happy with the theorem statement

@Johan Commelin were you having trouble with type classes?

#### Johan Commelin (Aug 02 2019 at 19:24):

Well, sets weren't finsets and such

#### Johan Commelin (Aug 02 2019 at 19:25):

There is a working statement on the jmc branch

#### Johan Commelin (Aug 02 2019 at 19:25):

I'm almost done with the proof that e is a basis

#### Reid Barton (Aug 02 2019 at 19:28):

Okay, I pushed a couple more bits (theorem statement adapted from your Johan--but it should be an exists)

#### Reid Barton (Aug 02 2019 at 19:29):

Not sure if the next-to-last statement is phrased optimally

#### Patrick Massot (Aug 02 2019 at 19:34):

In those terms, I'm working on f_matrix_adjacent and f_matrix_nonadjacent

#### Jesse Michael Han (Aug 02 2019 at 19:35):

g_injective was easy:

lemma g_injective {m : ℕ} : function.injective (g m) :=
begin
rw[g], intros x₁ x₂ H_eq, simp at *, exact H_eq.right
end


#### Reid Barton (Aug 02 2019 at 19:35):

I'm going to tackle the inequality that's the last sentence of the PDF I posted

#### Reid Barton (Aug 02 2019 at 19:35):

that leaves f_image_g and exists_eigenvalue

#### Johan Commelin (Aug 02 2019 at 19:36):

I'll push what I have now.

Ok, I pushed

#### Johan Commelin (Aug 02 2019 at 19:38):

It does contain a sorry. Will work on that soon.

#### Jesse Michael Han (Aug 02 2019 at 19:38):

i doubt f_image_g will be as easy but i can start on that. @Johan Commelin could i get push access as well?

afk

#### Jesse Michael Han (Aug 02 2019 at 19:42):

jesse-michael-han

#### Patrick Massot (Aug 02 2019 at 19:46):

Do we have a nice way to define the two injections from fin n -> bool to fin n+1 -> bool that differ on the zeroth element of fin n+1?

#### Patrick Massot (Aug 02 2019 at 19:46):

I guess I should use pattern matching

Check what I did

#### Johan Commelin (Aug 02 2019 at 19:47):

I've used cond (x 0) stuff

#### Patrick Massot (Aug 02 2019 at 19:48):

This is not quite the same question, is it?

Maybe not

#### Patrick Massot (Aug 02 2019 at 19:48):

You're going i the easier direction (decreasing n)

#### Johan Commelin (Aug 02 2019 at 19:49):

Right, I was too fast... sorry

#### Reid Barton (Aug 02 2019 at 19:52):

In principle I like building the equivalence Q (n+1) ≃ Q n ⊕ Q n out of stuff in data.equiv.basic/data.equiv.fin though it would be kind of verbose

#### Patrick Massot (Aug 02 2019 at 19:53):

I found the library bit I was missing

#### Patrick Massot (Aug 02 2019 at 19:53):

I can now write Q n → Q (n+1) := λ p, λ k, if h : k = 0 then tt else p (k.pred h)

#### Johan Commelin (Aug 02 2019 at 19:53):

That's what I used

#### Patrick Massot (Aug 02 2019 at 19:53):

I was missing pred

#### Johan Commelin (Aug 02 2019 at 19:53):

I already pushed that equiv @Reid Barton

#### Patrick Massot (Aug 02 2019 at 19:54):

Sorry Johan, I focused on your cond and missed pred

#### Reid Barton (Aug 02 2019 at 19:54):

Oh I see, just defined manually yeah

#### Reid Barton (Aug 02 2019 at 20:09):

I changed H from a finset back to a set though I'm not yet entirely sure whether it was a good idea

#### Johan Commelin (Aug 02 2019 at 20:18):

Ooh, you should also feel free to refactor Q.equiv_sum

#### Johan Commelin (Aug 02 2019 at 20:19):

If you want to use more fancy library functions (-;

finsets ftw.

#### Floris van Doorn (Aug 02 2019 at 20:33):

@Patrick Massot: I would suggest

def cons (x : α) (v : fin n → α) : fin (n+1) → α :=
λ j, fin.cases x v j


What is that?

#### Floris van Doorn (Aug 02 2019 at 20:36):

To define the maps Q n → Q (n+1), fin.cases is there exactly for that purpose.

Oh I see

#### Patrick Massot (Aug 02 2019 at 20:41):

It's still totally mysterious to me that your definition cannot be rewritten as fin.cases x v

#### Floris van Doorn (Aug 02 2019 at 20:56):

Lean is pretty bad at these kind of unification problems, unless it uses the [elab_as_eliminator] attribute. With that attribute it is hardcoded to look at the third explicit argument of fin.cases, and then figure out what to do using the type of the third argument. If you don't give it 3 arguments, it will do the standard unification procedure, which fails.

#### Patrick Massot (Aug 02 2019 at 20:57):

What do you get from using this definition rather than mine?

#### Patrick Massot (Aug 02 2019 at 20:57):

It seems harder to prove lemmas about it

#### Patrick Massot (Aug 02 2019 at 20:57):

but probably I'm missing library lemmas

#### Johan Commelin (Aug 02 2019 at 21:07):

I'm calling it a day

#### Johan Commelin (Aug 02 2019 at 21:07):

Unfortunately e is still not a basis

#### Johan Commelin (Aug 02 2019 at 21:08):

I pushed the mess that I have so far.

#### Patrick Massot (Aug 02 2019 at 21:08):

This is all very frustrating. I'm trying to learn how to make weird inductions in Lean

#### Patrick Massot (Aug 02 2019 at 21:08):

And I'm very bad at it

#### Jesse Michael Han (Aug 02 2019 at 21:14):

i'm halfway done with f_image_g

#### Floris van Doorn (Aug 02 2019 at 21:20):

My hope was that the lemmas you needed were already in the library. Although I don't see anything other than cases_zero and cases_succ. What else do you need?

#### Jesse Michael Han (Aug 02 2019 at 22:27):

i'm done with f_image_g except for these two annoying lemmas:

lemma cast_lemma_1 {m : ℕ} : 0 ≤ (1 + (nat.cast m) : ℝ) := sorry

lemma cast_lemma_2 {m : ℕ} : (nat.cast (nat.succ m) : ℝ) = (1 + nat.cast m : ℝ) := sorry


#### Jesse Michael Han (Aug 02 2019 at 22:30):

oh nevermind, i just needed to make a change:

lemma cast_lemma_1 {m : ℕ} : 0 ≤ (1 + (nat.cast m) : ℝ) :=
by {change (0 : ℝ) ≤ (1 + ↑m : ℝ), suffices this : 0 ≤ (↑m : ℝ), by {linarith}, simp}

lemma cast_lemma_2 {m : ℕ} : (nat.cast (nat.succ m) : ℝ) = (1 + nat.cast m : ℝ) :=
by change ↑(nat.succ m) = (1 + ↑m : ℝ); simp


#### Jesse Michael Han (Aug 02 2019 at 22:57):

[edited] oops i missed the invite link

#### Patrick Massot (Aug 02 2019 at 23:53):

I'm done computing the matrix

#### Patrick Massot (Aug 02 2019 at 23:58):

I haven't use @Johan Commelin xor adjacency definition, see https://github.com/leanprover-community/lean-sensitivity/blob/058def458c9a4023ec95aaf211c0f7a22f77a05d/src/sensitivity.lean#L232-L235. I hope my definition is the same as his. At least I can compute the matrix using it

#### Patrick Massot (Aug 02 2019 at 23:59):

I also used the explicit inductive definition of the dual basis, and proved the duality equations.

#### Patrick Massot (Aug 03 2019 at 00:00):

Note that I spent most of my time trying to prove fancy induction principle on Q n, messing around with elab_as_eliminator and induction ... using .... But nothing worked, so I reverted to good old cases.

#### Patrick Massot (Aug 03 2019 at 00:18):

Is there any reason we use bool everywhere instead of Prop?

#### Johan Commelin (Aug 03 2019 at 05:44):

@Patrick Massot You don't need bool_cases. You can just write cases h : x p.

#### Patrick Massot (Aug 03 2019 at 09:51):

Nice trick! I tried by_cases hp : x p = tt but this gave an inconvenient second case. I'm a bit disappointed that the proof wasn't finished while I slept. I'll be again away from Lean for the next 9 hours, so maybe this will be enough. Otherwise I'll play again tonight. Have fun!

#### Patrick Massot (Aug 03 2019 at 17:48):

@Jesse Michael Han I think you have slightly too much love for tidy. What about

lemma f_image_g' {m : ℕ} (w : V (m + 1)) (hv : ∃ v, w = g m v) :
(f (m + 1) : V (m + 1) → V (m + 1)) w = real.sqrt (m + 1) • w :=
begin
rcases hv with ⟨v, rfl⟩,
dsimp [g],
erw f,
simp [f_squared],
rw [smul_add, smul_smul, real.mul_self_sqrt (by exact_mod_cast zero_le _ : 0 ≤ (1 : ℝ) + m), add_smul, one_smul],
abel,
end


#### Patrick Massot (Aug 03 2019 at 17:49):

Do you mind if I replace your proof by this one? I looks closer to the paper proof

#### Jesse Michael Han (Aug 03 2019 at 17:50):

oh, i didn't see f_squared

yeah that looks much better

#### Patrick Massot (Aug 03 2019 at 17:51):

Did you look at the pdf proof?

#### Jesse Michael Han (Aug 03 2019 at 17:53):

yes, but i took a longer route in proving the left-side equality (because i essentially rederived f_squared)

#### Patrick Massot (Aug 03 2019 at 17:54):

Anyway, is anybody working on the next lemma?

#### Patrick Massot (Aug 03 2019 at 17:54):

I mean exists_eigenvalue

#### Patrick Massot (Aug 03 2019 at 17:55):

I know nothing about dimension in mathlib, but it looks like a good opportunity to learn

#### Jesse Michael Han (Aug 03 2019 at 17:56):

i'm not working on it

i was going to wait to hear back from reid

#### Patrick Massot (Aug 03 2019 at 18:05):

exists_mem_ne_zero_of_dim_pos looks very promising

#### Jesse Michael Han (Aug 03 2019 at 20:50):

i started a bit on degree_theorem; feel free to overwrite or build on what's there

i'm not sure if finsupp.mem_span_if_total is the correct way to extract a linear combination from a proof of membership in a span, but it reduces to a finset.sum which seems to be what we want.

#### Patrick Massot (Aug 03 2019 at 20:55):

I finished e_is_basis that @Johan Commelin almost did yesterday

#### Patrick Massot (Aug 03 2019 at 20:56):

Wait. @Jesse Michael Han did you proof start timeout?

#### Patrick Massot (Aug 03 2019 at 20:56):

I tried to merge and I see it times out

#### Patrick Massot (Aug 03 2019 at 20:58):

https://github.com/leanprover-community/lean-sensitivity/commit/0f1468180a143ba8d40276b2bf7198fc2c250093 is my attempt at the dimension argument

#### Patrick Massot (Aug 03 2019 at 20:58):

But I don't know enough cardinal theory to do finite dimensional linear algebra :sad:

i'll take a look

#### Patrick Massot (Aug 03 2019 at 20:59):

For instance I need to prove:

n : ℕ
⊢ 2 ^ n < cardinal.omega


#### Patrick Massot (Aug 03 2019 at 20:59):

and

n : ℕ,
⊢ 2 ^ n = 2 ^ ↑n


Where at least some of this stuff is in cardinals

#### Patrick Massot (Aug 03 2019 at 21:05):

I won't do more tonight.

#### Jesse Michael Han (Aug 03 2019 at 21:14):

OK, leanpkg test succeeds at my commit, but indeed times out after the merge. i'll fix it i fixed it

#### Chris Hughes (Aug 03 2019 at 21:21):

If you know everything is finite dimensional, you probably shouldn't be using cardinals. Everything about infinite dimension should be transferred to findim really, or you have to faff with coercions

#### Patrick Massot (Aug 03 2019 at 21:32):

Chris, the problem is we seem to have a lot more lemmas about dim than findim

#### Patrick Massot (Aug 03 2019 at 21:35):

For instance, do you have dim_sup_add_dim_inf_eq for findim?

#### Patrick Massot (Aug 03 2019 at 21:36):

Or do you have a nice way to import such theorems into the finite dimensional world?

#### Chris Hughes (Aug 03 2019 at 21:37):

I have virtually nothing. I guess when transfer comes along it will be easier. But they'll just be simp [nat.cast_add] or something.

#### Patrick Massot (Aug 03 2019 at 21:39):

Was this mirroring discussed with @Mario Carneiro? It seems a bit sad to duplicate all this, but we really want to be able to use finite dimensions as natural numbers

#### Mario Carneiro (Aug 03 2019 at 21:40):

most facts about numbers being equivalent to finite cardinals are proven

#### Patrick Massot (Aug 03 2019 at 21:41):

what do you mean?

#### Chris Hughes (Aug 03 2019 at 21:43):

Like cast is monotonic etc. Unfortunately, cardinals are not an ordered semiring, so the generic lemmas don't work.

#### Patrick Massot (Aug 03 2019 at 21:43):

Are they tagged for use by norm_cast?

#### Patrick Massot (Aug 03 2019 at 21:44):

For instance attribute [elim_cast] cardinal.nat_cast_in seems to be missing

#### Jesse Michael Han (Aug 03 2019 at 22:06):

i think the version of 2^n < omega you stated is parsed by Lean as monoid.pow, which is more annoying to deal with

but if you ensure it's the cardinal pow of casted nats, it's 2 lemmas away:

import set_theory.cardinal

universe u

example {n : ℕ} : (↑2) ^ (↑n : cardinal.{u}) < (cardinal.omega : cardinal.{u}) :=
by rw[<-cardinal.nat_cast_pow]; exact cardinal.nat_lt_omega _


#### Patrick Massot (Aug 03 2019 at 22:15):

Do we know that the restriction of linear_independent family to a subtype is linear_independent?

#### Patrick Massot (Aug 03 2019 at 22:24):

Anyway, I said I would stop more than one hour ago, so I should really stop now

#### Patrick Massot (Aug 03 2019 at 22:25):

Modulo the restriction thing, the proof of the dimension argument is reduced to these 2^n < omega things

#### Jesse Michael Han (Aug 03 2019 at 22:26):

the monoid.pow is annoying because you have to do an induction, but it's not bad:

example {n : ℕ} : (2 ^ n : cardinal) = (2 ^ (↑n : cardinal.{u}) : cardinal.{u}) :=
begin
induction n with n ih,
{simp},
{rw[nat.cast_succ, cardinal.power_add, <-ih, cardinal.power_one, mul_comm], refl },
end


you can get the first one from this one, i believe

#### Patrick Massot (Aug 03 2019 at 22:27):

I followed Chris's advice to get rid of dim as soon as I applied the lemmas

#### Patrick Massot (Aug 03 2019 at 22:28):

Nice, feel free to remove those sorries and push. I'll go to bed

#### Patrick Massot (Aug 03 2019 at 22:29):

Maybe you can even finish the whole thing while I sleep

#### Patrick Massot (Aug 03 2019 at 22:30):

Or maybe @Reid Barton will come back and cross the finish line for us

#### Patrick Massot (Aug 03 2019 at 22:31):

Zulip says his local time is 6:30pm

#### Patrick Massot (Aug 03 2019 at 22:31):

This leaves him the whole evening and night

#### Patrick Massot (Aug 03 2019 at 22:31):

and same for you!

Have fun!

#### Yao Liu (Aug 04 2019 at 04:46):

As a spectator, I was looking around and found (via Terry Tao's blog post) this interpretation https://arxiv.org/abs/1907.11175
namely, the $2^n$-dimensional space ought to be the exterior algebra (or Clifford algebra) of an $n$-dimensional vector space.

#### Jesse Michael Han (Aug 04 2019 at 21:07):

i'm trying to import analysis.normed_space.basic to use the triangle inequality, but this causes Lean on both my machines to start complaining about "equation compiler failed to generate bytecode for e._main", and something not being a rfl lemma, etc. the errors appear iff i have that import.

does anyone know why this would happen?

#### Kevin Buzzard (Aug 04 2019 at 21:12):

equation compiler failed to generate bytecode for 'e._main'
nested exception message:
code generation failed, VM does not have code for 'real.normed_field'


#### Kevin Buzzard (Aug 04 2019 at 21:16):

The entire file analysis.normed_space.basic is marked noncomputable so maybe it's no surprise the VM doesn't have code for real.normed_field

#### Kevin Buzzard (Aug 04 2019 at 21:17):

If you mark e noncomputable then most of the errors go away

#### Jesse Michael Han (Aug 04 2019 at 21:19):

indeed, but i was alarmed that previous proofs which were by refl were somehow no longer so after adding noncomputable

#### Jesse Michael Han (Aug 04 2019 at 21:19):

but that error can be fixed by changing rfl to by rw e...

#### Kevin Buzzard (Aug 04 2019 at 21:20):

you golfed me, I just found by unfold e :-)

#### Johan Commelin (Aug 05 2019 at 06:35):

Can someone give a status update? Is the only thing that needs to be done the tying together of some loose ends?

#### Chris Hughes (Aug 05 2019 at 06:42):

Looks like two sorries right now.

#### Chris Hughes (Aug 05 2019 at 06:42):

Neither are that hard.

#### Chris Hughes (Aug 05 2019 at 06:46):

I just proved that.

#### Chris Hughes (Aug 05 2019 at 06:46):

There are two sorries in the final theorem. I'm doing the first.

#### Chris Hughes (Aug 05 2019 at 06:59):

One sorry left now.

#### Johan Commelin (Aug 05 2019 at 08:17):

@Chris Hughes Are you still working on this?

#### Johan Commelin (Aug 05 2019 at 08:17):

I connected adjacent back to my definition that used dist.

#### Chris Hughes (Aug 05 2019 at 08:59):

I'm not. The last sorry looked like you needed to understand what was going on. Everything else I proved did not require that.

Ok, I see.

#### Patrick Massot (Aug 05 2019 at 09:42):

Johan, is there any use to the distance you defined, and relating it to adjacent? I'm not sure it makes adjacent so much more related to the usual definition. Maybe we could define a general graph class, and then adjacency in this context, and relate. But the real question is: what is the usual definition of the graph structure on Q n? Maybe the simplest answer goes through defining the (Z/2)^n action on Q n. For instance we could redefine Q n to be (Z/2)^n instead of this weird CS bool thing. Then define the canonical basis b for (Z/2)^n (it should already be in mathlib) and define adjacent x y by exists i, b i bul x = y.

#### Johan Commelin (Aug 05 2019 at 09:49):

I'm almost done with the final sorry.

#### Johan Commelin (Aug 05 2019 at 09:49):

I'll push what I have. Lunch time now.

#### Patrick Massot (Aug 05 2019 at 09:50):

Oh, I was starting on this final sorry

#### Patrick Massot (Aug 05 2019 at 09:51):

Do you mind if I finish during your lunch?

#### Patrick Massot (Aug 05 2019 at 09:56):

@Johan Commelin should I push?

#### Patrick Massot (Aug 05 2019 at 09:57):

Ok, let's say he was really having lunch

#### Patrick Massot (Aug 05 2019 at 09:57):

https://github.com/leanprover-community/lean-sensitivity/commit/f7be6abb34eafcd01df9417c99df34f8076362b9

#### Patrick Massot (Aug 05 2019 at 09:58):

Now we have a lot of cleanup to do before telling people about it

Nice, well done!

#### Johan Commelin (Aug 05 2019 at 10:22):

@Reid Barton @Rob Lewis @Jesse Michael Han @Chris Hughes @Floris van Doorn We have a theorem!

#### Kevin Buzzard (Aug 05 2019 at 10:25):

Well done!

I really like these "oh look here's some relatively simple-looking maths, how hard is it actually to formalise?" questions. A year or so ago my impression was "in Lean, it's probably going to be tough". Now my impression is turning to "it might be not too bad". We have cubing the cube, the IMO questions, working out pi to 7 decimal places, and now this.

#### Patrick Massot (Aug 05 2019 at 10:26):

It's still a lot harder than it should be

#### Kevin Buzzard (Aug 05 2019 at 10:26):

But I suspect it's a lot easier than it was.

#### Patrick Massot (Aug 05 2019 at 10:26):

Unless you already know perfectly all the relevant part of mathlib

Oh yes of course

#### Kevin Buzzard (Aug 05 2019 at 10:26):

It's almost getting to the point where it's as easy as I thought it would be before I knew anything about how this stuff worked.

#### Johan Commelin (Aug 05 2019 at 10:27):

Let's see if we can write transfer lemmas for this little project, to make things shorter

#### Kevin Buzzard (Aug 05 2019 at 10:27):

What does that mean?

#### Johan Commelin (Aug 05 2019 at 10:28):

Because we have Q n →₀ ℝ and V n, and they are canonically isomorphic.

for sure

#### Johan Commelin (Aug 05 2019 at 10:28):

Some proofs are easy on one side, others on the other.

#### Patrick Massot (Aug 05 2019 at 10:28):

What do you think about starting the refactor with:

notation Z/2 := zmodp 2 nat.prime_two

def Q (n : ℕ) := fin n → Z/2


#### Johan Commelin (Aug 05 2019 at 10:28):

This might be a good test case for the existing transfer api.

#### Johan Commelin (Aug 05 2019 at 10:28):

@Patrick Massot Why would that help?

#### Kevin Buzzard (Aug 05 2019 at 10:29):

I think your suggestion is a really worthwhile one Johan.

#### Patrick Massot (Aug 05 2019 at 10:29):

And then try to understand that std_basis thing, and define adjacency as I wrote it should be defined?

#### Johan Commelin (Aug 05 2019 at 10:29):

What does Z/2 have that bool doesn't have?

Looks

#### Patrick Massot (Aug 05 2019 at 10:29):

A group structure

#### Patrick Massot (Aug 05 2019 at 10:29):

Johan, is there any use to the distance you defined, and relating it to adjacent? I'm not sure it makes adjacent so much more related to the usual definition. Maybe we could define a general graph class, and then adjacency in this context, and relate. But the real question is: what is the usual definition of the graph structure on Q n? Maybe the simplest answer goes through defining the (Z/2)^n action on Q n. For instance we could redefine Q n to be (Z/2)^n instead of this weird CS bool thing. Then define the canonical basis b for (Z/2)^n (it should already be in mathlib) and define adjacent x y by exists i, b i bul x = y.

See above

#### Patrick Massot (Aug 05 2019 at 10:30):

I think this would give a much more recognizable adjacency relation

#### Kevin Buzzard (Aug 05 2019 at 10:30):

instead of this weird CS bool thing

Mathematicians still failing to come to terms with weird CS stuff

#### Patrick Massot (Aug 05 2019 at 10:31):

It's hard to express the fact that x and y are two different elements of a two elements sets in a nicer way than x = y +1

#### Johan Commelin (Aug 05 2019 at 10:31):

@Patrick Massot Ok, that seems fine.

#### Kevin Buzzard (Aug 05 2019 at 10:31):

x \ne y?

#### Patrick Massot (Aug 05 2019 at 10:32):

If I understand correctly mathlib still don't have the canonical basis of K^n (it has a more general std_basis for pi). It's time we fix that

#### Johan Commelin (Aug 05 2019 at 10:32):

Anyway, I have a meeting scheduled in 10 minutes... so I can't help too much with the refactor now.

#### Patrick Massot (Aug 05 2019 at 10:32):

I also need to go

#### Patrick Massot (Aug 05 2019 at 10:32):

Something easy that anyone can do is to collect all lemmas from that file that should be in mathlib and PR them

#### Patrick Massot (Aug 05 2019 at 10:33):

We should do that before refactoring because some of them will turn out to be unneeded for the sensitivity proof and will disappear if we don't rescue them first

#### Rob Lewis (Aug 05 2019 at 11:47):

I was away from Lean for the weekend and it looks like I missed all the fun. Nice job, guys!

#### Reid Barton (Aug 05 2019 at 12:04):

We should do that before refactoring because some of them will turn out to be unneeded for the sensitivity proof and will disappear if we don't rescue them first

I'm going to start by moving them to their own file

#### Reid Barton (Aug 05 2019 at 12:04):

Rob I think there's still plenty of clean up that would be nice to do. You had a shorter proof of f_squared right?

#### Rob Lewis (Aug 05 2019 at 12:05):

I just pushed it 20 seconds ago...

#### Rob Lewis (Aug 05 2019 at 12:05):

Looking at a few other proofs now that should be easy to clean up.

#### Reid Barton (Aug 05 2019 at 12:06):

Give me a couple minutes to push what I have simplified already

Sure thing.

OK, pushed

#### Reid Barton (Aug 05 2019 at 12:11):

Next I was going to try to replace the definition of adjacent by def adjacent' {n : ℕ} (p q : Q n) : Prop := ∃! i, p i ≠ q i and get rid of the dist stuff

#### Reid Barton (Aug 05 2019 at 12:12):

Although I guess this means proving something similar to adjacent_iff_dist

#### Reid Barton (Aug 05 2019 at 12:13):

By the way, what is this run_cmd tactic.skip magic about?

#### Rob Lewis (Aug 05 2019 at 12:14):

I suspect that will be nicer, but I'm not sure... I'm gonna try some more local cleanup toward the bottom.

#### Rob Lewis (Aug 05 2019 at 12:14):

I was editing the theorem below, which was causing the one above to recompile constantly, and it was really slow. Putting no-op code in between makes it stop recompiling the one above.

#### Rob Lewis (Aug 05 2019 at 12:15):

It wasn't meant to be pushed though, I deleted it.

#### Kevin Buzzard (Aug 05 2019 at 12:15):

Isn't there supposed to be some way of doing this with a .?

#### Rob Lewis (Aug 05 2019 at 12:16):

. might have the same effect. Not sure.

#### Johan Commelin (Aug 05 2019 at 12:19):

I always use .

#### Reid Barton (Aug 05 2019 at 12:25):

I'm constantly getting "excessive memory consumption" errors, is there some way to deal with these?

#### Reid Barton (Aug 05 2019 at 12:25):

The dependencies are definitely built

#### Johan Commelin (Aug 05 2019 at 12:36):

I added some foo_apply lemmas and golfed f_image_g.

#### Rob Lewis (Aug 05 2019 at 12:40):

I'm constantly getting "excessive memory consumption" errors, is there some way to deal with these?

Hmm, something's funny with the simp set. It's spending over two seconds in the simp only in the 0 case of f_squared, that seems excessive.

#### Rob Lewis (Aug 05 2019 at 12:41):

Or, maybe not the simp set. Even the definition of f takes a while. Probably a big type class search.

#### Reid Barton (Aug 05 2019 at 12:41):

I don't understand how anyone could have written any of this interactively. Did I break everything?

#### Rob Lewis (Aug 05 2019 at 12:42):

It's a little slow but it works fine for me.

restart Lean?

#### Rob Lewis (Aug 05 2019 at 12:46):

Adding this short-circuit helps in a few places:

def Vn_module {n} : module ℝ (V n) := by apply_instance
local attribute [instance, priority 10000] Vn_module


#### Reid Barton (Aug 05 2019 at 12:50):

Now leanpkg build has started printing goals and failing without printing any error message

#### Reid Barton (Aug 05 2019 at 12:51):

(not related to that module instance)

#### Patrick Massot (Aug 05 2019 at 12:59):

I don't understand how anyone could have written any of this interactively. Did I break everything?

I noticed it was very slow, but wasn't sure whether it was because I'm using my laptop. Anyway, I was doing the usual sorry dance (every have that is proved is replaced by a commented out proof and sorry).

#### Patrick Massot (Aug 05 2019 at 13:00):

I'd love to help refactoring but I'm on beach duty

#### Reid Barton (Aug 05 2019 at 13:03):

I found out how to increase the default memory limit for lean in emacs, so now I can load the whole file again

#### Johan Commelin (Aug 05 2019 at 13:04):

Why does Lean not understand what I mean when I write

def RQ_equiv_V : Π (n : ℕ), (Q n →₀ ℝ) ≃ₗ[ℝ] V n
| 0     := _
| (n+1) := _


#### Johan Commelin (Aug 05 2019 at 13:04):

It takes ages to parse/elaborate/tc this

#### Johan Commelin (Aug 05 2019 at 13:04):

Result: 4 deterministic timeouts

#### Rob Lewis (Aug 05 2019 at 13:04):

def Vn_module {n} : module ℝ (V n) := by apply_instance
def acg {n} : add_comm_semigroup (V n) := by apply_instance
def acm {n} : add_comm_monoid (V n) := by apply_instance
def hsr {n} : has_scalar ℝ (V n) := by apply_instance
def hav {n} : has_add (V n) := by apply_instance

local attribute [instance, priority 100000] acg acm hsr hav Vn_module


#### Rob Lewis (Aug 05 2019 at 13:05):

I'm timing right now, but it feels like a very significant speedup on the whole file.

#### Rob Lewis (Aug 05 2019 at 13:05):

Yeah, those short circuits reduce the compile time by more than 50%.

#### Johan Commelin (Aug 05 2019 at 13:05):

Doesn't help for this thing :sad:

#### Johan Commelin (Aug 05 2019 at 13:06):

Btw, should we even use real numbers?

#### Johan Commelin (Aug 05 2019 at 13:06):

For this problem nat.sqrt is just as good as real.sqrt, isn't it?

#### Johan Commelin (Aug 05 2019 at 13:07):

So we could do the whole thing with ℤ-modules

#### Johan Commelin (Aug 05 2019 at 13:07):

Anyway, I don't mind using real.

#### Johan Commelin (Aug 05 2019 at 13:08):

Without this RQ_equiv_V I don't think we can get very far with "transfer"-like techniques.

#### Johan Commelin (Aug 05 2019 at 13:24):

@Reid Barton Have your problems gone away?

Some of them

#### Rob Lewis (Aug 05 2019 at 13:27):

Do you have local changes that are causing this? It compiles with -T20000 for me, so there shouldn't be any memory issues.

#### Jesse Michael Han (Aug 05 2019 at 13:29):

I don't understand how anyone could have written any of this interactively.

in the case of degree_theorem, very painfully...

what is this "insert no-op code" magic? do i put a . or run_cmd tactic.skip above the current declaration i'm working on to stop recompilation of previous theorems?

#### Rob Lewis (Aug 05 2019 at 13:29):

The only suspicious thing I see in the profiling is that simp is spending a long time in tactic.join_user_simp_lemmas.

#### Johan Commelin (Aug 05 2019 at 13:30):

@Jesse Michael Han Yes. . is gold.

#### Reid Barton (Aug 05 2019 at 13:37):

I used to have some local changes but I still had problems when I got rid of them

#### Reid Barton (Aug 05 2019 at 13:37):

Is the default memory limit different in VS code maybe?

#### Kevin Buzzard (Aug 05 2019 at 13:38):

It's 100000 in VS Code I believe

#### Kevin Buzzard (Aug 05 2019 at 13:38):

The T50000 challenge was what happened when I halved it

#### Reid Barton (Aug 05 2019 at 13:44):

That's the "time" limit I thought

#### Kevin Buzzard (Aug 05 2019 at 13:44):

oh apologies. Memory limit is...

4096 megs

#### Reid Barton (Aug 05 2019 at 13:46):

Ah okay, that explains some things. In emacs it's 1024 megs

#### Jesse Michael Han (Aug 05 2019 at 13:52):

looks like something we should patch in the community version of lean-mode

4096 megs and constantly swapping

#### Johan Commelin (Aug 05 2019 at 14:23):

@Rob Lewis Did you manage to clean things up at the bottom of the file?

#### Johan Commelin (Aug 05 2019 at 14:24):

Do we have some sort of "cleaning up" roadmap?

#### Johan Commelin (Aug 05 2019 at 14:26):

The reason I wrote my dist function is that I imagined that we might rename Q to hypercube and put it in mathlib, and show that it is a (discrete) metric space, etc....

#### Johan Commelin (Aug 05 2019 at 14:27):

Not sure if we want to do things like that.

#### Rob Lewis (Aug 05 2019 at 14:28):

I got distracted by trying to speed things up. I have no major changes right now.

#### Rob Lewis (Aug 05 2019 at 14:29):

But performance-wise, I don't see any more obvious places to optimize. It seems to behave pretty reasonably.

#### Johan Commelin (Aug 05 2019 at 14:30):

Can you get the statement of RQ_equiv_V to work?

#### Johan Commelin (Aug 05 2019 at 14:30):

@Reid Barton What do you think of @Patrick Massot's suggestion for adjacency?

#### Johan Commelin (Aug 05 2019 at 14:31):

It's quite similar to your ∃! i, x i ≠ y i suggestion, but it exploits a bit of group structure.

#### Rob Lewis (Aug 05 2019 at 14:56):

local attribute [instance, priority 10000] finsupp.module classical.prop_decidable makes it work. The decidable instance isn't necessary but it speeds things up a little bit.

#### Rob Lewis (Aug 05 2019 at 14:56):

Once again, the type classes here are kind of a mess.

#### Johan Commelin (Aug 05 2019 at 14:58):

It's really sad that this creates a mess. It doesn't feel like we are doing something horrible.

#### Johan Commelin (Aug 05 2019 at 14:58):

I just pushed a compression of duality.

#### Jesse Michael Han (Aug 05 2019 at 15:34):

i'm working on turning degree_theorem into a calc proof after the existential instantiation of q

also thank you johan for the cleanup :^)

#### Reid Barton (Aug 05 2019 at 15:37):

i'm working on turning degree_theorem into a calc proof after the existential instantiation of q

Oh cool, I wanted to do this as well but currently I'm trying to simplify exists_eigenvalue a bit

#### Rob Lewis (Aug 05 2019 at 15:40):

Have you made any structural changes to exists_eigenvalue? I have a few cosmetic updates local, but nothing important.

#### Rob Lewis (Aug 05 2019 at 15:40):

I won't touch degree_theorem if Jesse is on it now.

#### Reid Barton (Aug 05 2019 at 15:43):

I'm trying to do all the conversion between cardinals and naturals at once

#### Reid Barton (Aug 05 2019 at 15:46):

Pushed, I think it is somewhat better now...

Nice.

#### Jesse Michael Han (Aug 05 2019 at 16:07):

also pushed my calcification

not sure what the correct style is for long calc proofs but i tried to prettify it

#### Johan Commelin (Aug 05 2019 at 16:47):

Nice work @Reid Barton and @Jesse Michael Han

#### Johan Commelin (Aug 05 2019 at 16:47):

I think that maybe we should just use begin ... end instead of by { .. } for the longer proofs in the calc block

#### Johan Commelin (Aug 05 2019 at 16:49):

Of course that's a very minor issue

#### Reid Barton (Aug 05 2019 at 17:01):

Going to head out for a while, but I feel it should somehow be easier to show that l q = ε q y

#### Johan Commelin (Aug 05 2019 at 17:07):

Yep... that's the kind of "transfer" thing that I wanted to do

#### Johan Commelin (Aug 05 2019 at 17:07):

But showing Q n ->0 R =_l V n is already non-trivial...

#### Johan Commelin (Aug 05 2019 at 17:08):

It seems that Rob found a fix.

#### Johan Commelin (Aug 05 2019 at 17:08):

@Jesse Michael Han what do you think of the following style?

theorem degree_theorem :
∃ q, q ∈ H ∧ real.sqrt (m + 1) ≤ (H ∩ q.adjacent).to_finset.card :=
begin
rcases exists_eigenvalue H ‹_› with ⟨y, ⟨⟨H_mem', H_mem''⟩, H_nonzero⟩⟩,
rcases (finsupp.mem_span_iff_total _).mp H_mem' with ⟨l, H_l₁, H_l₂⟩,
have hHe : H ≠ ∅ ,
{ contrapose! hH, rw [hH, set.empty_card'], exact nat.zero_lt_succ _ },
obtain ⟨q, H_mem_H, H_max⟩ : ∃ q, q ∈ H ∧ ∀ q', q' ∈ H → abs (l q') ≤ abs (l q),
{ cases set.exists_mem_of_ne_empty hHe with r hr,
cases @finset.max_of_mem _ _ (H.to_finset.image (λ q', abs (l q')))
(abs (l r)) (finset.mem_image_of_mem _ (set.mem_to_finset.2 hr)) with x hx,
rcases finset.mem_image.1 (finset.mem_of_max hx) with ⟨q, hq, rfl⟩,
refine ⟨q, ⟨set.mem_to_finset.1 hq, λ q' hq', _⟩⟩,
exact (finset.le_max_of_mem (finset.mem_image_of_mem _ (set.mem_to_finset.2 hq')) hx : _) },
have H_q_pos : 0 < abs (l q),
{ rw [abs_pos_iff],
assume h,
rw [finsupp.mem_supported'] at H_l₁,
have H_max' : ∀ q', l q' = 0,
{ intro q',
by_cases hq' : q' ∈ H,
{ revert q', simpa [h] using H_max },
{ exact H_l₁ _ hq' } },
have hl0 : l = 0,
{ ext, rw [H_max', finsupp.zero_apply] },
simp [hl0] at H_l₂,
exact H_nonzero H_l₂.symm },
refine ⟨q, ⟨‹_›, _⟩⟩,
suffices : real.sqrt (↑m + 1) * abs (l q) ≤ ↑(_) * abs (l q),
by { exact (mul_le_mul_right H_q_pos).mp ‹_› },

calc
real.sqrt (↑m + 1) * (abs (l q))
≤ abs (real.sqrt (↑m + 1) * l q) : by conv_lhs { rw [← abs_sqrt_nat, ← abs_mul] }
... ≤ abs (ε q (real.sqrt (↑m + 1) • y)) :
begin rw [linear_map.map_smul, smul_eq_mul, abs_mul, abs_mul],
apply mul_le_mul_of_nonneg_left _ _,
{ apply le_of_eq, congr' 1, rw [← H_l₂, finsupp.total_apply, finsupp.sum, linear_map.map_sum],
rw [finset.sum_eq_single q],
{ rw [linear_map.map_smul, smul_eq_mul, duality, if_pos rfl, mul_one], },
{ intros p hp hne,
simp [linear_map.map_smul, duality, hne.symm] },
{ intro h_q_ne_supp,
simp [finsupp.not_mem_support_iff.mp h_q_ne_supp] } },
{ exact abs_nonneg _ }
end
... ≤ l.support.sum (λ x : Q (m + 1), abs (l x) * abs ((ε q) ((f (m + 1) : _) (e x)))) :
begin
rw [← f_image_g y (by simpa using H_mem''), ← H_l₂, finsupp.total_apply,
finsupp.sum, linear_map.map_sum, linear_map.map_sum],
refine le_trans abs_triangle_sum _,
conv_lhs { congr, skip, simp [abs_mul] }
end
... ≤ finset.sum (l.support ∩ set.to_finset H ∩ set.to_finset (Q.adjacent q))
(λ (x : Q (m + 1)), abs (l x) * abs ((ε q) ((f (m + 1) : _) (e x)))) :
begin
rw [← finset.sum_subset],
{ intros x Hx, simp[-finsupp.mem_support_iff] at Hx, exact Hx.left },
{ intros x H_mem H_not_mem,
by_cases x ∈ H,
{ simp at H_mem H_not_mem, rw[f_matrix], have := (H_not_mem ‹_› ‹_›),
{ suffices : (l x) = 0, by {simp [this]},
rw [finsupp.mem_supported'] at H_l₁, exact H_l₁ _ ‹_› } }
end
... ≤ ↑(finset.card (l.support ∩ set.to_finset H ∩ set.to_finset (Q.adjacent q))) * abs (l q) :
begin
refine le_trans (finset.sum_le_sum _) _,
{ exact λ p, abs (l q) },
{ intros x Hx, rw [f_matrix], simp at Hx,
have := Hx.right.right, change Q.adjacent _ _ at this,
rw [if_pos this.symm, mul_one], exact H_max x Hx.2.1 },
end
... ≤ ↑(finset.card (set.to_finset (H ∩ Q.adjacent q))) * abs (l q) :
begin
refine (mul_le_mul_right ‹_›).mpr _, norm_cast,
refine finset.card_le_of_subset (finset.coe_subset.mp _),
simpa only [finset.coe_inter, finset.coe_to_finset', set.inter_assoc]
using set.inter_subset_right _ _
end
end


#### Rob Lewis (Aug 05 2019 at 17:13):

A fix to what? I'm playing around with changing the definition of adjacent right now.

#### Johan Commelin (Aug 05 2019 at 17:24):

Oh, to Lean not parsing RQ_equiv_V.

#### Johan Commelin (Aug 05 2019 at 17:25):

So I'll get back to filling in that definition now.

#### Johan Commelin (Aug 05 2019 at 17:25):

@Rob Lewis What do you propose as new definition of adjacent?

#### Rob Lewis (Aug 05 2019 at 17:27):

I was hoping def adjacent {n : ℕ} (p : Q n) : set (Q n) := λ q, ∃! i, p i ≠ q i would simplify things a bit. It basically exchanges the difficulty of adjacent_iff_dist for adjacent_succ_iff though.

#### Rob Lewis (Aug 05 2019 at 17:28):

My (not quite complete) proof of adjacent_succ_iff is a bit longer but arguably a bit simpler, and I don't think it's optimized.

#### Johan Commelin (Aug 05 2019 at 17:45):

For some reason

def equiv_unique {α : Type*} {β : Type*} [unique α] [discrete_field β] :
(α →₀ β) ≃ₗ[β] β :=
{ to_fun := λ f, f (default α),
inv_fun := finsupp.single (default α),
smul := λ b f, rfl,
left_inv := λ f, (finsupp.unique_single _).symm,
right_inv := λ b, finsupp.single_eq_same }


is also extremely slow.

#### Johan Commelin (Aug 05 2019 at 17:47):

And if I change discrete_field to comm_ring it doesn't find add_comm_group for the LHS.

#### Johan Commelin (Aug 05 2019 at 17:47):

Even after importing algebra.pi_instances

#### Jesse Michael Han (Aug 05 2019 at 17:48):

yeah that looks good

my original version actually had begin .. end instead of by {} as well, but i thought that mathlib style forbids nested begin end blocks

#### Johan Commelin (Aug 05 2019 at 17:51):

What's this??

equation type mismatch, term
equiv_unique (Q 0) ℝ
has type
(Q 0 →₀ ℝ) ≃ₗ[ℝ] ℝ
but is expected to have type
(Q 0 →₀ ℝ) ≃ₗ[ℝ] V 0


#### Johan Commelin (Aug 05 2019 at 17:51):

V 0 is defeq to real.

#### Johan Commelin (Aug 05 2019 at 17:51):

Why doesn't it see that?

#### Chris Hughes (Aug 05 2019 at 17:55):

Is the module structure defeq?

I think so.

#### Johan Commelin (Aug 05 2019 at 17:57):

noncomputable instance : Π n, add_comm_group (V n) :=
begin
apply nat.rec,
{ dunfold V, apply_instance },
{ introsI n IH, dunfold V, apply_instance }
end

noncomputable instance : Π n, vector_space ℝ (V n) :=
begin
apply nat.rec,
{ dunfold V, apply_instance },
{ introsI n IH, dunfold V, apply_instance }
end


#### Rob Lewis (Aug 05 2019 at 17:57):

Not thrilled with the proof of adjacent_succ_iff. I'm not sure this is an improvement.

#### Rob Lewis (Aug 05 2019 at 17:57):

But I need to head home and eat dinner now.

#### Johan Commelin (Aug 05 2019 at 19:31):

I pushed another cleanup of degree_theorem

#### Johan Commelin (Aug 05 2019 at 19:32):

Maybe some parts at the top of the proof should be factored out into separate lemmas.

#### Floris van Doorn (Aug 05 2019 at 20:41):

(deleted - wrong topic)

#### Patrick Massot (Aug 05 2019 at 23:53):

Who could try to add the following lines after the definition of epsilon, and see if the commented lines timeout?

variables (n : ℕ) (v : V n)
local notation Ψ := finsupp.equiv_fun_on_fintype.inv_fun

/-
This following fails with by apply_instance, but defining it doesn't seem to help.
instance tata : vector_space ℝ (Q n →₀ ℝ) :=
{..finsupp.module (Q n) ℝ, .. }
-/

def coeffs {n : ℕ} (v : V n) : Q n →₀ ℝ := Ψ (λ p : Q n, ε p v)
def somme {n : ℕ} := (finsupp.total (Q n) (V n) ℝ e)

#check coeffs v -- coeffs v : Q n →₀ ℝ
#check @somme n  -- somme : (Q n →₀ ℝ) →ₗ[ℝ] V n
#check linear_map.to_fun somme  -- somme.to_fun : (Q ?M_1 →₀ ℝ) → V ?M_1

-- The following lines timeout
--#check linear_map.to_fun somme (coeffs v)
--#check linear_map.to_fun (@somme n)
--#check (Q n →₀ ℝ) →ₗ[ℝ] V n


#### Patrick Massot (Aug 05 2019 at 23:57):

Independently of this, I still think that the way we prove e is a basis is not optimal. What we really care about is the decomposition of vectors v : V n as a sum over p in Q n of (ε p v) • (e p) (the issues above were met while trying to write down this formula using the linear algebra library). In our current proof of the main theorem, this formula is somewhat hidden, because we use the fact e is a basis to get a mysterious sequence of coefficients unrelated to ε. One improvement could be to prove ε is equal to dual_basis e and use stuff in dual.lean. But we could just as well directly prove the decomposition formula

The key is:

#### Patrick Massot (Aug 05 2019 at 23:57):

lemma epsilon_total {n : ℕ} {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 :=
begin
induction n with n ih,
{ dsimp [ε] at h, exact h (λ _, tt) },
{ cases v with v₁ v₂,
ext ; change _ = (0 : V n) ; simp only [] ; apply ih ; intro p ;
[ let q : Q (n+1) := λ i, if h : i = 0 then tt else p (i.pred h),
let q : Q (n+1) := λ i, if h : i = 0 then ff else p (i.pred h)],
all_goals {
specialize h q,
rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|> rw [ε, show q 0 = ff, from rfl, cond_ff] at h,
rwa show p = q ∘ fin.succ, by { ext, simp [q, fin.succ_ne_zero] } } }
end


#### Patrick Massot (Aug 05 2019 at 23:58):

Which we can apply to a vector minus its intended decomposition (using the duality lemma).

#### Patrick Massot (Aug 05 2019 at 23:59):

If we insist on keeping that e is a basis then the above lemma (together with the duality lemma) reproves it

#### Patrick Massot (Aug 05 2019 at 23:59):

(this is all assuming we can use lemmas about sums over finsupp...)

#### Patrick Massot (Aug 06 2019 at 00:02):

Another thing that is surprisingly painful is the proof of have H_q_pos : 0 < abs (l q), in the main theorem. I think we should use that fintype.normed_group is using the supremum norm. So abs (l q) is actually the norm of y, hence positive using norm_pos_iff

#### Patrick Massot (Aug 06 2019 at 00:05):

And then I think the big calc at the end should have more steps and use more general lemmas about linear maps and dual bases.

#### Rob Lewis (Aug 06 2019 at 13:03):

I didn't think of a nice way to optimize the proof of adj_succ_iff with the "exists unique" definition of adjacent. But I did notice that the detour through dist is completely unnecessary. This is all we need about adjacent:



#### Patrick Massot (Aug 06 2019 at 13:05):

This is my proposal but still phrased in terms of bool rather than Z/2

#### Patrick Massot (Aug 06 2019 at 13:06):

I think this is a pretty clean definition, very close to what you would say when explaining the statement

#### Patrick Massot (Aug 06 2019 at 13:07):

But I'm not claiming it makes the proof of adjacent_succ_iff as short as we'd like it to be

(deleted)

#### Patrick Massot (Aug 06 2019 at 14:11):

I returned to this and finished this proof. I add the following trivial preliminaries:

lemma ne_iff_eq_bnot {b b' : bool} : b ≠ b' ↔ b = bnot b' :=
by cases b ; cases b' ; simp

@[simp]
lemma not_eq_bnot : ∀ b : bool, ¬ b = bnot b
| tt := λ h, bool.no_confusion h
| ff := λ h, bool.no_confusion h

lemma fin.eq_succ_iff_pred_eq {n : ℕ} {i : fin (n + 1)} {l : fin n}
(h : i ≠ 0) : i = fin.succ l ↔ (fin.pred i h = l) :=
begin
split ; intro H,
{ simp only [H, h, fin.pred_succ] },
{ simp only [H.symm, fin.succ_pred] }
end


#### Patrick Massot (Aug 06 2019 at 14:13):

And then the adjacency stuff becomes:

/-- flip i p flips the i-th bit of p -/
def flip {n : ℕ} (i : fin n) : Q n → Q n :=
λ p k, if i = k then bnot (p k) else p k

/-- The adjacency relation on Q^n: two vertices of the hypercube are adjacent if they differ at one bit. -/
def adjacent {n : ℕ} : Q n → (set $Q n) := λ p, {q | ∃ i : fin n, q = flip i p} @[simp] lemma not_adjacent_zero (p q : Q 0) : p.adjacent q = false := begin rw eq_false, rintro ⟨i, h⟩, fin_cases i end lemma adjacent_succ_iff {p q : Q (n+1)} : p.adjacent q ↔ (p 0 = q 0 ∧ adjacent (p ∘ fin.succ) (q ∘ fin.succ)) ∨ (p 0 ≠ q 0 ∧ p ∘ fin.succ = q ∘ fin.succ) := begin split, { rintros ⟨i, h⟩, rw h, by_cases hi : i = 0, { right, rw [hi, flip], split ; simp, ext l, simp [(fin.succ_ne_zero _).symm] }, { left, split, { simp [hi, flip] }, { use i.pred hi, ext l, dsimp [flip], congr' 1, rw fin.eq_succ_iff_pred_eq } } }, { rintro (⟨h₀, ⟨i, h⟩⟩ | ⟨h₀, h⟩), { use i.succ, ext l, by_cases hl : l = 0, { simp only [hl, flip, fin.succ_ne_zero, h₀, bnot, if_false] }, { have := congr_fun h (l.pred hl), simp at this, rw this, dsimp [flip], simp only [fin.succ_pred], have := fin.eq_succ_iff_pred_eq hl, conv_lhs at this { rw eq_comm }, conv_rhs at this { rw eq_comm }, congr' 1, rw ← this } }, { use 0, ext l, by_cases hl : l = 0, { simp [flip, hl, ne_iff_eq_bnot.1 h₀] }, { rw ← fin.succ_pred l hl, have := congr_fun h (l.pred hl), simp only [function.comp_app] at this, rw ← this, simp [flip, ne.symm hl] } } } end  #### Patrick Massot (Aug 06 2019 at 14:13): It seems there is some kind of pain conservation law here #### Patrick Massot (Aug 06 2019 at 14:13): @Rob Lewis #### Patrick Massot (Aug 06 2019 at 14:14): Maybe that solution is a bit orthogonal to the general design of our proof since it doesn't use induction on n at all #### Patrick Massot (Aug 06 2019 at 14:32): I forget symmetry: lemma flip_flip {n : ℕ} (i : fin n) (p : Q n) : flip i (flip i p) = p := begin ext l, dsimp [flip], split_ifs, simp end @[symm] lemma adjacent_comm {p q : Q n} : p.adjacent q ↔ q.adjacent p := by split ; rintro ⟨i, h⟩ ; rw h ; use i ; rw flip_flip  #### Patrick Massot (Aug 06 2019 at 14:44): Who could try to add the following lines after the definition of epsilon, and see if the commented lines timeout? variables (n : ℕ) (v : V n) local notation Ψ := finsupp.equiv_fun_on_fintype.inv_fun /- This following fails with by apply_instance, but defining it doesn't seem to help. instance tata : vector_space ℝ (Q n →₀ ℝ) := {..finsupp.module (Q n) ℝ, .. } -/ def coeffs {n : ℕ} (v : V n) : Q n →₀ ℝ := Ψ (λ p : Q n, ε p v) def somme {n : ℕ} := (finsupp.total (Q n) (V n) ℝ e) #check coeffs v -- coeffs v : Q n →₀ ℝ #check @somme n -- somme : (Q n →₀ ℝ) →ₗ[ℝ] V n #check linear_map.to_fun somme -- somme.to_fun : (Q ?M_1 →₀ ℝ) → V ?M_1 -- The following lines timeout --#check linear_map.to_fun somme (coeffs v) --#check linear_map.to_fun (@somme n) --#check (Q n →₀ ℝ) →ₗ[ℝ] V n  Does anyone has any explanation for the above mystery? #### Rob Lewis (Aug 06 2019 at 14:50): You're right that the induction isn't necessary. Ultimately we need these two facts; everything below goes through fine with just these. These proofs are for the "exists unique" definition of adjacent. lemma adj_succ {p q : Q (n+1)} (h0 : p 0 ≠ q 0) : p ∘ fin.succ = q ∘ fin.succ ↔ p.adjacent q := begin split, { intro heq, use [0, h0], intros y hy, contrapose! hy, rw ←fin.succ_pred _ hy, apply congr_fun heq }, { rintros ⟨i, h_eq, h_uni⟩, ext x, by_contradiction hx, apply fin.succ_ne_zero x, rw [h_uni _ hx, h_uni _ h0] } end lemma adj_succ_of_zeq {p q : Q (n+1)} (h0 : p 0 = q 0) : Q.adjacent (p ∘ fin.succ) (q ∘ fin.succ) ↔ p.adjacent q := begin split, { rintros ⟨i, h_eq, h_uni⟩, use [i.succ, h_eq], intros y hy, rw [←fin.pred_inj, fin.pred_succ], { apply h_uni, change p (fin.pred _ _).succ ≠ q (fin.pred _ _).succ, simp [hy] }, { contrapose! hy, rw [hy, h0] }, { apply fin.succ_ne_zero } }, { rintros ⟨i, h_eq, h_uni⟩, have h_i : i ≠ 0, from λ h_i, absurd h0 (by rwa h_i at h_eq), use [i.pred h_i, show p (fin.succ (fin.pred i _)) ≠ q (fin.succ (fin.pred i _)), by rwa [fin.succ_pred]], intros y hy, simp [eq.symm (h_uni _ hy)] } end  #### Patrick Massot (Aug 06 2019 at 14:53): I don't have a strong opinion about this exists_unique vs flip. I think both definition directly relate to the intuitive definition. #### Patrick Massot (Aug 06 2019 at 14:53): Why do you separate those two lemmas? Does it make later things easier? #### Patrick Massot (Aug 06 2019 at 14:54): Could you try my finsupp.total mystery? #### Rob Lewis (Aug 06 2019 at 14:54): I don't have time to debug the type class thing right now, but you can look at the trace here and see if you can make any sense: set_option trace.class_instances true include v example := by try_for 10000 {exact linear_map.to_fun somme (coeffs v)}  #### Rob Lewis (Aug 06 2019 at 14:55): I think it ended up being a bit cleaner with them separate. But I generally try to avoid disjunctions, so that's why this feels cleaner to me. #### Patrick Massot (Aug 06 2019 at 15:13): (message too long, truncated at 262144 characters) #### Patrick Massot (Aug 06 2019 at 15:21): It seems adding the shortcut instance toto : module ℝ (Q n →₀ ℝ) := finsupp.module (Q n) ℝ  helps a lot #### Patrick Massot (Aug 06 2019 at 15:21): Although the coercion from linear_map to function still doesn't kick in #### Rob Lewis (Aug 06 2019 at 15:23): Yes, the messages get truncated, but 262144 characters is usually plenty to find the problem... #### Rob Lewis (Aug 06 2019 at 15:23): Unsurprisingly there are type class issues in this whole development. You can add that to the short circuit instances for V. #### Johan Commelin (Aug 06 2019 at 15:24): Why "unsurprisingly"? #### Rob Lewis (Aug 06 2019 at 15:24): https://github.com/leanprover-community/lean-sensitivity/tree/new_adj is about as clean as I can get the adjacent stuff for now. #### Johan Commelin (Aug 06 2019 at 15:24): To me this is quite a surprise #### Rob Lewis (Aug 06 2019 at 15:26): I think it's been clear for a while that we're kind of abusing type class search. Whether it's our setup, or the inference algorithm itself, these kinds of issues are showing up a lot. #### Patrick Massot (Aug 06 2019 at 15:26): It's pretty clear that either we are doing it wrong, or Lean 3's type class is doing it wrong #### Patrick Massot (Aug 06 2019 at 15:26): Rob was quicker... #### Patrick Massot (Aug 06 2019 at 15:28): Rob, I think you can merge into master, I don't think anyone has a much better idea #### Kevin Buzzard (Aug 06 2019 at 15:54): Can someone summarise the problems you're having? #### Patrick Massot (Aug 06 2019 at 16:21): Kevin, there are several problems. The one I was discussing with Rob is to get a definition of the adjacency relation on the hypercube which is both easily recognizable and convenient for the proofs. I think we sort of settled that. #### Patrick Massot (Aug 06 2019 at 16:23): Then I went outside to help my youngest daughter training to ride a bicycle without side wheels. She's making progress but was tired. So i returned, and took up the big problem. #### Patrick Massot (Aug 06 2019 at 16:23): Which is the sum manipulation and basis and dual basis things. #### Patrick Massot (Aug 06 2019 at 16:23): Now that instances work, here is my proposal: #### Patrick Massot (Aug 06 2019 at 16:23): instance coeffs_module (n) : module ℝ (Q n →₀ ℝ) := finsupp.module (Q n) ℝ def coeffs {n : ℕ} (v : V n) : Q n →₀ ℝ := finsupp.equiv_fun_on_fintype.inv_fun (λ p : Q n, ε p v) def somme {n : ℕ} : (Q n →₀ ℝ) → V n := finsupp.total (Q n) (V n) ℝ e /-- For any v : V n, \sum_{p ∈ Q n} (ε p v) • e p = v -/ lemma decomposition {n : ℕ} (v : V n) : somme (coeffs v) = v := begin suffices : ∀ (p : Q n), ε p (somme$ coeffs v) = ε p v,
{ refine eq_of_sub_eq_zero (epsilon_total _),
intros p,
rw [linear_map.map_sub, sub_eq_zero_iff_eq, this] },
intro p,
erw [somme, finsupp.total_apply, linear_map.map_sum],
simp only [duality, map_smul, smul_eq_mul],
rw finset.sum_eq_single p,
{ simp, refl },
{ intros q q_in q_ne,
simp [q_ne.symm] },
{ intro p_not_in,
simp [finsupp.not_mem_support_iff.1 p_not_in] }
end


#### Patrick Massot (Aug 06 2019 at 16:25):

Note how this doesn not use e.is_basis or equiv_sum

#### Patrick Massot (Aug 06 2019 at 16:25):

I think this is going more straightly to the point

#### Patrick Massot (Aug 06 2019 at 16:27):

Modulo all the finsupp weirdness, it says exactly what the docstring claims

#### Patrick Massot (Aug 06 2019 at 16:27):

I think this could be the basis for a refactor of the main proof

#### Rob Lewis (Aug 06 2019 at 16:28):

What's somme? I keep reading that as a misspelling of some...

Oh sorry

#### Patrick Massot (Aug 06 2019 at 16:28):

It's French for sum

Aha.

#### Patrick Massot (Aug 06 2019 at 16:29):

At some point I wanted to avoid name clash

#### Patrick Massot (Aug 06 2019 at 16:29):

Of course it uses epsilon_total that I posted earlier

#### Patrick Massot (Aug 06 2019 at 16:29):

lemma epsilon_total {n : ℕ} {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 :=
begin
induction n with n ih,
{ dsimp [ε] at h, exact h (λ _, tt) },
{ cases v with v₁ v₂,
ext ; change _ = (0 : V n) ; simp only [] ; apply ih ; intro p ;
[ let q : Q (n+1) := λ i, if h : i = 0 then tt else p (i.pred h),
let q : Q (n+1) := λ i, if h : i = 0 then ff else p (i.pred h)],
all_goals {
specialize h q,
rw [ε, show q 0 = tt, from rfl, cond_tt] at h <|> rw [ε, show q 0 = ff, from rfl, cond_ff] at h,
rwa show p = q ∘ fin.succ, by { ext, simp [q, fin.succ_ne_zero] } } }
end


#### Patrick Massot (Aug 06 2019 at 16:31):

and duality. Together those lemmas are equivalent to the fact that e and epsilon are dual bases.

#### Rob Lewis (Aug 06 2019 at 16:35):

I haven't worked through your earlier posts very carefully, but if there's a chance this could clean up the bottom of the file, I'm in favor of trying...

#### Patrick Massot (Aug 07 2019 at 00:58):

Ok, I pushed something. The main goal is to shorten the final proof, make it easier to read, and transfer as much as possible into for_mathlib.lean. I followed my plan of using the duality as outline in my previous messages. Maybe I went too far, and I'm actually fighting the linear algebra library. But I still like how the final proof looks like. And I guess that Lean night already lasted too long (looks like it's now almost 3am...)

#### Rob Lewis (Aug 07 2019 at 09:33):

Nice, I think it looks great!

#### Patrick Massot (Aug 07 2019 at 10:39):

What I think it the final big thing is to generalize and move to mathlib https://github.com/leanprover-community/lean-sensitivity/blob/19c2800c9330ddf7130dac4ce22b7d2eb51afcfd/src/sensitivity.lean#L193-L247. It should connect with https://github.com/leanprover-community/mathlib/blob/master/src/linear_algebra/dual.lean. We could have a lemma characterizing pairs of dual bases (taking as input our statements duality and epsilon_total and outputting the conjunction that e is a basis and epsilon is its dual basis). And then replace the rest of the what I outlined in the first link by general lemmas about dual bases. Or, maybe more flexibly, we could have a duality predicate about two families of vector saying they form dual bases, and then state all lemmas in dual.lean in term of this predicate. As usual with predicate vs construction, the gain appears in exactly the situation we are in, when we want an alternative construction for some reason.

#### Patrick Massot (Aug 07 2019 at 10:42):

Honestly, I spent way too much time working on this sensitivity thing. Maybe someone who understands linear algebra in mathlib (and especially dual.lean) should take over (@Johan Commelin?). Today I'll bring my son to Penhir for climbing.

#### Patrick Massot (Aug 09 2019 at 21:23):

I'm frustrated that we can't advertise our sensitivity conjecture formalization so I tried again. I wrote https://github.com/leanprover-community/lean-sensitivity/commit/ed3d288f0fe696cc5a8049cad612f503ae2f4da3 about pairs of maps constituting a dual basis. It was a nightmare because elaboration was failing everywhere. And when I try to use it in the main file I get random mismatches of decidable_whatever. Maybe I was wrong when I wrote that function coercions were the main issue. It seems that decidability classes are there each time we really suffer in mathlib (see also polynomials). I give up.

#### Patrick Massot (Aug 09 2019 at 21:23):

I guess Rob is our last hope.

#### David Michael Roberts (Aug 10 2019 at 10:35):

working out pi to 7 decimal places,

where was that done? I can't find it after a little look here in the chat.

#### Mario Carneiro (Aug 10 2019 at 10:46):

I think it was our pi day activity

#### Kevin Buzzard (Aug 10 2019 at 11:18):

They worked it out to a million decimal places in Coq once, but I would imagine the process took more than 24 hours in total. What has been interesting recently is that questions have come up and then a group of people have worked on them and within a day or two the code is up and running.

#### David Michael Roberts (Aug 10 2019 at 13:27):

Though the seven decimal places include the 3., that's still pretty nice.

#### Reid Barton (Aug 10 2019 at 14:13):

I also have the impression that decidable_eq requirements are somehow responsible for a lot of pain, though I have no data or understanding of why that would be.

#### Rob Lewis (Aug 21 2019 at 09:54):

@Patrick Massot What were the issues you were having here? It seems like things compile, and I don't see any nightmares in the file right now.

#### Rob Lewis (Aug 21 2019 at 09:54):

I was planning to try to move some of the lemmas to mathlib and put this in the archive. Are there still major changes you want to make?

#### Patrick Massot (Aug 21 2019 at 10:59):

I think I've explained it in previous messages. This minor nightmare is https://github.com/leanprover-community/lean-sensitivity/blob/lean-3.4.2/src/sensitivity.lean#L154-L247 which was meant to be replaced by calling https://github.com/leanprover-community/lean-sensitivity/blob/lean-3.4.2/src/for_mathlib.lean#L25-L103 but I couldn't make it work because of conflicting decidable instances (mixing actual instances and classical.prop_decidable I guess). Also https://github.com/leanprover-community/lean-sensitivity/blob/lean-3.4.2/src/sensitivity.lean#L117-L140 looks stupid since we then explicitly describe a basis.

#### Patrick Massot (Aug 21 2019 at 11:00):

I would really love it if you could have a look at this decidability nightmare

#### Patrick Massot (Aug 21 2019 at 11:01):

When we rushed to prove this theorem I thought that within one week we would be able to post comments to all blogs discussing this theorem to point out it was very quickly formalized. Instead we have one more proof that formalization is not practicable for stupid reasons.

#### Rob Lewis (Aug 21 2019 at 11:13):

I'll see what I can do.

#### Kevin Buzzard (Aug 21 2019 at 11:28):

I wasn't involved but I thought that it was indeed quickly formalised

#### Rob Lewis (Aug 21 2019 at 11:32):

It was quickly formalized but it's not a perfect formalization. To brag about something this short, it kind of has to be done canonically, and the problem (I think) is that Patrick struggled to get the canonical proof to work.

#### Patrick Massot (Aug 21 2019 at 11:33):

We don't need it to be perfect, but I'd like it to be recognizable maths

#### Rob Lewis (Aug 21 2019 at 13:44):

@Patrick Massot I just pushed an update. Is this what you had in mind? The decidability issues were nothing major. We were missing a decidable_eq instance for V n, which was confusing things in a few places.

#### Rob Lewis (Aug 21 2019 at 13:52):

In fact, the specific dec_eq instance I gave it isn't necessary. Defining it using classical.dec_eq is fine too. But without the explicit instance, it seems to be inferring different dec_eqs in different places.

#### Rob Lewis (Aug 21 2019 at 13:52):

It's all kind of ironic since V definitely isn't decidable. There are non-defeq ways to pretend that it is.

#### Patrick Massot (Aug 21 2019 at 14:54):

Yes, it looks good. I'm happy you found it easy. I'm so upset by those kinds of problems that my mind refuse to work on them.

#### Patrick Massot (Aug 21 2019 at 14:54):

What is the point of getting calc_lemma out of the theorem proof?

#### Kevin Buzzard (Aug 21 2019 at 14:54):

We mathematicians just instinctively deny that such (decidability) issues can exist, because we've been ignoring them for centuries.

#### Patrick Massot (Aug 21 2019 at 14:55):

I think https://github.com/leanprover-community/lean-sensitivity/blob/a4b69d68217b7b8319a03f3406f4fba6147b2f91/src/sensitivity.lean#L194-L202 are not needed, we can use their proofs where we need them

#### Patrick Massot (Aug 21 2019 at 14:57):

And we still have that silly dimension computation. We should have a mathlib lemma stating that if V has a basis index by a finite type then its findim is the cardinal of this finite type, and of course a lemma computing the cardinal of fin n to bool

#### Rob Lewis (Aug 21 2019 at 14:59):

What is the point of getting calc_lemma out of the theorem proof?

That calc block is a memory hog. I moved it out to make it easier to fix, it doesn't have to stay out. Also gave me a chance to try extract_goal, which stumbles a bit with let statements.

#### Rob Lewis (Aug 21 2019 at 15:00):

I think https://github.com/leanprover-community/lean-sensitivity/blob/a4b69d68217b7b8319a03f3406f4fba6147b2f91/src/sensitivity.lean#L194-L202 are not needed, we can use their proofs where we need them

Yeah. Again, just slightly easier to put them there while making the updates.

#### Rob Lewis (Aug 21 2019 at 16:02):

And we still have that silly dimension computation. We should have a mathlib lemma stating that if V has a basis index by a finite type then its findim is the cardinal of this finite type, and of course a lemma computing the cardinal of fin n to bool

This is more annoying than it should be because of cardinal universes.

#### Patrick Massot (Aug 21 2019 at 16:03):

I really think mathlib should hide this to users who manipulate only finite-dimensional vector spaces (as we do in this proof)

#### Patrick Massot (Aug 21 2019 at 16:03):

If we can't do that then the linear algebra library has a serious issue

#### Rob Lewis (Aug 21 2019 at 16:09):

I think this is what linear_algebra/finite_dimensional.lean is trying to do, but there's still some glue missing.

#### Rob Lewis (Aug 21 2019 at 16:12):

fg doesn't seem to be linked up with the existence of a finite basis, as far as I can tell.

#### Rob Lewis (Aug 21 2019 at 23:26):

Turns out I work better late at night and this was much easier than I thought. https://github.com/leanprover-community/lean-sensitivity/commit/af28ecfab7f412f7d451a4ff4cf328aad322eae3

#### Patrick Massot (Aug 22 2019 at 15:16):

Thanks Rob! I finally had some time to look at it. I would still prefer to hide cardinal even more (or at least have only one of dim_V or dim_V') but it's already much better. I feel sufficiently confident that we are close to something we could share (and I feel sufficiently confident I don't want to write that referee report I should be writing) that I made a cosmetic pass on the whole file: https://github.com/leanprover-community/lean-sensitivity/commit/4feaed5a407676a45327854595bd3e4b319c4f7e I hope there aren't too many controversial changes (especially for equation compiler addicts). Everyone is free to tweak it.

#### Patrick Massot (Aug 22 2019 at 15:18):

I also reintegrated the calc block in the main proof.

#### Patrick Massot (Aug 22 2019 at 15:32):

And now we can go on removing stuff that just got merged in mathlib, and continue emptying for_mathlib.lean

#### Rob Lewis (Aug 22 2019 at 16:00):

It looks good! I just pushed an update that gets rid of dim_V'. But updating mathlib breaks the assumption_mod_castin findim_V, I'm not sure why.

#### Rob Lewis (Aug 22 2019 at 16:12):

Fixed. https://github.com/leanprover-community/lean-sensitivity/tree/upgraded_mathlib on a branch for now so it doesn't interfere with update-mathlib. After the next nightly comes out, we can upgrade to that and merge to master.

#### Rob Lewis (Aug 22 2019 at 16:15):

@Paul-Nicolas Madelaine At https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/cardinal.lean#L589, is nat_cast_pow (and nat_cast_le) a good elim_cast lemma? Maybe I was wrong to add that.

#### Patrick Massot (Aug 23 2019 at 08:16):

Rob, do you understand the crazy https://github.com/leanprover-community/lean-sensitivity/commit/658b12067f73e85fe27e6108bed92b2148c454da or is it the result of random desperate modifications?

#### Rob Lewis (Aug 23 2019 at 08:45):

That commit in particular, or the short circuits more generally? They were local to the namespace V before, which ended right after they were declared, so they were doing absolutely nothing.

Oh ok

#### Patrick Massot (Aug 23 2019 at 08:46):

I'm sorry I messed up that

#### Patrick Massot (Aug 23 2019 at 08:47):

I just pushed some more tweaks to make statements look nicer (at least to my eye)

#### Patrick Massot (Aug 23 2019 at 08:47):

Did you make progress on the mathlib bump issue?

#### Rob Lewis (Aug 23 2019 at 08:48):

No worries. It was obvious something was wrong when I opened it on my laptop, the extra 25 seconds to compile are noticeable.

#### Rob Lewis (Aug 23 2019 at 08:49):

I think the next mathlib nightly goes up once the next PR gets merged and built, right?

#### Rob Lewis (Aug 23 2019 at 08:49):

Then we run leanpkg upgrade on the upgraded_mathlib branch and rebase.

#### Patrick Massot (Aug 23 2019 at 08:50):

I think the remaining ugliness in statements now all come from elaboration issues (the obvious ones like (f (m + 1) : _) w = √(m + 1) • w but also the sneaky ones like being forced to write √(m + 1) ≤ Card (H ∩ q.adjacent) instead of switching sides to match the way we would say it).

#### Patrick Massot (Aug 23 2019 at 08:51):

Oh, I thought you had trouble with the question you asked PN

#### Rob Lewis (Aug 23 2019 at 08:52):

Oh, that's fixed locally, I was just wondering if it should be a global change.

#### Patrick Massot (Aug 23 2019 at 08:52):

apply' just got merged so we should get a new nightly soon

#### Patrick Massot (Aug 23 2019 at 08:53):

Of course we can always trigger a new nightly build by hand if we are in a hurry

#### Patrick Massot (Aug 23 2019 at 08:54):

Back to mathematics, I wonder why the theorem is stated (in our formalization and in the original paper) for positive n. Isn't the statement obviously true when n = 0?

#### Rob Lewis (Aug 23 2019 at 08:54):

I'll need to run soon, got a friend in town visiting. But your changes look fine. There's dead code on lines 344-345.

#### Patrick Massot (Aug 23 2019 at 08:55):

oops, forgot to delete that. I'll do it right now

#### Paul-Nicolas Madelaine (Aug 23 2019 at 09:31):

@Rob Lewis nat_cast_le is a good elim_cast lemma and nat_cast_pow should be a move_cast lemma.
something to keep in mind that I should also write explicitely in the documentation is that move_cast lemmas are going to be used from right to left.
so in that case, the nat_cast_pow lemma will turn ↑n ^ m into ↑(pow n m), which can be a bit weird if the ^ notation is defined on cardinals.
I'll add these notes to the documentation as soon as I am done with the report.

#### Patrick Massot (Aug 23 2019 at 11:12):

Ok, we are up to date with mathlib, and ready for the next round of PR

#### Jesse Michael Han (Aug 24 2019 at 19:11):

on the reduction branch i started on the reduction of the original sensitivity conjecture to the degree theorem we formalized

#### Jesse Michael Han (Aug 24 2019 at 19:12):

it looks manageable except that the proof of gotsman_linial_equivalence uses Fourier transforms

#### Patrick Massot (Aug 24 2019 at 19:59):

That sounds like a big "except"

#### Daniel Donnelly (Aug 24 2019 at 20:09):

Why can't Lean handle FT? Not that I need it for my app or anything...

#### Patrick Massot (Aug 24 2019 at 20:14):

Oh, it can. But someone needs to explain it to Lean.

#### Patrick Massot (Aug 24 2019 at 20:14):

And analysis is not mathlib's strong point

#### Scott Morrison (Aug 24 2019 at 22:59):

It's not really Fourier transforms in the Gotsman-Linial argument --- it's just the Z/2Z valued version, no analysis involved at all.

#### Scott Morrison (Aug 24 2019 at 22:59):

In fact the proof is just a few lines, even easier than Huang's recent argument.

#### Daniel Donnelly (Aug 24 2019 at 23:05):

I can attest to that. Has to do with sums of roots of unity in any field.

#### Jesse Michael Han (Aug 24 2019 at 23:06):

oh, good

then maybe soon we can say that we really formalized the sensitivity conjecture

#### Scott Morrison (Aug 24 2019 at 23:32):

The Gotsman-Linial argument is in https://www.sciencedirect.com/science/article/pii/0097316592900608, which is free online. There's also a restatement of the proof at https://blog.computationalcomplexity.org/2019/07/degree-and-sensitivity.html.

#### Scott Morrison (Aug 24 2019 at 23:34):

I'm not sure what EnjoysMath meant, but there's nothing in the argument about sums of roots of unity, it's just counting signs in the GL argument.

#### Rob Lewis (Aug 27 2019 at 07:30):

I was trying to figure out why this project was so slow to compile on my laptop. Looks like we have another performance issue when we get deep into the mathlib file hierarchy: building the default simp set at the beginning of for_mathlib.lean takes 1.5 sec (on my laptop, 1 sec on my desktop). This happens once in every declaration that uses simp without only.

#### Johan Commelin (Aug 27 2019 at 07:34):

/me hears Kenny rolling on the floor lauging out loud

#### Johan Commelin (Aug 27 2019 at 07:35):

@Kenny Lau In how many different languages do you know the word “Schadenfreude”?

#### Scott Morrison (Aug 27 2019 at 08:20):

Like, maybe this enterprise is actually doomed, bad. :-)

#### Chris Hughes (Aug 27 2019 at 08:28):

I think this is maybe a case for being careful about minimising imports. It won't improve speed for everyone, but certainly it will improve speed a lot of the time. I think there were a lot of unnecessary imports for that proof.

#### Johan Commelin (Aug 27 2019 at 08:41):

[…] building the default simp set at the beginning of for_mathlib.lean takes 1.5 sec (on my laptop, 1 sec on my desktop). This happens once in every declaration that uses simp without only.

Isn't this something that can be cached?

#### Rob Lewis (Aug 27 2019 at 08:51):

It's not like it's an inherent problem -- I don't think Isabelle has the same behavior. Caching the simp set is probably pretty complicated because of multithreading. There's maybe something to be done there, but definitely not doable from mathlib.

#### Rob Lewis (Aug 27 2019 at 08:52):

It's the best case I've heard yet for minimizing imports. But I'm not sure how much it will really buy in the end. Maybe it helps this specific proof, but it will be a recurring issue.

#### Rob Lewis (Aug 27 2019 at 08:54):

It's fairly slow even just importing analysis.normed_space.basic.

#### Scott Morrison (Aug 27 2019 at 09:03):

I wonder if we should also be using local attribute [simp] more, or custom simp sets.

#### Floris van Doorn (Aug 27 2019 at 15:35):

I was always wondering whether the amount of simp declarations would cause performance issues. Limiting the number of imports might help a bit, but that is not a sustainable solution. Other potential solutions:

• Can we write a user command at the top of a file that generates and caches the standard simp set, which all declarations in that file can then use? (Potentially modifying them a little bit, since some new simp-lemmas might be added).
• As Scott said, make extensive use of simp-sets: instead of marking everything with @[simp] we mark things as topology_simp and linear_algebra_simp and with simp with topology_simp. Obviously this is a less nice user experience.
• Be more restrictive with marking declarations as simp. Maybe not every simplification should be a simp-lemma. This will probably not make a big enough impact, since most simp-lemmas should remain simp-lemmas.

#### Rob Lewis (Aug 27 2019 at 16:53):

Can we write a user command at the top of a file that generates and caches the standard simp set, which all declarations in that file can then use? (Potentially modifying them a little bit, since some new simp-lemmas might be added).

And define a new tactic simp' to use our cache? That would probably be doable. I'm not sure how efficiently we can generate a cache compared to the built in methods. And I think it's pretty common to progressively prove a bunch of simp lemmas in a file, which may use each other, and then a lot of theorems that use these simp rules right after. We'd have to modify a lot of proofs and/or regenerate the cache a bunch of times per file.

#### Rob Lewis (Aug 27 2019 at 16:54):

I wonder if we should also be using local attribute [simp] more, or custom simp sets.

This seems like the most effective way to speed things up, and also a huge pain.

#### Rob Lewis (Aug 27 2019 at 16:54):

The alternative, of course, is to not change anything for now and see how things look in :four_leaf_clover: .

#### Rob Lewis (Aug 27 2019 at 16:58):

There are some simp sets that are pretty self-contained. I'm thinking of all the rules for making sense of filters. That would be a pretty natural thing to factor out of the default simp set.

#### Johan Commelin (Aug 27 2019 at 16:59):

Why is this not an issue in Isabelle?

#### Patrick Massot (Aug 27 2019 at 17:31):

Johan, did you ever read https://github.com/leanprover/lean/wiki/Simplifier-Features to see what the simplifier could look like?

#### Johan Commelin (Aug 27 2019 at 17:42):

Patrick, nope, I didn't.

#### Johan Commelin (Aug 27 2019 at 17:45):

It's an inspiring wiki page, thanks for the link!

Last updated: May 06 2021 at 18:20 UTC