type mismatch

Stream: mathlib4

[Oliver]

How to revise:

  rcases h_bound_h with ⟨C, h_final_bound⟩
  exists C, x_rec
  constructor
  · sorry  -- Prove x_rec is s-sparse
  constructor
  · exact h_meas_rec
  · exact h_final_bound

to fix:

 type mismatch
  h_final_bound
has type
  h.norm ≤ C * x.norm / √↑s : Prop
but is expected to have type
  (Vec.norm fun i => x i - x_rec i) ≤ C * x.norm / √↑s : Prop

?

Thanks.

[Kim Morrison]

#mwe, please! It's essential for people to even start answering your question.

[Oliver]

Kim Morrison said:

#mwe, please! It's essential for people to even start answering your question.

import Mathlib.Data.Real.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Real.Sqrt
import Mathlib.Tactic.NormNum
import Mathlib.Data.Finset.Card
import Mathlib.Data.Real.NNReal

def Vec (n : Nat) := Fin n → ℝ
def Matrix (m n : Nat) := Fin m → Fin n → ℝ

[Kim Morrison]

@Oliver, your #mwe needs to show the problem when opened in the playground. (Icon in the top right of the code block in the displayed message.)