How to prove decidability for PosDef?

Stream: new members

[jsodd]

Today I've tried to formalize the multivariate Gaussian distribution by just copying the corresponding univariate Mathlib file and editing it. As expected, I stumbled upon some problems immediately. Here's one of them:

noncomputable
def gaussianPDFRn
  (μ : n → ℝ)
  (Sigma : Matrix n n ℝ)
  (x : n → ℝ) : ℝ :=
  have hSigma : Decidable Sigma.PosDef := by sorry
  if (Sigma.PosDef : Prop) then
    ( 2 * π * (Sigma.det) )^(-(Fintype.card n : ℝ) / 2)
      * rexp ( - (x - μ) ⬝ᵥ Sigma⁻¹ *ᵥ (x - μ) )
  else
    0

I have no idea how to prove that Sigma.PosDef is Decidable and apply? doesn't help much...

[Kyle Miller]

If you're defining something noncomputable, just use the classical decidability, like have : hSigma := Classical.propDecidable Sigma.PosDef

[Kyle Miller]

You might also be able to do have := Classical.propDecidable

[jsodd]

Like this?

noncomputable
def gaussianPDFRn
  (μ : n → ℝ)
  (Sigma : Matrix n n ℝ)
  (x : n → ℝ) : ℝ :=
  have := Classical.propDecidable Sigma.PosDef
  if (Sigma.PosDef : Prop) then
    ( 2 * π * (Sigma.det) )^(-(Fintype.card n : ℝ) / 2)
      * rexp ( - (x - μ) ⬝ᵥ Sigma⁻¹ *ᵥ (x - μ) )
  else
    0

Seems to be working, thanks a lot! Could you please help me understand what is going on with this decidability?

[jsodd]

By "what is going on" I mean why doesn't lean somehow infer it from the fact that n is of finite type and \R is quite simple.

[Kyle Miller]

Decidability has to do with being able to run the definition as a computer program. Real numbers generally aren't computable this way, and Classical.propDecidable introduces an "algorithm" that doesn't actually compute positive definiteness.

The fundamental problem is that it's not decidable whether a general real number is positive or negative, so there's no hope deciding whether a matrix is positive definite or not.

The noncomputable modifier indicates that you aren't looking for a computer program that computes the function, so there's no need to try to use a "real" decidable instance, one that has any computational content.

[Eric Wieser]

In theory we could make it decidable on matrices of rational or integer coefficients, right?

[Eric Wieser]

(I think that would be reasonable to have in mathlib to help slim_check and decide, but I also think it's probably not a good use of anyone's time to write)

[jsodd]

Thank you very much for the explanation, it's clear now!

Another question about decidability: why Nonempty \R also runs into decidability issues? It seems to have nothing to do with computations...

[Eric Wieser]

Eric Wieser said:

(I think that would be reasonable to have in mathlib to help slim_check and decide, but I also think it's probably not a good use of anyone's time to write)

Actually, formalizing https://en.wikipedia.org/wiki/Sylvester%27s_criterion might be a nice project, from which DecidablePred PosDef falls out naturally

[Eric Wieser]

Here's the statement, in case anyone feels like being sniped:

import Mathlib

variable {m n R} [CommRing R] [StarRing R] [PartialOrder R] [StarOrderedRing R]


/-- https://en.wikipedia.org/wiki/Sylvester%27s_criterion -/
theorem posDef_fin_iff_det {A : Matrix (Fin n) (Fin n) R} :
    A.PosDef ↔ ∀ i (h : i ≤ n), 0 < (A.submatrix (Fin.castLE h) (Fin.castLE h)).det :=
  -- this is the interesting mathematical result
  sorry

theorem posDef_iff_forall_det [Fintype n] [DecidableEq n] {A : Matrix n n R} (s : Flag (Finset n)) :
    A.PosDef ↔ ∀ si ∈ s, 0 < (A.submatrix (fun x : si => x) (fun x : si => x)).det := by
  -- find the equivalence with `Fin (Fintype.card n)` that respect the `IsChain`
  sorry

open scoped List in
theorem posDef_iff_forall_det' [Fintype n] [DecidableEq n] {A : Matrix n n R} (s : List n)
    (hs : s.Nodup) (hs' : Finset.univ = ⟨(s : Multiset n), hs⟩) :
    A.PosDef ↔ ∀ si ∈ s.inits, 0 < (A.submatrix (fun x : {x // x ∈ si} => x) (fun x : {x // x ∈ si} => x)).det := by
  -- find the equivalence with `Fin (Fintype.card n)` with `e i = s.indexOf i`
  sorry

instance [Fintype n] [DecidableEq n] [@DecidableRel R (· < ·)] {A : Matrix n n R} : Decidable A.PosDef :=
  match h : (Finset.univ : Finset n) with
  | ⟨m, hm⟩ => by
    revert hm
    refine Quotient.recOnSubsingleton m fun l (hl : l.Nodup) hu => ?_
    exact @decidable_of_iff' _ _ (posDef_iff_forall_det' l hl hu) (List.decidableBAll _ _)

[jsodd]

Eric Wieser said:

theorem posDef_fin_iff_det {A : Matrix (Fin n) (Fin n) R} :
    A.PosDef ↔ ∀ i (h : i ≤ n), 0 < (A.submatrix (Fin.castLE h) (Fin.castLE h)).det :=
  -- this is the interesting mathematical result
  sorry

exact? says that False.elim m achieves the goal.

[Eric Wieser]

That's lean being stupid, m is not part of that statement

[jsodd]

Clearly yes, but why does it say so? It doesn't give any error with this "solution".

[Eric Wieser]

After you write that solution, what does hovering over posDef_fin_iff_det say?

[jsodd]

image.png

[Eric Wieser]

Right, it added {m : False}!

[jsodd]

So {m : Type*} needed?

[Eric Wieser]

Or just delete {m} from my example

[jsodd]

But, in general, what's the best practice for setting up variables here?

[Eric Wieser]

{m : Type*} would indeed avoid the issue

[Eric Wieser]

Best practices will be changing in the next Lean version, such that this problem won't happen any more, I think