sensitivity conjecture

Stream: maths

[Johan Commelin]

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]

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

[Johan Commelin]

And how far did you get with the inverse matrix?

[Chris Hughes]

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]

But this isn't in mathlib yet, right?

[Chris Hughes]

No.

[Chris Hughes]

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

[Reid Barton]

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]

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]

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

[Chris Hughes]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

Is there an easy way to see the pdf version?

[Kevin Buzzard]

rofl kids these days

[Reid Barton]

One sec

[Reid Barton]

sensitivity.pdf

[Johan Commelin]

That looks quite formalisable, I think.

[Johan Commelin]

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

[Johan Commelin]

Anything else that we need?

[Johan Commelin]

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

[Reid Barton]

Haven't started

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

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]

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

[Johan Commelin]

The rest is straight-forward, I think.

[Rob Lewis]

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]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

I was about to get started actually

[Johan Commelin]

Why do you build mathlib?

[Johan Commelin]

I haven't built mathlib in 3 months

[Reid Barton]

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

[Reid Barton]

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]

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

[Rob Lewis]

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]

Ah yes, linear_map.fst/snd/prod

[Reid Barton]

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

Is noncomputable theory inside a section?

[Rob Lewis]

noncomputable theory doesn't always propogate to aux decls.

[Reid Barton]

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

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

[Rob Lewis]

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]

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]

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]

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]

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

[Floris van Doorn]

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

[Johan Commelin]

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]

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

Dual basis is in mathlib

[Reid Barton]

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]

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]

I agree it's not cheating by much.

[Johan Commelin]

@Floris van Doorn But you changed the definition of V

[Reid Barton]

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]

Which is I think what Rob was going to do

[Floris van Doorn]

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]

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

[Johan Commelin]

Do we want to define e directly?

[Johan Commelin]

I don't really care.

[Johan Commelin]

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

[Reid Barton]

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]

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

[Rob Lewis]

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]

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]

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]

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]

but maybe in that aspect the recursive definition is easier.

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

It should suffice to prove linear independence

[Reid Barton]

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]

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

Yeah that's true

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

Ooh, that def should be a simp-lemma

[Reid Barton]

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]

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

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

This one sounds good

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

Need to feed some kids :children_crossing: brb

[Johan Commelin]

Huh, there is no has_xor typeclass??

[Johan Commelin]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Patrick Massot]

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

[Johan Commelin]

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]

Johan, which definition of Q n is this using?

[Patrick Massot]

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

[Reid Barton]

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

[Reid Barton]

then perhaps we can distribute the representation decisions

[Patrick Massot]

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

[Johan Commelin]

This is with Q n := fin n → bool

[Reid Barton]

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

[Reid Barton]

Except with a correct statement of f_matrix_nonadjacent

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Patrick Massot]

thanks!

[Patrick Massot]

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

[Patrick Massot]

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

[Rob Lewis]

@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]

Sure!

[Reid Barton]

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]

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]

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

[Johan Commelin]

Since you are admin of leanprover-community, right?

[Reid Barton]

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]

Oh, maybe. But thanks anyway!

[Rob Lewis]

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]

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

[Reid Barton]

I pushed another commit about g

[Patrick Massot]

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

[Patrick Massot]

(which I indeed modified from Johan's message)

[Jesse Michael Han]

i'm also happy to contribute

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

[Reid Barton]

Oh dang, H is not a great name

[Reid Barton]

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

[Johan Commelin]

I'm inductively proving that e is a basis.

[Johan Commelin]

See the jmc branch

[Patrick Massot]

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

[Patrick Massot]

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

[Reid Barton]

Lean isn't yet happy with the theorem statement

@Johan Commelin were you having trouble with type classes?

[Johan Commelin]

Well, sets weren't finsets and such

[Johan Commelin]

There is a working statement on the jmc branch

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Patrick Massot]

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

[Jesse Michael Han]

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]

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

[Reid Barton]

that leaves f_image_g and exists_eigenvalue

[Johan Commelin]

I'll push what I have now.

[Johan Commelin]

Ok, I pushed

[Johan Commelin]

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

