Module

Jacobian.lean

Nyll.ProCGroups.FoxDifferential.Common.Jacobian

13 declarations indexed from sourceView source ↗

Module documentation

Fox differential: common — jacobian

The principal declarations in this module are:

foxJacobianMatrix

A Fox-Jacobian family packaged as a finite matrix.

foxJacobianId

The identity Fox-Jacobian family with Kronecker-delta entries.

foxJacobianMatrix_apply

The packaged Fox-Jacobian matrix entry is the corresponding Jacobian family entry.

foxJacobianId_apply

The identity Fox-Jacobian evaluates to the Kronecker-delta coefficient at the chosen pair of indices.

Imports2

Mathlib.Algebra.Module.LinearMap.Basic
Mathlib.Data.Matrix.Mul

Imported by4

def

foxJacobianMatrix

L41 ↗

FoxDifferential.foxJacobianMatrix

Documentation

A Fox-Jacobian family packaged as a finite matrix.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}

Lean source · statement

def foxJacobianMatrix (jac : X → Y → R) : Matrix X Y R

theorem

foxJacobianMatrix_apply

L47 ↗

FoxDifferential.foxJacobianMatrix_apply

Documentation

The packaged Fox-Jacobian matrix entry is the corresponding Jacobian family entry.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}
omit [Ring R] in

Lean source · statement

theorem foxJacobianMatrix_apply (jac : X → Y → R) (x : X) (y : Y) :
    foxJacobianMatrix jac x y = jac x y

def

foxJacobianId

L56 ↗

FoxDifferential.foxJacobianId

Documentation

The identity Fox-Jacobian family with Kronecker-delta entries.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}
section Identity
variable [DecidableEq X]

Lean source · statement

def foxJacobianId : X → X → R

theorem

foxJacobianId_apply

L63 ↗

FoxDifferential.foxJacobianId_apply

Documentation

The identity Fox-Jacobian evaluates to the Kronecker-delta coefficient at the chosen pair of indices.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}
section Identity
variable [DecidableEq X]

Lean source · statement

theorem foxJacobianId_apply (x y : X) :
    foxJacobianId (R := R) (X := X) x y = (Pi.single x (1 : R) : X → R) y

theorem

foxJacobianMatrix_id

L69 ↗

FoxDifferential.foxJacobianMatrix_id

Documentation

The identity Fox-Jacobian family is the identity matrix.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}
section Identity
variable [DecidableEq X]

Lean source · statement

theorem foxJacobianMatrix_id :
    foxJacobianMatrix (R := R) (X := X) (Y := X) (foxJacobianId (R := R) (X := X)) =
      (1 : Matrix X X R)

def

foxJacobianLinearMap

L85 ↗

FoxDifferential.foxJacobianLinearMap

Documentation

A Fox-Jacobian family determines the corresponding finite linear map between free coefficient modules.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}

Lean source · full declaration

def foxJacobianLinearMap [Fintype X] (jac : X → Y → R) :
    (X → R) →ₗ[R] (Y → R) where
  toFun v := fun y => ∑ x : X, v x * jac x y
  map_add' v w := by
    funext y
    simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
  map_smul' a v := by
    funext y
    simp only [Pi.smul_apply]
    change (∑ x : X, (a * v x) * jac x y) = a * ∑ x : X, v x * jac x y
    simp only [mul_assoc, Finset.mul_sum]

theorem

foxJacobianLinearMap_apply

L102 ↗

FoxDifferential.foxJacobianLinearMap_apply

Documentation

The linear map associated with a Fox-Jacobian family is evaluated by the finite matrix coefficient formula.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}

Lean source · statement

theorem foxJacobianLinearMap_apply
    [Fintype X]
    (jac : X → Y → R) (v : X → R) (y : Y) :
    foxJacobianLinearMap jac v y = ∑ x : X, v x * jac x y

theorem

foxJacobianLinearMap_eq_vecMul

L109 ↗

FoxDifferential.foxJacobianLinearMap_eq_vecMul

Documentation

The Fox-Jacobian linear map is row-vector multiplication by the corresponding matrix.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}

Lean source · statement

theorem foxJacobianLinearMap_eq_vecMul
    [Fintype X]
    (jac : X → Y → R) (v : X → R) :
    foxJacobianLinearMap jac v = Matrix.vecMul v (foxJacobianMatrix jac)

theorem

foxJacobianLinearMap_id

