linear_independent

Stream: maths

[Johan Commelin]

If my goal is linear_independent K s,
how do I turn this into the statement that the coefficient a_i is zero if sum a_i s_i = 0?
This part of the API seems to do lots of abstract stuff, but I'm missing this down to earth condition.

[Johan Commelin]

Maybe it is hidden in 5 layers of defeqs, but that doesn't seem user friendly to me.

[Johan Commelin]

@Kenny Lau Any hints?

[Kenny Lau]

oh no

[Kenny Lau]

iirc the lemma isn’t there

[Johannes Hölzl]

There is linear_independent_iffand lc.total is the sum operator

[Johannes Hölzl]

by the way, I'm working on adding the linear structure on the function (pi) space & for finsupp if you need this

[Johan Commelin]

I'm feeling really miserable today. People have said that it is a sobering thought that Lean does not know complex analysis. Well, as far as I know Lean also doesn't know anything about finite-dimensional vector spaces. And that's quite depressing.
I've tried to prove that V and its dual have the same dimension, and I get stuck in a maze of complicated definitions that don't fit in my brain-RAM. It probably means that I haven't understood the API for linear maps and modules... I'm not sure if that says something about me, or about the API.

[Mario Carneiro]

Do we have the dual vector space?

[Patrick Massot]

If we have linear maps and the instance saying that a field is a vector space over itself then we have duals, right?

[Mario Carneiro]

right. I'm trying to reconstruct the proof Johan is talking about

[Mario Carneiro]

what's the basis for the dual space?

[Patrick Massot]

I agree that the status of linear algebra in mathlib is much more depressing than the status of complex analysis. But we need to make choices, we can't work on everything at the same time

[Patrick Massot]

If you have a basis for the original space then you get the dual basis

[Mario Carneiro]

do you have to invent an inner product to define the dual basis

[Patrick Massot]

no

[Patrick Massot]

If the basis is (e_1, ..., e_n) then the dual basis is defined by l_i(e_j) = 1 if i =j, 0 otherwise

[Patrick Massot]

You need to know that a linear map can be specified by specifying it on a basis

[Mario Carneiro]

okay. We have that though

[Mario Carneiro]

I think it's called constr

[Mario Carneiro]

But this isn't always a basis, right? in infinite dimensions it breaks down

[Patrick Massot]

You don't talk about basis in infinite dimension, this would be a bad idea

[Mario Carneiro]

So we have a dual_basis function that takes any basis and makes a lin ind set in the dual space

[Mario Carneiro]

and if the original space is f.d then it's also a basis

[Patrick Massot]

yes

[Patrick Massot]

In infinite dimensions the dual tends to be bigger than the original space

[Mario Carneiro]

oh right, I just remembered that I had plans to redo linear_independent because it uses sets instead of families

[Patrick Massot]

ooh

[Patrick Massot]

That would be nice

[Mario Carneiro]

it's a lot more natural for everything except zorn's lemma

[Mario Carneiro]

but that's just one proof

[Patrick Massot]

Let's do more elementary maths since Jeremy opened the way with calculus. But not too elementary, I just spend one hour teaching how to "prove" the equivalence of five definitions of "convex polygon", I will never ever try to Lean that "proof"

[Patrick Massot]

I makes me think we need a Johannes countdown topic. I think we are getting dangerously close, and we still don't have integrals

[Johan Commelin]

Sorry, I was away for a while, because someone entered my office. Now I need to catch a train, so I will just dump the contents of my depression in this chat:

/-
Copyright (c) 2019 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin
-/

import linear_algebra.dimension linear_algebra.tensor_product
import set_theory.ordinal
noncomputable theory

local attribute [instance] classical.prop_decidable

section
variables (R : Type*) (M : Type*)
variables [comm_ring R] [add_comm_group M] [module R M]

def module.dual := M →ₗ[R] R

open module

instance : add_comm_group (dual R M) :=
by delta dual; apply_instance

instance : module R (dual R M) :=
by delta dual; apply_instance

def eval : M →ₗ[R] (dual R (dual R M)) := linear_map.id.flip

variables {R} {M}
def pairing : (dual R M) → M → R := λ (f : M →ₗ[R] R) m, f m

end

namespace is_basis
variables {K : Type*} {V : Type*}
variables [discrete_field K] [add_comm_group V] [vector_space K V]
variables {B : set V} (h : is_basis K B)
include h
open vector_space module submodule linear_map cardinal

def dual : set (module.dual K V) :=
{f : V →ₗ[K] K | ∃ v ∈ B, f v = 1 ∧ ∀ w ∈ B, w ≠ v → f w = 0}

def dual_elem (v : V) : module.dual K V :=
h.constr $ λ w, if w = v then 1 else 0

lemma dual_elem_mem (v ∈ B) : h.dual_elem v ∈ h.dual :=
begin
  use [v,H],
  split; intros; erw [constr_basis]; simp *,
end

lemma mem_dual_iff (f : module.dual K V) :
  f ∈ h.dual ↔ ∃ v ∈ B, f = h.dual_elem v :=
begin
  split; intro H; rcases H with ⟨v, hv, H⟩,
  { use [v,hv],
    apply h.ext,
    intros w hw,
    erw [constr_basis _ hw],
    split_ifs with hwv,
    { rw hwv, exact H.1 },
    { apply H.2 w hw hwv, } },
  { rw H, apply h.dual_elem_mem v hv }
