Commutator-Free Lie Group Methods

This file defines the algebraic skeleton of commutator-free Lie group methods. Such methods advance by composing exponentials of linear combinations of stage generators, avoiding explicit commutators in the method format.

Main definitions

• StageCombination - coefficients of a linear combination of stage generators
• ExponentialAction - an abstract exponential action on a state space
• CommutatorFreeMethod - stage and step exponential coefficient lists
• CommutatorFreeMethod.stagePoint - stage point from precomputed generators
• CommutatorFreeMethod.step - one commutator-free step from precomputed generators

References

• Celledoni, Marthinsen, Owren, Commutator-free Lie group methods
• Owren, Order conditions for commutator-free Lie group methods

@[reducible, inline]

abbrev BSeries.StageCombination (ι : Type u) (R : Type v) : Type (max u v)

Coefficients of a linear combination of stage generators.

Equations

• BSeries.StageCombination ι R = (ι → R)

def BSeries.StageCombination.eval {ι : Type u} {R : Type v} {E : Type w} [Fintype ι] [Semiring R] [AddCommMonoid E] [Module R E] (c : StageCombination ι R) (K : ι → E) : E

Evaluate a stage linear combination on stage generator data.

Equations

• c.eval K = ∑ i : ι, c i • K i

theorem BSeries.StageCombination.eval_congr {ι : Type u} {R : Type v} {E : Type w} [Fintype ι] [Semiring R] [AddCommMonoid E] [Module R E] {c d : StageCombination ι R} {K L : ι → E} (hc : ∀ (i : ι), c i = d i) (hK : ∀ (i : ι), K i = L i) : c.eval K = d.eval L

theorem BSeries.StageCombination.eval_congr_coeff {ι : Type u} {R : Type v} {E : Type w} [Fintype ι] [Semiring R] [AddCommMonoid E] [Module R E] {c d : StageCombination ι R} (K : ι → E) (hc : ∀ (i : ι), c i = d i) : c.eval K = d.eval K

theorem BSeries.StageCombination.eval_congr_data {ι : Type u} {R : Type v} {E : Type w} [Fintype ι] [Semiring R] [AddCommMonoid E] [Module R E] (c : StageCombination ι R) {K L : ι → E} (hK : ∀ (i : ι), K i = L i) : c.eval K = c.eval L

@[simp]

theorem BSeries.StageCombination.eval_zero_coeff {ι : Type u} {R : Type v} {E : Type w} [Fintype ι] [Semiring R] [AddCommMonoid E] [Module R E] (K : ι → E) : eval (fun (x : ι) => 0) K = 0

@[simp]

theorem BSeries.StageCombination.eval_zero_data {ι : Type u} {R : Type v} {E : Type w} [Fintype ι] [Semiring R] [AddCommMonoid E] [Module R E] (c : StageCombination ι R) : (c.eval fun (x : ι) => 0) = 0

@[simp]

theorem BSeries.StageCombination.eval_punit {R : Type v} {E : Type w} [Semiring R] [AddCommMonoid E] [Module R E] (c : StageCombination PUnit.{u_1 + 1} R) (K : PUnit.{u_1 + 1} → E) : c.eval K = c PUnit.unit • K PUnit.unit

structure BSeries.ExponentialAction (A : Type u) (M : Type v) [Zero A] : Type (max u v)

An abstract exponential action generated by elements of A.

• act : A → M → M
• act_zero (y : M) : self.act 0 y = y

def BSeries.ExponentialAction.applyList {A : Type u} {M : Type v} [Zero A] (Φ : ExponentialAction A M) : List A → M → M

Compose exponentials in list order.

Equations

• Φ.applyList [] x✝ = x✝
• Φ.applyList (a :: as) x✝ = Φ.applyList as (Φ.act a x✝)

@[simp]

theorem BSeries.ExponentialAction.applyList_nil {A : Type u} {M : Type v} [Zero A] (Φ : ExponentialAction A M) (y : M) : Φ.applyList [] y = y

@[simp]

theorem BSeries.ExponentialAction.applyList_cons {A : Type u} {M : Type v} [Zero A] (Φ : ExponentialAction A M) (a : A) (as : List A) (y : M) : Φ.applyList (a :: as) y = Φ.applyList as (Φ.act a y)

@[simp]

theorem BSeries.ExponentialAction.applyList_singleton {A : Type u} {M : Type v} [Zero A] (Φ : ExponentialAction A M) (a : A) (y : M) : Φ.applyList [a] y = Φ.act a y

theorem BSeries.ExponentialAction.applyList_congr {A : Type u} {M : Type v} [Zero A] {Φ : ExponentialAction A M} {as bs : List A} : as = bs → ∀ (y : M), Φ.applyList as y = Φ.applyList bs y

@[simp]

theorem BSeries.ExponentialAction.applyList_zero_singleton {A : Type u} {M : Type v} [Zero A] (Φ : ExponentialAction A M) (y : M) : Φ.applyList [0] y = y

structure BSeries.CommutatorFreeMethod (ι : Type u) (R : Type v) : Type (max u v)

A commutator-free method represented by lists of stage-generator combinations.

• stageExps : ι → List (StageCombination ι R)
• stepExps : List (StageCombination ι R)

def BSeries.CommutatorFreeMethod.identity (ι : Type u) (R : Type v) : CommutatorFreeMethod ι R

The method with no exponential evaluations.

Equations

• BSeries.CommutatorFreeMethod.identity ι R = { stageExps := fun (x : ι) => [], stepExps := [] }

def BSeries.CommutatorFreeMethod.singleExponential (R : Type v) [One R] : CommutatorFreeMethod PUnit.{u_1 + 1} R

A one-stage, one-exponential method with coefficient 1.

Equations

