Dense exact bivariate polynomials

The outer list records increasing powers of x; each inner list records increasing powers of y. Transparent list arithmetic lets the kernel normalize small polynomial certificates.

@[reducible, inline]

abbrev LeanPool.Besicovitch.DenseUnivariate : Type

A dense univariate polynomial with coefficients in increasing degree order.

Equations

• LeanPool.Besicovitch.DenseUnivariate = List ℚ

def LeanPool.Besicovitch.DenseUnivariate.add : DenseUnivariate → DenseUnivariate → DenseUnivariate

Add coefficient lists, padding the shorter list by zeros.

Equations

• LeanPool.Besicovitch.DenseUnivariate.add [] x✝ = x✝
• x✝.add [] = x✝
• LeanPool.Besicovitch.DenseUnivariate.add (a :: p) (b :: q) = (a + b) :: LeanPool.Besicovitch.DenseUnivariate.add p q

def LeanPool.Besicovitch.DenseUnivariate.scale (a : ℚ) (p : DenseUnivariate) : DenseUnivariate

Multiply every coefficient by a rational scalar.

Equations

• LeanPool.Besicovitch.DenseUnivariate.scale a p = List.map (fun (x : ℚ) => a * x) p

def LeanPool.Besicovitch.DenseUnivariate.neg (p : DenseUnivariate) : DenseUnivariate

Negate every coefficient.

Equations

• p.neg = List.map (fun (x : ℚ) => -x) p

def LeanPool.Besicovitch.DenseUnivariate.mul : DenseUnivariate → DenseUnivariate → DenseUnivariate

Exact polynomial multiplication by coefficient convolution.

Equations

• LeanPool.Besicovitch.DenseUnivariate.mul [] x✝ = []
• LeanPool.Besicovitch.DenseUnivariate.mul (a :: p) x✝ = (LeanPool.Besicovitch.DenseUnivariate.scale a x✝).add (0 :: LeanPool.Besicovitch.DenseUnivariate.mul p x✝)

noncomputable def LeanPool.Besicovitch.DenseUnivariate.eval : DenseUnivariate → ℝ → ℝ

Evaluate a dense polynomial over the reals by Horner's rule.

Equations

• LeanPool.Besicovitch.DenseUnivariate.eval [] x✝ = 0
• LeanPool.Besicovitch.DenseUnivariate.eval (a :: p) x✝ = ↑a + x✝ * LeanPool.Besicovitch.DenseUnivariate.eval p x✝

def LeanPool.Besicovitch.DenseUnivariate.coefficientL1Norm (p : DenseUnivariate) : ℚ

The sum of the absolute values of the coefficients.

Equations

• p.coefficientL1Norm = (List.map abs p).sum

def LeanPool.Besicovitch.DenseUnivariate.deriv : DenseUnivariate → DenseUnivariate

Formal differentiation, using P = a + x Q and P' = Q + x Q'.

Equations

• LeanPool.Besicovitch.DenseUnivariate.deriv [] = []
• LeanPool.Besicovitch.DenseUnivariate.deriv (head :: p) = LeanPool.Besicovitch.DenseUnivariate.add p (0 :: LeanPool.Besicovitch.DenseUnivariate.deriv p)

theorem LeanPool.Besicovitch.DenseUnivariate.coefficientL1Norm_nonneg (p : DenseUnivariate) : 0 ≤ p.coefficientL1Norm

theorem LeanPool.Besicovitch.DenseUnivariate.eval_add (p q : DenseUnivariate) (x : ℝ) : (p.add q).eval x = p.eval x + q.eval x

theorem LeanPool.Besicovitch.DenseUnivariate.eval_scale (a : ℚ) (p : DenseUnivariate) (x : ℝ) : (scale a p).eval x = ↑a * p.eval x

theorem LeanPool.Besicovitch.DenseUnivariate.eval_neg (p : DenseUnivariate) (x : ℝ) : p.neg.eval x = -p.eval x

theorem LeanPool.Besicovitch.DenseUnivariate.eval_mul (p q : DenseUnivariate) (x : ℝ) : (p.mul q).eval x = p.eval x * q.eval x

theorem LeanPool.Besicovitch.DenseUnivariate.eval_deriv_cons (a : ℚ) (p : DenseUnivariate) (x : ℝ) : (deriv (a :: p)).eval x = p.eval x + x * p.deriv.eval x

