instanciate NormedAddCommGroup

Stream: new members

[Gaëtan Serré]

Hello, I am trying to instanciate NormedAddCommGroup for a specific set of functions. I created a norm, proving the necessary stuff on it, and created the needed instances of HMul and HAdd. However, after providing each field of NormedAddCommGroup, I still get multiple errors such as

type mismatch
  Iff.rfl
has type
  ?m.360618 ↔ ?m.360618 : Prop
but is expected to have type
  (fun n f ↦ n * f) 0 x✝ = 0 : Prop

The fact is that this proposition: (fun n f ↦ n * f) 0 x✝ = 0 : Prop is not trivial but I am able to prove it. However, I don't know how to provide the proof for the typechecker to be happy.
Do you know how I can do that? (I am sorry for not providing a MWE, but, in this particular case, it's quite hard to produce a simple one)

[Ruben Van de Velde]

I would need to see more code to figure out what's going on

[Gaëtan Serré]

Ok I'll try to produce a MWE

[Gaëtan Serré]

(Note that I have multiple fields that are filled by sorry)

[Gaëtan Serré]

import Mathlib

open Classical MeasureTheory ENNReal NNReal

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

variable {d : ℕ} {Ω : Set (Vector ℝ d)} [MeasureSpace Ω]

def L2 (μ : Measure Ω) := {f : Ω → ℝ | ∃ C, ∫ x, |f x|^2 ∂μ <= C}

def H (e : ℕ → Ω → ℝ) (μ : Measure Ω) := {f | f ∈ L2 μ ∧ ∃ (a : ℕ → ℝ), (f = λ x ↦ (∑' i, (a i) * e i x)) ∧ Summable (λ i ↦ (a i)^2)}

def h_repr {e : ℕ → Ω → ℝ} {μ : Measure Ω} (f : H e μ) := {a : ℕ → ℝ | (f = λ x ↦ (∑' i, a i * e i x)) ∧ (Summable (λ i ↦ (a i)^2))}

lemma h_repr_ne {e : ℕ → Ω → ℝ} {μ : Measure Ω} (f : H e μ) : (h_repr f).Nonempty := by
  rcases f.2 with ⟨_, ⟨a, ha⟩⟩
  use a
  exact ha

noncomputable def H_inner {e : ℕ → Ω → ℝ} {μ : Measure Ω} (f g : H e μ) : ℝ := ∑' i, (v.1 i) * ((h_repr_ne f).some i) * ((h_repr_ne g).some i)

variable {e : ℕ → Ω → ℝ} {μ : Measure Ω}

instance : HAdd (H v μ) (H v μ) (H v μ) where
  hAdd := λ f g ↦ ⟨(λ x ↦ f.1 x + g.1 x), by sorry⟩

instance : HMul ℝ (H v μ) (H v μ) where
  hMul := λ a f ↦ ⟨λ x ↦ a * f.1 x, by sorry⟩

instance : Zero (H e μ) where
  zero := ⟨λ _ ↦ 0, by sorry⟩

noncomputable instance : Norm (H v μ) where
  norm := λ f ↦ Real.sqrt (H_inner f f)

noncomputable instance : NormedAddCommGroup (H e μ) where
  norm := λ f ↦ norm f
  add := λ f g ↦ f + g
  add_assoc := by sorry
  zero_add := by sorry
  add_zero := by sorry
  nsmul := λ n f ↦ (n : ℝ) * f
  neg := λ f ↦ (-1 : ℝ) * f
  zsmul := λ z f ↦ (z : ℝ) * f
  add_left_neg := by sorry
  add_comm := by sorry
  dist_self := by sorry
  dist_comm := by sorry
  dist_triangle := by sorry
  edist_dist := by sorry
  eq_of_dist_eq_zero := by sorry

[Gaëtan Serré]

I tried to make a simpler example that what I have but a have a lot more of sorry now

[Gaëtan Serré]

I wondering if it will work if fill all these sorry.

[Ruben Van de Velde]

The issue is with proof fields that have a default proof that doesn't work for your data fields; this could get you further:

noncomputable instance : NormedAddCommGroup (H e μ) where
  norm := λ f ↦ norm f
  add := λ f g ↦ f + g
  add_assoc := by sorry
  zero_add := by sorry
  add_zero := by sorry
  nsmul := λ n f ↦ (n : ℝ) * f
  neg := λ f ↦ (-1 : ℝ) * f
  zsmul := λ z f ↦ (z : ℝ) * f
  add_left_neg := by sorry
  add_comm := by sorry
  dist_self := by sorry
  dist_comm := by sorry
  dist_triangle := by sorry
  edist_dist := by sorry
  eq_of_dist_eq_zero := by sorry
  nsmul_zero := by sorry
  nsmul_succ := by sorry
  zsmul_zero' := by sorry
  zsmul_succ' := by sorry
  zsmul_neg' := by sorry
  dist := by sorry
  edist := by sorry
  toUniformSpace := by sorry
  uniformity_dist := by sorry
  toBornology := by sorry
  cobounded_sets := by sorry
  dist_eq := by sorry

[Gaëtan Serré]

Oh God! Ok thank you very much!

[Ruben Van de Velde]

(This is a known sharp edge that could use improvement)