Exact logarithms of positive rationals

Eliminating declaration equations combines the logarithms of declared factors with rational coefficients, producing values such as (log 2)/2 - log 3. This module represents such values exactly and decides their equality without evaluating a logarithm or a root.

An Expr is a finite list of pairs (c, q) of a rational coefficient and a positive rational, denoting ∑ c * log q (eval). radical clears denominators, returning a positive rational q and a positive natural N with log q = N * eval xs (radical_log). So an expression denotes zero exactly when q = 1 (isZero_iff), a test carried out in ℚ.

LogFactor is the quotient of Expr by equality of denotation. It is a ℚ-module with decidable equality, so RationalSolver can eliminate over it. Its real interpretation interpret is an injective ℚ-linear map (interpret_injective), which lets DeclSolver.solve_isSome_iff transfer solvability to real valuations. The same radical gives the radicand and root degree of DeclSolver.ExactFactor (radical_exp). No real arithmetic is executed.

@[reducible, inline]

abbrev LambdaS.LogFactor.PositiveRat : Type

Positive rationals: the declared factors whose logarithms an Expr combines.

Equations

• LambdaS.LogFactor.PositiveRat = { q : ℚ // 0 < q }

@[reducible, inline]

abbrev LambdaS.LogFactor.Expr : Type

A formal rational combination of logarithms: [(c₁, q₁), …, (cₙ, qₙ)] denotes c₁ log q₁ + … + cₙ log qₙ.

Equations

• LambdaS.LogFactor.Expr = List (ℚ × LambdaS.LogFactor.PositiveRat)

noncomputable def LambdaS.LogFactor.eval : Expr → ℝ

The real number an expression denotes. Noncomputable; used only in statements and proofs.

Equations

• LambdaS.LogFactor.eval [] = 0
• LambdaS.LogFactor.eval ((c, q) :: xs) = ↑c * Real.log ↑↑q + LambdaS.LogFactor.eval xs

theorem LambdaS.LogFactor.eval_ofFn {n : ℕ} (c : Fin n → ℚ) (q : Fin n → PositiveRat) : eval (List.ofFn fun (i : Fin n) => (c i, q i)) = ∑ i : Fin n, ↑(c i) * Real.log ↑↑(q i)

Evaluate an explicitly indexed finite family of logarithm coefficients.

def LambdaS.LogFactor.radical : Expr → ℚ × ℕ

Return (q, N), with q a positive rational and N a positive natural, such that the expression denotes log q / N (radical_log, radical_pos). The integer powers clear denominators without factoring any integer.

Equations

• LambdaS.LogFactor.radical [] = (1, 1)
• LambdaS.LogFactor.radical ((c, q) :: xs) = (↑q ^ (c.num * ↑(LambdaS.LogFactor.radical xs).2) * (LambdaS.LogFactor.radical xs).1 ^ c.den, c.den * (LambdaS.LogFactor.radical xs).2)

theorem LambdaS.LogFactor.radical_pos (xs : Expr) : 0 < (radical xs).1 ∧ 0 < (radical xs).2

theorem LambdaS.LogFactor.radical_log (xs : Expr) : Real.log ↑(radical xs).1 = ↑(radical xs).2 * eval xs

The defining property of radical: for (q, N) = radical xs, log q = N * eval xs.

theorem LambdaS.LogFactor.radical_exp (xs : Expr) : Real.exp (eval xs) ^ (radical xs).2 = ↑(radical xs).1

The returned rational and positive degree specify the positive real factor without evaluating a logarithm or a root in the executable representation.

def LambdaS.LogFactor.isZero (xs : Expr) : Bool

The executable zero test; its decision takes place entirely in ℚ.

Equations

• LambdaS.LogFactor.isZero xs = ((LambdaS.LogFactor.radical xs).1 == 1)

theorem LambdaS.LogFactor.isZero_iff (xs : Expr) : isZero xs = true ↔ eval xs = 0

Exact zero test. An expression denotes zero exactly when its cleared radicand is 1.

theorem LambdaS.LogFactor.eval_append (xs ys : Expr) : eval (xs ++ ys) = eval xs + eval ys

def LambdaS.LogFactor.scaleExpr (c : ℚ) (xs : Expr) : Expr

Equations

• LambdaS.LogFactor.scaleExpr c xs = List.map (fun (a : ℚ × LambdaS.LogFactor.PositiveRat) => (c * a.1, a.2)) xs

theorem LambdaS.LogFactor.eval_scaleExpr (c : ℚ) (xs : Expr) : eval (scaleExpr c xs) = ↑c * eval xs

@[instance_reducible]

instance LambdaS.LogFactor.exprSetoid : Setoid Expr

Two expressions are equivalent when they denote the same real number; exprRelDecidable decides this with isZero on their difference.

Equations

• LambdaS.LogFactor.exprSetoid = { r := fun (xs ys : LambdaS.LogFactor.Expr) => LambdaS.LogFactor.eval xs = LambdaS.LogFactor.eval ys, iseqv := LambdaS.LogFactor.exprSetoid._proof_1 }

@[instance_reducible]

instance LambdaS.LogFactor.exprRelDecidable : DecidableRel ⇑exprSetoid

Equations

• LambdaS.LogFactor.exprRelDecidable xs ys = decidable_of_iff (LambdaS.LogFactor.isZero (xs ++ LambdaS.LogFactor.scaleExpr (-1) ys) = true) ⋯

def LambdaS.LogFactor : Type

Exact logarithms of positive rational numbers, closed under rational linear combinations.

Equations

• LambdaS.LogFactor = Quotient LambdaS.LogFactor.exprSetoid

@[instance_reducible]

instance LambdaS.LogFactor.instDecidableEq : DecidableEq LogFactor

Equations

• LambdaS.LogFactor.instDecidableEq = Quotient.decidableEq

def LambdaS.LogFactor.ofExpr (xs : Expr) : LogFactor

Equations

• LambdaS.LogFactor.ofExpr xs = ⟦xs⟧

noncomputable def LambdaS.LogFactor.value : LogFactor → ℝ

Equations

• LambdaS.LogFactor.value = Quotient.lift LambdaS.LogFactor.eval ⋯

theorem LambdaS.LogFactor.value_injective : Function.Injective value

@[instance_reducible]

instance LambdaS.LogFactor.instZero : Zero LogFactor

Equations

• LambdaS.LogFactor.instZero = { zero := LambdaS.LogFactor.ofExpr [] }

@[instance_reducible]

instance LambdaS.LogFactor.instAdd : Add LogFactor

Equations

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

@[instance_reducible]

instance LambdaS.LogFactor.instSMulRat : SMul ℚ LogFactor

Equations

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

@[instance_reducible]

instance LambdaS.LogFactor.instNeg : Neg LogFactor

Equations

• LambdaS.LogFactor.instNeg = { neg := fun (x : LambdaS.LogFactor) => -1 • x }

@[instance_reducible]

instance LambdaS.LogFactor.instSub : Sub LogFactor

Equations

• LambdaS.LogFactor.instSub = { sub := fun (x y : LambdaS.LogFactor) => x + -y }

@[instance_reducible]

instance LambdaS.LogFactor.instSMulNat : SMul ℕ LogFactor

Equations

• LambdaS.LogFactor.instSMulNat = { smul := fun (n : ℕ) (x : LambdaS.LogFactor) => ↑n • x }

@[instance_reducible]

instance LambdaS.LogFactor.instSMulInt : SMul ℤ LogFactor

Equations

• LambdaS.LogFactor.instSMulInt = { smul := fun (n : ℤ) (x : LambdaS.LogFactor) => ↑n • x }

@[simp]

theorem LambdaS.LogFactor.value_zero : value 0 = 0

@[simp]

theorem LambdaS.LogFactor.value_add (x y : LogFactor) : (x + y).value = x.value + y.value

@[simp]

theorem LambdaS.LogFactor.value_smul (c : ℚ) (x : LogFactor) : (c • x).value = c • x.value

@[simp]

theorem LambdaS.LogFactor.value_neg (x : LogFactor) : (-x).value = -x.value

@[simp]

theorem LambdaS.LogFactor.value_sub (x y : LogFactor) : (x - y).value = x.value - y.value

@[simp]

theorem LambdaS.LogFactor.value_nsmul (n : ℕ) (x : LogFactor) : (n • x).value = n • x.value

@[simp]

theorem LambdaS.LogFactor.value_zsmul (n : ℤ) (x : LogFactor) : (n • x).value = n • x.value

@[instance_reducible]

instance LambdaS.LogFactor.instAddCommGroup : AddCommGroup LogFactor

Equations

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

@[instance_reducible]

instance LambdaS.LogFactor.instModuleRat : Module ℚ LogFactor

Equations

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

noncomputable def LambdaS.LogFactor.interpret : LogFactor →ₗ[ℚ] ℝ

The real interpretation is noncomputable; all operations on its domain are executable.

Equations

• LambdaS.LogFactor.interpret = { toFun := LambdaS.LogFactor.value, map_add' := LambdaS.LogFactor.value_add, map_smul' := LambdaS.LogFactor.value_smul }

theorem LambdaS.LogFactor.interpret_injective : Function.Injective ⇑interpret

Distinct LogFactors denote distinct reals, so exact equality agrees with real equality.

theorem LambdaS.LogFactor.eq_iff_interpret (x y : LogFactor) : x = y ↔ interpret x = interpret y

@[simp]

theorem LambdaS.LogFactor.interpret_ofExpr (xs : Expr) : interpret (ofExpr xs) = eval xs

def LambdaS.LogFactor.ofRat (q : ℚ) (hq : 0 < q) : LogFactor

Construct the exact logarithm of a declared positive rational factor.

Equations

• LambdaS.LogFactor.ofRat q hq = LambdaS.LogFactor.ofExpr [(1, ⟨q, hq⟩)]

@[simp]

theorem LambdaS.LogFactor.interpret_ofRat (q : ℚ) (hq : 0 < q) : interpret (ofRat q hq) = Real.log ↑q