theorem LeanPool.Besicovitch.DenseUnivariate.hasDerivAt_eval (p : DenseUnivariate) (x : ℝ) : HasDerivAt p.eval (p.deriv.eval x) x

Formal differentiation computes the derivative of dense evaluation.

theorem LeanPool.Besicovitch.DenseUnivariate.abs_eval_le_coefficientL1Norm (p : DenseUnivariate) {x : ℝ} (hx : |x| ≤ 1) : |p.eval x| ≤ ↑p.coefficientL1Norm

The coefficient norm bounds evaluation on the unit interval.

@[reducible, inline]

abbrev LeanPool.Besicovitch.DenseBivariatePolynomial : Type

A dense bivariate polynomial, with the outer index giving the first-variable degree.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial = List LeanPool.Besicovitch.DenseUnivariate

def LeanPool.Besicovitch.DenseBivariatePolynomial.add : DenseBivariatePolynomial → DenseBivariatePolynomial → DenseBivariatePolynomial

Add two dense bivariate polynomials.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.add [] x✝ = x✝
• x✝.add [] = x✝
• LeanPool.Besicovitch.DenseBivariatePolynomial.add (a :: p) (b :: q) = a.add b :: LeanPool.Besicovitch.DenseBivariatePolynomial.add p q

def LeanPool.Besicovitch.DenseBivariatePolynomial.scale (a : ℚ) (p : DenseBivariatePolynomial) : DenseBivariatePolynomial

Multiply by a rational scalar.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.scale a p = List.map (LeanPool.Besicovitch.DenseUnivariate.scale a) p

def LeanPool.Besicovitch.DenseBivariatePolynomial.neg (p : DenseBivariatePolynomial) : DenseBivariatePolynomial

Negate a dense bivariate polynomial.

Equations

• p.neg = List.map LeanPool.Besicovitch.DenseUnivariate.neg p

def LeanPool.Besicovitch.DenseBivariatePolynomial.scaleRow (a : DenseUnivariate) (p : DenseBivariatePolynomial) : DenseBivariatePolynomial

Multiply each outer coefficient by a univariate polynomial.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.scaleRow a p = List.map a.mul p

def LeanPool.Besicovitch.DenseBivariatePolynomial.mul : DenseBivariatePolynomial → DenseBivariatePolynomial → DenseBivariatePolynomial

Exact bivariate polynomial multiplication.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.mul [] x✝ = []
• LeanPool.Besicovitch.DenseBivariatePolynomial.mul (a :: p) x✝ = (LeanPool.Besicovitch.DenseBivariatePolynomial.scaleRow a x✝).add ([] :: LeanPool.Besicovitch.DenseBivariatePolynomial.mul p x✝)

def LeanPool.Besicovitch.DenseBivariatePolynomial.literal (a : ℚ) : DenseBivariatePolynomial

A constant bivariate polynomial.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.literal a = [[a]]

def LeanPool.Besicovitch.DenseBivariatePolynomial.first : DenseBivariatePolynomial

The first variable.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.first = [[0], [1]]

def LeanPool.Besicovitch.DenseBivariatePolynomial.second : DenseBivariatePolynomial

The second variable.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.second = [[0, 1]]

def LeanPool.Besicovitch.DenseBivariatePolynomial.pow (p : DenseBivariatePolynomial) : ℕ → DenseBivariatePolynomial

Natural powers of a dense bivariate polynomial.

Equations

• p.pow 0 = LeanPool.Besicovitch.DenseBivariatePolynomial.literal 1
• p.pow n.succ = (p.pow n).mul p

noncomputable def LeanPool.Besicovitch.DenseBivariatePolynomial.eval : DenseBivariatePolynomial → ℝ → ℝ → ℝ

Evaluate a dense bivariate polynomial by nested Horner rules.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.eval [] x✝¹ x✝ = 0
• LeanPool.Besicovitch.DenseBivariatePolynomial.eval (a :: p) x✝¹ x✝ = a.eval x✝ + x✝¹ * LeanPool.Besicovitch.DenseBivariatePolynomial.eval p x✝¹ x✝

def LeanPool.Besicovitch.DenseBivariatePolynomial.coefficientL1Norm (p : DenseBivariatePolynomial) : ℚ

The sum of the absolute values of all coefficients.

