Actual algebra of coherent all-order fields, including multiplication by the genuine coefficient towers of the source deformation.

noncomputable def EulerAllOrderCorrectionData.FieldTower.add {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) : FieldTower P T

Add, bundling field, realization, value_eq.

Equations

• A.add B = { field := A.field + B.field, realization := fun (q : ℕ) => A.realization q + B.realization q, value_eq := ⋯ }

noncomputable def EulerAllOrderCorrectionData.FieldTower.smul {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (c : ℝ) : FieldTower P T

Smul, bundling field, realization, value_eq.

Equations

• A.smul c = { field := c • A.field, realization := fun (q : ℕ) => c • A.realization q, value_eq := ⋯ }

theorem EulerAllOrderCorrectionData.FieldTower.add_pointField {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) (t : ↑(Set.Icc 0 T)) : (A.add B).pointField t = fun (x : EulerLiftedGradientSpace.LiftDomain P) => A.pointField t x + B.pointField t x

theorem EulerAllOrderCorrectionData.FieldTower.smul_pointField {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (c : ℝ) (t : ↑(Set.Icc 0 T)) : (A.smul c).pointField t = fun (x : EulerLiftedGradientSpace.LiftDomain P) => c • A.pointField t x

noncomputable def EulerAllOrderCorrectionData.FieldTower.multiply {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (C : CoefficientTower P T) : FieldTower P T

Multiply, bundling field, realization, value_eq.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerAllOrderCorrectionData.FieldTower.multiply_field {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (C : CoefficientTower P T) (t : ↑(Set.Icc 0 T)) : (A.multiply C).field t = (C.coefficient t).operator (A.field t)

theorem EulerAllOrderCorrectionData.FieldTower.multiply_pointField {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (C : CoefficientTower P T) (t : ↑(Set.Icc 0 T)) : (A.multiply C).pointField t = fun (x : EulerLiftedGradientSpace.LiftDomain P) => ((C.coefficient t).coefficient x) (A.pointField t x)