Closed differentiability for strongly continuous linear isometric actions.

theorem EulerIsometricAction.hasFDerivAt_all {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : P → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : P) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (u : E) (D : P →L[ℝ] E) (h : HasFDerivAt (fun (a : P) => (τ a) u) D 0) (a : P) : HasFDerivAt (fun (b : P) => (τ b) u) ((τ a).toContinuousLinearMap ∘SL D) a

theorem EulerIsometricAction.orbits_tendstoUniformly {P : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : P → E →ₗᵢ[ℝ] E) {ι : Type u_3} {l : Filter ι} (u : ι → E) (v : E) (hu : Filter.Tendsto u l (nhds v)) : TendstoUniformly (fun (n : ι) (a : P) => (τ a) (u n)) (fun (a : P) => (τ a) v) l

theorem EulerIsometricAction.derivatives_tendstoUniformly {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : P → E →ₗᵢ[ℝ] E) {ι : Type u_3} {l : Filter ι} (D : ι → P →L[ℝ] E) (D₀ : P →L[ℝ] E) (hD : Filter.Tendsto D l (nhds D₀)) : TendstoUniformly (fun (n : ι) (a : P) => (τ a).toContinuousLinearMap ∘SL D n) (fun (a : P) => (τ a).toContinuousLinearMap ∘SL D₀) l

theorem EulerIsometricAction.hasFDerivAt_limit {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : P → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : P) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (hzero : ∀ (u : E), (τ 0) u = u) (u : ℕ → E) (D : ℕ → P →L[ℝ] E) (u₀ : E) (D₀ : P →L[ℝ] E) (h : ∀ (n : ℕ), HasFDerivAt (fun (a : P) => (τ a) (u n)) (D n) 0) (hu : Filter.Tendsto u Filter.atTop (nhds u₀)) (hD : Filter.Tendsto D Filter.atTop (nhds D₀)) : HasFDerivAt (fun (a : P) => (τ a) u₀) D₀ 0

Derivatives of an isometric orbit form a closed operator.