Zulip Chat Archive

Stream: new members

Topic: Help Formating a Proof in Lean


Max Bobbin (Apr 24 2022 at 21:07):

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 (Apr 24 2022 at 21:09):

#backticks

Max Bobbin (Apr 24 2022 at 21:10):

Kevin Buzzard said:

#backticks

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

Eric Wieser (Apr 24 2022 at 21:52):

Your type of density looks wrong to me

Eric Wieser (Apr 24 2022 at 21:53):

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 (Apr 24 2022 at 21:57):

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

Eric Wieser (Apr 24 2022 at 22:01):

"function of X" means "X → _`

Eric Wieser (Apr 24 2022 at 22:02):

The issue here is the _, not the X

Max Bobbin (Apr 24 2022 at 22:02):

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

Max Bobbin (Apr 24 2022 at 22:03):

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 (Apr 24 2022 at 22:04):

That sounds right to me

Eric Wieser (Apr 24 2022 at 22:06):

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 (Apr 24 2022 at 22:07):

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 (Apr 24 2022 at 22:07):

Let me rewrite that with a forall statement.

Eric Wieser (Apr 24 2022 at 22:09):

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

Max Bobbin (Apr 24 2022 at 22:10):

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 (Apr 24 2022 at 22:12):

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

Max Bobbin (Apr 24 2022 at 22:13):

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 (Apr 24 2022 at 22:14):

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

Max Bobbin (Apr 24 2022 at 22:14):

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 (Apr 24 2022 at 22:14):

I think you meant ρ t V not ρ t

Max Bobbin (Apr 24 2022 at 22:15):

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 (Apr 24 2022 at 22:16):

But density is a function of position

Eric Wieser (Apr 24 2022 at 22:16):

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

Eric Wieser (Apr 24 2022 at 22:17):

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

Eric Wieser (Apr 24 2022 at 22:17):

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

Max Bobbin (Apr 24 2022 at 22:18):

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

Max Bobbin (Apr 24 2022 at 22:20):

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

Max Bobbin (Apr 24 2022 at 22:21):

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 (Apr 24 2022 at 22:22):

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

Eric Wieser (Apr 24 2022 at 22:22):

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

Max Bobbin (Apr 24 2022 at 22:23):

The control volume is constant

Eric Wieser (Apr 24 2022 at 22:23):

Then M is not a function of the position vector

Max Bobbin (Apr 24 2022 at 22:24):

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

Mario Carneiro (Apr 24 2022 at 22:24):

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

Eric Wieser (Apr 24 2022 at 22:25):

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

Max Bobbin (Apr 24 2022 at 22:25):

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 (Apr 24 2022 at 22:26):

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 (Apr 24 2022 at 22:27):

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

Eric Wieser (Apr 24 2022 at 22:28):

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

Eric Wieser (Apr 24 2022 at 22:28):

(aka differentiate with respect to t holding V constant)

Max Bobbin (Apr 24 2022 at 22:30):

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

Max Bobbin (Apr 24 2022 at 22:31):

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

Max Bobbin (Apr 24 2022 at 22:32):

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 (Apr 24 2022 at 22:34):

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 (Apr 24 2022 at 22:35):

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 (Apr 24 2022 at 22:35):

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

Max Bobbin (Apr 24 2022 at 22:36):

Thats a good idea, I will start there

Eric Wieser (Apr 24 2022 at 22:36):

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

Max Bobbin (Apr 25 2022 at 02:51):

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 (Apr 25 2022 at 03:40):

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


Last updated: Dec 20 2023 at 11:08 UTC