Computational Reflection for Weighted ℓ¹ Spaces

This file provides computable versions of key operations and reflection lemmas that allow native_decide to verify bounds when inputs are rational.

Strategy

For each abstract ℝ operation, we provide:

1. A computable ℚ version
2. A reflection lemma: abstract_ℝ (↑q) = ↑(computable_ℚ q)

This bridges the gap between abstract Mathlib definitions and numerical verification.

IsRat: Typeclass for ℝ values that are really ℚ

Inspired by ComputableReal's IsComputable typeclass. Source: https://github.com/Timeroot/ComputableReal.git

Tracks that an ℝ value equals a specific ℚ, enabling decidable comparisons.

class IsRat (x : ℝ) : Type

Typeclass asserting that x : ℝ equals IsRat.q x for some rational

• q : ℚ
• eq : x = ↑(q x)

instance IsRat.instRat (r : ℚ) : IsRat ↑r

Equations

• IsRat.instRat r = { q := r, eq := ⋯ }

instance IsRat.instNat (n : ℕ) : IsRat ↑n

Equations

• IsRat.instNat n = { q := ↑n, eq := ⋯ }

instance IsRat.instInt (z : ℤ) : IsRat ↑z

Equations

• IsRat.instInt z = { q := ↑z, eq := ⋯ }

instance IsRat.instOfNat0 : IsRat 0

Equations

• IsRat.instOfNat0 = { q := 0, eq := IsRat.instOfNat0._proof_1 }

instance IsRat.instOfNat1 : IsRat 1

Equations

• IsRat.instOfNat1 = { q := 1, eq := IsRat.instOfNat1._proof_1 }

instance IsRat.instNeg {x : ℝ} [hx : IsRat x] : IsRat (-x)

Equations

• IsRat.instNeg = { q := -IsRat.q x, eq := ⋯ }

instance IsRat.instInv {x : ℝ} [hx : IsRat x] : IsRat x⁻¹

Equations

• IsRat.instInv = { q := (IsRat.q x)⁻¹, eq := ⋯ }

instance IsRat.instAdd {x y : ℝ} [hx : IsRat x] [hy : IsRat y] : IsRat (x + y)

Equations

• IsRat.instAdd = { q := IsRat.q x + IsRat.q y, eq := ⋯ }

instance IsRat.instSub {x y : ℝ} [hx : IsRat x] [hy : IsRat y] : IsRat (x - y)

Equations

• IsRat.instSub = { q := IsRat.q x - IsRat.q y, eq := ⋯ }

instance IsRat.instMul {x y : ℝ} [hx : IsRat x] [hy : IsRat y] : IsRat (x * y)

Equations

• IsRat.instMul = { q := IsRat.q x * IsRat.q y, eq := ⋯ }

instance IsRat.instDiv {x y : ℝ} [hx : IsRat x] [hy : IsRat y] : IsRat (x / y)

Equations

• IsRat.instDiv = { q := IsRat.q x / IsRat.q y, eq := ⋯ }

instance IsRat.instPow {x : ℝ} [hx : IsRat x] (n : ℕ) : IsRat (x ^ n)

Equations

• IsRat.instPow n = { q := IsRat.q x ^ n, eq := ⋯ }

instance IsRat.instAbs {x : ℝ} [hx : IsRat x] : IsRat |x|

Equations

• IsRat.instAbs = { q := |IsRat.q x|, eq := ⋯ }

instance IsRat.instDecidableLE {x y : ℝ} [hx : IsRat x] [hy : IsRat y] : Decidable (x ≤ y)

Decidable ≤ for IsRat values

Equations

• IsRat.instDecidableLE = decidable_of_iff (IsRat.q x ≤ IsRat.q y) ⋯

instance IsRat.instDecidableLT {x y : ℝ} [hx : IsRat x] [hy : IsRat y] : Decidable (x < y)

Decidable < for IsRat values

Equations

• IsRat.instDecidableLT = decidable_of_iff (IsRat.q x < IsRat.q y) ⋯

instance IsRat.instDecidableEq {x y : ℝ} [hx : IsRat x] [hy : IsRat y] : Decidable (x = y)

Decidable = for IsRat values

Equations

