Help with Normed Space Error

Stream: maths

[Max Bobbin]

I am working on showing the derivation of the continuity equation from the divergence theorem. Currently, I am trying to define the relation between mass and density through an integral over the volume. However, when I set up the integral in my hypotheses, Lean gives an error regarding normed groups. The error is normed_group ((fin 3 → ℝ) → fin 3 → E) I've attached the relevant portion of the code below. I'm hoping someone can help explain how to get rid of the error. I thought I defined all the proper normed and complete space stuff for Lean. The error is at hM.

To give more information about the variables
$\rho$ is density and is a function of the position vector of the material and time. v is velocity and is a function of the position vector of the material and time. Density is the quantity of the material divided by the volume of the control volume. So we can write the mass of the control volume (M) to be equal to the triple integral over the control volume of density. So, I think mass should also be a function of the position vector of the material and time, but I could also be wrong. I keep going back and forth if mass should be a function of the position vector of the material.

import data.real.basic
import analysis.normed.group.basic
import analysis.normed_space.basic
import topology.uniform_space.cauchy
import analysis.calculus.fderiv
import analysis.calculus.deriv
import init.data.set
import data.set.prod
import measure_theory.integral.integrable_on
import algebra.big_operators.basic
import init.core
import measure_theory.integral.interval_integral

open set finset topological_space function filter
open_locale big_operators interval

universe u

variables {E : Type u} [normed_group E] [normed_space ℝ E] [complete_space E]
local notation `ℝ³` := fin 3 → ℝ
local notation `ℝ² ` := fin (2) → ℝ
local notation `E³` := fin (3) → E
local notation `e` i := pi.single i 1
example
(V1 V2: (ℝ³))
(ρ : ℝ → ℝ³ → E³) --density takes in a and the three dimensional field
(t : ℝ)
(v : ℝ → ℝ³ → E³) -- velocity is the same form as density
(M : ℝ → ℝ³ → E³) -- Mass is the same form as density
(hM : M t =  ∫ (V : ℝ³) in set.Icc V1 V2, (ρ t) ) --the mass at time, t is the integral of density over the volume
:

:=
begin

end

[Eric Wieser]

You need to put something between the : and the :=; the statement you're trying to prove

[Max Bobbin]

Eric Wieser said:

You need to put something between the : and the :=; the statement you're trying to prove

I edited my post to put in a junk statement V1 = V2 into the prove line. My problem is with my hypothesis hM where it doesn't parce because it can't prove normed_group ((fin 3 → ℝ) → fin 3 → E), but I'm not sure what Lean means by this error