Rational hitting lists: quantum series

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/QuantumSeries.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

def Complexity.RationalHitting.QuantumSeries.line {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (g : Γ) : Submodule K R

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

Equations

• Complexity.RationalHitting.QuantumSeries.line B g = K ∙ ↑(B g)

theorem Complexity.RationalHitting.QuantumSeries.line_mul {Γ : Type v_1} {K : Type v_2} {R : Type v_3} [AddCommGroup Γ] [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) {g h : Γ} {x y : R} (hx : x ∈ line B g) (hy : y ∈ line B h) : x * y ∈ line B (g + h)

theorem Complexity.RationalHitting.QuantumSeries.line_isUnit {Γ : Type v_1} {K : Type v_2} {R : Type v_3} [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) {g : Γ} {x : R} (hx : x ∈ line B g) (hne : x ≠ 0) : IsUnit x

def Complexity.RationalHitting.QuantumSeries.coefficientRing {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) : Subring (HahnSeries Γ R)

The Hahn-series subring with each coefficient on its prescribed monomial line.

Equations

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

theorem Complexity.RationalHitting.QuantumSeries.coefficientRing_noZeroDivisors {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) : NoZeroDivisors ↥(coefficientRing B h0 hB)

theorem Complexity.RationalHitting.HahnGeometric.power_finite_co_support {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (g : Γ) : {a : ℕ | ((fun (n : ℕ) => x ^ n) a).coeff g ≠ 0}.Finite

noncomputable def Complexity.RationalHitting.HahnGeometric.geometricPowers {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : HahnSeries Γ R) : HahnSeries.SummableFamily Γ R ℕ

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.

Equations

• Complexity.RationalHitting.HahnGeometric.geometricPowers x = { toFun := fun (n : ℕ) => (if 0 < x.orderTop then x else 0) ^ n, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ }

@[simp]

theorem Complexity.RationalHitting.HahnGeometric.geometricPowers_toFun {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : HahnSeries Γ R) (n : ℕ) : (geometricPowers x) n = (if 0 < x.orderTop then x else 0) ^ n

theorem Complexity.RationalHitting.HahnGeometric.geometricPowers_of_orderTop_pos {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (n : ℕ) : (geometricPowers x) n = x ^ n

theorem Complexity.RationalHitting.HahnGeometric.geometricPowers_of_not_orderTop_pos {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : ¬0 < x.orderTop) : geometricPowers x = HahnSeries.SummableFamily.single 0 1

@[simp]

theorem Complexity.RationalHitting.HahnGeometric.geometricPowers_zero {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] : geometricPowers 0 = HahnSeries.SummableFamily.single 0 1

@[simp]

theorem Complexity.RationalHitting.HahnGeometric.coe_geometricPowers {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : ⇑(geometricPowers x) = HPow.hPow x

theorem Complexity.RationalHitting.HahnGeometric.embDomain_succ_smul_geometricPowers {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (x • geometricPowers x).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } = geometricPowers x - HahnSeries.SummableFamily.ofFinsupp (Finsupp.single 0 1)

theorem Complexity.RationalHitting.HahnGeometric.one_sub_self_mul_hsum_geometricPowers {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {x : HahnSeries Γ R} (hx : 0 < x.orderTop) : (1 - x) * (geometricPowers x).hsum = 1

theorem Complexity.RationalHitting.HahnGeometric.normalized_pos {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : HahnSeries Γ R) (u : Rˣ) (hu : x.leadingCoeff = ↑u) : 0 < (1 - (HahnSeries.single (-x.order)) ↑u⁻¹ * x).orderTop

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

theorem Complexity.RationalHitting.HahnGeometric.normalized_right_inverse {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x : HahnSeries Γ R) (u : Rˣ) (hu : x.leadingCoeff = ↑u) : x * ((geometricPowers (1 - (HahnSeries.single (-x.order)) ↑u⁻¹ * x)).hsum * (HahnSeries.single (-x.order)) ↑u⁻¹) = 1

theorem Complexity.RationalHitting.QuantumSeries.line_inv_unit {Γ : Type v_1} {K : Type v_2} {R : Type v_3} [AddCommGroup Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) {g : Γ} (u : Rˣ) (hu : ↑u ∈ line B g) : ↑u⁻¹ ∈ line B (-g)

theorem Complexity.RationalHitting.QuantumSeries.single_mem {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) {g : Γ} {r : R} (hr : r ∈ line B g) : (HahnSeries.single g) r ∈ coefficientRing B h0 hB

theorem Complexity.RationalHitting.QuantumSeries.hsum_mem {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) {α : Type u_4} (x : HahnSeries.SummableFamily Γ R α) (hx : ∀ (i : α), x i ∈ coefficientRing B h0 hB) : x.hsum ∈ coefficientRing B h0 hB

theorem Complexity.RationalHitting.QuantumSeries.inverse_candidate_mem {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) (x : HahnSeries Γ R) (hx : x ∈ coefficientRing B h0 hB) (u : Rˣ) (hu : x.leadingCoeff = ↑u) : (HahnGeometric.geometricPowers (1 - (HahnSeries.single (-x.order)) ↑u⁻¹ * x)).hsum * (HahnSeries.single (-x.order)) ↑u⁻¹ ∈ coefficientRing B h0 hB

theorem Complexity.RationalHitting.QuantumSeries.inverse_exists {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) (x : ↥(coefficientRing B h0 hB)) (hx : x ≠ 0) : ∃ (y : ↥(coefficientRing B h0 hB)), x * y = 1

theorem Complexity.RationalHitting.QuantumSeries.coefficientRing_isUnit_or_eq_zero {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) (x : ↥(coefficientRing B h0 hB)) : IsUnit x ∨ x = 0

@[reducible, inline]

noncomputable abbrev Complexity.RationalHitting.QuantumSeries.divisionRing {Γ : Type u_1} {K : Type u_2} {R : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Field K] [Ring R] [Algebra K R] [Nontrivial R] (B : Γ → Rˣ) (h0 : B 0 = 1) (hB : ∀ (g h : Γ), ∃ (c : K), ↑(B g) * ↑(B h) = c • ↑(B (g + h))) : DivisionRing ↥(coefficientRing B h0 hB)

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

Equations

• Complexity.RationalHitting.QuantumSeries.divisionRing B h0 hB = DivisionRing.ofIsUnitOrEqZero ⋯