• IsRat.instDecidableEq = decidable_of_iff (IsRat.q x = IsRat.q y) ⋯

Positive Rationals

structure PosRat : Type

Positive rationals

• val : ℚ
• pos : 0 < self.val

def instDecidableEqPosRat.decEq (x✝ x✝¹ : PosRat) : Decidable (x✝ = x✝¹)

Equations

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

instance instDecidableEqPosRat : DecidableEq PosRat

Equations

• instDecidableEqPosRat = instDecidableEqPosRat.decEq

instance PosRat.instCoeRat : Coe PosRat ℚ

Equations

• PosRat.instCoeRat = { coe := PosRat.val }

@[simp]

theorem PosRat.coe_pos (ν : PosRat) : 0 < ν.val

noncomputable def PosRat.toPosReal (ν : PosRat) : PosReal

Convert to PosReal

Equations

• ν.toPosReal = ⟨↑ν.val, ⋯⟩

@[simp]

theorem PosRat.toPosReal_val (ν : PosRat) : ↑ν.toPosReal = ↑ν.val

Computable Absolute Value

def Rat.abs (q : ℚ) : ℚ

Computable absolute value on ℚ

Equations

• q.abs = if q < 0 then -q else q

@[simp]

theorem Rat.abs_nonneg (q : ℚ) : 0 ≤ q.abs

theorem Rat.abs_eq_abs (q : ℚ) : ↑q.abs = ↑|q|

Computable Scaled Norm

def scaledNorm_rat (ν : ℚ) (n : ℕ) (x : ℚ) : ℚ

Computable scaled norm: |x| * ν^n

Equations

• scaledNorm_rat ν n x = x.abs * ν ^ n

theorem scaledNorm_eq_rat (ν : PosRat) (n : ℕ) (x : ℚ) : ↑|x| * ↑ν.toPosReal ^ n = ↑(scaledNorm_rat ν.val n x)

Reflection: scaledNorm on ℚ inputs equals ℚ computation

Computable Weighted ℓ¹ Norm (Finite)

def finl1Norm_rat {n : ℕ} (ν : ℚ) (x : Fin n → ℚ) : ℚ

Computable finite weighted ℓ¹ norm: Σᵢ |xᵢ| * νⁱ

Equations

• finl1Norm_rat ν x = ∑ i : Fin n, (x i).abs * ν ^ ↑i

theorem finl1Norm_eq_rat {n : ℕ} (ν : PosRat) (x : Fin n → ℚ) : ∑ i : Fin n, ↑|x i| * ↑ν.toPosReal ^ ↑i = ↑(finl1Norm_rat ν.val x)

Reflection for finite weighted norm

Computable Matrix Column Norm

def matrixColNorm_rat {m n : ℕ} (ν : ℚ) (A : Matrix (Fin m) (Fin n) ℚ) (j : Fin n) : ℚ

Computable column norm: (1/ν^j) * Σᵢ |Aᵢⱼ| * νⁱ

Equations

• matrixColNorm_rat ν A j = 1 / ν ^ ↑j * ∑ i : Fin m, (A i j).abs * ν ^ ↑i

def finWeightedMatrixNorm_rat {n : ℕ} (ν : ℚ) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) : ℚ

Computable matrix norm: max over columns

Equations

• finWeightedMatrixNorm_rat ν A = Finset.univ.sup' ⋯ fun (j : Fin (n + 1)) => matrixColNorm_rat ν A j

Computable Cauchy Product (Finite)

def cauchyProduct_rat (a b : ℕ → ℚ) (n : ℕ) : ℚ

Computable Cauchy product at index n

Equations

• cauchyProduct_rat a b n = ∑ kl ∈ Finset.antidiagonal n, a kl.1 * b kl.2

def cauchyProductFin_rat {n : ℕ} (a b : Fin (n + 1) → ℚ) (k : ℕ) : ℚ

Cauchy product for finite sequences (zero-padded)

Equations

• cauchyProductFin_rat a b k = ∑ ij ∈ Finset.antidiagonal k, (if hij : ij.1 ≤ n then a ⟨ij.1, ⋯⟩ else 0) * if hij : ij.2 ≤ n then b ⟨ij.2, ⋯⟩ else 0

