Help Formating a Proof in Lean

Stream: new members

[Max Bobbin]

Hello,

I am working on understanding derivatives in Lean, and am trying to use the work done on proving the divergence theorem for Bochner integrals to show the relationship between the derivative and integral form of the continuity equation. To give some background, I am a senior undergrad chemical engineer working on a project to formalize scientific equations.

The pdf I've attached is an outline of what I'm trying to write. I guess what I still don't fully understand in Lean is exactly how to write out a function, especially since I know functions from a scientific background rather than a general math background. For instance, in my outline, I'm unsure how exactly I should write density and velocity in Lean. I also attached the code I've started on, but it's not correct, I just tried to get everything written down so I could have a starting point. I ran into problems of Lean throwing errors of not having different spaces defined, but even if I try to define them Lean doesn't use them. Or I run into the problem of getting the types to match up, which makes me think I am understanding how to apply the types for my functions wrong. I really appreciate any help you can give!

ContinuityFromDivergence.pdf

I tried to comment on my thought process. My first question is more about Types. I still have trouble understanding exactly how they translate from my perception of Math. I just wanted to include my code for clarity of what I'm trying to do.

--The continuity equation for mass over a control volume
import data.real.basic
import analysis.calculus.fderiv
import analysis.calculus.deriv
import measure_theory.integral.interval_integral

open_locale big_operators


local notation `ℝ³` := fin 3 → ℝ
local notation `ℝ² ` := fin (2) → ℝ

theorem some_name
(μ : measure_theory.measure ℝ³ . measure_theory.volume_tac)
(M : ℝ → ℝ³) (ρ v : ℝ → ℝ³ → ℝ³ ) -- Mass, density
(t : ℝ)
(V1 V2: (ℝ³))  -- consider a finite volume V which is defined on ℝ³ FOr Lean we define V as V2 - V1
(V : ℝ³) (hV : V1 ≤ V2)

