FDeriv Helper Lemmas for Global Theorem

This file contains helper lemmas for computing fderiv in coordinate directions. These show that fderiv f y (e_i) equals the partial derivative in direction i.

Main Results

• fderiv_rotR_rotM_in_e0 - fderiv of rotR ∘ rotM in direction e₀ gives rotR'
• fderiv_rotR_rotM_in_e1 - fderiv of rotR ∘ rotM in direction e₁ gives rotR ∘ rotMθ
• fderiv_rotR_rotM_in_e2 - fderiv of rotR ∘ rotM in direction e₂ gives rotR ∘ rotMφ
• fderiv_rotR'_rotM_in_e0 - fderiv of rotR' ∘ rotM in direction e₀ gives -rotR
• fderiv_rotR'_rotM_in_e1 - fderiv of rotR' ∘ rotM in direction e₁ gives rotR' ∘ rotMθ

theorem GlobalTheorem.HasDerivAt_rotR' (α : ℝ) (v : Euc(2)) : HasDerivAt (fun (x : ℝ) => (rotR' x) v) (-(rotR α) v) α

theorem GlobalTheorem.fderiv_rotR_any_M_in_e0 (S : Euc(3)) (y : GlobalTheorem.E✝ 3) (M : ℝ → ℝ → Euc(3) →L[ℝ] Euc(2)) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR (z.ofLp 0)) ((M (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (fun (z : GlobalTheorem.E✝² 3) => (rotR (z.ofLp 0)) ((M (z.ofLp 1) (z.ofLp 2)) S)) y) (EuclideanSpace.single 0 1) = (rotR' (y.ofLp 0)) ((M (y.ofLp 1) (y.ofLp 2)) S)

fderiv of rotR with any M in direction e₀ gives rotR'

theorem GlobalTheorem.fderiv_rotR_rotM_in_e0 (S : Euc(3)) (y : GlobalTheorem.E✝ 3) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (fun (z : GlobalTheorem.E✝² 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) (EuclideanSpace.single 0 1) = (rotR' (y.ofLp 0)) ((rotM (y.ofLp 1) (y.ofLp 2)) S)

fderiv of rotR (y.ofLp 0) (rotM (y.ofLp 1) (y.ofLp 2) S) in direction e₀ gives rotR'

theorem GlobalTheorem.fderiv_rotR_rotM_in_e2 (S : Euc(3)) (y : GlobalTheorem.E✝ 3) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (fun (z : GlobalTheorem.E✝² 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) (EuclideanSpace.single 2 1) = (rotR (y.ofLp 0)) ((rotMφ (y.ofLp 1) (y.ofLp 2)) S)

fderiv of rotR (y.ofLp 0) (rotM (y.ofLp 1) (y.ofLp 2) S) in direction e₂ gives rotR ∘ rotMφ

theorem GlobalTheorem.fderiv_rotR_rotM_in_e1 (S : Euc(3)) (y : GlobalTheorem.E✝ 3) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (fun (z : GlobalTheorem.E✝² 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) (EuclideanSpace.single 1 1) = (rotR (y.ofLp 0)) ((rotMθ (y.ofLp 1) (y.ofLp 2)) S)

fderiv of rotR (y.ofLp 0) (rotM (y.ofLp 1) (y.ofLp 2) S) in direction e₁ gives rotR ∘ rotMθ

theorem GlobalTheorem.fderiv_rotR'_rotM_in_e0 (S : Euc(3)) (y : GlobalTheorem.E✝ 3) (α θ φ : ℝ) (hα : y.ofLp 0 = α) (hθ : y.ofLp 1 = θ) (hφ : y.ofLp 2 = φ) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR' (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (fun (z : GlobalTheorem.E✝² 3) => (rotR' (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) (EuclideanSpace.single 0 1) = -(rotR α) ((rotM θ φ) S)

fderiv of rotR' (y.ofLp 0) (rotM (y.ofLp 1) (y.ofLp 2) S) in direction e₀ gives -rotR

theorem GlobalTheorem.fderiv_rotR'_rotM_in_e1 (S : Euc(3)) (y : GlobalTheorem.E✝ 3) (α θ φ : ℝ) (hα : y.ofLp 0 = α) (hθ : y.ofLp 1 = θ) (hφ : y.ofLp 2 = φ) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR' (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (fun (z : GlobalTheorem.E✝² 3) => (rotR' (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) (EuclideanSpace.single 1 1) = (rotR' α) ((rotMθ θ φ) S)

fderiv of rotR' (y.ofLp 0) (rotM (y.ofLp 1) (y.ofLp 2) S) in direction e₁ gives rotR' α (rotMθ θ φ S)

theorem GlobalTheorem.fderiv_rotR'_rotM_in_e2 (S : Euc(3)) (y : GlobalTheorem.E✝ 3) (α θ φ : ℝ) (hα : y.ofLp 0 = α) (hθ : y.ofLp 1 = θ) (hφ : y.ofLp 2 = φ) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR' (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (fun (z : GlobalTheorem.E✝² 3) => (rotR' (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) (EuclideanSpace.single 2 1) = (rotR' α) ((rotMφ θ φ) S)

fderiv of rotR' (y.ofLp 0) (rotM (y.ofLp 1) (y.ofLp 2) S) in direction e₂ gives rotR' α (rotMφ θ φ S)

fderiv of rotproj_inner in coordinate directions

These combine fderiv_inner_const with fderiv_rotR_rotM_in_e* to give formulas for partial derivatives of rotproj_inner directly.

theorem GlobalTheorem.fderiv_rotproj_inner_in_e0 (S : Euc(3)) (w : Euc(2)) (y : GlobalTheorem.E✝ 3) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (rotproj_inner S w) y) (EuclideanSpace.single 0 1) = inner ℝ ((rotR' (y.ofLp 0)) ((rotM (y.ofLp 1) (y.ofLp 2)) S)) w

fderiv of rotproj_inner in direction e₀

theorem GlobalTheorem.fderiv_rotproj_inner_in_e1 (S : Euc(3)) (w : Euc(2)) (y : GlobalTheorem.E✝ 3) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (rotproj_inner S w) y) (EuclideanSpace.single 1 1) = inner ℝ ((rotR (y.ofLp 0)) ((rotMθ (y.ofLp 1) (y.ofLp 2)) S)) w

fderiv of rotproj_inner in direction e₁

theorem GlobalTheorem.fderiv_rotproj_inner_in_e2 (S : Euc(3)) (w : Euc(2)) (y : GlobalTheorem.E✝ 3) (hf_diff : DifferentiableAt ℝ (fun (z : GlobalTheorem.E✝¹ 3) => (rotR (z.ofLp 0)) ((rotM (z.ofLp 1) (z.ofLp 2)) S)) y) : (fderiv ℝ (rotproj_inner S w) y) (EuclideanSpace.single 2 1) = inner ℝ ((rotR (y.ofLp 0)) ((rotMφ (y.ofLp 1) (y.ofLp 2)) S)) w

fderiv of rotproj_inner in direction e₂

nth_partial of rotproj_inner in coordinate directions

These lift the pointwise fderiv_rotproj_inner_in_e* to function-level equalities of nth_partial, eliminating the funext/congrArg boilerplate at each use site.

theorem GlobalTheorem.nth_partial_rotproj_inner_e0 (S : Euc(3)) (w : Euc(2)) : nth_partial 0 (rotproj_inner S w) = fun (y : Euc(3)) => inner ℝ ((rotR' (y.ofLp 0)) ((rotM (y.ofLp 1) (y.ofLp 2)) S)) w

theorem GlobalTheorem.nth_partial_rotproj_inner_e1 (S : Euc(3)) (w : Euc(2)) : nth_partial 1 (rotproj_inner S w) = fun (y : Euc(3)) => inner ℝ ((rotR (y.ofLp 0)) ((rotMθ (y.ofLp 1) (y.ofLp 2)) S)) w

theorem GlobalTheorem.nth_partial_rotproj_inner_e2 (S : Euc(3)) (w : Euc(2)) : nth_partial 2 (rotproj_inner S w) = fun (y : Euc(3)) => inner ℝ ((rotR (y.ofLp 0)) ((rotMφ (y.ofLp 1) (y.ofLp 2)) S)) w