equality of derivatives

Stream: new members

[ZhiKai Pong]

import Mathlib

variable (f : ℝ → EuclideanSpace ℝ (Fin 3)) (g : ℝ → EuclideanSpace ℝ (Fin 3))

example (h : (fun x => fderiv ℝ f x 1) = (fun x => fderiv ℝ g x 1)) : f = g + C := by
  sorry

I guess there are two parts to my question:

1. I'm not sure how to state this in the first place (as in I'm not sure how to express the notion "for some constant C")
2. Tried looking around but couldn't find relevant info to show this.

I think this doesn't require indefinite integrals? But I actually couldn't find much on that either, and would like some pointers to where I can find examples of indefinite integrals in mathlib

[Aaron Liu]

You likely also need some differentiability assumptions

[ZhiKai Pong]

Aaron Liu said:

You likely also need some differentiability assumptions

I assume this is sufficient:

import Mathlib

variable (f : ℝ → EuclideanSpace ℝ (Fin 3)) (g : ℝ → EuclideanSpace ℝ (Fin 3))

example (h : (fun x => fderiv ℝ f x 1) = (fun x => fderiv ℝ g x 1))
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g): f = g + C := by
  sorry

[Kevin Buzzard]

It's currently wrong for the trivial reason that it says "for all C, f = g + C". You want "exists C, f = g + C" (and you want C to be a constant, right now C is a function due to the autoImplicit footgun).

[ZhiKai Pong]

import Mathlib

variable (f : ℝ → EuclideanSpace ℝ (Fin 3)) (g : ℝ → EuclideanSpace ℝ (Fin 3))

example (h : (fun x => fderiv ℝ f x 1) = (fun x => fderiv ℝ g x 1))
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g): ∃ C : EuclideanSpace ℝ (Fin 3), f x = g x + C := by
  sorry

is this more correct?

[Aaron Liu]

Right now this says "for any specific x, f x and g x differ by some constant C where C can depend on x", but you want to have one value C that works for all x.

[ZhiKai Pong]

hmm does this avoid the x dependence? or do I have to use the ∀ x quantifier as well?

import Mathlib

variable (f : ℝ → EuclideanSpace ℝ (Fin 3)) (g : ℝ → EuclideanSpace ℝ (Fin 3))

example (h : (fun x => fderiv ℝ f x 1) = (fun x => fderiv ℝ g x 1))
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) :
    ∃ (C : EuclideanSpace ℝ (Fin 3)), (fun x => f x) = (fun x => g x + C) := by
  sorry

[Eric Wieser]

Either approach would work

[Kevin Buzzard]

@ZhiKai Pong I think you would do well to set_option autoImplicit false at the top of your file; that way you would have seen the problems with your first two attempts. The third one looks good to me. (I have this option set to false for FLT because I personally have no use for the benefits which autoimplicits bring and I enjoy very much the guardrails which having it set to true brings).

[ZhiKai Pong]

thanks, and how should I proceed to prove this?

[Kevin Buzzard]

For that one you'll need to ask someone who knows something about the analysis library!

[Kevin Buzzard]

Surely the first thing to do is to reduce it to the claim that if a function (g-f) is differentiable and has derivative 0, then it's constant. And then I guess you hope it's in the library...

[Kevin Buzzard]

leanexplore.com suggests docs#is_const_of_deriv_eq_zero

[Kevin Buzzard]

And looking at the type of that seems to indicate that

def deriv (f : 𝕜 → F) (x : 𝕜) :=
  fderiv 𝕜 f x 1

you should be using deriv not fderiv.

[ZhiKai Pong]

Ha I was staring at docs#fderiv_const without getting anywhere, this is very useful thank you

[ZhiKai Pong]

I think there is a corresponding docs#is_const_of_fderiv_eq_zero so I should be fine (want to do this in full generality for now and simplify later if I can as I'm just trying to understand how this works in general)

[Kevin Buzzard]

yeah fderiv_const is the easy way.

[Kevin Buzzard]

You'll find it harder to use docs#is_const_of_fderiv_eq_zero because your hypothesis only has fderiv \R f x 1, not fderiv \R f x. That's why I'm pointing you to the deriv version (your domain is 1-dimensional so you can take a shortcut).

[ZhiKai Pong]

Tried both routes but both still stuck - don't know how to convert the statement into the final form
Edit: got the first one

import Mathlib

variable (f : ℝ → EuclideanSpace ℝ (Fin 3)) (g : ℝ → EuclideanSpace ℝ (Fin 3))

example (h : (fun x => fderiv ℝ f x 1) = (fun x => fderiv ℝ g x 1))
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g): ∃ (C : EuclideanSpace ℝ (Fin 3)), (fun x => f x) = (fun x => g x + C) := by
  have h' : ∀ (x : ℝ), deriv (fun y => f y - g y) x = 0 := by
    intro x
    rw [deriv_sub]
    simp_all
    repeat fun_prop
  have hfg := is_const_of_deriv_eq_zero (Differentiable.sub hf hg) h'
  have hfg' : ∀ (x y : ℝ), f x = g x + (f y - g y) := by --`c` = f y - g y
    intro x y
    rw [← hfg x y]
    simp
  use (f 0 - g 0)
  funext x i
  rw [hfg' x 0]

example (h : (fun x => fderiv ℝ f x 1) = (fun x => fderiv ℝ g x 1))
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g): ∃ (C : EuclideanSpace ℝ (Fin 3)), (fun x => f x) = (fun x => g x + C) := by
  have h' : (fderiv ℝ (fun x => (f x - g x))) = 0 := by
    ext x i
    rw [fderiv_sub]
    simp_all
    repeat fun_prop
  rw [← fderiv_const] at h' --how do I "set" the value of `c`
  sorry

