Determining Integral

Stream: Is there code for X?

[Max Bobbin]

Hi,

I'm working with a group that is trying to formalize scientific equations and I had a question about integration. I'm pretty sure I understand setting up the derivative notation and I understand the general Lebesgue integral notation. I was wondering if someone could point me in the right direction to go about showing that if a function, (f : a -> b), has a second derivative equal to 0, then f must be of the form C1*a+C2. This also leads into another question I had where if I define a function, (f : a -> b), can I then go on to define that f is of the form, say, a^2+2? Also, how would this work if I had a function that took in two varaibles, like (f : a->b->c), and I wanted to say f is of the form ab. So far I've run into the problem where Lean expects ab to be of type c, but a is of type a and b is of type b, and it also can't multiply type a by type b. I may be going around this the wrong way, still learning about Lean and math formalization. Thank you for your help! :smiley:

[Kevin Buzzard]

Can you formalise the statement that if a function has second derivative zero then it's linear? If so then you could sorry the proof and post it here as a #mwe

[Junyan Xu]

a, b in a -> b should not be variables; they should be types, like ℝ -> ℝ. If you want to write the function that maps a to a^2+2 you write λ a, a ^ 2 + 2.

[Max Bobbin]

I attached the code I have so far. I defined a function f, and defined its first and second derivative, and that f'' = 0. Our current goal is to derive the four basic kinematic equations from two differential equations, V = dx/dt and a = dV/dt. For instance, I can show from those two equations that v = v0+a*t, which is a function for velocity which is the initial velocity plus the acceleration multiplied by time. My original thought was to define f as a function that mapped a t --> X, which mapped a time (t) to a position (X), but I think from Junyan's response, I am understanding the meaning of f : t--> X wrong. Also, with the code attached below, a problem I am having is how to formulate the statement I want to prove, so I left it as a comment.

import analysis.calculus.fderiv
import measure_theory.measure.measure_space

universes u_1 u_2 u_3
example
{t :Type u_1} {X : Type u_2} {𝕜 : Type u_3}
--Create normed space for each variable
[normed_group t ]
[normed_space ℝ t]
[normed_group X ]
[normed_space ℝ X]
[measurable_space t]
{μ : measure_theory.measure t}
--Define f as a function that represents the distance at any time t
(f : t → X)
(τ : t)
{f' : t → (t →L[ℝ] X)}
{f'' : t →L[ℝ] t →L[ℝ] X}
(h1 : has_fderiv_at f (f' τ) τ) --Has a first derivative
(h2 : has_fderiv_at f' f'' τ) --Has a second derivation
(h3 : f'' = 0) --second derivative is 0
{t0 : t}
{t1 : t}
:
--f is linear
:=
begin
sorry,
end

[Max Bobbin]

This also leads me to a larger question about what the best way it is to define function and such, especially differential equations including partial differential equations.

[Heather Macbeth]

@Max Bobbin Please use #backticks so we can copy-paste it more easily!

[Max Bobbin]

My apologies, I was not aware of this. Thank you so much! Reposting the code now

[Heather Macbeth]

This should do what you want:

import analysis.calculus.deriv

universes u_2

example {X : Type u_2} [normed_group X ] [normed_space ℝ X]
  (f f' : ℝ → X) -- Define f as a function that represents the distance at any time t
  (h1 : ∀ τ, has_deriv_at f (f' τ) τ) --Has a first derivative
  (h2 : ∀ τ, has_deriv_at f' 0 τ) : --second derivative is 0
  ∃ a b : X, ∀ τ, f τ = τ • a + b := --f is linear
begin
  sorry,
end

[Heather Macbeth]

(You had time as taking values in a real normed space t, which I've switched to having time take values just in the real numbers.)

[Heather Macbeth]

Mathlib has the corresponding fact for first derivatives (zero first derivative implies constant): docs#constant_of_deriv_within_zero. I'm not sure if the fact exists yet for second derivatives.

[Max Bobbin]

This is awesome! Thank you, this makes more sense and should clear up my confusion.