Exact formal inverse-branch calculations for the two explicit examples. These do not assert a general Lagrange–Good or half-pair inversion theorem.

def GaussianMomentsCounterexamples.geometricSeries : PowerSeries ℂ

The geometric series, defined coefficientwise.

Equations

• GaussianMomentsCounterexamples.geometricSeries = PowerSeries.mk fun (x : ℕ) => 1

@[simp]

theorem GaussianMomentsCounterexamples.geometricSeries_coeff (m : ℕ) : (PowerSeries.coeff m) geometricSeries = 1

theorem GaussianMomentsCounterexamples.geometricSeries_mul_one_sub : geometricSeries * (1 - PowerSeries.X) = 1

theorem GaussianMomentsCounterexamples.one_sub_mul_geometricSeries : (1 - PowerSeries.X) * geometricSeries = 1

theorem GaussianMomentsCounterexamples.one_sub_X_ne_zero : 1 - PowerSeries.X ≠ 0

theorem GaussianMomentsCounterexamples.geometricSeries_eq_inv : geometricSeries = (1 - PowerSeries.X)⁻¹

noncomputable def GaussianMomentsCounterexamples.branchZeta : PowerSeries ℂ

The branch t/(1-t), with formal division by a unit.

Equations

• GaussianMomentsCounterexamples.branchZeta = PowerSeries.X * GaussianMomentsCounterexamples.geometricSeries

theorem GaussianMomentsCounterexamples.one_add_branchZeta : 1 + branchZeta = geometricSeries

@[simp]

theorem GaussianMomentsCounterexamples.branchZeta_constantCoeff : PowerSeries.constantCoeff branchZeta = 0

theorem GaussianMomentsCounterexamples.branchZeta_eq : branchZeta = PowerSeries.X * (1 - PowerSeries.X)⁻¹

noncomputable def GaussianMomentsCounterexamples.discoveryH (z : Fin 2 → PowerSeries ℂ) : Fin 2 → PowerSeries ℂ

The explicit polynomial map H from the discovery calculation.

Equations

• GaussianMomentsCounterexamples.discoveryH z = ![(1 - z 0) * (1 + z 1), 1 + z 1]

noncomputable def GaussianMomentsCounterexamples.discoveryBranch : Fin 2 → PowerSeries ℂ

The formal branch (t, t/(1-t)) of the discovery vector field.

Equations

• GaussianMomentsCounterexamples.discoveryBranch = ![PowerSeries.X, GaussianMomentsCounterexamples.branchZeta]

theorem GaussianMomentsCounterexamples.discoveryBranch_equation (i : Fin 2) : discoveryBranch i = PowerSeries.X * discoveryH discoveryBranch i

noncomputable def GaussianMomentsCounterexamples.discoveryHPolynomial : Fin 2 → MvPolynomial (Fin 2) ℂ

The polynomial map whose evaluation is discoveryH.

Equations

• GaussianMomentsCounterexamples.discoveryHPolynomial = ![(1 - MvPolynomial.X 0) * (1 + MvPolynomial.X 1), 1 + MvPolynomial.X 1]

theorem GaussianMomentsCounterexamples.discoveryHPolynomial_eval (z : Fin 2 → PowerSeries ℂ) (i : Fin 2) : MvPolynomial.eval₂ PowerSeries.C z (discoveryHPolynomial i) = discoveryH z i

theorem GaussianMomentsCounterexamples.discoveryBranch_unique (g : Fin 2 → PowerSeries ℂ) (hg : ∀ (i : Fin 2), g i = PowerSeries.X * discoveryH g i) : g = discoveryBranch

The displayed branch is the unique solution of g=tH(g).

noncomputable def GaussianMomentsCounterexamples.discoveryJacobian : Matrix (Fin 2) (Fin 2) (PowerSeries ℂ)

The Jacobian matrix of H evaluated on the branch.

Equations

• GaussianMomentsCounterexamples.discoveryJacobian = !![-(1 + GaussianMomentsCounterexamples.branchZeta), 1 - PowerSeries.X; 0, 1]

theorem GaussianMomentsCounterexamples.discoveryJacobian_correspondence (i j : Fin 2) : discoveryJacobian i j = MvPolynomial.eval₂ PowerSeries.C discoveryBranch ((MvPolynomial.pderiv j) (discoveryHPolynomial i))

The displayed matrix is the actual polynomial Jacobian evaluated on the branch.

theorem GaussianMomentsCounterexamples.discovery_determinant : (1 - PowerSeries.X • discoveryJacobian).det = 1

noncomputable def GaussianMomentsCounterexamples.halfPairV (z : PowerSeries ℂ) : PowerSeries ℂ

The quadratic coefficient v in the three-variable construction.

Equations

• GaussianMomentsCounterexamples.halfPairV z = -PowerSeries.C (1 / 2) * (1 + z) * (2 + z)

theorem GaussianMomentsCounterexamples.halfPair_branch_equation : branchZeta = PowerSeries.X * (1 + branchZeta)

theorem GaussianMomentsCounterexamples.halfPair_radicand : 1 - 2 * PowerSeries.X * halfPairV branchZeta = geometricSeries ^ 2

theorem GaussianMomentsCounterexamples.halfPair_radicand_inverse : 1 - 2 * PowerSeries.X * halfPairV branchZeta = (1 - PowerSeries.X)⁻¹ ^ 2

noncomputable def GaussianMomentsCounterexamples.halfPairH : Polynomial ℂ

The polynomial h(z)=1+z in the three-variable discovery formula.

Equations

• GaussianMomentsCounterexamples.halfPairH = 1 + Polynomial.X

theorem GaussianMomentsCounterexamples.halfPair_denominator : 1 - PowerSeries.X * Polynomial.eval₂ PowerSeries.C branchZeta (Polynomial.derivative halfPairH) = 1 - PowerSeries.X

theorem GaussianMomentsCounterexamples.halfPair_inverse_sqrt : (1 - PowerSeries.X) ^ 2 * (1 - 2 * PowerSeries.X * halfPairV branchZeta) = 1

The normalized inverse square root is 1-t: its square times the radicand is one.

theorem GaussianMomentsCounterexamples.halfPair_inverse_sqrt_unique (s : PowerSeries ℂ) (hs0 : PowerSeries.constantCoeff s = 1) (hs : s ^ 2 * (1 - 2 * PowerSeries.X * halfPairV branchZeta) = 1) : s = 1 - PowerSeries.X

Constant coefficient one selects the unique inverse square-root branch.

theorem GaussianMomentsCounterexamples.halfPair_cancellation : (1 - PowerSeries.X) * geometricSeries = 1

The normalized inverse square-root factor cancels the denominator exactly.