Example: Reflection for Y₀ Finite Part

The finite part of Y₀ is: Σᵢ |Σⱼ Aᵢⱼ * Fⱼ| * νⁱ

This is computable when A, F are rational matrices/vectors.

def matVecMul_rat {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (v : Fin n → ℚ) : Fin m → ℚ

Computable matrix-vector product

Equations

• matVecMul_rat A v i = ∑ j : Fin n, A i j * v j

def Y₀_fin_rat {m n : ℕ} (ν : ℚ) (A : Matrix (Fin m) (Fin n) ℚ) (v : Fin n → ℚ) : ℚ

Computable Y₀ finite part: Σᵢ |[A·v]ᵢ| * νⁱ

Equations

• Y₀_fin_rat ν A v = ∑ i : Fin m, (matVecMul_rat A v i).abs * ν ^ ↑i

Decidability for ℚ comparisons

instance instDecidableRelRatLt_radiiPolynomial : DecidableRel fun (x1 x2 : ℚ) => x1 < x2

Equations

• instDecidableRelRatLt_radiiPolynomial = inferInstance

instance instDecidableRelRatLe_radiiPolynomial : DecidableRel fun (x1 x2 : ℚ) => x1 ≤ x2

Equations

• instDecidableRelRatLe_radiiPolynomial = inferInstance

Computable Max (Finset.sup')

def finsetMax_rat {α : Type u_1} (s : Finset α) (hs : s.Nonempty) (f : α → ℚ) : ℚ

Computable max over a Finset

Equations

• finsetMax_rat s hs f = s.sup' hs f

theorem finsetSup'_eq_rat {α : Type u_1} (s : Finset α) (hs : s.Nonempty) (f : α → ℚ) : ↑(s.sup' hs f) = s.sup' hs fun (a : α) => ↑(f a)

Reflection for Finset.sup' when f maps to ℚ

theorem finWeightedMatrixNorm_rat_eq_sup' {n : ℕ} (ν : PosRat) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) : ↑(finWeightedMatrixNorm_rat ν.val A) = Finset.univ.sup' ⋯ fun (j : Fin (n + 1)) => ↑(matrixColNorm_rat ν.val A j)

Expansion for finWeightedMatrixNorm_rat

Finite Sequence as Zero-Padded Infinite Sequence

def finToSeq_rat {n : ℕ} (x : Fin (n + 1) → ℚ) : ℕ → ℚ

Zero-pad a finite sequence

Equations

• finToSeq_rat x k = if h : k ≤ n then x ⟨k, ⋯⟩ else 0

@[simp]

theorem finToSeq_rat_lt {n : ℕ} (x : Fin (n + 1) → ℚ) (k : ℕ) (hk : k ≤ n) : finToSeq_rat x k = x ⟨k, ⋯⟩

@[simp]

theorem finToSeq_rat_ge {n : ℕ} (x : Fin (n + 1) → ℚ) (k : ℕ) (hk : n < k) : finToSeq_rat x k = 0

Computable Cauchy Product with Reflection

def cauchyProduct_fin_rat {n : ℕ} (a b : Fin (n + 1) → ℚ) (k : ℕ) : ℚ

Cauchy product at index k for zero-padded sequences

Equations

• cauchyProduct_fin_rat a b k = cauchyProduct_rat (finToSeq_rat a) (finToSeq_rat b) k

theorem cauchyProduct_fin_rat_eq {n : ℕ} (a b : Fin (n + 1) → ℚ) (k : ℕ) : cauchyProduct_fin_rat a b k = ∑ ij ∈ Finset.antidiagonal k, finToSeq_rat a ij.1 * finToSeq_rat b ij.2

Component-wise Cauchy product definition

theorem cauchyProduct_cast (a b : ℕ → ℚ) (k : ℕ) : ↑(cauchyProduct_rat a b k) = ((fun (i : ℕ) => ↑(a i)) ⋆ fun (i : ℕ) => ↑(b i)) k

Reflection: CauchyProduct on ℚ sequences casts correctly

F(ā) = ā ⋆ ā - c computation

def F_component_rat {n : ℕ} (a : Fin (n + 1) → ℚ) (c : ℕ → ℚ) (k : ℕ) : ℚ

Computable F₀ = ā₀² - λ₀

Equations

• F_component_rat a c k = cauchyProduct_fin_rat a a k - c k

def paramSeq_rat (lam0 : ℚ) : ℕ → ℚ

The paramSeq c = (λ₀, 1, 0, 0, ...)

Equations

• paramSeq_rat lam0 0 = lam0
• paramSeq_rat lam0 1 = 1
• paramSeq_rat lam0 x✝ = 0

@[simp]

theorem paramSeq_rat_zero (lam0 : ℚ) : paramSeq_rat lam0 0 = lam0

@[simp]

theorem paramSeq_rat_one (lam0 : ℚ) : paramSeq_rat lam0 1 = 1

@[simp]

theorem paramSeq_rat_ge_two (lam0 : ℚ) (k : ℕ) (hk : 2 ≤ k) : paramSeq_rat lam0 k = 0

Full Y₀ Computation

def Y₀_finite_rat {n : ℕ} (ν : ℚ) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) (a : Fin (n + 1) → ℚ) (lam0 : ℚ) : ℚ