[Jesse Michael Han]

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]

afk

[Reid Barton]

What's your github username again?

[Jesse Michael Han]

jesse-michael-han

[Reid Barton]

Cool, added

[Patrick Massot]

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]

I guess I should use pattern matching

[Johan Commelin]

Check what I did

[Johan Commelin]

I've used cond (x 0) stuff

[Patrick Massot]

This is not quite the same question, is it?

[Johan Commelin]

Maybe not

[Patrick Massot]

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

[Johan Commelin]

Right, I was too fast... sorry

[Reid Barton]

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]

I found the library bit I was missing

[Patrick Massot]

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

[Johan Commelin]

That's what I used

[Patrick Massot]

I was missing pred

[Johan Commelin]

I already pushed that equiv @Reid Barton

[Patrick Massot]

Sorry Johan, I focused on your cond and missed pred

[Reid Barton]

Oh I see, just defined manually yeah

[Reid Barton]

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]

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

[Johan Commelin]

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

[Chris Hughes]

finsets ftw.

[Floris van Doorn]

@Patrick Massot: I would suggest

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

[Patrick Massot]

What is that?

[Floris van Doorn]

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

[Patrick Massot]

Oh I see

[Patrick Massot]

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

[Floris van Doorn]

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]

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

[Patrick Massot]

It seems harder to prove lemmas about it

[Patrick Massot]

but probably I'm missing library lemmas

[Johan Commelin]

I'm calling it a day

[Johan Commelin]

Unfortunately e is still not a basis

[Johan Commelin]

I pushed the mess that I have so far.

[Patrick Massot]

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

[Patrick Massot]

And I'm very bad at it

[Jesse Michael Han]

i'm halfway done with f_image_g

[Floris van Doorn]

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]

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]

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]

[edited] oops i missed the invite link

[Patrick Massot]

I'm done computing the matrix

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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

[Johan Commelin]

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

[Patrick Massot]

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]

@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]

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

[Jesse Michael Han]

oh, i didn't see f_squared

yeah that looks much better

[Patrick Massot]

Did you look at the pdf proof?

[Jesse Michael Han]

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

[Patrick Massot]

Anyway, is anybody working on the next lemma?

[Patrick Massot]

I mean exists_eigenvalue

[Patrick Massot]

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

[Jesse Michael Han]

i'm not working on it

i was going to wait to hear back from reid

[Patrick Massot]

exists_mem_ne_zero_of_dim_pos looks very promising

[Jesse Michael Han]

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]

I finished e_is_basis that @Johan Commelin almost did yesterday

[Patrick Massot]

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

[Patrick Massot]

I tried to merge and I see it times out

[Patrick Massot]

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

[Patrick Massot]

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

[Jesse Michael Han]

i'll take a look

[Patrick Massot]

For instance I need to prove:

n : ℕ
⊢ 2 ^ n < cardinal.omega

[Patrick Massot]

and

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

Where at least some of this stuff is in cardinals

[Patrick Massot]

I won't do more tonight.

[Jesse Michael Han]

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

[Chris Hughes]

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]

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

[Patrick Massot]

For instance, do you have dim_sup_add_dim_inf_eq for findim?

[Patrick Massot]

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

[Chris Hughes]

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]

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]

most facts about numbers being equivalent to finite cardinals are proven

[Patrick Massot]

what do you mean?

[Chris Hughes]

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

[Patrick Massot]

Are they tagged for use by norm_cast?

[Patrick Massot]

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

[Jesse Michael Han]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Jesse Michael Han]

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]

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

[Patrick Massot]

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

[Patrick Massot]

Maybe you can even finish the whole thing while I sleep

[Patrick Massot]

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

[Patrick Massot]

Zulip says his local time is 6:30pm

[Patrick Massot]

This leaves him the whole evening and night

[Patrick Massot]

and same for you!

[Patrick Massot]

Have fun!

[Yao Liu]

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]

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]

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]

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]

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

[Jesse Michael Han]

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

[Jesse Michael Han]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Chris Hughes]

Looks like two sorries right now.

[Chris Hughes]

Neither are that hard.

[Johan Commelin]

