Zulip Chat Archive

Stream: new members

Topic: function cont diffable from set to internal

Abu Al Hassan (Mar 28 2023 at 10:10):

Hello, I have a function such that it's continuous on a segment from some point x_star to some other point x_star + α • d. Where x_star and d are vectors and α is real. Then I should be able to write this such as the following where the function only takes in a input c in reals in a interval [0, α] and scales d by c and transforms it by x_star.

import tactic -- imports all the Lean tactics
import data.real.basic -- imports the real numbers
import analysis.calculus.cont_diff
open set

-- Declare a type E with some properties
variables (E : Type*) [normed_add_comm_group E] [normed_space  E]

theorem MWE (f : E  ) (u : set E) (h_open : is_open u) (α: ) (x_star d: E)
(h_xstar: x_star  u) (h_d_not_zero: d  0) (h_d_in_u: d  u)
(h_twice_continuous_diffable: cont_diff_on  2 (λ (x : E), f x) (segment  x_star (x_star + α  d)))  :
cont_diff_on  2 (λ (c : ), f (x_star + c  d)) (Icc 0 α) :=

I would have thought there is some 'rw ___' command I can use to show this is essentially equivalent to 'h_twice_continuous_diffable' but maybe i am wrong and i have to do this in a multistep proof.

Sebastien Gouezel (Mar 28 2023 at 10:18):

Can you use docs#cont_diff_on.comp?

Abu Al Hassan (Mar 28 2023 at 21:48):

Thank you, Sebastien! This is exactly what I was looking for. Got it to work.

Last updated: Dec 20 2023 at 11:08 UTC