(F : ℝ³ → ℝ³) -- flux of our fluid
(F' : (ℝ³) → (ℝ³) →L[ℝ] ℝ³) -- a partial derivatvie of our vector
--define how our flux term F relates to density and velocity
(hF : F = (ρ t) • (v t)) --I feel like I'm using the wrong operator here. This part isn't as important, we
--could just leave it as the flux term F, but I wanted to have my final result in terms of velocity and density

--define how mass relates to density
(hM : M t = ∫ (V : ℝ³) in set.Icc V1 V2, (ρ t) ) --Mass of control volume at time t is equal to triple integral
-- of density at time t over the control volume
(hM' : deriv M t = ∫(V : ℝ³) in set.Icc V1 V2, (fderiv ℝ ρ t)) --the time derivative version of hM

--stuff for divergence theorem, I think. I copied this over to have in case I needed it or for reference
(s : set (ℝ³)) -- set of ℝ³ whcih are the variables of our function (like our dimensions mass can flow)
(hs : s.countable) -- the set is finite (we don't have infinite dimensions)
(Hc : continuous_on F (set.Icc V1 V2)) --Our function is continous inside the control volume
-- Hd says that f is differentiable on the interior
(Hd : ∀ (x : fin (3) → ℝ), x ∈ set.pi set.univ (λ (i : fin (3)), set.Ioo (V1 i) (V2 i)) \ s → has_fderiv_at F (F' x) x)
-- Hi defines the divergence and says it is integrable on our control volume
(Hi :measure_theory.integrable_on (λ (x : ℝ³), ∑ (i : fin (3)), (F' x) (pi.single i 1) i) (set.Icc V1 V2) μ)

--differential form of the continuity equation
(DiffCont : fderiv ℝ M t = - ∑ (i : fin (3)), ((∫ (x : fin 2 → ℝ) in set.Icc (V1 ∘ (i.succ_above)) (V2 ∘ (i.succ_above)), F (i.insert_nth (V2 i) x) i) - ∫ (x : fin 2 → ℝ) in set.Icc (V1 ∘ (i.succ_above)) (V2 ∘ (i.succ_above)), F (i.insert_nth (V1 i) x) i))
:
∫ (x : ℝ³) in set.Icc V1 V2, fderiv ℝ ρ t + ∑(i : fin 3), (F' x) (pi.single i 1) i = 0
:=
begin

end

[Kevin Buzzard]

#backticks

[Max Bobbin]

Kevin Buzzard said:

#backticks

sorry, back ticks didn't copy over, my apolgies, fixed now

[Eric Wieser]

Your type of density looks wrong to me

[Eric Wieser]

It's a function of position and time, but it shouldn't be a value in ℝ³; surely it's a scalar at every point?

[Max Bobbin]

But if position is a vector function, and density is a function of position, wouldn't that make it a vector too?

[Eric Wieser]

"function of X" means "X → _`

[Eric Wieser]

The issue here is the _, not the X

[Max Bobbin]

Right, right, sorry. I got confused with a different part. I read density and understood velocity

[Max Bobbin]

I agree density should be scalar, I got caught up in the idea that position was a vector, so density must be one as well, but that makes sense. Would that mean density looks something like: ρ : ℝ → ℝ³ → ℝ?

[Eric Wieser]

That sounds right to me

[Eric Wieser]

hM looks fishy to me too; that doesn't say "mass and density are related in the obvious way across all time", but the much weaker condition "at this one point in time they happen to coincide"

[Max Bobbin]

Ah, ok. Thats where my understanding was lacking. I keep forgetting that frediv doesn't mean across all t, just a specific t.

[Max Bobbin]

Let me rewrite that with a forall statement.

[Eric Wieser]

Perhaps I just can't see it on my small mobile screen, but do you even mention s anywhere?

[Max Bobbin]

By s, do you mean the set of ℝ³? That comes in at the bottom for the hypothesis about the derivative in the control volume.

[Eric Wieser]

So s is countably many points at which F isn't differentiable?

[Max Bobbin]

so I rewrote hM to be: hM : ∀ (t:ℝ), M t = ∫ (V : ℝ³) in set.Icc V1 V2,(ρ t) but Lean gives the same error I've received before of "failed to synthesize type class instance for" with normed_group ((fin 3 → ℝ) → ℝ) in the proof statement on the infoviewer. I'm not sure exactly what Lean is expecting and failing to find

[Eric Wieser]

Why are you integrating over V but not doing anything with V?

[Max Bobbin]

I copied s, hs, Hc, Hd, and Hi over from the divergence theorem proof for Bochner integrals in case I need that stuff in the future and for reference.

[Eric Wieser]

I think you meant ρ t V not ρ t

[Max Bobbin]

To be honest, I'm not sure. The integral still is a little fuzzy for me. I guess I didn't put V in because in my outline I had it as dV

[Eric Wieser]

But density is a function of position

[Eric Wieser]

So you have to tell ρ what position you want the density at

[Eric Wieser]

Lean wants you to write $\int f(x) dx$, not $\int f\ dx$

[Eric Wieser]

If you write the second it assumes you're integrating a constant

[Max Bobbin]

Ahh, I see my mistake, Ok. That's the shorthand from engineering screwing me over :grinning:

[Max Bobbin]

So for my mass part, would it be better to write M as M : ℝ → ℝ?

[Max Bobbin]

I guess I'm trying to think if M is a function of the position vector, and I feel like it is since it depends on the size of the control volume, but that may also be satisfied in the integral and not apart of the function M?

[Eric Wieser]

If your control volume changes over time, then I guess V1 and V2 should also be functions of time

[Eric Wieser]

Aren't control volumes normally picked to be static / constant though?

[Max Bobbin]

The control volume is constant

[Eric Wieser]

Then M is not a function of the position vector

[Max Bobbin]

Cool, ok. This is starting to make a lot more sense.

[Mario Carneiro]

rho is a function of the position vector, but M is obtained by integrating over it so it is not position-dependent

[Eric Wieser]

I suspect hM' is redundant in the face of hM, assuming you add the missing ∀s discussed above

[Max Bobbin]

So should my hM' statement be similar to the hM statement? I added the forall statement, but I'm not sure if its correct to use deriv or fderiv in this case. I also am running into a problem where it doesn't like me having V at the end when I have the fderiv
(hM' : ∀ (t:ℝ), fderiv ℝ M t = ∫(V : ℝ³) in set.Icc V1 V2, (fderiv ℝ ρ t) V)

[Max Bobbin]

Oh really, I thought I would need to add it, but I guess if I define how M relates to V, I can plug that into the derivative of M in my continuity equation

[Eric Wieser]

You should be able to prove hM' using hM, meaning you only need the latter

[Eric Wieser]

I think you likely want deriv ℝ (λ t, ρ t V) t or similar there

[Eric Wieser]

(aka differentiate with respect to t holding V constant)

[Max Bobbin]

Would I need the ℝ for deriv? I thought you only need that for fderiv to specify the linear map?

[Max Bobbin]

Oh joy!!! I used the deriv (λ t, ρ t V) t and I am error free!

[Max Bobbin]

I really appreciate all your help. Slowly it's all starting to make sense, but it's definitely a huge learning curve to leave a field of relatively simple mathematics compared to this stuff.

[Eric Wieser]

Apologies for the ℝ, I'm on mobile and guessing heavily! I'm glad my comments are still putting you on the right track

[Max Bobbin]

You're all good! I just wanted to make sure, because I was afraid I had misunderstood the difference between fderiv and deriv, lol.

[Eric Wieser]

As an exercise, you might want to try proving hM' from hM, now that you know how to state both

[Max Bobbin]

Thats a good idea, I will start there

[Eric Wieser]

If you're lucky, library_search will find the proof for you

[Max Bobbin]

Eric Wieser said:

If you're lucky, library_search will find the proof for you

So I noticed while trying to prove the first part, that a lot of integral theorems in Lean are set up as ∫ (V : ℝ³) in set.Ioc V1 V2, ... but the divergence theorem integral is different and uses set.Icc instead of set.Ioc. Do you know why that is and if that affects anything with the proof? I didn't know if that makes it more difficult to prove the first part about hM'

[Max Bobbin]

I found a solution, didn't realize there was a theorem to convert an integral over Icc to Ioc