A reusable joint C¹ criterion from time and parameter derivatives.

theorem AVenhance.Infra.Flow.contDiff_one_of_time_and_parameter_derivatives {P : Type u_1} {G : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] (f dtime : ℝ × P → G) (dparam : ℝ × P → P →L[ℝ] G) (hTime : ∀ (t : ℝ) (z : P), HasDerivAt (fun (r : ℝ) => f (r, z)) (dtime (t, z)) t) (hParam : ∀ (t : ℝ) (z : P), HasStrictFDerivAt (fun (w : P) => f (t, w)) (dparam (t, z)) z) (hTimeCont : Continuous dtime) (hParamCont : Continuous dparam) : ContDiff ℝ 1 f

Joint C¹ regularity follows when the time derivative and strict parameter derivative exist on their slices and vary continuously together.

noncomputable def AVenhance.Infra.Flow.JointC1Core.jointTimeDerivativeCLM {P : Type u_1} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (dtime : ℝ × P → G) (q : ℝ × P) : ℝ →L[ℝ] G

Continuous linear time-direction map associated with a prescribed time derivative.

Equations

• AVenhance.Infra.Flow.JointC1Core.jointTimeDerivativeCLM dtime q = ContinuousLinearMap.toSpanSingleton ℝ (dtime q)

theorem AVenhance.Infra.Flow.JointC1Core.jointFDerivAt_on_open {P : Type u_1} {G : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : ℝ × P → G) (s : Set (ℝ × P)) (hs : IsOpen s) (dtime : ℝ × P → G) (dparam : ℝ × P → P →L[ℝ] G) (hTime : ∀ (t : ℝ) (z : P), (t, z) ∈ s → HasDerivAt (fun (r : ℝ) => f (r, z)) (dtime (t, z)) t) (hParam : ∀ (t : ℝ) (z : P), (t, z) ∈ s → HasStrictFDerivAt (fun (w : P) => f (t, w)) (dparam (t, z)) z) (hTimeCont : ContinuousOn dtime s) (hParamCont : ContinuousOn dparam s) (q : ℝ × P) (hq : q ∈ s) : HasFDerivAt f ((jointTimeDerivativeCLM dtime q).coprod (dparam q)) q

Pointwise joint derivative on an open region, assembled from the two coordinate-slice derivatives.

theorem AVenhance.Infra.Flow.JointC1Core.jointFDerivAt_family_on_open {P : Type u_1} {G : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : ℝ × P → G) (s : Set (ℝ × P)) (hs : IsOpen s) (dtime : ℝ × P → G) (dparam : ℝ × P → P →L[ℝ] G) (hTime : ∀ (t : ℝ) (z : P), (t, z) ∈ s → HasDerivAt (fun (r : ℝ) => f (r, z)) (dtime (t, z)) t) (hParam : ∀ (t : ℝ) (z : P), (t, z) ∈ s → HasStrictFDerivAt (fun (w : P) => f (t, w)) (dparam (t, z)) z) (hTimeCont : ContinuousOn dtime s) (hParamCont : ContinuousOn dparam s) (q : ℝ × P) : q ∈ s → HasFDerivAt f ((jointTimeDerivativeCLM dtime q).coprod (dparam q)) q

theorem AVenhance.Infra.Flow.hasFDerivAt_of_time_and_parameter_derivatives {P : Type u_1} {G : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] (f dtime : ℝ × P → G) (dparam : ℝ × P → P →L[ℝ] G) (hTime : ∀ (t : ℝ) (z : P), HasDerivAt (fun (r : ℝ) => f (r, z)) (dtime (t, z)) t) (hParam : ∀ (t : ℝ) (z : P), HasStrictFDerivAt (fun (w : P) => f (t, w)) (dparam (t, z)) z) (hTimeCont : Continuous dtime) (hParamCont : Continuous dparam) (q : ℝ × P) : HasFDerivAt f ((ContinuousLinearMap.toSpanSingleton ℝ (dtime q)).coprod (dparam q)) q

Pointwise total derivative assembled from a time derivative and a parameter derivative whose families are continuous.

theorem AVenhance.Infra.Flow.JointC1Core.jointDerivative_continuousOn {P : Type u_1} {G : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] (dtime : ℝ × P → G) (dparam : ℝ × P → P →L[ℝ] G) (s : Set (ℝ × P)) (hTimeCont : ContinuousOn dtime s) (hParamCont : ContinuousOn dparam s) : ContinuousOn (fun (q : ℝ × P) => (jointTimeDerivativeCLM dtime q).coprod (dparam q)) s

theorem AVenhance.Infra.Flow.JointC1Core.contDiffOn_one_of_continuous_derivative_on_open {P : Type u_1} {G : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : ℝ × P → G) (s : Set (ℝ × P)) (hs : IsOpen s) (D : ℝ × P → ℝ × P →L[ℝ] G) (hF : ∀ q ∈ s, HasFDerivAt f (D q) q) (hD : ContinuousOn D s) : ContDiffOn ℝ 1 f s

Convert a continuous family of total derivatives into ContDiffOn C¹ on an open set.

theorem AVenhance.Infra.Flow.contDiffOn_one_of_time_and_parameter_derivatives {P : Type u_1} {G : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup G] [NormedSpace ℝ G] (f : ℝ × P → G) (s : Set (ℝ × P)) (hs : IsOpen s) (dtime : ℝ × P → G) (dparam : ℝ × P → P →L[ℝ] G) (hTime : ∀ (t : ℝ) (z : P), (t, z) ∈ s → HasDerivAt (fun (r : ℝ) => f (r, z)) (dtime (t, z)) t) (hParam : ∀ (t : ℝ) (z : P), (t, z) ∈ s → HasStrictFDerivAt (fun (w : P) => f (t, w)) (dparam (t, z)) z) (hTimeCont : ContinuousOn dtime s) (hParamCont : ContinuousOn dparam s) : ContDiffOn ℝ 1 f s

The open-set version of the joint C¹ criterion, used on forward-time regions of augmented flows.