Equations

• p.coefficientL1Norm = (List.map LeanPool.Besicovitch.DenseUnivariate.coefficientL1Norm p).sum

def LeanPool.Besicovitch.DenseBivariatePolynomial.derivFirst : DenseBivariatePolynomial → DenseBivariatePolynomial

Formal differentiation with respect to the first variable.

Equations

• LeanPool.Besicovitch.DenseBivariatePolynomial.derivFirst [] = []
• LeanPool.Besicovitch.DenseBivariatePolynomial.derivFirst (head :: p) = LeanPool.Besicovitch.DenseBivariatePolynomial.add p ([] :: LeanPool.Besicovitch.DenseBivariatePolynomial.derivFirst p)

def LeanPool.Besicovitch.DenseBivariatePolynomial.derivSecond (p : DenseBivariatePolynomial) : DenseBivariatePolynomial

Formal differentiation with respect to the second variable.

Equations

• p.derivSecond = List.map LeanPool.Besicovitch.DenseUnivariate.deriv p

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.coefficientL1Norm_nonneg (p : DenseBivariatePolynomial) : 0 ≤ p.coefficientL1Norm

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_add (p q : DenseBivariatePolynomial) (x y : ℝ) : (p.add q).eval x y = p.eval x y + q.eval x y

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_scale (a : ℚ) (p : DenseBivariatePolynomial) (x y : ℝ) : (scale a p).eval x y = ↑a * p.eval x y

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_neg (p : DenseBivariatePolynomial) (x y : ℝ) : p.neg.eval x y = -p.eval x y

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_scaleRow (a : DenseUnivariate) (p : DenseBivariatePolynomial) (x y : ℝ) : (scaleRow a p).eval x y = a.eval y * p.eval x y

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_mul (p q : DenseBivariatePolynomial) (x y : ℝ) : (p.mul q).eval x y = p.eval x y * q.eval x y

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_constant (a : ℚ) (x y : ℝ) : (literal a).eval x y = ↑a

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_first (x y : ℝ) : first.eval x y = x

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_second (x y : ℝ) : second.eval x y = y

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_pow (p : DenseBivariatePolynomial) (n : ℕ) (x y : ℝ) : (p.pow n).eval x y = p.eval x y ^ n

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.eval_derivFirst_cons (a : DenseUnivariate) (p : DenseBivariatePolynomial) (x y : ℝ) : (derivFirst (a :: p)).eval x y = p.eval x y + x * p.derivFirst.eval x y

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.hasDerivAt_eval_first (p : DenseBivariatePolynomial) (x y : ℝ) : HasDerivAt (fun (u : ℝ) => p.eval u y) (p.derivFirst.eval x y) x

derivFirst computes the derivative along a first-coordinate line.

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.hasDerivAt_eval_second (p : DenseBivariatePolynomial) (x y : ℝ) : HasDerivAt (fun (v : ℝ) => p.eval x v) (p.derivSecond.eval x y) y

derivSecond computes the derivative along a second-coordinate line.

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.abs_eval_le_coefficientL1Norm (p : DenseBivariatePolynomial) {x y : ℝ} (hx : |x| ≤ 1) (hy : |y| ≤ 1) : |p.eval x y| ≤ ↑p.coefficientL1Norm

The coefficient norm bounds evaluation on the real unit square.

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.abs_eval_sub_le_derivFirst (p : DenseBivariatePolynomial) {x₁ x₂ y : ℝ} (hx₁ : |x₁| ≤ 1) (hx₂ : |x₂| ≤ 1) (hy : |y| ≤ 1) : |p.eval x₂ y - p.eval x₁ y| ≤ ↑p.derivFirst.coefficientL1Norm * |x₂ - x₁|

The first formal derivative bounds variation along a horizontal line in the unit square.

theorem LeanPool.Besicovitch.DenseBivariatePolynomial.abs_eval_sub_le_derivSecond (p : DenseBivariatePolynomial) {x y₁ y₂ : ℝ} (hx : |x| ≤ 1) (hy₁ : |y₁| ≤ 1) (hy₂ : |y₂| ≤ 1) : |p.eval x y₂ - p.eval x y₁| ≤ ↑p.derivSecond.coefficientL1Norm * |y₂ - y₁|

The second formal derivative bounds variation along a vertical line in the unit square.