[ZhiKai Pong]

aha I got stuck when I had to "choose a random real number" and I don't know how to introduce a real out of nowhere, then I realized I can just use existing instances e.g. 0

Is the second route doable? using ← fderiv_const creates a synthetic placeholder and I'm not sure how to use it

[Xipan Xiao]

I got a proof. Basically it uses the same idea. You may take a look if you really want to:

import Mathlib

open scoped Topology
open Real
open Filter

variable (f g : ℝ → EuclideanSpace ℝ (Fin 3))

example
  (hf : Differentiable ℝ f)
  (hg : Differentiable ℝ g)
  (h : ∀ x, fderiv ℝ f x 1 = fderiv ℝ g x 1) :
  ∃ C, f = fun x ↦ g x + C := by

  let diff := fun x ↦ f x - g x

  have h_deriv_zero_at_1 : ∀ x, fderiv ℝ diff x 1 = 0 := by
    intro x
    rw [fderiv_sub (hf x) (hg x)]
    exact sub_eq_zero_of_eq (h x)

  have h_deriv_zero : ∀ x, fderiv ℝ diff x = 0 := by
    intro x
    apply ContinuousLinearMap.ext
    intro v
    obtain ⟨r, rfl⟩ : ∃ r : ℝ, v = r • (1 : ℝ) := ⟨v, by simp⟩
    calc
      (fderiv ℝ diff x) (r • 1) = r • (fderiv ℝ diff x) 1 := by simp
      _= r • 0 := by rw [h_deriv_zero_at_1]
      _= 0 := by simp

  let C := diff 0
  use C
  ext x i
  have diff_is_const := is_const_of_fderiv_eq_zero (hf.sub hg) h_deriv_zero
  have : f x = g x + C := by exact sub_eq_iff_eq_add'.mp (diff_is_const x 0)
  exact congrFun this i

[Kevin Buzzard]

This is longer than it needs to be because you're using is_const_of_fderiv_eq_zero and not is_const_of_deriv_eq_zero

[Kevin Buzzard]

example
    (hf : Differentiable ℝ f)
    (hg : Differentiable ℝ g)
    (h : ∀ x, fderiv ℝ f x 1 = fderiv ℝ g x 1) :
    ∃ C, f = fun x ↦ g x + C := by
  use f 0 - g 0
  ext1 x
  rw [← sub_eq_iff_eq_add']
  refine is_const_of_deriv_eq_zero (hf.sub hg) ?_ x 0
  peel h with y h
  rwa [deriv_sub (hf y) (hg y), sub_eq_zero]

I've never used the calculus library before so probably there are more optimisations that one can make

[Xipan Xiao]

much simpler!

[ZhiKai Pong]

A variant of what's discussed above:

import Mathlib

variable (f : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))

example {s : EuclideanSpace ℝ (Fin 3)} (h : ∀ x, inner ℝ (fderiv ℝ f x s) s = 0)
    (hf : Differentiable ℝ f) :
    ∀ x, ∃ (C : EuclideanSpace ℝ (Fin 3)), inner ℝ (f x - C) s = 0 := by
  have h' : ∀ x, fderiv ℝ (fun x => (inner ℝ (f x) s)) x s = 0 := by
    intro x
    rw [fderiv_inner_apply]
    simp [-PiLp.inner_apply]
    rw [h]
    repeat fun_prop
  apply is_const_of_fderiv_eq_zero at h' --I want this but only restricted in direction of s

Given that the derivative of a vector-valued function f along direction s is always orthogonal to s, I want to show that f itself must also be orthogonal to s minus some constant. I think docs#is_const_of_fderiv_eq_zero is stronger in the sense that it requires globally the derivative must be zero, but this time I want it to be in one specific direction only. This is also not in 1d so I don't think this can be simplified to deriv either. Any suggestions on how to proceed?

[ZhiKai Pong]

maybe derivative along one direction can be made into 1d but I don't know how to do this in lean.

[Aaron Liu]

import Mathlib

variable (f : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))

example {s : EuclideanSpace ℝ (Fin 3)}
    -- (h : ∀ x, inner ℝ (fderiv ℝ f x s) s = 0) (hf : Differentiable ℝ f)
    : ∀ x, ∃ (C : EuclideanSpace ℝ (Fin 3)), inner ℝ (f x - C) s = 0 := by
  intro x
  use f x
  simp

But that's probably not what you wanted

[ZhiKai Pong]

ah the ordering is wrong, C has to go before x

(for a moment I thought I had the whole thing formulated incorrectly but I think it's just this?)

[ZhiKai Pong]

import Mathlib

variable (f : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3))

example {s : EuclideanSpace ℝ (Fin 3)} (h : ∀ x, inner ℝ (fderiv ℝ f x s) s = 0)
    (hf : Differentiable ℝ f) :
    ∃ (C : EuclideanSpace ℝ (Fin 3)), ∀ x, inner ℝ (f x - C) s = 0 := by
  have h' : ∀ x, fderiv ℝ (fun x => (inner ℝ (f x) s)) x s = 0 := by
    intro x
    rw [fderiv_inner_apply]
    simp [-PiLp.inner_apply]
    rw [h]
    repeat fun_prop
  apply is_const_of_fderiv_eq_zero at h' --I want this but only restricted in direction of s

[ZhiKai Pong]

sorry still stuck on this - I think I'm not sure what's the best way to express "a vector-valued function has constant component along direction s" which may help with more intermediate statements. I'm not sure having h' here is helpful and would appreciate any pointers.