HexRootsMathlib.Basic

source

@[reducible, inline]

noncomputable abbrev HexRootsMathlib.toPolyℂ (p : Hex.ZPoly) :

Polynomial ℂ

The complex cast of an executable integer polynomial.

Equations

HexRootsMathlib.toPolyℂ p = Polynomial.map (Int.castRingHom ℂ) (HexPolyZMathlib.toPolynomial p)

Instances For

source

@[simp]

theorem HexRootsMathlib.coeff_toPolyℂ (p : Hex.ZPoly) (n : ℕ) :

(toPolyℂ p).coeff n = ↑(Hex.DensePoly.coeff p n)

Coefficients of the complex cast are the complex casts of the executable coefficients.

source

theorem HexRootsMathlib.natDegree_toPolyℂ (p : Hex.ZPoly) :

(toPolyℂ p).natDegree = Hex.DensePoly.natDegree p

The complex cast preserves the executable natural degree.

source

theorem HexRootsMathlib.le_two_pow_ceilLog2 (m : ℕ) :

m ≤ 2 ^ Hex.ceilLog2 m

The executable natural ceiling logarithm is an upper base-two logarithm.

source

theorem HexRootsMathlib.two_pow_ceilLog2_lt_two_mul (m : ℕ) (hm : 0 < m) :

2 ^ Hex.ceilLog2 m < 2 * m

A positive natural lies above half the power of two selected by the executable ceiling logarithm.

source

def HexRootsMathlib.Dyadic.toReal (x : Dyadic) :

ℝ

The real value of an exact dyadic number, through its rational value.

Equations

HexRootsMathlib.Dyadic.toReal x = ↑x.toRat

Instances For

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_zero :

toReal 0 = 0

The real value of zero is zero.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_ofInt (n : ℤ) :

toReal (Dyadic.ofInt n) = ↑n

The real value of an integer dyadic is the corresponding integer.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_one :

toReal 1 = 1

The real value of one is one.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_two :

toReal 2 = 2

The real value of two is two.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_add (x y : Dyadic) :

toReal (x + y) = toReal x + toReal y

The real-value map preserves addition.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_neg (x : Dyadic) :

toReal (-x) = -toReal x

The real-value map preserves negation.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_sub (x y : Dyadic) :

toReal (x - y) = toReal x - toReal y

The real-value map preserves subtraction.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_mul (x y : Dyadic) :

toReal (x * y) = toReal x * toReal y

The real-value map preserves multiplication.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_pow (x : Dyadic) (n : ℕ) :

toReal (x ^ n) = toReal x ^ n

The real-value map preserves natural powers.

source

theorem HexRootsMathlib.Dyadic.toRat_shiftRight (x : Dyadic) (i : ℤ) :

(x >>> i).toRat = x.toRat * 2 ^ (-i)

toRat turns a right shift into multiplication by a negative power of two.

source

theorem HexRootsMathlib.Dyadic.toRat_shiftLeft (x : Dyadic) (i : ℤ) :

(x <<< i).toRat = x.toRat * 2 ^ i

toRat turns a left shift into multiplication by a power of two.

source

theorem HexRootsMathlib.Dyadic.toReal_shiftLeft (x : Dyadic) (i : ℤ) :

toReal (x <<< i) = toReal x * 2 ^ i

The real value of a left shift is multiplication by a power of two.

source

theorem HexRootsMathlib.Dyadic.toReal_shiftRight (x : Dyadic) (i : ℤ) :

toReal (x >>> i) = toReal x * 2 ^ (-i)

The real value of a right shift is multiplication by a negative power of two.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_le_toReal_iff {x y : Dyadic} :

toReal x ≤ toReal y ↔ x ≤ y

Real-value comparison reflects and preserves dyadic non-strict order.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_lt_toReal_iff {x y : Dyadic} :

toReal x < toReal y ↔ x < y

Real-value comparison reflects and preserves dyadic strict order.

source

theorem HexRootsMathlib.Dyadic.toReal_injective :