Y₀ finite part: Σᵢ₌₀ᴺ |[A·F(ā)]ᵢ| * νⁱ

Equations

• Y₀_finite_rat ν A a lam0 = ∑ i : Fin (n + 1), (∑ j : Fin (n + 1), A i j * F_component_rat a (paramSeq_rat lam0) ↑j).abs * ν ^ ↑i

def Y₀_tail_rat {n : ℕ} (ν : ℚ) (a : Fin (n + 1) → ℚ) : ℚ

Y₀ tail part: (1/(2|ā₀|)) * Σₙ₌ₙ₊₁²ᴺ (Σ convolution terms) * νⁿ

Equations

• Y₀_tail_rat ν a = 1 / (2 * (a 0).abs) * ∑ k ∈ Finset.Icc (n + 1) (2 * n), (∑ ij ∈ Finset.Icc (k - n) n, (finToSeq_rat a ij).abs * (finToSeq_rat a (k - ij)).abs) * ν ^ k

def Y₀_rat {n : ℕ} (ν : ℚ) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) (a : Fin (n + 1) → ℚ) (lam0 : ℚ) : ℚ

Full Y₀ bound

Equations

• Y₀_rat ν A a lam0 = Y₀_finite_rat ν A a lam0 + Y₀_tail_rat ν a

Z₁ Computation (simplest)

def Z₁_rat {n : ℕ} (ν : ℚ) (a : Fin (n + 1) → ℚ) : ℚ

Z₁ = (1/|ā₀|) * Σₙ₌₁ᴺ |āₙ| * νⁿ

Equations

• Z₁_rat ν a = 1 / (a 0).abs * ∑ k ∈ Finset.Icc 1 n, (finToSeq_rat a k).abs * ν ^ k

Z₀ Computation

def DF_fin_rat {n : ℕ} (a : Fin (n + 1) → ℚ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ

DF(ā) finite block: 2 * lower triangular Toeplitz from ā. Takes raw ℚ vector. Used by Z₀_rat, Z₂_rat.

Equations

• DF_fin_rat a i j = if j ≤ i then 2 * a ⟨↑i - ↑j, ⋯⟩ else 0

def IADF_rat {n : ℕ} (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) (a : Fin (n + 1) → ℚ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ

I - A·DF(ā)

Equations

• IADF_rat A a = 1 - A * DF_fin_rat a

def Z₀_rat {n : ℕ} (ν : ℚ) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) (a : Fin (n + 1) → ℚ) : ℚ

Z₀ = ‖I - A·DF(ā)‖_{1,ν}

Equations

• Z₀_rat ν A a = finWeightedMatrixNorm_rat ν (IADF_rat A a)

Z₂ Computation

def Z₂_rat {n : ℕ} (ν : ℚ) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) (a : Fin (n + 1) → ℚ) : ℚ

Z₂ = 2 * max(‖A‖_{1,ν}, 1/(2|ā₀|))

Equations

• Z₂_rat ν A a = 2 * max (finWeightedMatrixNorm_rat ν A) (1 / (2 * (a 0).abs))

