OAI/Computability/RationalHitting/QuantumSeries.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.QuantumSeries.line line 15

    Source documentation

    Each exponent has the one-dimensional coefficient line of its ordered quantum monomial. Lexicographic leading terms do not require a domain matrix coefficient ring.

    def line (B : Γ → Rˣ) (g : Γ) : Submodule K R := K ∙ (B g : R)
  2. lemma OAI.RationalHitting.QuantumSeries.line_mul line 17
  3. lemma OAI.RationalHitting.QuantumSeries.line_isUnit line 31
  4. def OAI.RationalHitting.QuantumSeries.coefficientRing line 40
  5. lemma OAI.RationalHitting.QuantumSeries.coefficientRing_noZeroDivisors line 67
  6. theorem OAI.RationalHitting.HahnGeometric.power_finite_co_support line 100
  7. def OAI.RationalHitting.HahnGeometric.geometricPowers line 125

    Source documentation

    A summable family of geometricPowers of a Hahn series x. If x has non-positive orderTop, then return a junk value given by pretending x = 0.

    def geometricPowers (x : R⟦Γ⟧) : SummableFamily Γ R ℕ where
…
  8. theorem OAI.RationalHitting.HahnGeometric.geometricPowers_of_orderTop_pos line 141
  9. theorem OAI.RationalHitting.HahnGeometric.geometricPowers_of_not_orderTop_pos line 145
  10. theorem OAI.RationalHitting.HahnGeometric.geometricPowers_zero line 151
  11. theorem OAI.RationalHitting.HahnGeometric.coe_geometricPowers line 160
  12. theorem OAI.RationalHitting.HahnGeometric.embDomain_succ_smul_geometricPowers line 165
  13. theorem OAI.RationalHitting.HahnGeometric.one_sub_self_mul_hsum_geometricPowers line 176
  14. lemma OAI.RationalHitting.HahnGeometric.normalized_pos line 183

    Source documentation

    A unit leading coefficient permits the usual normalization, without any commutativity assumption on the coefficient ring.

    lemma normalized_pos (x : HahnSeries Γ R) (u : Rˣ)
    (hu : x.leadingCoeff = (u : R)) :
    0 < (1 - single (-x.order) (↑u⁻¹ : R) * x).orderTop := by
…
  15. lemma OAI.RationalHitting.HahnGeometric.normalized_right_inverse line 210
  16. lemma OAI.RationalHitting.QuantumSeries.line_inv_unit line 238
  17. lemma OAI.RationalHitting.QuantumSeries.single_mem line 264
  18. lemma OAI.RationalHitting.QuantumSeries.hsum_mem line 271
  19. lemma OAI.RationalHitting.QuantumSeries.inverse_candidate_mem line 280
  20. lemma OAI.RationalHitting.QuantumSeries.inverse_exists line 300
  21. lemma OAI.RationalHitting.QuantumSeries.coefficientRing_isUnit_or_eq_zero line 317
  22. abbrev OAI.RationalHitting.QuantumSeries.divisionRing line 331

    Source documentation

    An actual division ring containing all ordered quantum-monomial series; no finite-dimensional-domain or external division-algebra theorem is assumed.

    noncomputable abbrev divisionRing : DivisionRing (coefficientRing B h0 hB) :=
…

    Mentions: OAI.RationalHitting.QuantumSeries.coefficientRing