Lagrange.degree_interpolate_lt
theorem Lagrange.degree_interpolate_lt :
∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F),
Set.InjOn v ↑s → ((Lagrange.interpolate s v) r).degree < ↑s.card
The theorem `Lagrange.degree_interpolate_lt` states that for any field `F`, any type `ι` with decidable equality, any finite set `s` of type `ι`, any function `v` from `ι` to `F` that is injective on `s`, and any function `r` from `ι` to `F`, the degree of the polynomial obtained by interpolating `r` using the Lagrange method with nodes given by `v` on the set `s` is strictly less than the cardinality of `s`. This means that the Lagrange interpolation polynomial is of degree less than the number of nodes.
More concisely: For any injective function `v` mapping a finite set `s` to a field `F`, the degree of the Lagrange interpolation polynomial of `F`-valued function `r` using `v` is strictly less than the cardinality of `s`.
|
Lagrange.eq_interpolate_iff
theorem Lagrange.eq_interpolate_iff :
∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F)
{f : Polynomial F},
Set.InjOn v ↑s →
((f.degree < ↑s.card ∧ ∀ i ∈ s, Polynomial.eval (v i) f = r i) ↔ f = (Lagrange.interpolate s v) r)
This theorem, `Lagrange.eq_interpolate_iff`, states the characteristic property of Lagrange interpolation. For any field `F`, type `ι` with decidable equality, finite set `s` of `ι`, nodal map `v : ι → F` which is injective on `s`, value function `r : ι → F` and a polynomial `f : Polynomial F`, the polynomial `f` is equal to the Lagrange interpolation of `s`, `v`, `r` if and only if two conditions are met: the degree of the polynomial `f` is less than the cardinality of `s`, and the polynomial `f` evaluated at `v i` equals `r i` for all `i` in `s`. In other words, the Lagrange interpolation is the unique polynomial of degree `< Fintype.card ι` which takes the value of the `r i` on the `v i`.
More concisely: The theorem `Lagrange.eq_interpolate_iff` in Lean 4 states that a polynomial equals the Lagrange interpolation of given nodal map and values if and only if its degree is less than the number of nodes and it matches the values at the nodes.
|
Lagrange.eval_interpolate_at_node
theorem Lagrange.eval_interpolate_at_node :
∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι} {v : ι → F}
(r : ι → F), Set.InjOn v ↑s → i ∈ s → Polynomial.eval (v i) ((Lagrange.interpolate s v) r) = r i
The theorem `Lagrange.eval_interpolate_at_node` states that for any field `F`, index type `ι` with decidable equality, a finite set `s` of indices, an index `i`, a nodal map `v` from `ι` to `F`, and a value function `r` from `ι` to `F`, if `v` is injective on the set `s` and `i` is an element of `s`, then the value of the polynomial obtained by the Lagrange interpolation of `s`, `v`, and `r` evaluated at `v i` is equal to `r i`. In essence, this theorem ensures that the Lagrange interpolation polynomial accurately reproduces the given value `r i` at each node `v i` in the set.
More concisely: For any injective nodal map `v` from an index type `ι` to a field `F`, finite set `s ⊆ ι`, index `i ∈ s`, and value function `r : ι → F`, the Lagrange interpolation polynomial of `s`, `v`, and `r` evaluates to `r i` at `v i`.
|
Lagrange.interpolate_apply
theorem Lagrange.interpolate_apply :
∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] (s : Finset ι) (v r : ι → F),
(Lagrange.interpolate s v) r = s.sum fun i => Polynomial.C (r i) * Lagrange.basis s v i
The theorem `Lagrange.interpolate_apply` asserts that for any field `F`, index set `ι` with a decidable equality relation, a finite set `s` of indices, and two functions `v` and `r` mapping from `ι` to `F`, the application of the Lagrange interpolation function to `s` and `v`, evaluated at `r`, is equivalent to the sum over `s` of the product of the constant polynomial based on `r i` and the Lagrange basis polynomial for `s`, `v`, and `i`. In simpler terms, this theorem establishes the relationship between the Lagrange interpolation of a set of points and the sum of the products of their corresponding constant polynomials and basis polynomials.
More concisely: The theorem asserts that the value of the Lagrange interpolation function of a set of points and their corresponding constants, evaluated at a given point, equals the sum of the products of the constants and the basis polynomials for each point.
|
Lagrange.eval_interpolate_not_at_node'
theorem Lagrange.eval_interpolate_not_at_node' :
∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F)
{x : F},
Set.InjOn v ↑s →
s.Nonempty →
(∀ i ∈ s, x ≠ v i) →
Polynomial.eval x ((Lagrange.interpolate s v) r) =
(s.sum fun i => Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i) /
s.sum fun i => Lagrange.nodalWeight s v i * (x - v i)⁻¹
This theorem states the second barycentric form of the Lagrange interpolating polynomial. Given a field `F`, a set of nodes `s` of type `ι` (where `ι` has decidable equality), a nodal map `v : ι → F` and a value function `r : ι → F`, the theorem asserts that for any `x` in `F` not equal to any node value `v i` for `i` in `s`, the evaluation of the interpolation polynomial at `x` is equal to the sum over all nodes of the product of the nodal weight, the reciprocal of the difference between `x` and the node value, and the value at the node, all divided by the sum over all nodes of the product of the nodal weight and the reciprocal of the difference between `x` and the node value. This holds when `v` is injective on `s` and `s` is nonempty.
More concisely: Given a field `F`, a finite, injective set of nodes `s` with nodal map `v : ι → F` and value function `r : ι → F`, for any `x` in `F` not equal to any `v i` for `i` in `s`, the Lagrange interpolating polynomial evaluates to the weighted sum over `s` of `r i` multiplied by the reciprocal of the difference between `x` and `v i`, weighted by the inverse of the nodal weight, where the sum of these weights is equal to the reciprocal of the Vandermonde determinant of `v(s)`.
|
Lagrange.nodal_subgroup_eq_X_pow_card_sub_one
theorem Lagrange.nodal_subgroup_eq_X_pow_card_sub_one :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (G : Subgroup Rˣ) [inst_2 : Fintype ↥G],
Lagrange.nodal (↑G).toFinset Units.val = Polynomial.X ^ Fintype.card ↥G - 1
This theorem states that the vanishing polynomial on a multiplicative subgroup is of the form X^n - 1. More specifically, given any commutative ring `R` and a multiplicative subgroup `G` of the group of units in `R`, if `G` is a finite type, then the `Lagrange.nodal` function, applied to the set of elements in `G` (treated as a finite set) and the function that extracts the underlying values from the units, results in the polynomial X^n - 1, where n is the cardinality, or the number of elements, in the subgroup `G`.
More concisely: For any commutative ring `R` and finite multiplicative subgroup `G` of its unit group, the characteristic polynomial of `G` is X^n - 1, where `n` is the number of elements in `G`.
|
Lagrange.basisDivisor_self
theorem Lagrange.basisDivisor_self : ∀ {F : Type u_1} [inst : Field F] {x : F}, Lagrange.basisDivisor x x = 0 := by
sorry
This theorem, called `Lagrange.basisDivisor_self`, states that for any field `F` and any element `x` in that field, the polynomial `Lagrange.basisDivisor x x` equals the zero polynomial. In other words, if you use the same value for both `x` and `y` in the definition of the `Lagrange.basisDivisor`, the resulting polynomial is identically zero. This is a special case of the general behavior of the `Lagrange.basisDivisor`, which is designed to equal `1` when evaluated at `x` and `0` when evaluated at `y`—clearly, if `x` and `y` are the same, it must equal `0`.
More concisely: For any field `F` and element `x` in `F`, the polynomial `Lagrange.basisDivisor x x` equals the zero polynomial.
|
Mathlib.LinearAlgebra.Lagrange._auxLemma.1
theorem Mathlib.LinearAlgebra.Lagrange._auxLemma.1 :
∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, (a - b = 0) = (a = b)
This theorem, from the `Mathlib.LinearAlgebra.Lagrange` library, states that for any type `G` that forms an additive group, given any two elements `a` and `b` of that group, the condition that the difference of `a` and `b` equals zero is equivalent to the condition that `a` equals `b`. In other words, in any additive group, subtracting an element from itself always results in the zero element.
More concisely: In an additive group, the difference of any two elements is the zero element if and only if the elements are equal.
|
Lagrange.eval_nodal
theorem Lagrange.eval_nodal :
∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} {x : R},
Polynomial.eval x (Lagrange.nodal s v) = s.prod fun i => x - v i
The theorem `Lagrange.eval_nodal` states that for any commutative ring `R`, any finite set `s`, any function `v` mapping from the set to the ring, and any element `x` of the ring, the evaluation of the nodal polynomial (defined by `s` and `v`) at `x` is equivalent to the product of `x - v i` for each element `i` in `s`. In mathematical terms, if we have a polynomial constructed using the nodes defined by `v` and `s`, when we substitute `x` into this polynomial, the result is the product of `x - v i` taken over all `i` in the finite set `s`.
More concisely: For any commutative ring R, finite set s, and function v from s to R, the evaluation of the nodal polynomial constructed from s and v at an element x of R equals the product of (x - v i) for all i in s.
|
Lagrange.eval_interpolate_not_at_node
theorem Lagrange.eval_interpolate_not_at_node :
∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F)
{x : F},
(∀ i ∈ s, x ≠ v i) →
Polynomial.eval x ((Lagrange.interpolate s v) r) =
Polynomial.eval x (Lagrange.nodal s v) * s.sum fun i => Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i
This theorem states that for a given field `F`, a set of indices `s`, a nodal map `v`, and a function `r`, if `x` is not a root of any `v i` for `i` in `s`, then the value of the Lagrange interpolation polynomial at `x` is equal to the value of the nodal polynomial at `x`, multiplied by the sum of each element in `s` of the product of the nodal weight, the inverse of `x - v i`, and `r i`. Essentially, it is explaining the first barycentric form of the Lagrange interpolating polynomial.
More concisely: Given a field `F`, a set of indices `s`, a nodal map `v`, a function `r`, and a point `x` not lying in the set of roots of `v`, the Lagrange interpolation polynomial equals the nodal polynomial value at `x` multiplied by the sum over `i` in `s` of the product of the nodal weight, the inverse of `x - v i`, and `r i`.
|
Polynomial.eq_of_degree_le_of_eval_finset_eq
theorem Polynomial.eq_of_degree_le_of_eval_finset_eq :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {f g : Polynomial R} (s : Finset R),
f.degree ≤ ↑s.card →
f.degree = g.degree →
f.leadingCoeff = g.leadingCoeff → (∀ x ∈ s, Polynomial.eval x f = Polynomial.eval x g) → f = g
This theorem states that for any commutative ring `R` and two polynomials `f` and `g` defined over `R`, if they have the same degree and the same leading coefficient, and if they evaluate to the same value for any element in a set `s` of distinct values whose cardinality is equal to or greater than their common degree, then the two polynomials `f` and `g` are equal. Essentially, it says that two polynomials are the same if they act the same way on a sufficiently large number of distinct inputs, under the condition that they have the same highest order term.
More concisely: If two polynomials over a commutative ring with the same degree and leading coefficient evaluate to the same value at every distinct element in their domain of definition of cardinality greater than or equal to their common degree, then they are equal.
|