I'm tackling adjacent_symm

[Chris Hughes]

I just proved that.

[Chris Hughes]

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

[Chris Hughes]

One sorry left now.

[Johan Commelin]

@Chris Hughes Are you still working on this?

[Johan Commelin]

I connected adjacent back to my definition that used dist.

[Chris Hughes]

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]

Ok, I see.

[Patrick Massot]

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]

I'm almost done with the final sorry.

[Johan Commelin]

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

[Patrick Massot]

Oh, I was starting on this final sorry

[Patrick Massot]

Do you mind if I finish during your lunch?

[Patrick Massot]

@Johan Commelin should I push?

[Patrick Massot]

Ok, let's say he was really having lunch

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

Nice, well done!

[Johan Commelin]

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

[Kevin Buzzard]

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]

It's still a lot harder than it should be

[Kevin Buzzard]

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

[Patrick Massot]

Unless you already know perfectly all the relevant part of mathlib

[Patrick Massot]

Oh yes of course

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

What does that mean?

[Johan Commelin]

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

[Kevin Buzzard]

for sure

[Johan Commelin]

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

[Patrick Massot]

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]

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

[Johan Commelin]

@Patrick Massot Why would that help?

[Kevin Buzzard]

I think your suggestion is a really worthwhile one Johan.

[Patrick Massot]

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

[Johan Commelin]

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

[Kevin Buzzard]

Looks

[Patrick Massot]

A group structure

[Patrick Massot]

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]

I think this would give a much more recognizable adjacency relation

[Kevin Buzzard]

instead of this weird CS bool thing

Mathematicians still failing to come to terms with weird CS stuff

[Patrick Massot]

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]

@Patrick Massot Ok, that seems fine.

[Kevin Buzzard]

x \ne y?

[Patrick Massot]

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]

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

[Patrick Massot]

I also need to go

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Reid Barton]

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]

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]

I just pushed it 20 seconds ago...

[Rob Lewis]

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

[Reid Barton]

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

[Rob Lewis]

Sure thing.

[Reid Barton]

OK, pushed

[Reid Barton]

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]

Although I guess this means proving something similar to adjacent_iff_dist

[Reid Barton]

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

[Rob Lewis]

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

[Rob Lewis]

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]

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

[Kevin Buzzard]

You're giving away your secrets!

[Kevin Buzzard]

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

[Rob Lewis]

. might have the same effect. Not sure.

[Johan Commelin]

I always use .

[Reid Barton]

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

[Reid Barton]

The dependencies are definitely built

[Johan Commelin]

I added some foo_apply lemmas and golfed f_image_g.

[Rob Lewis]

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]

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

[Reid Barton]

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

[Rob Lewis]

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

[Kevin Buzzard]

restart Lean?

[Rob Lewis]

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]

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

[Reid Barton]

(not related to that module instance)

[Kevin Buzzard]

reboot your computer??

[Patrick Massot]

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]

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

[Reid Barton]

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]

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]

It takes ages to parse/elaborate/tc this

[Johan Commelin]

Result: 4 deterministic timeouts

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Johan Commelin]

Doesn't help for this thing :sad:

[Johan Commelin]

Btw, should we even use real numbers?

[Johan Commelin]

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

[Johan Commelin]

So we could do the whole thing with ℤ-modules

[Johan Commelin]

Anyway, I don't mind using real.

[Johan Commelin]

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

[Johan Commelin]

@Reid Barton Have your problems gone away?

[Reid Barton]

Some of them

[Rob Lewis]

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]

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]

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]

@Jesse Michael Han Yes. . is gold.

[Reid Barton]

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

[Reid Barton]

Is the default memory limit different in VS code maybe?

[Kevin Buzzard]

It's 100000 in VS Code I believe

[Kevin Buzzard]

The T50000 challenge was what happened when I halved it

[Reid Barton]

That's the "time" limit I thought

[Kevin Buzzard]

oh apologies. Memory limit is...

[Kevin Buzzard]

4096 megs

[Reid Barton]

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

[Jesse Michael Han]

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

4096 megs and constantly swapping

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

Not sure if we want to do things like that.