end

lemma dual_elem_eq_repr (v ∈ B) (w : V) :
  pairing (h.dual_elem v) w = h.repr w v :=
_

def to_dual : V →ₗ[K] module.dual K V :=
h.constr $ λ v, h.dual_elem v

lemma to_dual_ker : h.to_dual.ker = ⊥ :=
begin
  ext v,
  split,
  { rw [mem_ker, mem_bot],
    intro hv,
    sorry },
  { rw mem_bot, intro h, simp [h], }
end

-- lemma lc_dual_elem (l : lc K (module.dual K V))
-- (hl : ∀ (f : module.dual K V), f ∉ h.dual → l f = 0)
-- (v : V) (hv : v ∈ B) :
--   l (h.dual_elem v hv) = (pairing K V).to_fun
--     ((lc.total K (module.dual K V)).to_fun l) v :=
-- begin
--   have := lc.total_apply l,
--   change ((lc.total K (module.dual K V)).to_fun l) = _ at this,
--   erw this, clear this,
--   erw finsupp.apply_sum,
--   revert hl,
--   apply finsupp.induction l,
--   { intro hl,
--     rw [finsupp.zero_apply, finsupp.sum_zero_index],
--     symmetry,
--     apply zero_apply v, },
--   { intros f k l' _ _ IH hl',
--     rw [finsupp.add_apply, IH, finsupp.sum_add_index,
--         finsupp.sum_single_index],
--     { congr' 1,
--       by_cases H : f ∈ h.dual,
--         { rw [finsupp.single_apply, smul_apply],
--           split_ifs with hf,
--           { rw [hf, dual_elem, constr_basis _ hv], simp, },
--           sorry },
--         {  }
--        } } }
-- end

lemma dual_is_basis (B : set V) (h : is_basis K B) (hfin : dim K V < omega) :
  is_basis K (h.dual) :=
begin
  split,
  { sorry },
  -- { rw [linear_independent_iff],
  --   intros l hl H,
  --   ext f,
  --   by_cases hf : f ∈ h.dual,
  --   { rw lc.total_apply at H,
  --     rw mem_dual_iff at hf,
  --     rcases hf with ⟨v, hv, hf⟩,
  --     rw hf,
  --     sorry },
  --   { rw [lc.mem_supported'] at hl,
  --     apply hl f hf, } },
  { apply le_antisymm,
    { simp },
    { intros x hx,

      sorry } }
end

end is_basis

lemma eval_ker : (eval K V).ker = ⊥ :=
begin
  ext,
  split,
  { rw [mem_ker, mem_bot],
    intro h,
    sorry },
  { rw mem_bot, intro h, simp [h], }
end

end

[Patrick Massot]

Indeed there are too many sets in this story

[Johan Commelin]

By the way, today's xkcd is also about depressing elementary topics: https://xkcd.com/2117/
Maybe this can cheer us up a bit...

[Mario Carneiro]

the definition of is_basis.dual is definitely not going to be easy to work with

[Mario Carneiro]

BTW I think that XKCD is a great example of why decidability matters in mathematics

[Kevin Buzzard]

Differentiation is a science, integration is an art.

[Johannes Hölzl]

@Johan Commelin I'm currently preparing a push for the vector space structure of the function space and for finsupp: https://github.com/johoelzl/mathlib/commits/master (specially https://github.com/johoelzl/mathlib/commit/c83c049126030c524cf63e70273635b5d9f26476 and https://github.com/johoelzl/mathlib/commit/592e3c7a2dfbd5826919b4605559d35d4d75938f)

[Johannes Hölzl]

I don't know if any of this material might help for your proof

[Johannes Hölzl]

Instead of defining is_basis.dual directly, it might be easier to use the image of dual_elem

[Johan Commelin]

Hmm, I don't think that's where the problems are... the iff that I prove afterwards let's you move between the two.

[Johannes Hölzl]

Ah, that's what mem_dual is for

[Johan Commelin]

It's just that I'm running into many type class errors because it doesn't know how to coerce a linear map into a function. And then I manually add .to_fun and it typechecks, but then all sorts of rw and simp don't trigger. And it's just a pain.

[Johan Commelin]

It also made me a bit worried about if bundling + coercions is a good idea...

[Johannes Hölzl]

the coercion into functions worked quiet well for me

[Johannes Hölzl]

I had more problems with the decidability instance required for finsupp

[Johan Commelin]

I couldn't apply lc.total _ _ to an l : lc in theorem statements.

[Johan Commelin]

You can see the hackery in the code dump above.

[Johan Commelin]

-- lemma lc_dual_elem (l : lc K (module.dual K V))
-- (hl : ∀ (f : module.dual K V), f ∉ h.dual → l f = 0)
-- (v : V) (hv : v ∈ B) :
--   l (h.dual_elem v hv) = (pairing K V).to_fun
--     ((lc.total K (module.dual K V)).to_fun l) v :=
-- begin
--   have := lc.total_apply l,
--   change ((lc.total K (module.dual K V)).to_fun l) = _ at this,
--   erw this, clear this,

[Johan Commelin]

I have to write ((lc.total K (module.dual K V)).to_fun l

[Johan Commelin]

And then the first 3 lines of the proof are hackery to get lc.total_apply working.