Full Radii Polynomial

def radiiPoly_rat (Y₀ Z₀ Z₁ Z₂ r : ℚ) : ℚ

p(r) = Z₂·r² - (1 - Z₀ - Z₁)·r + Y₀

Equations

• radiiPoly_rat Y₀ Z₀ Z₁ Z₂ r = Z₂ * r ^ 2 - (1 - Z₀ - Z₁) * r + Y₀

def computeRadiiPoly_rat {n : ℕ} (ν : ℚ) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) (a : Fin (n + 1) → ℚ) (lam0 r : ℚ) : ℚ

All-in-one radii polynomial computation

Equations

• computeRadiiPoly_rat ν A a lam0 r = radiiPoly_rat (Y₀_rat ν A a lam0) (Z₀_rat ν A a) (Z₁_rat ν a) (Z₂_rat ν A a) r

Reflection Lemmas: Abstract ℝ = Computable ℚ

These lemmas bridge abstract Mathlib definitions to computable ℚ versions, enabling native_decide verification of bounds.

def Matrix.castRat {m k : ℕ} (A : Matrix (Fin m) (Fin k) ℚ) : Matrix (Fin m) (Fin k) ℝ

Cast ℚ matrix to ℝ matrix

Equations

• A.castRat i j = ↑(A i j)

def Fin.castRat {k : ℕ} (v : Fin k → ℚ) : Fin k → ℝ

Cast ℚ vector to ℝ vector

Equations

• Fin.castRat v i = ↑(v i)

theorem matrixColNorm_eq_rat {n : ℕ} (ν : PosRat) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) (j : Fin (n + 1)) : l1Weighted.matrixColNorm ν.toPosReal A.castRat j = ↑(matrixColNorm_rat ν.val A j)

Reflection for matrixColNorm

theorem finWeightedMatrixNorm_eq_rat {n : ℕ} (ν : PosRat) (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℚ) : l1Weighted.finWeightedMatrixNorm ν.toPosReal A.castRat = ↑(finWeightedMatrixNorm_rat ν.val A)

Reflection for finWeightedMatrixNorm

theorem Z₁_bound_eq_rat {n : ℕ} (ν : PosRat) (a : Fin (n + 1) → ℚ) : 1 / |Fin.castRat a 0| * ∑ k ∈ Finset.Icc 1 n, ↑|finToSeq_rat a k| * ↑ν.toPosReal ^ k = ↑(Z₁_rat ν.val a)

Reflection for Z₁_bound: (1/|ā₀|) * Σₙ₌₁ᴺ |āₙ| * νⁿ

theorem finToSeq_rat_cast {n : ℕ} (a : Fin (n + 1) → ℚ) (k : ℕ) : ↑(finToSeq_rat a k) = if h : k ≤ n then ↑(a ⟨k, ⋯⟩) else 0

Helper: finToSeq_rat casts correctly

theorem cauchyProduct_fin_eq_rat {n : ℕ} (a b : Fin (n + 1) → ℚ) (k : ℕ) : ((fun (i : ℕ) => ↑(finToSeq_rat a i)) ⋆ fun (i : ℕ) => ↑(finToSeq_rat b i)) k = ↑(cauchyProduct_fin_rat a b k)

Reflection for Cauchy product of finite ℚ sequences

ApproxSolution over ℚ

A ℚ version of ApproxSolution that enables computational reflection.

structure ApproxSolution_rat (N : ℕ) : Type

Approximate solution with ℚ coefficients

• aBar_fin : Fin (N + 1) → ℚ
• aBar_zero_ne : self.aBar_fin 0 ≠ 0

noncomputable def ApproxSolution_rat.toReal {N : ℕ} (a : ApproxSolution_rat N) : Example_7_7.ApproxSolution N

Convert to real ApproxSolution

Equations

• a.toReal = { aBar_fin := fun (i : Fin (N + 1)) => ↑(a.aBar_fin i), aBar_zero_ne := ⋯ }

def ApproxSolution_rat.toSeq_rat {N : ℕ} (a : ApproxSolution_rat N) : ℕ → ℚ

The ℚ sequence (zero-padded)

Equations

• a.toSeq_rat = finToSeq_rat a.aBar_fin