[Rob Lewis]

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

[Rob Lewis]

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

[Johan Commelin]

Can you get the statement of RQ_equiv_V to work?

[Johan Commelin]

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

[Johan Commelin]

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

[Rob Lewis]

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]

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

[Johan Commelin]

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

[Johan Commelin]

I just pushed a compression of duality.

[Jesse Michael Han]

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]

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]

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

[Rob Lewis]

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

[Reid Barton]

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

[Reid Barton]

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

[Rob Lewis]

Nice.

[Jesse Michael Han]

also pushed my calcification

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

[Johan Commelin]

Nice work @Reid Barton and @Jesse Michael Han

[Johan Commelin]

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

[Johan Commelin]

Of course that's a very minor issue

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

It seems that Rob found a fix.

[Johan Commelin]

@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]

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

[Johan Commelin]

Oh, to Lean not parsing RQ_equiv_V.

[Johan Commelin]

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

[Johan Commelin]

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

[Rob Lewis]

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]

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]

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]

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

[Johan Commelin]

Even after importing algebra.pi_instances

[Jesse Michael Han]

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]

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]

V 0 is defeq to real.

[Johan Commelin]

Why doesn't it see that?

[Chris Hughes]

Is the module structure defeq?

[Johan Commelin]

I think so.

[Rob Lewis]

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

[Johan Commelin]

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]

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

[Rob Lewis]

But I need to head home and eat dinner now.

[Johan Commelin]

I pushed another cleanup of degree_theorem

[Johan Commelin]

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

[Floris van Doorn]

(deleted - wrong topic)

[Patrick Massot]

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]

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]

The key is:

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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]

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]

I'm currently playing with this adjacent_succ_iff thing

[Patrick Massot]

Using my proposed definition of adjacent

[Rob Lewis]

Which definition is that?

[Patrick Massot]

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

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

(deleted)

[Patrick Massot]

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]

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]

It seems there is some kind of pain conservation law here

[Patrick Massot]

@Rob Lewis

[Patrick Massot]

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]

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]

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]

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]

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]

Why do you separate those two lemmas? Does it make later things easier?

[Patrick Massot]

Could you try my finsupp.total mystery?

[Rob Lewis]

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]

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]

(message too long, truncated at 262144 characters)

[Patrick Massot]

It seems adding the shortcut

instance toto : module ℝ (Q n →₀ ℝ) :=
finsupp.module (Q n) ℝ

helps a lot

[Patrick Massot]

Although the coercion from linear_map to function still doesn't kick in

[Rob Lewis]

Yes, the messages get truncated, but 262144 characters is usually plenty to find the problem...

[Rob Lewis]

Unsurprisingly there are type class issues in this whole development. You can add that to the short circuit instances for V.

[Johan Commelin]

Why "unsurprisingly"?

[Rob Lewis]

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]

To me this is quite a surprise

[Rob Lewis]

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]

It's pretty clear that either we are doing it wrong, or Lean 3's type class is doing it wrong

[Patrick Massot]

Rob was quicker...

[Patrick Massot]

Rob, I think you can merge into master, I don't think anyone has a much better idea

[Kevin Buzzard]

Can someone summarise the problems you're having?

[Patrick Massot]

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]

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]

Which is the sum manipulation and basis and dual basis things.

[Patrick Massot]

Now that instances work, here is my proposal:

[Patrick Massot]

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]

Note how this doesn not use e.is_basis or equiv_sum

[Patrick Massot]

I think this is going more straightly to the point

[Patrick Massot]

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

[Patrick Massot]

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

[Rob Lewis]

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

[Patrick Massot]

Oh sorry

[Patrick Massot]

It's French for sum

[Rob Lewis]

Aha.

[Patrick Massot]

At some point I wanted to avoid name clash

[Patrick Massot]

Of course it uses epsilon_total that I posted earlier

[Patrick Massot]

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]

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

[Patrick Massot]

What do you think about this?

[Rob Lewis]

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]

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]

Nice, I think it looks great!

[Patrick Massot]

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]

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]

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]

I guess Rob is our last hope.

[David Michael Roberts]

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]

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]