• BSeries.CommutatorFreeMethod.singleExponential R = { stageExps := fun (x : PUnit.{?u.1 + 1}) => [], stepExps := [fun (x : PUnit.{?u.1 + 1}) => 1] }

def BSeries.CommutatorFreeMethod.stageGenerators {ι : Type u} {R : Type v} {A : Type w} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (cf : CommutatorFreeMethod ι R) (K : ι → A) (i : ι) : List A

Stage generators produced by evaluating the stage exponential combinations.

Equations

• cf.stageGenerators K i = List.map (fun (c : BSeries.StageCombination ι R) => c.eval K) (cf.stageExps i)

def BSeries.CommutatorFreeMethod.stepGenerators {ι : Type u} {R : Type v} {A : Type w} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (cf : CommutatorFreeMethod ι R) (K : ι → A) : List A

Step generators produced by evaluating the output exponential combinations.

Equations

• cf.stepGenerators K = List.map (fun (c : BSeries.StageCombination ι R) => c.eval K) cf.stepExps

def BSeries.CommutatorFreeMethod.stagePoint {ι : Type u} {R : Type v} {A : Type w} {M : Type x} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (cf : CommutatorFreeMethod ι R) (Φ : ExponentialAction A M) (K : ι → A) (i : ι) (y : M) : M

A stage point obtained by composing the stage exponentials.

Equations

• cf.stagePoint Φ K i y = Φ.applyList (cf.stageGenerators K i) y

def BSeries.CommutatorFreeMethod.step {ι : Type u} {R : Type v} {A : Type w} {M : Type x} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (cf : CommutatorFreeMethod ι R) (Φ : ExponentialAction A M) (K : ι → A) (y : M) : M

One commutator-free step from precomputed stage generators.

Equations

• cf.step Φ K y = Φ.applyList (cf.stepGenerators K) y

@[simp]

theorem BSeries.CommutatorFreeMethod.identity_stageGenerators {ι : Type u} {R : Type v} {A : Type w} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (K : ι → A) (i : ι) : (identity ι R).stageGenerators K i = []

@[simp]

theorem BSeries.CommutatorFreeMethod.identity_stepGenerators {ι : Type u} {R : Type v} {A : Type w} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (K : ι → A) : (identity ι R).stepGenerators K = []

@[simp]

theorem BSeries.CommutatorFreeMethod.identity_stagePoint {ι : Type u} {R : Type v} {A : Type w} {M : Type x} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (Φ : ExponentialAction A M) (K : ι → A) (i : ι) (y : M) : (identity ι R).stagePoint Φ K i y = y

@[simp]

theorem BSeries.CommutatorFreeMethod.identity_step {ι : Type u} {R : Type v} {A : Type w} {M : Type x} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (Φ : ExponentialAction A M) (K : ι → A) (y : M) : (identity ι R).step Φ K y = y

theorem BSeries.CommutatorFreeMethod.stageGenerators_congr_data {ι : Type u} {R : Type v} {A : Type w} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (cf : CommutatorFreeMethod ι R) {K L : ι → A} (hK : ∀ (i : ι), K i = L i) (i : ι) : cf.stageGenerators K i = cf.stageGenerators L i

theorem BSeries.CommutatorFreeMethod.stepGenerators_congr_data {ι : Type u} {R : Type v} {A : Type w} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (cf : CommutatorFreeMethod ι R) {K L : ι → A} (hK : ∀ (i : ι), K i = L i) : cf.stepGenerators K = cf.stepGenerators L

theorem BSeries.CommutatorFreeMethod.stagePoint_congr_data {ι : Type u} {R : Type v} {A : Type w} {M : Type x} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (cf : CommutatorFreeMethod ι R) (Φ : ExponentialAction A M) {K L : ι → A} (hK : ∀ (i : ι), K i = L i) (i : ι) (y : M) : cf.stagePoint Φ K i y = cf.stagePoint Φ L i y

theorem BSeries.CommutatorFreeMethod.step_congr_data {ι : Type u} {R : Type v} {A : Type w} {M : Type x} [Fintype ι] [Semiring R] [AddCommMonoid A] [Module R A] (cf : CommutatorFreeMethod ι R) (Φ : ExponentialAction A M) {K L : ι → A} (hK : ∀ (i : ι), K i = L i) (y : M) : cf.step Φ K y = cf.step Φ L y

@[simp]

theorem BSeries.CommutatorFreeMethod.singleExponential_stageGenerators {R : Type v} {A : Type w} [Semiring R] [AddCommMonoid A] [Module R A] (K : PUnit.{u_1 + 1} → A) (i : PUnit.{u_1 + 1}) : (singleExponential R).stageGenerators K i = []

@[simp]

theorem BSeries.CommutatorFreeMethod.singleExponential_stepGenerators {R : Type v} {A : Type w} [Semiring R] [AddCommMonoid A] [Module R A] (K : PUnit.{u_1 + 1} → A) : (singleExponential R).stepGenerators K = [K PUnit.unit]

@[simp]

theorem BSeries.CommutatorFreeMethod.singleExponential_stagePoint {R : Type v} {A : Type w} {M : Type x} [Semiring R] [AddCommMonoid A] [Module R A] (Φ : ExponentialAction A M) (K : PUnit.{u_1 + 1} → A) (i : PUnit.{u_1 + 1}) (y : M) : (singleExponential R).stagePoint Φ K i y = y

@[simp]

theorem BSeries.CommutatorFreeMethod.singleExponential_step {R : Type v} {A : Type w} {M : Type x} [Semiring R] [AddCommMonoid A] [Module R A] (Φ : ExponentialAction A M) (K : PUnit.{u_1 + 1} → A) (y : M) : (singleExponential R).step Φ K y = Φ.act (K PUnit.unit) y