Path integral

Stream: mathlib4

[Yury G. Kudryashov]

Hi, I'm going to define something like

variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {a b c : E}

noncomputable def pathIntegral (ω : E → E →L[ℝ] F) (γ : Path a b) : F :=
  ∫ t in (0)..1, ω (γ.extend t) (derivWithin γ.extend I t)

In some cases, you need E → E →L[ℂ] F instead, so it makes sense to define it for any [RCLike K]. However, this means that the vector spaces will need both [NormedSpace ℝ _] and [NormedSpace K _] instances. What should I do? Assume these instances? Use ℝ-linear maps and use restrictScalars whenever I need other space? Something else?