Module

Taylor.lean

Nyll.AlgebraicCurves.Places.Taylor

16 declarations indexed from sourceView source ↗

Module documentation

Taylor

Imports1

Nyll.AlgebraicCurves.Places.Evaluation

Imported by23

def

taylorRem

L29 ↗

AlgebraicCurve.Place.taylorRem

Documentation

The iterated Taylor remainder obtained by subtracting the value at the place and dividing by t.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place

Lean source · full declaration

def taylorRem (v : Place K F) (t f : F) : ℕ → F
  | 0 => f
  | r + 1 => (taylorRem v t f r - algebraMap K F (v.evalAt (taylorRem v t f r))) * t⁻¹

def

taylorCoeff

L34 ↗

AlgebraicCurve.Place.taylorCoeff

Documentation

The coefficient of order r, obtained by evaluating the iterated Taylor remainder.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place

Lean source · statement

def taylorCoeff (v : Place K F) (t : F) (r : ℕ) (f : F) : K

theorem

taylorRem_zero

L40 ↗

AlgebraicCurve.Place.taylorRem_zero

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F) (t f : F)

Lean source · statement

theorem taylorRem_zero : taylorRem v t f 0 = f

theorem

taylorRem_succ

L42 ↗

AlgebraicCurve.Place.taylorRem_succ

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F) (t f : F)

Lean source · statement

theorem taylorRem_succ (r : ℕ) :
    taylorRem v t f (r + 1)
      = (taylorRem v t f r - algebraMap K F (v.evalAt (taylorRem v t f r))) * t⁻¹

theorem

taylorCoeff_zero

L46 ↗

AlgebraicCurve.Place.taylorCoeff_zero

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F) (t f : F)

Lean source · statement

theorem taylorCoeff_zero : taylorCoeff v t 0 f = v.evalAt f

theorem

taylorCoeff_eq

L48 ↗

AlgebraicCurve.Place.taylorCoeff_eq

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F) (t f : F)

Lean source · statement

theorem taylorCoeff_eq (r : ℕ) : taylorCoeff v t r f = v.evalAt (taylorRem v t f r)

theorem

taylorRem_succ'

L50 ↗

AlgebraicCurve.Place.taylorRem_succ'

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F) (t f : F)

Lean source · statement

theorem taylorRem_succ' (r : ℕ) :
    taylorRem v t f (r + 1)
      = (taylorRem v t f r - algebraMap K F (taylorCoeff v t r f)) * t⁻¹

theorem

taylorRem_eq_add_mul_succ

L54 ↗

AlgebraicCurve.Place.taylorRem_eq_add_mul_succ

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F) (t f : F)

Lean source · statement

theorem taylorRem_eq_add_mul_succ {t : F} (ht : t ≠ 0) (f : F) (r : ℕ) :
    taylorRem v t f r
      = algebraMap K F (taylorCoeff v t r f) + t * taylorRem v t f (r + 1)

theorem

eq_sum_taylorCoeff_mul_pow_add_pow_mul_taylorRem

L60 ↗

AlgebraicCurve.Place.eq_sum_taylorCoeff_mul_pow_add_pow_mul_taylorRem

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F) (t f : F)

Lean source · statement

theorem eq_sum_taylorCoeff_mul_pow_add_pow_mul_taylorRem {t : F} (ht : t ≠ 0) (f : F) (n : ℕ) :
    f = (∑ q ∈ Finset.range n, algebraMap K F (taylorCoeff v t q f) * t ^ q)
        + t ^ n * taylorRem v t f n

def

jetMatrix

L74 ↗

AlgebraicCurve.jetMatrix

Documentation

The matrix of the prescribed Taylor coefficients of the functions at the given places.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def jetMatrix {M : ℕ} (P : Fin M → Place K F) (t : Fin M → F) (e : Fin M → ℕ)
    (f : Fin M → F) : Matrix (Fin M) (Fin M) K

theorem

jetMatrix_apply

L78 ↗

AlgebraicCurve.jetMatrix_apply

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem jetMatrix_apply {M : ℕ} (P : Fin M → Place K F) (t : Fin M → F) (e : Fin M → ℕ)
    (f : Fin M → F) (i j : Fin M) :
    jetMatrix P t e f i j = (P i).taylorCoeff (t i) (e i) (f j)

theorem

jetMatrix_order_zero

L82 ↗

AlgebraicCurve.jetMatrix_order_zero

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem jetMatrix_order_zero {M : ℕ} (P : Fin M → Place K F) (t : Fin M → F)
    (f : Fin M → F) :
    jetMatrix P t (fun _ => 0) f = Matrix.of fun i j => (P i).evalAt (f j) := rfl

def

jetMult

L88 ↗

AlgebraicCurve.jetMult

Documentation

The number of indices at which the given list of places equals v.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open Classical in

Lean source · statement

def jetMult {M : ℕ} (P : Fin M → Place K F) (v : Place K F) : ℕ

def

jetDivisor

L92 ↗

AlgebraicCurve.jetDivisor

Documentation

The effective divisor counting the occurrences of the given places.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def jetDivisor {M : ℕ} (P : Fin M → Place K F) : Divisor K F

theorem

jetDivisor_apply

L95 ↗

AlgebraicCurve.jetDivisor_apply

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem jetDivisor_apply {M : ℕ} (P : Fin M → Place K F) (v : Place K F) :
    jetDivisor P v = (jetMult P v : ℤ)

def

IsConfluentPattern

L103 ↗

AlgebraicCurve.IsConfluentPattern

Documentation

A pattern with a common parameter at equal places and distinct orders below their multiplicity.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def IsConfluentPattern {M : ℕ} (P : Fin M → Place K F) (t : Fin M → F) (e : Fin M → ℕ) :
    Prop

Module documentation

Taylor

Declarations