FinMatrix.Matrix.MatrixRFun

Require Export RExt.
Require Export RealFunction.
Require Export MatrixModule.

Matrix theory come from common implementations

Module Export MatrixTheoryRFun := RingMatrixTheory RingElementTypeRFun.

Open Scope R_scope.
Open Scope Rfun_scope.
Open Scope vec_scope.
Open Scope mat_scope.

Derivative of matrix

标量(函数)对矩阵(函数)的梯度

Section test.
  Let f00 : A := fun t => 1.
  Let f01 : A := fun t => 2.
  Let f10 : A := fun t => 3.
  Let f11 : A := fun t => 4.
  Let l1 := [[f00 ;f01 ];[f10 ;f11 ]].
  Let m1 := @l2m 2 2 l1.

End test.

Section Example4CoordinateSystem.
  Open Scope fun_scope.
  Notation "1" := Aone : fun_scope.
  Notation "0" := Azero : fun_scope.

  Variable ψ θ ϕ : A.
  Let cθ : A := fun t => cos (θ t).
  Let sθ : A := fun t => sin (θ t).
  Let c ψ : A := fun t => cos (ψ t).
  Let s ψ : A := fun t => sin (ψ t).
  Let cϕ : A := fun t => cos (ϕ t).
  Let sϕ : A := fun t => sin (ϕ t).

  Let Rx := mkmat_3_3 1 0 0 0 cϕ sϕ 0 (-sϕ) cϕ.
  Let Ry := mkmat_3_3 cθ 0 (-sθ) 0 1 0 sθ 0 cθ.
  Let Rz := mkmat_3_3 c ψ s ψ 0 (-s ψ) c ψ 0 0 0 1.
  Let Rbe :=
        mkmat_3_3
          (cθ * c ψ) (c ψ * sθ * sϕ - s ψ * cϕ)
          (c ψ * sθ * cϕ + sϕ * s ψ) (cθ * s ψ)
          (s ψ * sθ * sϕ + c ψ * cϕ)
          (s ψ * sθ * cϕ - c ψ * sϕ)
          (-sθ) (sϕ * cθ) (cϕ * cθ).
  Lemma Rbe_ok : (Rbe = Rz \T * Ry \T * Rx \T)%M.
  Proof. apply m2l_inj. cbv. list_eq; extensionality x; ring. Qed.

End Example4CoordinateSystem.