@[simp]

theorem ApproxSolution_rat.toReal_aBar_fin {N : ℕ} (a : ApproxSolution_rat N) (i : Fin (N + 1)) : a.toReal.aBar_fin i = ↑(a.aBar_fin i)

theorem ApproxSolution_rat.toReal_toSeq {N : ℕ} (a : ApproxSolution_rat N) (k : ℕ) : a.toReal.toSeq k = ↑(a.toSeq_rat k)

toSeq of toReal = cast of toSeq_rat

theorem ApproxSolution_rat.toReal_toL1_toSeq {N : ℕ} (ν : PosReal) (a : ApproxSolution_rat N) (k : ℕ) : lpWeighted.toSeq a.toReal.toL1 k = ↑(a.toSeq_rat k)

lpWeighted.toSeq of toL1 = cast of toSeq_rat

Matrix over ℚ

def Matrix.ofRat {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) : Matrix (Fin m) (Fin n) ℝ

ℚ matrix cast to ℝ

Equations

• A.ofRat i j = ↑(A i j)

@[simp]

theorem Matrix.ofRat_apply {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℚ) (i : Fin m) (j : Fin n) : A.ofRat i j = ↑(A i j)

Full Reflection Lemmas for Bounds

def DF_fin_of_rat {N : ℕ} (a : ApproxSolution_rat N) : Matrix (Fin (N + 1)) (Fin (N + 1)) ℚ

DF(ā) finite block from ApproxSolution_rat. Same computation as DF_fin_rat, but takes ApproxSolution_rat instead of raw ℚ vector. Used for reflection lemmas connecting abstract Example_7_7.DF_fin to computable version.

Equations

• DF_fin_of_rat a i j = if ↑j ≤ ↑i then 2 * a.aBar_fin ⟨↑i - ↑j, ⋯⟩ else 0

theorem DF_fin_eq_rat {N : ℕ} (a : ApproxSolution_rat N) : Example_7_7.DF_fin a.toReal = (DF_fin_of_rat a).ofRat

DF_fin reflection

theorem Z₀_bound_eq_rat' {N : ℕ} (ν : PosRat) (a : ApproxSolution_rat N) (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℚ) : Example_7_7.Z₀_bound a.toReal A.ofRat = ↑(Z₀_rat ν.val A a.aBar_fin)

Z₀_bound on ℚ inputs = Z₀_rat

theorem Z₂_bound_eq_rat' {N : ℕ} (ν : PosRat) (a : ApproxSolution_rat N) (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℚ) : Example_7_7.Z₂_bound a.toReal A.ofRat = ↑(Z₂_rat ν.val A a.aBar_fin)

theorem Z₁_bound_eq_rat' {N : ℕ} (ν : PosRat) (a : ApproxSolution_rat N) : Example_7_7.Z₁_bound a.toReal = ↑(Z₁_rat ν.val a.aBar_fin)

Z₁_bound on ℚ inputs = Z₁_rat

def F_fin_rat {N : ℕ} (lam0 : ℚ) (a : Fin (N + 1) → ℚ) : Fin (N + 1) → ℚ

F_fin on ℚ inputs: the finite components of F(ā) = ā⋆ā - c

Equations

• F_fin_rat lam0 a n = cauchyProduct_fin_rat a a ↑n - paramSeq_rat lam0 ↑n

theorem F_fin_eq_rat {N : ℕ} (ν : PosRat) (lam0 : ℚ) (a : ApproxSolution_rat N) (n : Fin (N + 1)) : Example_7_7.F_fin (↑lam0) a.toReal n = ↑(F_fin_rat lam0 a.aBar_fin n)

F_fin reflection: abstract F_fin equals F_fin_rat on ℚ inputs

theorem Y₀_bound_eq_rat' {N : ℕ} (ν : PosRat) (lam0 : ℚ) (a : ApproxSolution_rat N) (A : Matrix (Fin (N + 1)) (Fin (N + 1)) ℚ) : Example_7_7.Y₀_bound (↑lam0) a.toReal A.ofRat = ↑(Y₀_rat ν.val A a.aBar_fin lam0)

Y₀_bound on ℚ inputs = Y₀_rat