Documentation

LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.PrincipalComponentTensor

API checks for extension of scalars on a homogeneous component #

The fixture has two distinct finite-support exponents and a nonzero infinite-support coefficient in P_1. Its two tensor coordinates are checked independently. The forward map agrees with multiplication of representatives, and both inverse identities hold on the fixture.

source
noncomputable def Tests.approachZeroPrincipalComponent :
Berarducci.PrincipalComponent ℚ 1

The intrinsic degree-one class of the approach-zero series.

Equations
Instances For
    source
    def Tests.tensorExponentZero :
    ↥(HahnSeries.Nonpositive.exponentMonoid ℝ)

    The exponent zero in the nonpositive real cone.

    Equations
    Instances For
      source
      def Tests.tensorExponentNegOne :
      ↥(HahnSeries.Nonpositive.exponentMonoid ℝ)

      The exponent negative one in the nonpositive real cone.

      Equations
      Instances For
        source
        noncomputable def Tests.approachZeroTwoExponentTensor :
        TensorProduct ℚ (Berarducci.PrincipalComponent ℚ 1) ↥Berarducci.FiniteSupportRing

        A tensor with nonzero coordinates at the two distinct exponents 0 and -1.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Tests.approachZeroTwoExponentTensor_coordinates :
          ((TensorProduct.equivFinsuppOfBasisRight HahnSeries.Nonpositive.finiteSupportBasis) approachZeroTwoExponentTensor) tensorExponentZero = approachZeroPrincipalComponent ∧ ((TensorProduct.equivFinsuppOfBasisRight HahnSeries.Nonpositive.finiteSupportBasis) approachZeroTwoExponentTensor) tensorExponentNegOne = 2 • approachZeroPrincipalComponent

          Both coordinates of the two-exponent fixture are retained by the canonical tensor-basis presentation.

          source
          theorem Tests.approachZeroTwoExponentTensor_ne_zero :
          approachZeroTwoExponentTensor ≠ 0

          The two-exponent tensor is nonzero; in particular, it is not a one-term presentation in which one of the two monomials has silently been discarded.

          source
          theorem Tests.approachZeroTwoExponentTensor_forward :
          (Berarducci.principalComponentTensorEquiv ℚ 1) approachZeroTwoExponentTensor = (HahnSeries.Nonpositive.degreeFiniteSupportResidueEquiv ℚ) (HahnSeries.Nonpositive.finiteSupportMonomial tensorExponentZero) • (Berarducci.principalComponentToHahnDegreeLayer ℚ 1) approachZeroPrincipalComponent + (HahnSeries.Nonpositive.degreeFiniteSupportResidueEquiv ℚ) (HahnSeries.Nonpositive.finiteSupportMonomial tensorExponentNegOne) • (Berarducci.principalComponentToHahnDegreeLayer ℚ 1) (2 • approachZeroPrincipalComponent)

          The public extension-of-scalars equivalence sends the two-exponent fixture to the sum of the two corresponding homogeneous products.

          source
          theorem Tests.approachZeroTensorNegOne_representative :
          (Berarducci.principalComponentTensorMap ℚ 1) (approachZeroPrincipalComponent ⊗ₜ[ℚ] HahnSeries.Nonpositive.finiteSupportMonomial tensorExponentNegOne) = Berarducci.degreeLayerMk 1 (↑(HahnSeries.Nonpositive.finiteSupportMonomial tensorExponentNegOne) * approachZeroNonpositive) approachZeroTensorNegOne_representative._proof_1

          The representative formula sends the negative-one pure tensor to the degree-one class of the translated approach-zero series.

          source
          theorem Tests.approachZeroTwoExponentTensor_roundtrip :
          (Berarducci.principalComponentTensorEquiv ℚ 1).symm ((Berarducci.principalComponentTensorEquiv ℚ 1) approachZeroTwoExponentTensor) = approachZeroTwoExponentTensor

          The public inverse is a genuine inverse on the nontrivial two-exponent fixture.