L120 ↗

FoxDifferential.foxJacobianLinearMap_id

Documentation

The identity Fox-Jacobian induces the identity linear map on the finite free coefficient module.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}

Lean source · statement

theorem foxJacobianLinearMap_id [Fintype X] [DecidableEq X] :
    foxJacobianLinearMap (R := R) (X := X) (Y := X) (foxJacobianId (R := R) (X := X)) =
      (LinearMap.id : (X → R) →ₗ[R] (X → R))

theorem

foxJacobianLinearMap_comp

L141 ↗

FoxDifferential.foxJacobianLinearMap_comp

Documentation

Composition of finite Fox-Jacobian linear maps is given by multiplication of the corresponding Jacobian matrices.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}
variable {Z : Type z}

Lean source · full declaration

theorem foxJacobianLinearMap_comp
    [Fintype X] [Fintype Y]
    (jacXY : X → Y → R) (jacYZ : Y → Z → R) :
    (foxJacobianLinearMap jacYZ).comp (foxJacobianLinearMap jacXY) =
      foxJacobianLinearMap (fun x z => ∑ y : Y, jacXY x y * jacYZ y z) := by
  ext v z
  change
    (∑ y : Y, (∑ x : X, v x * jacXY x y) * jacYZ y z) =
      ∑ x : X, v x * ∑ y : Y, jacXY x y * jacYZ y z
  calc
    (∑ y : Y, (∑ x : X, v x * jacXY x y) * jacYZ y z) =
        ∑ y : Y, ∑ x : X, (v x * jacXY x y) * jacYZ y z := by
          simp only [Finset.sum_mul]
    _ = ∑ x : X, ∑ y : Y, (v x * jacXY x y) * jacYZ y z := by
          rw [Finset.sum_comm]
    _ = ∑ x : X, v x * ∑ y : Y, jacXY x y * jacYZ y z := by
          refine Finset.sum_congr rfl ?_
          intro x _
          rw [Finset.mul_sum]
          refine Finset.sum_congr rfl ?_
          intro y _
          rw [mul_assoc]

theorem

foxJacobianMatrix_comp

L165 ↗

FoxDifferential.foxJacobianMatrix_comp

Documentation

Composition of Fox-Jacobian matrices is finite matrix multiplication.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}
variable {Z : Type z}

Lean source · full declaration

theorem foxJacobianMatrix_comp
    [Fintype Y]
    (jacXY : X → Y → R) (jacYZ : Y → Z → R) :
    foxJacobianMatrix (R := R) (X := X) (Y := Z)
        (fun x z => ∑ y : Y, jacXY x y * jacYZ y z) =
      foxJacobianMatrix (R := R) (X := X) (Y := Y) jacXY *
        foxJacobianMatrix (R := R) (X := Y) (Y := Z) jacYZ := by
  apply Matrix.ext
  intro x z
  exact
    (Matrix.mul_apply
      (M := foxJacobianMatrix (R := R) (X := X) (Y := Y) jacXY)
      (N := foxJacobianMatrix (R := R) (X := Y) (Y := Z) jacYZ)).symm

theorem

foxJacobianLinearMap_single

L183 ↗

FoxDifferential.foxJacobianLinearMap_single

Documentation

A Fox-Jacobian linear map sends a standard source coordinate to the corresponding Jacobian row.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}
variable {Z : Type z}

Lean source · statement

theorem foxJacobianLinearMap_single [Fintype X] [DecidableEq X] (jac : X → Y → R) (x : X) :
    foxJacobianLinearMap jac (Pi.single x (1 : R)) = jac x

theorem

linearMap_ext_pi_single

L199 ↗

FoxDifferential.linearMap_ext_pi_single

Documentation

Linear maps out of finite coordinate vectors are determined by their values on the standard coordinate vectors.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v w z
section JacobianLinearMap
variable {R : Type u} [Ring R]
variable {X : Type v}
variable {Y : Type w}
variable {Z : Type z}
variable {M : Type*} [AddCommMonoid M] [Module R M]

Lean source · statement

theorem linearMap_ext_pi_single
    [Finite X] [DecidableEq X]
    {L₁ L₂ : (X → R) →ₗ[R] M}
    (h : ∀ x : X, L₁ (Pi.single x (1 : R)) = L₂ (Pi.single x (1 : R))) :
    L₁ = L₂

Module documentation

Fox differential: common — jacobian

Declarations