inner product on `ℝ×ℝ` and definition of `InnerProductSpace`

Stream: mathlib4

[Tomas Skrivan]

In my project, SciLean, I'm not using mathlib's derivative or inner product because natural norm on spaces like ℝ×ℝ is max norm and not l2 norm. Therefore ℝ×ℝ is not inner product space thus I can't simply take gradient of a function with type ℝ×ℝ → ℝ.

The core issue is that I cannot use ContinuousLinerMap.adjoint function to define gradient on functions of type ℝ×ℝ → ℝ

The suggested way to deal with it is to work WithLp 2 _ type synonym or work with EucledianSpace. I find this extremely unsatisfactory.

For example if I want to work with function:

#check fun (x : ℝ×ℝ) (i : Fin n) => x.1^i.1 + x.2

I'm supposed to write it in this way

#check fun x : WithLp 2 (ℝ×ℝ) => (WithLp.equiv 2 (Fin n → ℝ)).symm fun (i : Fin n) => (WithLp.equiv 2 (ℝ×ℝ) x).1^i.1 + (WithLp.equiv 2 (ℝ×ℝ) x).2

which is completely unreadable.

---

I really want adjoint for function of type like ℝ×ℝ → ℝ. I'm proposing to have typeclass like InnerProductSpace that does not require that the induced norm from inner product is equal to the existing norm. The requirement is softened to only topological equivalence. Let's call this class ProtoInnerProductSpace so the definitions would look like:

class ProtoInnerProductSpace (𝕜 : Type*) (E : Type*) [RCLike 𝕜] [NormedAddCommGroup E] extends
  NormedSpace 𝕜 E, Inner 𝕜 E where
  /-- Norm induced by inner is topologicaly equivalent to the given norm -/
  inner_top_equiv_norm : ∃ c d : ℝ,
    c > 0 ∧ d > 0 ∧
    ∀ x : E, (c • ‖x‖^2 ≤ re (inner x x)) ∧ (re (inner x x) ≤ d • ‖x‖^2)
  /-- The inner product is *hermitian*, taking the `conj` swaps the arguments. -/
  conj_symm : ∀ x y, conj (inner y x) = inner x y
  /-- The inner product is additive in the first coordinate. -/
  add_left : ∀ x y z, inner (x + y) z = inner x z + inner y z
  /-- The inner product is conjugate linear in the first coordinate. -/
  smul_left : ∀ x y r, inner (r • x) y = conj r * inner x y

class InnerProductSpace (𝕜 : Type*) (E : Type*) [RCLike 𝕜] [NormedAddCommGroup E] extends
  ProtoInnerProductSpace 𝕜 E where
  /-- The inner product induces the norm. -/
  norm_sq_eq_inner : ∀ x : E, ‖x‖ ^ 2 = re (inner x x)

This way I can provide instance of ProtoInnerProductSpace for X×Y and ι → X.

Would this be a sensible change?

[Eric Wieser]

Surely by WithLp 2 ℝ×ℝ you mean WithLp 2 (ℝ×ℝ)?

[Tomas Skrivan]

Eric Wieser said:

Surely by WithLp 2 ℝ×ℝ you mean WithLp 2 (ℝ×ℝ)?

Ohh yes, fixed!

[Jireh Loreaux]

@Tomas Skrivan see also this thread where I discuss some related issues about adjoints.