# Zulip Chat Archive

## 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

See also Donald Knuth's condensation of the proof: https://www.cs.stanford.edu/~knuth/papers/huang.pdf

#### 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?

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

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

#### Chris Hughes (Aug 02 2019 at 13:05):

Is there an easy way to see the pdf version?

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

rofl kids these days

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

One sec

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

#### 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?

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

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 rw [f, nat.cast_add, add_smul], simp [fn2], rw [add_comm], convert add_sub_cancel _ _ 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_p`

s.

#### 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_p`

s.

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):

How about

/-- 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

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

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.

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

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 `sorry`

s 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 `sorry`

s 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.

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

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?

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

afk

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

What's your github username again?

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

`jesse-michael-han`

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

Cool, added

#### 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

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

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?

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

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 (-;

#### Chris Hughes (Aug 02 2019 at 20:23):

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

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

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.

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

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:

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

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

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

#### 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!

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

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.

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

I'm tackling adjacent_symm

#### 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.

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

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):

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

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

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

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

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

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.

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

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?

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

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

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

Sure thing.

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

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):

You're giving away your secrets!

#### 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.

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

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)

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

reboot your computer??

#### 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):

Does adding this before help?

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?

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

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...

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

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...

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

Nice.

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

also pushed my `calc`

ification

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 ‹_› ‹_›), change ¬ Q.adjacent _ _ at this, simp [Q.adjacent_comm, this] }, { 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 }, { simp only [mul_one, finset.sum_const, add_monoid.smul_one, add_monoid.smul_eq_mul] } 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 α), add := λ f g, finsupp.add_apply, 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?

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

I think so.

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

https://github.com/leanprover-community/lean-sensitivity/tree/new_adj

#### 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

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

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`

:

def adjacent : Π {n : ℕ}, Q n → (set $ Q n) | 0 p q := false | (n+1) p q := (p 0 = q 0 ∧ adjacent (p ∘ fin.succ) (q ∘ fin.succ)) ∨ (p 0 ≠ q 0 ∧ p ∘ fin.succ = q ∘ fin.succ) lemma adjacent.symm : ∀ {n} {p q : Q n}, p.adjacent q → q.adjacent p | (n+1) p q (or.inl ⟨h_eq, h_adj⟩) := or.inl ⟨h_eq.symm, h_adj.symm⟩ | (n+1) p q (or.inr ⟨h_ne, h_eq⟩) := or.inr ⟨h_ne.symm, h_eq.symm⟩ lemma adjacent_comm {p q : Q n} : p.adjacent q ↔ q.adjacent p := ⟨adjacent.symm, adjacent.symm⟩ 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) := iff.refl _ lemma not_adjacent_zero (p q : Q 0) : ¬ p.adjacent q := by rintros ⟨v, _⟩; apply fin_zero_elim v

Using an inductive prop for `adjacent`

looks very slightly cleaner, I think, but forces some packing and unpacking in `adjacent_succ_iff`

.

inductive adjacent : ∀ {n}, Q n → Q n → Prop | zero {n} {p q : Q (n+1)} : p 0 ≠ q 0 → p ∘ fin.succ = q ∘ fin.succ → adjacent p q | nonzero {n} {p q : Q (n+1)} : p 0 = q 0 → adjacent (p ∘ fin.succ) (q ∘ fin.succ) → adjacent p q

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

I'm currently playing with this `adjacent_succ_iff`

thing

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

Using my proposed definition of `adjacent`

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

Which definition is that?

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

/-- `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 def adjacent {n : ℕ} : Q n → (set $ Q n) := λ p, {q | ∃ i : fin n, q = flip i p}

#### 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

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

(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`

...

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

Oh sorry

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

It's French for sum

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

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.

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

What do you think about this?

#### 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):

see https://github.com/leanprover-community/mathlib/blob/master/src/data/real/pi.lean#L193-L229 and the linked gist at https://gist.github.com/fpvandoorn/5b405988bc2e61953d56e3597db16ecf

#### 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_cast`

in `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.

#### Patrick Massot (Aug 23 2019 at 08:46):

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):

Wow, that’s really bad.

#### 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