Derivatives of real projections

A constant projection has zero projected derivative without regularity assumptions. Prescribed projected derivatives also hold almost everywhere across exceptional levels.

theorem ContinuousLinearMap.apply_deriv_eq_of_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (π : E →L[ℝ] ℝ) {θ : ℝ → ℝ} {γ : ℝ → E} {θ' t : ℝ} (hπ : ⇑π ∘ γ = θ) (hθ : HasDerivAt θ θ' t) (hγ : DifferentiableAt ℝ γ t ∨ deriv θ t = 0) : π (deriv γ t) = θ'

A real projection has the prescribed derivative if the curve is differentiable, or if the derivative of the projected curve vanishes.

theorem ContinuousLinearMap.apply_deriv_eq_zero_of_forall_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : E →L[ℝ] ℝ) {γ : ℝ → E} {c : ℝ} (hγ : ∀ (t : ℝ), L (γ t) = c) (t : ℝ) : L (deriv γ t) = 0

A constant real projection has zero projected derivative, including where the curve is not differentiable and its total derivative is defined to be zero.

theorem ContinuousLinearMap.apply_deriv_ae_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {θ θ' : ℝ → ℝ} {γ : ℝ → E} (π : E →L[ℝ] ℝ) (hπ : ⇑π ∘ γ = θ) {s S : Set ℝ} (hs : s.Countable) (hS : S.Countable) (hdθ : ∀ t ∈ Set.Ioo a b \ s, HasDerivAt θ (θ' t) t) (hdγ : ∀ t ∈ Set.Ioo a b \ s, θ t ∉ S → DifferentiableAt ℝ γ t) : (fun (t : ℝ) => π (deriv γ t)) =ᵐ[MeasureTheory.volume.restrict (Set.Ioc a b)] θ'

A real projection of a curve has the prescribed derivative almost everywhere, even when exceptional projection levels have uncountable preimages.