I think it was our pi day activity

[Kevin Buzzard]

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]

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

[Reid Barton]

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]

@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]

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]

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]

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

[Patrick Massot]

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]

I'll see what I can do.

[Kevin Buzzard]

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

[Rob Lewis]

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]

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

[Rob Lewis]

@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]

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]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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]

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]

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]

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]

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]

I really think mathlib should hide this to users who manipulate only finite-dimensional vector spaces (as we do in this proof)

[Patrick Massot]

If we can't do that then the linear algebra library has a serious issue

[Rob Lewis]

I think this is what linear_algebra/finite_dimensional.lean is trying to do, but there's still some glue missing.

[Rob Lewis]

fg doesn't seem to be linked up with the existence of a finite basis, as far as I can tell.

[Rob Lewis]

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]

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]

I also reintegrated the calc block in the main proof.

[Patrick Massot]

And now we can go on removing stuff that just got merged in mathlib, and continue emptying for_mathlib.lean

[Rob Lewis]

It looks good! I just pushed an update that gets rid of dim_V'. But updating mathlib breaks the assumption_mod_castin findim_V, I'm not sure why.

[Rob Lewis]

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]

@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]

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]

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]

Oh ok

[Patrick Massot]

I'm sorry I messed up that

[Patrick Massot]

I just pushed some more tweaks to make statements look nicer (at least to my eye)

[Patrick Massot]

Did you make progress on the mathlib bump issue?

[Rob Lewis]

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]

I think the next mathlib nightly goes up once the next PR gets merged and built, right?

[Rob Lewis]

Then we run leanpkg upgrade on the upgraded_mathlib branch and rebase.

[Patrick Massot]

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]

Oh, I thought you had trouble with the question you asked PN

[Rob Lewis]

Oh, that's fixed locally, I was just wondering if it should be a global change.

[Patrick Massot]

apply' just got merged so we should get a new nightly soon

[Patrick Massot]

Of course we can always trigger a new nightly build by hand if we are in a hurry

[Patrick Massot]

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]

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]

oops, forgot to delete that. I'll do it right now

[Paul-Nicolas Madelaine]

@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]

Ok, we are up to date with mathlib, and ready for the next round of PR

[Jesse Michael Han]

on the reduction branch i started on the reduction of the original sensitivity conjecture to the degree theorem we formalized

[Jesse Michael Han]

it looks manageable except that the proof of gotsman_linial_equivalence uses Fourier transforms

[Patrick Massot]

That sounds like a big "except"

[Daniel Donnelly]

Why can't Lean handle FT? Not that I need it for my app or anything...

[Patrick Massot]

Oh, it can. But someone needs to explain it to Lean.

[Patrick Massot]

And analysis is not mathlib's strong point

[Scott Morrison]

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]

In fact the proof is just a few lines, even easier than Huang's recent argument.

[Daniel Donnelly]

I can attest to that. Has to do with sums of roots of unity in any field.

[Jesse Michael Han]

oh, good

then maybe soon we can say that we really formalized the sensitivity conjecture

[Scott Morrison]

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]

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]

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]

/me hears Kenny rolling on the floor lauging out loud

[Johan Commelin]

@Kenny Lau In how many different languages do you know the word “Schadenfreude”?

[Scott Morrison]

Wow, that’s really bad.

[Scott Morrison]

Like, maybe this enterprise is actually doomed, bad. :-)

[Chris Hughes]

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]

[…] 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]

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]

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]

It's fairly slow even just importing analysis.normed_space.basic.

[Scott Morrison]

I wonder if we should also be using local attribute [simp] more, or custom simp sets.

[Floris van Doorn]

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]

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]

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]

The alternative, of course, is to not change anything for now and see how things look in :four_leaf_clover: .

[Rob Lewis]

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]

Why is this not an issue in Isabelle?

[Patrick Massot]

Johan, did you ever read https://github.com/leanprover/lean/wiki/Simplifier-Features to see what the simplifier could look like?

[Johan Commelin]

Patrick, nope, I didn't.

[Johan Commelin]

It's an inspiring wiki page, thanks for the link!