Identification of the translated mean coefficients

Literal L² operator conjugation agrees with translation of the actual bounded matrix fields and the actual smooth compact cutoffs in the Newtonian boundary operator. These identities connect the fixed inverse to spatial coefficient calculus.

theorem EulerMeanOperatorTranslation.translateOperator_multiplier (a : EulerSmoothLimit.Space) (A : EulerMeanCoefficients.Field) : translateOperator a (EulerMeanCoefficients.multiplier A) = EulerMeanCoefficients.multiplier (EulerMeanCoefficients.translated A a)

Conjugation of the genuine multiplier is multiplication by the translated field.

theorem EulerMeanOperatorTranslation.translatePath_operatorPath (T : ℝ) (A : C(↑(Set.Icc 0 T), EulerMeanCoefficients.Field)) (a : EulerSmoothLimit.Space) : translatePath T a (EulerMeanCoefficients.operatorPath T A) = EulerMeanCoefficients.operatorPath T (EulerMeanCoefficients.translatedPath T A a)

The actual uniformly continuous coefficient path translates by spatial conjugation.

theorem EulerMeanOperatorTranslation.translateOperator_mixedBoundary (a : EulerSmoothLimit.Space) (χ ψ : EulerMeanBoundary.Cutoff) : translateOperator a (EulerMeanBoundary.mixedBoundaryOperator χ ψ) = EulerMeanBoundary.mixedBoundaryOperator (χ.translate a) (ψ.translate a)

Conjugation translates both actual cutoffs in the Newtonian boundary operator.

theorem EulerMeanOperatorTranslation.translateOperator_boundary (a : EulerSmoothLimit.Space) (χ : EulerMeanBoundary.Cutoff) : translateOperator a (EulerMeanBoundary.boundaryOperator χ) = EulerMeanBoundary.boundaryOperator (χ.translate a)

The source's diagonal boundary operator is exactly translated in the fixed inverse.