Function.Injective toReal

The real-value map is injective.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_abs (x : Dyadic) :

toReal (Hex.Dyadic.abs x) = |toReal x|

The real-value map preserves the executable dyadic absolute value.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_max (x y : Dyadic) :

toReal (Hex.Dyadic.max x y) = max (toReal x) (toReal y)

The real-value map preserves the executable dyadic maximum.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_min (x y : Dyadic) :

toReal (Hex.Dyadic.min x y) = min (toReal x) (toReal y)

The real-value map preserves the executable dyadic minimum.

source

theorem HexRootsMathlib.Dyadic.toReal_le_two_pow_ceilLog2 (x : Dyadic) (hx : 0 < toReal x) :

toReal x ≤ 2 ^ Hex.Dyadic.ceilLog2 x

The executable dyadic ceiling logarithm bounds every positive dyadic by the corresponding power of two.

source

theorem HexRootsMathlib.Dyadic.two_pow_ceilLog2_lt_two_mul_toReal (x : Dyadic) (hx : 0 < toReal x) :

2 ^ Hex.Dyadic.ceilLog2 x < 2 * toReal x

The power selected by the executable dyadic ceiling logarithm is less than twice the positive input.

source

@[simp]

theorem HexRootsMathlib.Dyadic.toReal_ofIntWithPrec (n prec : ℤ) :

toReal (Dyadic.ofIntWithPrec n prec) = ↑n * 2 ^ (-prec)

The real value of n * 2 ^ (-prec) represented as a dyadic.

source

def HexRootsMathlib.GaussDyadic.toComplex (z : Hex.GaussDyadic) :

ℂ

The complex value of an exact Gaussian dyadic.

Equations

HexRootsMathlib.GaussDyadic.toComplex z = { re := HexRootsMathlib.Dyadic.toReal z.1, im := HexRootsMathlib.Dyadic.toReal z.2 }

Instances For

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_re (z : Hex.GaussDyadic) :

(toComplex z).re = Dyadic.toReal z.1

The real part of the complex value is the real value of the first coordinate.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_im (z : Hex.GaussDyadic) :

(toComplex z).im = Dyadic.toReal z.2

The imaginary part of the complex value is the real value of the second coordinate.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_ofInt (n : ℤ) :

toComplex (Hex.GaussDyadic.ofInt n) = ↑n

Casting an integer Gaussian dyadic gives the corresponding complex integer.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_add (z w : Hex.GaussDyadic) :

toComplex (z.add w) = toComplex z + toComplex w

The complex-value map preserves Gaussian-dyadic addition.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_sub (z w : Hex.GaussDyadic) :

toComplex (z.sub w) = toComplex z - toComplex w

The complex-value map preserves Gaussian-dyadic subtraction.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_conj (z : Hex.GaussDyadic) :

toComplex z.conj = star (toComplex z)

The complex-value map preserves Gaussian-dyadic conjugation.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_mul (z w : Hex.GaussDyadic) :

toComplex (z.mul w) = toComplex z * toComplex w

The complex-value map preserves Gaussian-dyadic multiplication.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_nsmul (n : ℕ) (z : Hex.GaussDyadic) :

toComplex (Hex.GaussDyadic.nsmul n z) = ↑n * toComplex z

Casting a natural multiple of a Gaussian dyadic gives scalar multiplication in ℂ.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toComplex_pow (z : Hex.GaussDyadic) (n : ℕ) :

toComplex (z.pow n) = toComplex z ^ n

Casting an exact Gaussian-dyadic power gives the corresponding complex power.

source

@[simp]

theorem HexRootsMathlib.GaussDyadic.toReal_normSq (z : Hex.GaussDyadic) :

Dyadic.toReal z.normSq = Complex.normSq (toComplex z)

The real value of the exact squared modulus is the complex squared modulus.

source

theorem HexRootsMathlib.GaussDyadic.toComplex_injective :

Function.Injective toComplex

The complex-value map is injective.