Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
This package proves the exact best uniform error for real polynomial approximation of the reciprocal function on a positive compact interval.
Parameters 4 core · 5 supporting This module records the interval shape and geometric decay parameters in the exact best uniform approximation error for the reciprocal function. ★ reciprocalError_one_sq
Parameters for reciprocal approximation on a positive interval
This module records the interval shape and geometric decay parameters in the
exact best uniform approximation error for the reciprocal function. It also
reduces the parameters on [1,K²] to elementary rational expressions.
def intervalShape reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
The lower endpoint and upper endpoint determine the interval shape parameter, given by their sum divided by their difference.
Definition (Lean source)
parameters
a b :
ℝ
def
intervalShape a b :
ℝ
given by
(a + b) / (b - a)
def intervalDecay reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
The lower endpoint and upper endpoint determine the geometric decay parameter, given by the interval shape parameter v minus the square root of v² − 1.
Definition (Lean source)
parameters
a b :
ℝ
def
intervalDecay a b :
ℝ
given by
def reciprocalError reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
The interval endpoints and degree bound m determine the reciprocal approximation error, given by twice the m-th power of the decay parameter, divided by the interval length times (v² − 1), where v is the interval shape parameter.
Definition (Lean source)
parameters
a b :
ℝ
m :
ℕ
def
reciprocalError a b m :
ℝ
given by
2 * intervalDecay a b ^ m / ((b - a) * ((intervalShape a b) ^ 2 - 1))
theorem reciprocalError_one_sq reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
A natural number K at least two implies that the degree-K reciprocal approximation error on the interval from one to K² equals (K² − 1) / (2 K²) times the K-th power of (K − 1) / (K + 1).
Formal statement
hypotheses
K :
ℕ
hK :
2 ≤ K
conclusion
reciprocalError 1 ((K : ℝ) ^ 2) K
= (((K : ℝ) ^ 2 - 1) / (2 * (K : ℝ) ^ 2)) * (((K : ℝ) - 1) / ((K : ℝ) + 1)) ^ K
Proof (Lean source)
theorem reciprocalError_one_sq (K : ℕ) (hK : 2 ≤ K) :
reciprocalError 1 ((K : ℝ) ^ 2) K =
(((K : ℝ) ^ 2 - 1) / (2 * (K : ℝ) ^ 2)) *
(((K : ℝ) - 1) / ((K : ℝ) + 1)) ^ K := by
let x : ℝ := K
have hx : 2 ≤ x := by
change (2 : ℝ) ≤ (K : ℝ)
exact_mod_cast hK
have hdpos : 0 < x ^ 2 - 1 := by nlinarith
have hd : x ^ 2 - 1 ≠ 0 := ne_of_gt hdpos
have hxne : x ≠ 0 := by positivity
have hv : intervalShape 1 (x ^ 2) = (1 + x ^ 2) / (x ^ 2 - 1) := rfl
rw [reciprocalError, intervalDecay_one_sq K hK]
change 2 * ((x - 1) / (x + 1)) ^ K /
((x ^ 2 - 1) * ((intervalShape 1 (x ^ 2)) ^ 2 - 1)) =
((x ^ 2 - 1) / (2 * x ^ 2)) * ((x - 1) / (x + 1)) ^ K
rw [hv]
field_simp
have hden : (1 + x ^ 2) ^ 2 - (x ^ 2 - 1) ^ 2 = 4 * x ^ 2 := by ring
rw [hden]
field_simp [hxne]
ring
5 supporting declarations (lemmas, instances)
-
intervalShape_gt_onetheorem — A positive lower endpoint and strictly larger upper endpoint imply that the interval shape exceeds one.Proof (Lean source)
theorem intervalShape_gt_one {a b : ℝ} (ha : 0 < a) (hab : a < b) : 1 < intervalShape a b := by unfold intervalShape have hba : 0 < b - a := sub_pos.mpr hab apply (lt_div_iff₀ hba).2 nlinarith -
intervalDecay_mem_Iootheorem — A positive lower endpoint and strictly larger upper endpoint imply that the decay parameter lies strictly between zero and one.Proof (Lean source)
theorem intervalDecay_mem_Ioo {a b : ℝ} (ha : 0 < a) (hab : a < b) : intervalDecay a b ∈ Ioo (0 : ℝ) 1 := by let v := intervalShape a b let s := sqrt (v ^ 2 - 1) have hv : 1 < v := intervalShape_gt_one ha hab have hsarg : 0 ≤ v ^ 2 - 1 := by nlinarith have hs : 0 ≤ s := Real.sqrt_nonneg _ have hs2 : s ^ 2 = v ^ 2 - 1 := Real.sq_sqrt hsarg have hsv : s < v := by by_contra h have hvs : v ≤ s := le_of_not_gt h nlinarith [sq_nonneg (s - v)] have hρ : 0 < v - s := sub_pos.mpr hsv have hsum : 1 < v + s := by linarith have hprod : (v - s) * (v + s) = 1 := by nlinarith have hρlt : v - s < 1 := by nlinarith [mul_pos hρ (sub_pos.mpr hsum)] exact ⟨by simpa [intervalDecay, v, s] using hρ, by simpa [intervalDecay, v, s] using hρlt⟩ -
intervalDecay_add_invtheorem — A positive lower endpoint and strictly larger upper endpoint imply that the decay parameter plus its reciprocal equals twice the interval shape.hypothesesa b :ℝha :0 < ahab :a < bconclusionProof (Lean source)
theorem intervalDecay_add_inv {a b : ℝ} (ha : 0 < a) (hab : a < b) : intervalDecay a b + (intervalDecay a b)⁻¹ = 2 * intervalShape a b := by let v := intervalShape a b let s := sqrt (v ^ 2 - 1) have hv : 1 < v := intervalShape_gt_one ha hab have hsarg : 0 ≤ v ^ 2 - 1 := by nlinarith have hs2 : s ^ 2 = v ^ 2 - 1 := Real.sq_sqrt hsarg have hρ : 0 < intervalDecay a b := (intervalDecay_mem_Ioo ha hab).1 have hprod : (v - s) * (v + s) = 1 := by nlinarith have hinv : (intervalDecay a b)⁻¹ = v + s := by have hne : v - s ≠ 0 := by change 0 < v - s at hρ exact ne_of_gt hρ change (v - s)⁻¹ = v + s field_simp nlinarith [hs2] rw [hinv] change (v - s) + (v + s) = 2 * v ring -
reciprocalError_postheorem — A positive lower endpoint, strictly larger upper endpoint, and finite degree imply that the claimed reciprocal error is positive.Proof (Lean source)
theorem reciprocalError_pos {a b : ℝ} (ha : 0 < a) (hab : a < b) (m : ℕ) : 0 < reciprocalError a b m := by unfold reciprocalError have hv : 1 < intervalShape a b := intervalShape_gt_one ha hab have hρ : 0 < intervalDecay a b := (intervalDecay_mem_Ioo ha hab).1 have hsq : 0 < (intervalShape a b) ^ 2 - 1 := by nlinarith exact div_pos (by positivity) (mul_pos (sub_pos.mpr hab) hsq) -
intervalDecay_one_sqtheorem — A natural number K at least two implies that the decay parameter of the interval from one to K² equals (K − 1) / (K + 1).hypothesesK :ℕhK :2 ≤ KconclusionintervalDecay 1 ((K : ℝ) ^ 2) = ((K : ℝ) - 1) / ((K : ℝ) + 1)Proof (Lean source)
theorem intervalDecay_one_sq (K : ℕ) (hK : 2 ≤ K) : intervalDecay 1 ((K : ℝ) ^ 2) = ((K : ℝ) - 1) / ((K : ℝ) + 1) := by let x : ℝ := K have hx : 2 ≤ x := by change (2 : ℝ) ≤ (K : ℝ) exact_mod_cast hK have hdpos : 0 < x ^ 2 - 1 := by nlinarith have hd : x ^ 2 - 1 ≠ 0 := ne_of_gt hdpos have hxplus : x + 1 ≠ 0 := by positivity have hv : intervalShape 1 (x ^ 2) = (1 + x ^ 2) / (x ^ 2 - 1) := rfl have harg : 0 ≤ (intervalShape 1 (x ^ 2)) ^ 2 - 1 := by have hshape : 1 < intervalShape 1 (x ^ 2) := intervalShape_gt_one (by norm_num) (by nlinarith) nlinarith have hroot : sqrt ((intervalShape 1 (x ^ 2)) ^ 2 - 1) = 2 * x / (x ^ 2 - 1) := by apply (Real.sqrt_eq_iff_eq_sq harg (by positivity)).2 rw [hv] field_simp ring change intervalShape 1 (x ^ 2) - sqrt ((intervalShape 1 (x ^ 2)) ^ 2 - 1) = (x - 1) / (x + 1) rw [hroot, hv] field_simp ring
WitnessPolynomial 3 core · 3 supporting The residual polynomial here is the one in Plonka and Tasche, Theorem 3.4. ★ reciprocalResidualPoly_at_shape
Chebyshev polynomial witness for reciprocal approximation
The residual polynomial here is the one in Plonka and Tasche, Theorem 3.4.
Using the integer-indexed Chebyshev polynomial T (-1) = T 1 makes its formula
valid at degree zero as well. Dividing its normalized difference by X
produces an explicit polynomial approximant.
def reciprocalResidualPoly reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
The interval endpoints and degree bound m determine the Chebyshev residual polynomial, given by the Chebyshev polynomial of degree m + 1 divided by the interval's decay parameter, minus twice the Chebyshev polynomial of degree m, plus the decay parameter times the Chebyshev polynomial of degree m − 1; when m = 0 the last term uses index −1, which is the Chebyshev polynomial of degree one.
Definition (Lean source)
parameters
a b :
ℝ
m :
ℕ
def
given by
C (intervalDecay a b)⁻¹ * Chebyshev.T ℝ ((m : ℤ) + 1)
- C 2 * Chebyshev.T ℝ (m : ℤ)
+ C (intervalDecay a b) * Chebyshev.T ℝ ((m : ℤ) - 1)
def reciprocalApproxPoly reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
The interval endpoints and degree bound m determine the explicit reciprocal approximating polynomial: take the residual polynomial composed with the affine map x ↦ v − 2x / (b − a), where v is the interval shape parameter, divide it by the residual polynomial's value at v, subtract the result from one, and divide by x, discarding the constant term.
Definition (Lean source)
parameters
a b :
ℝ
m :
ℕ
def
given by
(C 1 - C ((reciprocalResidualPoly a b m).eval (intervalShape a b))⁻¹ * (reciprocalResidualPoly a b m).comp (C (intervalShape a b) - C (2 / (b - a)) * X)).divX
theorem reciprocalResidualPoly_at_shape reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
A positive lower endpoint, strictly larger upper endpoint, and degree bound m imply that the residual polynomial evaluated at the interval shape parameter v equals 2 (v² − 1) divided by the m-th power of the decay parameter.
Formal statement
hypotheses
a b :
ℝ
ha :
0 < a
hab :
a < b
m :
ℕ
conclusion
(reciprocalResidualPoly a b m).eval (intervalShape a b)
= 2 * ((intervalShape a b) ^ 2 - 1) / intervalDecay a b ^ m
Proof (Lean source)
theorem reciprocalResidualPoly_at_shape {a b : ℝ}
(ha : 0 < a) (hab : a < b) (m : ℕ) :
(reciprocalResidualPoly a b m).eval (intervalShape a b) =
2 * ((intervalShape a b) ^ 2 - 1) / intervalDecay a b ^ m := by
let ρ := intervalDecay a b
let v := intervalShape a b
have hρ : ρ ≠ 0 := ne_of_gt (intervalDecay_mem_Ioo ha hab).1
have hsum : ρ + ρ⁻¹ = 2 * v := intervalDecay_add_inv ha hab
have hquad : ρ ^ 2 - 2 * v * ρ + 1 = 0 := by
field_simp at hsum ⊢
nlinarith
change (reciprocalResidualPoly a b m).eval v = 2 * (v ^ 2 - 1) / ρ ^ m
induction m using Nat.twoStepInduction with
| zero =>
simp only [reciprocalResidualPoly, Nat.cast_zero, zero_add, zero_sub,
Chebyshev.T_zero, Chebyshev.T_one, Chebyshev.T_neg_one,
eval_add, eval_sub, eval_mul, eval_C, eval_X, eval_one, pow_zero, div_one]
change ρ⁻¹ * v - 2 * 1 + ρ * v = 2 * (v ^ 2 - 1)
field_simp [hρ] at hsum ⊢
linear_combination v * hsum
| one =>
simp only [reciprocalResidualPoly, Nat.cast_one, one_add_one_eq_two,
sub_self, Chebyshev.T_zero, Chebyshev.T_one, Chebyshev.T_two,
eval_add, eval_sub, eval_mul, eval_C, eval_X, eval_pow, eval_one,
eval_ofNat, pow_one]
change ρ⁻¹ * (2 * v ^ 2 - 1) - 2 * v + ρ * 1 =
2 * (v ^ 2 - 1) / ρ
field_simp [hρ]
linear_combination hquad
| more n ih₀ ih₁ =>
rw [reciprocalResidualPoly_recurrence]
simp only [eval_sub, eval_mul, eval_ofNat, eval_X, ih₀, ih₁]
rw [← hsum]
simp only [pow_succ]
field_simp [hρ]
ring
3 supporting declarations (lemmas, instances)
-
reciprocalResidualPoly_degree_letheorem — The interval endpoints and degree bound imply that the residual polynomial has degree at most one more than the bound.Proof (Lean source)
theorem reciprocalResidualPoly_degree_le (a b : ℝ) (m : ℕ) : (reciprocalResidualPoly a b m).natDegree ≤ m + 1 := by unfold reciprocalResidualPoly apply natDegree_add_le_of_degree_le · simpa using (natDegree_sub_le_of_le (m := m + 1) (n := m + 1) (p := C (intervalDecay a b)⁻¹ * Chebyshev.T ℝ ((m : ℤ) + 1)) (q := C 2 * Chebyshev.T ℝ (m : ℤ)) (by · calc (C (intervalDecay a b)⁻¹ * Chebyshev.T ℝ ((m : ℤ) + 1)).natDegree ≤ (Chebyshev.T ℝ ((m : ℤ) + 1)).natDegree := natDegree_C_mul_le _ _ _ = m + 1 := by rw [Chebyshev.natDegree_T]; omega) (by calc (C 2 * Chebyshev.T ℝ (m : ℤ)).natDegree ≤ (Chebyshev.T ℝ (m : ℤ)).natDegree := natDegree_C_mul_le _ _ _ = m := by simp [Chebyshev.natDegree_T] _ ≤ m + 1 := by omega)) · calc (C (intervalDecay a b) * Chebyshev.T ℝ ((m : ℤ) - 1)).natDegree ≤ (Chebyshev.T ℝ ((m : ℤ) - 1)).natDegree := natDegree_C_mul_le _ _ _ = ((m : ℤ) - 1).natAbs := Chebyshev.natDegree_T ℝ _ _ ≤ m + 1 := by omega -
reciprocalApproxPoly_degree_letheorem — For any two endpoints and any degree bound, the explicit reciprocal approximant has degree at most that bound.Proof (Lean source)
theorem reciprocalApproxPoly_degree_le {a b : ℝ} (m : ℕ) : (reciprocalApproxPoly a b m).natDegree ≤ m := by let R := reciprocalResidualPoly a b m let Q := C (intervalShape a b) - C (2 / (b - a)) * X have hQ : Q.natDegree ≤ 1 := by apply (natDegree_sub_le_iff_left (n := 1) ((natDegree_C_mul_le (2 / (b - a)) X).trans natDegree_X_le)).2 simp have hR : R.natDegree ≤ m + 1 := reciprocalResidualPoly_degree_le a b m have hnum : (C 1 - C (R.eval (intervalShape a b))⁻¹ * R.comp Q).natDegree ≤ m + 1 := by apply (natDegree_sub_le_iff_right (n := m + 1) (by simp)).2 exact (natDegree_C_mul_le _ _).trans ((natDegree_comp_le).trans (by nlinarith)) change (C 1 - C (R.eval (intervalShape a b))⁻¹ * R.comp Q).divX.natDegree ≤ m rw [natDegree_divX_eq_natDegree_tsub_one] omega -
reciprocalApproxPoly_residualtheorem — Positive interval endpoints, a nonzero evaluation point, and a degree bound imply the shifted-residual identity for the explicit reciprocal approximant.hypothesesa b z :ℝha :0 < ahab :a < bhz :z ≠ 0m :ℕconclusionz⁻¹ - (reciprocalApproxPoly a b m).eval z= (reciprocalResidualPoly a b m).eval (intervalShape a b - 2 * z / (b - a)) / (z * (reciprocalResidualPoly a b m).eval (intervalShape a b))Proof (Lean source)
theorem reciprocalApproxPoly_residual {a b z : ℝ} (ha : 0 < a) (hab : a < b) (hz : z ≠ 0) (m : ℕ) : z⁻¹ - (reciprocalApproxPoly a b m).eval z = (reciprocalResidualPoly a b m).eval (intervalShape a b - 2 * z / (b - a)) / (z * (reciprocalResidualPoly a b m).eval (intervalShape a b)) := by let v := intervalShape a b let R := reciprocalResidualPoly a b m let Q : Polynomial ℝ := C v - C (2 / (b - a)) * X let P : Polynomial ℝ := C 1 - C (R.eval v)⁻¹ * R.comp Q have hv : 1 < v := intervalShape_gt_one ha hab have hρ : 0 < intervalDecay a b := (intervalDecay_mem_Ioo ha hab).1 have hRv : R.eval v ≠ 0 := by change (reciprocalResidualPoly a b m).eval (intervalShape a b) ≠ 0 rw [reciprocalResidualPoly_at_shape ha hab] have hsq : 0 < v ^ 2 - 1 := by nlinarith exact ne_of_gt (div_pos (by positivity) (pow_pos hρ m)) have hQ0 : Q.eval 0 = v := by simp [Q] have hP0 : P.coeff 0 = 0 := by rw [coeff_zero_eq_eval_zero] simp only [P, eval_sub, eval_mul, eval_C, eval_comp, hQ0] field_simp [hRv] ring have hP : X * P.divX = P := by have h := X_mul_divX_add P rwa [hP0, map_zero, add_zero] at h have hEval := congrArg (eval z) hP simp only [P, eval_mul, eval_X, eval_sub, eval_C, eval_comp] at hEval have hQz : Q.eval z = v - 2 * z / (b - a) := by simp [Q] ring rw [hQz] at hEval change z * P.divX.eval z = 1 - (R.eval v)⁻¹ * R.eval (v - 2 * z / (b - a)) at hEval change z⁻¹ - P.divX.eval z = R.eval (v - 2 * z / (b - a)) / (z * R.eval v) field_simp [hz, hRv] at hEval ⊢ linear_combination -hEval
AlternatingAngles 1 core · 0 supporting For each geometric parameter 0 < ρ < 1, the sine and cosine factors in the reciprocal residual square identities have interlacing zeros from zero to pi. ★ exists_reciprocalAlternatingAngles
Alternating zeros of reciprocal residual square factors
For each geometric parameter 0 < ρ < 1, the sine and cosine factors in
the reciprocal residual square identities have interlacing zeros from zero
to pi. This statement isolates the analytic node construction from the
polynomial identities and interval change of variables.
theorem exists_reciprocalAlternatingAngles reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
For a decay parameter ρ strictly between zero and one and a degree bound m, there are m + 2 strictly increasing angles between zero and π such that, counting from zero, at each even-indexed angle θ one has sin((m + 1)θ/2) − ρ sin((m − 1)θ/2) = 0, and at each odd-indexed angle θ one has cos((m + 1)θ/2) − ρ cos((m − 1)θ/2) = 0.
Formal statement
hypotheses
conclusion
∃ angles : Fin (m + 2) → ℝ,
StrictMono angles
Proof (Lean source)
theorem exists_reciprocalAlternatingAngles
{ρ : ℝ} (hρ : ρ ∈ Ioo (0 : ℝ) 1) (m : ℕ) :
∃ angles : Fin (m + 2) → ℝ,
StrictMono angles ∧
(∀ i, angles i ∈ Icc (0 : ℝ) pi) ∧
(∀ i : Fin (m + 2), if Even (i : ℕ) then
sin (((m : ℝ) + 1) * angles i / 2) -
ρ * sin (((m : ℝ) - 1) * angles i / 2) = 0
else
cos (((m : ℝ) + 1) * angles i / 2) -
ρ * cos (((m : ℝ) - 1) * angles i / 2) = 0) := by
classical
have hchoice (i : Fin (m + 2)) :
∃ θ : ℝ,
(if (i : ℕ) = 0 then θ = 0
else angleGrid m ((i : ℕ) - 1) < θ ∧ θ ≤ angleGrid m i) ∧
(if Even (i : ℕ) then reciprocalSinFactor m ρ θ
else reciprocalCosFactor m ρ θ) = 0 := by
by_cases hi : (i : ℕ) = 0
· refine ⟨0, ?_, ?_⟩
· simp [hi]
· simp [hi, reciprocalSinFactor]
· obtain ⟨θ, hl, hr, hz⟩ :=
exists_reciprocal_zero_in_cell hρ m i (Nat.pos_of_ne_zero hi) (by
have := i.isLt
omega)
exact ⟨θ, by simp [hi, hl, hr], hz⟩
choose angles ha using hchoice
refine ⟨angles, ?_, ?_, ?_⟩
· intro i j hij
have hijv : (i : ℕ) < (j : ℕ) := hij
by_cases hi : (i : ℕ) = 0
· have hj : (j : ℕ) ≠ 0 := by omega
have hai : angles i = 0 := by simpa [hi] using (ha i).1
have haj : angleGrid m ((j : ℕ) - 1) < angles j := by
have h := (ha j).1
simp only [if_neg hj] at h
exact h.1
have hg : 0 ≤ angleGrid m ((j : ℕ) - 1) :=
(angleGrid_mem m _ (by have := j.isLt; omega)).1
linarith
· have hj : (j : ℕ) ≠ 0 := by omega
have hai : angles i ≤ angleGrid m i := by
have h := (ha i).1
simp only [if_neg hi] at h
exact h.2
have haj : angleGrid m ((j : ℕ) - 1) < angles j := by
have h := (ha j).1
simp only [if_neg hj] at h
exact h.1
have hg : angleGrid m i ≤ angleGrid m ((j : ℕ) - 1) :=
(angleGrid_strictMono m).monotone (by omega)
linarith
· intro i
by_cases hi : (i : ℕ) = 0
· have hai : angles i = 0 := by simpa [hi] using (ha i).1
rw [hai]
exact ⟨le_refl _, Real.pi_pos.le⟩
· have hl : angleGrid m ((i : ℕ) - 1) < angles i := by
have h := (ha i).1
simp only [if_neg hi] at h
exact h.1
have hr : angles i ≤ angleGrid m i := by
have h := (ha i).1
simp only [if_neg hi] at h
exact h.2
have hgl : 0 ≤ angleGrid m ((i : ℕ) - 1) :=
(angleGrid_mem m _ (by have := i.isLt; omega)).1
have hgr : angleGrid m i ≤ pi :=
(angleGrid_mem m _ (by have := i.isLt; omega)).2
exact ⟨by linarith, by linarith⟩
· intro i
by_cases he : Even (i : ℕ)
· simpa [he, reciprocalSinFactor] using (ha i).2
· simpa [he, reciprocalCosFactor] using (ha i).2
AlternationLower 1 core · 0 supporting This module extracts the sufficient direction of polynomial equioscillation from Causalean's normalized Lagrange weights. ★ alternatingResidual_certifiesBest
Alternating residuals certify the best uniform error
This module extracts the sufficient direction of polynomial equioscillation from Causalean's normalized Lagrange weights. It is useful independently of reciprocal approximation.
theorem alternatingResidual_certifiesBest reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
On a nondegenerate interval from a to b, let the target f be continuous on the interval, E a nonnegative error level, and P a candidate polynomial of degree at most m whose residual f − P is at most E in absolute value on the whole interval. If there are m + 2 strictly increasing nodes in the interval at which the residual equals E with alternating signs, starting with +E at the first node, then both the uniform error of the candidate on the interval and the best uniform error over all polynomials of degree at most m equal E.
Formal statement
hypotheses
f :
ℝ → ℝ
a b E :
ℝ
m :
ℕ
hab :
a < b
hf :
ContinuousOn f (Icc a b)
hE :
0 ≤ E
P :
hdegree :
P.natDegree ≤ m
hbound :
∀ x ∈ Icc a b, |f x - P.eval x| ≤ E
nodes :
Fin (m + 2) → ℝ
hmono :
StrictMono nodes
hmem :
∀ i, nodes i ∈ Icc a b
halt :
∀ i, f (nodes i) - P.eval (nodes i) = (-1 : ℝ) ^ (i : ℕ) * E
Proof (Lean source)
theorem alternatingResidual_certifiesBest
{f : ℝ → ℝ} {a b E : ℝ} {m : ℕ}
(hab : a < b) (hf : ContinuousOn f (Icc a b))
(hE : 0 ≤ E) (P : Polynomial ℝ) (hdegree : P.natDegree ≤ m)
(hbound : ∀ x ∈ Icc a b, |f x - P.eval x| ≤ E)
(nodes : Fin (m + 2) → ℝ) (hmono : StrictMono nodes)
(hmem : ∀ i, nodes i ∈ Icc a b)
(halt : ∀ i, f (nodes i) - P.eval (nodes i) = (-1 : ℝ) ^ (i : ℕ) * E) :
uniformApproxError f a b P = E ∧ bestUniformApproxError f a b m = E := by
classical
let w : Fin (m + 2) → ℝ := normalizedLagrangeWeight nodes
have hinj : Injective nodes := hmono.injective
have hmass : ∑ i, |w i| = 1 :=
sum_abs_normalizedLagrangeWeight_eq_one hinj
have hpower (i : Fin (m + 2)) :
(-1 : ℝ) ^ (m + 1 - (i : ℕ)) * (-1 : ℝ) ^ (i : ℕ) =
(-1 : ℝ) ^ (m + 1) := by
rw [← pow_add, Nat.sub_add_cancel]
omega
have hresidual :
∑ i, w i * (f (nodes i) - P.eval (nodes i)) =
(-1 : ℝ) ^ (m + 1) * E := by
calc
∑ i, w i * (f (nodes i) - P.eval (nodes i)) =
∑ i, ((-1 : ℝ) ^ (m + 1) * E) * |w i| := by
apply Finset.sum_congr rfl
intro i _
have hwalt : w i = (-1 : ℝ) ^ (m + 1 - (i : ℕ)) * |w i| :=
normalizedLagrangeWeight_alternates hmono i
rw [halt i]
calc
w i * ((-1 : ℝ) ^ (i : ℕ) * E) =
((-1 : ℝ) ^ (m + 1 - (i : ℕ)) * (-1 : ℝ) ^ (i : ℕ)) * E * |w i| := by
conv_lhs => rw [hwalt]
ring
_ = (-1 : ℝ) ^ (m + 1) * E * |w i| := by rw [hpower i]
_ = (-1 : ℝ) ^ (m + 1) * E := by
rw [← Finset.mul_sum, hmass, mul_one]
have hcontinuous (Q : Polynomial ℝ) :
ContinuousOn (fun x => f x - Q.eval x) (Icc a b) :=
hf.sub Q.continuous.continuousOn
have hupper : uniformApproxError f a b P ≤ E :=
(intervalSupNorm_le_iff (hcontinuous P) hab.le).mpr hbound
have hlower (Q : Polynomial ℝ) (hQ : Q.natDegree ≤ m) :
E ≤ uniformApproxError f a b Q := by
have hQzero : ∑ i, w i * Q.eval (nodes i) = 0 :=
sum_normalizedLagrangeWeight_mul_eval_eq_zero hinj hQ
have hPzero : ∑ i, w i * P.eval (nodes i) = 0 :=
sum_normalizedLagrangeWeight_mul_eval_eq_zero hinj hdegree
have hsum :
∑ i, w i * (f (nodes i) - Q.eval (nodes i)) =
(-1 : ℝ) ^ (m + 1) * E := by
calc
∑ i, w i * (f (nodes i) - Q.eval (nodes i)) =
(∑ i, w i * f (nodes i)) - ∑ i, w i * Q.eval (nodes i) := by
rw [← Finset.sum_sub_distrib]
apply Finset.sum_congr rfl
intro i _
ring
_ = ∑ i, w i * f (nodes i) := by rw [hQzero, sub_zero]
_ = (∑ i, w i * (f (nodes i) - P.eval (nodes i))) +
∑ i, w i * P.eval (nodes i) := by
rw [← Finset.sum_add_distrib]
apply Finset.sum_congr rfl
intro i _
ring
_ = (-1 : ℝ) ^ (m + 1) * E := by rw [hPzero, add_zero, hresidual]
have hpoint (i : Fin (m + 2)) :
|f (nodes i) - Q.eval (nodes i)| ≤ uniformApproxError f a b Q :=
((intervalSupNorm_le_iff (hcontinuous Q) hab.le).mp le_rfl) _ (hmem i)
have hsum_bound :
|∑ i, w i * (f (nodes i) - Q.eval (nodes i))| ≤
uniformApproxError f a b Q := by
calc
|∑ i, w i * (f (nodes i) - Q.eval (nodes i))| ≤
∑ i, |w i * (f (nodes i) - Q.eval (nodes i))| :=
Finset.abs_sum_le_sum_abs _ _
_ ≤ ∑ i, |w i| * uniformApproxError f a b Q := by
apply Finset.sum_le_sum
intro i _
rw [abs_mul]
exact mul_le_mul_of_nonneg_left (hpoint i) (abs_nonneg _)
_ = uniformApproxError f a b Q := by
rw [← Finset.sum_mul, hmass, one_mul]
rw [hsum, abs_mul, abs_pow, abs_neg, abs_one, one_pow, one_mul,
abs_of_nonneg hE] at hsum_bound
exact hsum_bound
have hP_lower : E ≤ uniformApproxError f a b P := hlower P hdegree
have hP_eq : uniformApproxError f a b P = E := le_antisymm hupper hP_lower
refine ⟨hP_eq, le_antisymm ?_ ?_⟩
· exact (bestUniformApproxError_le (f := f) (r := a) (s := b) hdegree).trans_eq hP_eq
· unfold bestUniformApproxError
apply le_csInf
· exact ⟨uniformApproxError f a b P, P, hdegree, rfl⟩
· rintro e ⟨Q, hQ, rfl⟩
exact hlower Q hQ
Main 2 core · 2 supporting For every positive real interval and every natural degree bound, this module identifies the best uniform polynomial approximation error for x ↦ x⁻¹. ★ bestUniformApproxError_reciprocal★ bestUniformApproxError_reciprocal_one_sq
Exact best uniform approximation of the reciprocal function
For every positive real interval and every natural degree bound, this module
identifies the best uniform polynomial approximation error for x ↦ x⁻¹.
The formula follows from an explicit Chebyshev polynomial, its sharp bound,
and alternating equality points. It also gives the interval [1,K²] formula
used in finite moment duality.
theorem bestUniformApproxError_reciprocal reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
A positive lower endpoint, strictly larger upper endpoint, and degree bound m imply that the best uniform error in approximating 1 / z on the interval by polynomials of degree at most m equals exactly 2 ρ^m divided by (b − a)(v² − 1), where v = (a + b) / (b − a) and ρ = v minus the square root of v² − 1.
Formal statement
hypotheses
a b :
ℝ
ha :
0 < a
hab :
a < b
m :
ℕ
conclusion
bestUniformApproxError (fun z : ℝ => z⁻¹) a b m
= (let v := (a + b) / (b - a) let ρ := v - sqrt (v ^ 2 - 1) 2 * ρ ^ m / ((b - a) * (v ^ 2 - 1)))
Proof (Lean source)
theorem bestUniformApproxError_reciprocal {a b : ℝ}
(ha : 0 < a) (hab : a < b) (m : ℕ) :
bestUniformApproxError (fun z : ℝ => z⁻¹) a b m =
(let v := (a + b) / (b - a)
let ρ := v - sqrt (v ^ 2 - 1)
2 * ρ ^ m / ((b - a) * (v ^ 2 - 1))) := by
have hf : ContinuousOn (fun z : ℝ => z⁻¹) (Icc a b) := by
apply ContinuousOn.inv₀ continuousOn_id
intro z hz
exact ne_of_gt (lt_of_lt_of_le ha hz.1)
have hres : ContinuousOn
(fun z : ℝ => z⁻¹ - (reciprocalApproxPoly a b m).eval z)
(Icc a b) := hf.sub (reciprocalApproxPoly a b m).continuous.continuousOn
have hbound : ∀ z ∈ Icc a b,
|z⁻¹ - (reciprocalApproxPoly a b m).eval z| ≤ reciprocalError a b m :=
(intervalSupNorm_le_iff hres hab.le).mp (reciprocalApproxPoly_upper ha hab m)
obtain ⟨nodes, hmono, hmem, halt⟩ :=
reciprocalApproxPoly_alternates ha hab m
have hbest := (alternatingResidual_certifiesBest hab hf
(le_of_lt (reciprocalError_pos ha hab m))
(reciprocalApproxPoly a b m) (reciprocalApproxPoly_degree_le m)
hbound nodes hmono hmem halt).2
exact hbest
theorem bestUniformApproxError_reciprocal_one_sq reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
For a natural number K at least two, the best uniform error in approximating 1 / z on the interval from one to K² by polynomials of degree at most K equals (K² − 1) / (2 K²) times the K-th power of (K − 1) / (K + 1).
Formal statement
hypotheses
K :
ℕ
hK :
2 ≤ K
conclusion
bestUniformApproxError (fun z : ℝ => z⁻¹) 1 ((K : ℝ) ^ 2) K
= (((K : ℝ) ^ 2 - 1) / (2 * (K : ℝ) ^ 2)) * (((K : ℝ) - 1) / ((K : ℝ) + 1)) ^ K
Proof (Lean source)
theorem bestUniformApproxError_reciprocal_one_sq
(K : ℕ) (hK : 2 ≤ K) :
bestUniformApproxError (fun z : ℝ => z⁻¹) 1 ((K : ℝ) ^ 2) K =
(((K : ℝ) ^ 2 - 1) / (2 * (K : ℝ) ^ 2)) *
(((K : ℝ) - 1) / ((K : ℝ) + 1)) ^ K := by
have hKreal : (2 : ℝ) ≤ (K : ℝ) := by exact_mod_cast hK
have hbound : (1 : ℝ) < (K : ℝ) ^ 2 := by nlinarith
rw [bestUniformApproxError_reciprocal (by norm_num) hbound K]
change reciprocalError 1 ((K : ℝ) ^ 2) K = _
exact reciprocalError_one_sq K hK
2 supporting declarations (lemmas, instances)
-
reciprocalApproxPoly_uppertheorem — A positive lower endpoint, strictly larger upper endpoint, and degree bound m imply that the explicit reciprocal approximating polynomial approximates the function 1 / z uniformly on the interval within the reciprocal approximation error.hypothesesa b :ℝha :0 < ahab :a < bm :ℕconclusionuniformApproxError (fun z : ℝ => z⁻¹) a b (reciprocalApproxPoly a b m)≤ reciprocalError a b mProof (Lean source)
theorem reciprocalApproxPoly_upper {a b : ℝ} (ha : 0 < a) (hab : a < b) (m : ℕ) : uniformApproxError (fun z : ℝ => z⁻¹) a b (reciprocalApproxPoly a b m) ≤ reciprocalError a b m := by -- Combine `reciprocalApproxPoly_residual`, `reciprocalResidualPoly_bound`, -- `reciprocalResidualPoly_at_shape`, and `intervalSupNorm_le_iff`. have hcontinuous : ContinuousOn (fun z : ℝ => z⁻¹ - (reciprocalApproxPoly a b m).eval z) (Icc a b) := by apply ContinuousOn.sub · apply ContinuousOn.inv₀ continuousOn_id intro z hz exact ne_of_gt (lt_of_lt_of_le ha hz.1) · exact (reciprocalApproxPoly a b m).continuous.continuousOn change intervalSupNorm (fun z : ℝ => z⁻¹ - (reciprocalApproxPoly a b m).eval z) a b ≤ _ apply (intervalSupNorm_le_iff hcontinuous hab.le).2 intro z hz have hzpos : 0 < z := lt_of_lt_of_le ha hz.1 have hd : 0 < b - a := sub_pos.mpr hab have hv : 1 < intervalShape a b := intervalShape_gt_one ha hab have hs : 0 < intervalShape a b ^ 2 - 1 := by nlinarith have hρ : 0 < intervalDecay a b := (intervalDecay_mem_Ioo ha hab).1 have hRpos : 0 < (reciprocalResidualPoly a b m).eval (intervalShape a b) := by rw [reciprocalResidualPoly_at_shape ha hab] exact div_pos (by positivity) (pow_pos hρ m) have hden : 0 < z * (reciprocalResidualPoly a b m).eval (intervalShape a b) := mul_pos hzpos hRpos rw [reciprocalApproxPoly_residual ha hab (ne_of_gt hzpos) m, abs_div, abs_of_pos hden] have hnum := reciprocalResidualPoly_bound ha hab hz m have hnum' : |(reciprocalResidualPoly a b m).eval (intervalShape a b - 2 * z / (b - a))| ≤ 4 * z / (b - a) := by convert hnum using 1 ring calc |(reciprocalResidualPoly a b m).eval (intervalShape a b - 2 * z / (b - a))| / (z * (reciprocalResidualPoly a b m).eval (intervalShape a b)) ≤ (4 * z / (b - a)) / (z * (reciprocalResidualPoly a b m).eval (intervalShape a b)) := div_le_div_of_nonneg_right hnum' hden.le _ = reciprocalError a b m := by rw [reciprocalResidualPoly_at_shape ha hab] unfold reciprocalError field_simp [ne_of_gt hzpos, ne_of_gt hd, ne_of_gt hs, ne_of_gt hρ] ring -
reciprocalApproxPoly_alternatestheorem — A positive lower endpoint, strictly larger upper endpoint, and degree bound imply the existence of ordered points with alternating residual values for the explicit reciprocal approximant.hypothesesa b :ℝha :0 < ahab :a < bm :ℕconclusion∃ nodes : Fin (m + 2) → ℝ,StrictMono nodesconclusion 2i :(nodes i)⁻¹ - (reciprocalApproxPoly a b m).eval (nodes i)= (-1 : ℝ) ^ (i : ℕ) * reciprocalError a b mProof (Lean source)
theorem reciprocalApproxPoly_alternates {a b : ℝ} (ha : 0 < a) (hab : a < b) (m : ℕ) : ∃ nodes : Fin (m + 2) → ℝ, StrictMono nodes ∧ (∀ i, nodes i ∈ Icc a b) ∧ (∀ i, (nodes i)⁻¹ - (reciprocalApproxPoly a b m).eval (nodes i) = (-1 : ℝ) ^ (i : ℕ) * reciprocalError a b m) := by -- Apply `reciprocalResidualPoly_alternating_nodes`, then simplify using -- `reciprocalApproxPoly_residual` and the value of `R(v)`. obtain ⟨nodes, hmono, hmem, halt⟩ := reciprocalResidualPoly_alternating_nodes ha hab m refine ⟨nodes, hmono, hmem, ?_⟩ intro i have hzpos : 0 < nodes i := lt_of_lt_of_le ha (hmem i).1 have hd : 0 < b - a := sub_pos.mpr hab have hv : 1 < intervalShape a b := intervalShape_gt_one ha hab have hs : 0 < intervalShape a b ^ 2 - 1 := by nlinarith have hρ : 0 < intervalDecay a b := (intervalDecay_mem_Ioo ha hab).1 rw [reciprocalApproxPoly_residual ha hab (ne_of_gt hzpos) m, halt i, reciprocalResidualPoly_at_shape ha hab] unfold reciprocalError field_simp [ne_of_gt hzpos, ne_of_gt hd, ne_of_gt hs, ne_of_gt hρ] ring
ResidualOscillation 1 core · 1 supporting The sharp residual bound and m+2 alternating equality points are the analytic core of the reciprocal best approximation formula. ★ reciprocalResidualPoly_alternating_nodes
Bounded oscillation of the reciprocal Chebyshev residual
The sharp residual bound and m+2 alternating equality points are the
analytic core of the reciprocal best approximation formula. These lemmas
state the two independent conclusions needed by the final alternation proof.
theorem reciprocalResidualPoly_alternating_nodes reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
For a positive lower endpoint a and a strictly larger upper endpoint b and a degree bound m, there are m + 2 strictly increasing points x of the interval from a to b such that, writing v for the interval shape parameter and t = v − 2x / (b − a) for the transformed point, the residual polynomial at t equals 2 (v − t) at the even-indexed points (counting from zero) and −2 (v − t) at the odd-indexed points.
Formal statement
hypotheses
a b :
ℝ
ha :
0 < a
hab :
a < b
m :
ℕ
conclusion
∃ nodes : Fin (m + 2) → ℝ,
StrictMono nodes
conclusion 2
i :
(reciprocalResidualPoly a b m).eval (intervalShape a b - 2 * nodes i / (b - a))
= (-1 : ℝ) ^ (i : ℕ) * (2 * (intervalShape a b - (intervalShape a b - 2 * nodes i / (b - a))))
Proof (Lean source)
theorem reciprocalResidualPoly_alternating_nodes {a b : ℝ}
(ha : 0 < a) (hab : a < b) (m : ℕ) :
∃ nodes : Fin (m + 2) → ℝ,
StrictMono nodes ∧
(∀ i, nodes i ∈ Icc a b) ∧
(∀ i,
(reciprocalResidualPoly a b m).eval
(intervalShape a b - 2 * nodes i / (b - a)) =
(-1 : ℝ) ^ (i : ℕ) *
(2 * (intervalShape a b -
(intervalShape a b - 2 * nodes i / (b - a))))) := by
-- Use `exists_reciprocalAlternatingAngles` with `ρ = intervalDecay a b`.
-- Set `nodes i = (a+b)/2 - (b-a)*cos (angles i)/2`. By
-- `Real.strictAntiOn_cos`, the cosine sequence is strictly decreasing,
-- and the positive factor `b-a` makes the node sequence strictly
-- increasing. `Real.cos_mem_Icc` gives interval membership after clearing
-- denominators. Show `v - 2*nodes i/(b-a) = cos (angles i)` algebraically.
-- At even `i`, the angle lemma kills the sine square, so the residual is
-- `+2*(v-cos θ)`; at odd `i`, it kills the cosine square, giving the
-- negative value. `(-1 : ℝ)^i` is `1` or `-1` by parity.
obtain ⟨angles, hmono, hmem, hzero⟩ :=
exists_reciprocalAlternatingAngles (intervalDecay_mem_Ioo ha hab) m
let nodes : Fin (m + 2) → ℝ := fun i =>
(a + b - (b - a) * cos (angles i)) / 2
have hd : 0 < b - a := sub_pos.mpr hab
have hshift (i : Fin (m + 2)) :
intervalShape a b - 2 * nodes i / (b - a) = cos (angles i) := by
dsimp [nodes, intervalShape]
field_simp
ring
refine ⟨nodes, ?_, ?_, ?_⟩
· intro i j hij
have hc : cos (angles j) < cos (angles i) :=
Real.strictAntiOn_cos (hmem i) (hmem j) (hmono hij)
dsimp [nodes]
have hp := mul_lt_mul_of_pos_left hc hd
linarith
· intro i
have hc := Real.cos_mem_Icc (angles i)
dsimp [nodes]
constructor <;> nlinarith [mul_le_mul_of_nonneg_left hc.1 hd.le,
mul_le_mul_of_nonneg_left hc.2 hd.le]
· intro i
rw [hshift]
by_cases he : Even (i : ℕ)
· have hz := hzero i
simp only [if_pos he] at hz
rw [reciprocalResidualPoly_sin_square ha hab m (angles i), hz]
simp [Even.neg_one_pow he]
· have hz := hzero i
simp only [if_neg he] at hz
rw [reciprocalResidualPoly_cos_square ha hab m (angles i), hz]
have ho : Odd (i : ℕ) := Nat.not_even_iff_odd.mp he
simp [Odd.neg_one_pow ho]
1 supporting declaration (lemmas, instances)
-
reciprocalResidualPoly_boundtheorem — Positive interval endpoints, an interval point, and a degree bound imply the sharp absolute bound for the shifted residual polynomial.hypothesesconclusion|(reciprocalResidualPoly a b m).eval (intervalShape a b - 2 * z / (b - a))|≤ 2 * (intervalShape a b - (intervalShape a b - 2 * z / (b - a)))Proof (Lean source)
theorem reciprocalResidualPoly_bound {a b z : ℝ} (ha : 0 < a) (hab : a < b) (hz : z ∈ Icc a b) (m : ℕ) : |(reciprocalResidualPoly a b m).eval (intervalShape a b - 2 * z / (b - a))| ≤ 2 * (intervalShape a b - (intervalShape a b - 2 * z / (b - a))) := by -- Set `t = v - 2*z/(b-a)`. `a ≤ z ≤ b` gives `-1 ≤ t ≤ 1`: -- expand `intervalShape`, clear the positive denominator `b-a`, and use -- `linarith`. Obtain `θ ∈ Icc 0 pi` with `cos θ = t` from -- `Real.surjOn_cos`. The sine-square identity gives -- `R(t) ≤ 2*(v-t)`; the cosine-square identity gives its negative lower -- bound. Both use `0 < 2/ρ` from `intervalDecay_mem_Ioo`. Finish with -- `abs_le.mpr`. Mathlib also has `Real.cos_mem_Icc` for the reverse map. have hd : 0 < b - a := sub_pos.mpr hab have ht : intervalShape a b - 2 * z / (b - a) ∈ Icc (-1 : ℝ) 1 := by have heq : intervalShape a b - 2 * z / (b - a) = (a + b - 2 * z) / (b - a) := by unfold intervalShape ring rw [heq] constructor · apply (le_div_iff₀ hd).2 nlinarith [hz.2] · apply (div_le_iff₀ hd).2 nlinarith [hz.1] obtain ⟨θ, _, hθ⟩ := Real.surjOn_cos ht have hρ : 0 ≤ 2 / intervalDecay a b := le_of_lt (div_pos (by norm_num) (intervalDecay_mem_Ioo ha hab).1) have hs := reciprocalResidualPoly_sin_square ha hab m θ have hc := reciprocalResidualPoly_cos_square ha hab m θ rw [hθ] at hs hc apply abs_le.mpr constructor <;> nlinarith [sq_nonneg (sin (((m : ℝ) + 1) * θ / 2) - intervalDecay a b * sin (((m : ℝ) - 1) * θ / 2)), sq_nonneg (cos (((m : ℝ) + 1) * θ / 2) - intervalDecay a b * cos (((m : ℝ) - 1) * θ / 2))]
ResidualSquareIdentities 1 core · 1 supporting The two trigonometric square identities from Plonka and Tasche, Lemma 3.3, turn the Chebyshev residual into sharp upper and lower bounds on [-1,1]. ★ reciprocalResidualPoly_sin_square
Square identities for the reciprocal residual
The two trigonometric square identities from Plonka and Tasche, Lemma 3.3,
turn the Chebyshev residual into sharp upper and lower bounds on [-1,1].
They also identify the equality conditions used to construct alternation points.
theorem reciprocalResidualPoly_sin_square reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.Reciprocal
For a positive lower endpoint a and a strictly larger upper endpoint b, a degree bound m, and an angle θ, the residual polynomial evaluated at cos θ equals 2 (v − cos θ) minus 2 / ρ times the square of sin((m + 1)θ/2) − ρ sin((m − 1)θ/2), where v is the interval shape parameter and ρ the decay parameter.
Formal statement
hypotheses
a b :
ℝ
ha :
0 < a
hab :
a < b
m :
ℕ
θ :
ℝ
conclusion
(reciprocalResidualPoly a b m).eval (cos θ)
= 2 * (intervalShape a b - cos θ)
- (2 / intervalDecay a b) * (sin (((m : ℝ) + 1) * θ / 2) - intervalDecay a b * sin (((m : ℝ) - 1) * θ / 2)) ^ 2
Proof (Lean source)
theorem reciprocalResidualPoly_sin_square {a b : ℝ}
(ha : 0 < a) (hab : a < b) (m : ℕ) (θ : ℝ) :
(reciprocalResidualPoly a b m).eval (cos θ) =
2 * (intervalShape a b - cos θ) -
(2 / intervalDecay a b) *
(sin (((m : ℝ) + 1) * θ / 2) -
intervalDecay a b * sin (((m : ℝ) - 1) * θ / 2)) ^ 2 := by
-- Expand `T_real_cos`, then apply the cosine subtraction and double-angle
-- identities. `intervalDecay_add_inv` identifies `ρ + ρ⁻¹` with `2v`.
-- A useful intermediate form (Plonka--Tasche, Lemma 3.3) is
-- R(cos θ) - 2(v-cos θ) = ρ⁻¹(cos((m+1)θ)-1)
-- - 2(cos(mθ)-cos θ) + ρ(cos((m-1)θ)-1).
-- Rewrite the three differences as squares/products of half-angle sines;
-- `ring` then factors the result. The integer Chebyshev index covers m=0.
let ρ := intervalDecay a b
let v := intervalShape a b
let x := (((m : ℝ) + 1) * θ) / 2
let y := (((m : ℝ) - 1) * θ) / 2
have hρ : ρ ≠ 0 := ne_of_gt (intervalDecay_mem_Ioo ha hab).1
have hsum : ρ + ρ⁻¹ = 2 * v := intervalDecay_add_inv ha hab
have hR : (reciprocalResidualPoly a b m).eval (cos θ) =
ρ⁻¹ * cos (((m : ℝ) + 1) * θ) -
2 * cos ((m : ℝ) * θ) +
ρ * cos (((m : ℝ) - 1) * θ) := by
simp only [reciprocalResidualPoly, eval_add, eval_sub, eval_mul, eval_C,
Chebyshev.T_real_cos]
push_cast
ring
have hplus : cos (((m : ℝ) + 1) * θ) = 1 - 2 * sin x ^ 2 := by
calc
_ = cos (2 * x) := by congr 1; dsimp [x]; ring
_ = _ := Real.cos_two_mul_eq_one_sub x
have hminus : cos (((m : ℝ) - 1) * θ) = 1 - 2 * sin y ^ 2 := by
calc
_ = cos (2 * y) := by congr 1; dsimp [y]; ring
_ = _ := Real.cos_two_mul_eq_one_sub y
have hx : (((m : ℝ) * θ + θ) / 2) = x := by dsimp [x]; ring
have hy : (((m : ℝ) * θ - θ) / 2) = y := by dsimp [y]; ring
have hmid : cos ((m : ℝ) * θ) - cos θ =
-2 * sin x * sin y := by
simpa only [hx, hy] using Real.cos_sub_cos ((m : ℝ) * θ) θ
change (reciprocalResidualPoly a b m).eval (cos θ) =
2 * (v - cos θ) - (2 / ρ) * (sin x - ρ * sin y) ^ 2
rw [hR, hplus, hminus]
have hmid' : cos ((m : ℝ) * θ) =
cos θ - 2 * sin x * sin y := by linarith
rw [hmid']
field_simp [hρ] at hsum ⊢
nlinarith [hsum]
1 supporting declaration (lemmas, instances)
-
reciprocalResidualPoly_cos_squaretheorem — Positive interval endpoints, a degree bound, and an angle imply the cosine-square identity for the residual at that angle.hypothesesa b :ℝha :0 < ahab :a < bm :ℕθ :ℝconclusion(reciprocalResidualPoly a b m).eval (cos θ)= -2 * (intervalShape a b - cos θ)+ (2 / intervalDecay a b) * (cos (((m : ℝ) + 1) * θ / 2) - intervalDecay a b * cos (((m : ℝ) - 1) * θ / 2)) ^ 2Proof (Lean source)
theorem reciprocalResidualPoly_cos_square {a b : ℝ} (ha : 0 < a) (hab : a < b) (m : ℕ) (θ : ℝ) : (reciprocalResidualPoly a b m).eval (cos θ) = -2 * (intervalShape a b - cos θ) + (2 / intervalDecay a b) * (cos (((m : ℝ) + 1) * θ / 2) - intervalDecay a b * cos (((m : ℝ) - 1) * θ / 2)) ^ 2 := by -- Expand `T_real_cos`, then apply the cosine addition and double-angle -- identities. `intervalDecay_add_inv` identifies `ρ + ρ⁻¹` with `2v`. -- The corresponding intermediate form is -- R(cos θ) + 2(v-cos θ) = ρ⁻¹(cos((m+1)θ)+1) -- - 2(cos(mθ)+cos θ) + ρ(cos((m-1)θ)+1). -- Rewrite the three sums as half-angle cosine products and factor by `ring`. let ρ := intervalDecay a b let v := intervalShape a b let x := (((m : ℝ) + 1) * θ) / 2 let y := (((m : ℝ) - 1) * θ) / 2 have hρ : ρ ≠ 0 := ne_of_gt (intervalDecay_mem_Ioo ha hab).1 have hsum : ρ + ρ⁻¹ = 2 * v := intervalDecay_add_inv ha hab have hR : (reciprocalResidualPoly a b m).eval (cos θ) = ρ⁻¹ * cos (((m : ℝ) + 1) * θ) - 2 * cos ((m : ℝ) * θ) + ρ * cos (((m : ℝ) - 1) * θ) := by simp only [reciprocalResidualPoly, eval_add, eval_sub, eval_mul, eval_C, Chebyshev.T_real_cos] push_cast ring have hplus : cos (((m : ℝ) + 1) * θ) = 2 * cos x ^ 2 - 1 := by calc _ = cos (2 * x) := by congr 1; dsimp [x]; ring _ = _ := Real.cos_two_mul x have hminus : cos (((m : ℝ) - 1) * θ) = 2 * cos y ^ 2 - 1 := by calc _ = cos (2 * y) := by congr 1; dsimp [y]; ring _ = _ := Real.cos_two_mul y have hx : (((m : ℝ) * θ + θ) / 2) = x := by dsimp [x]; ring have hy : (((m : ℝ) * θ - θ) / 2) = y := by dsimp [y]; ring have hmid : cos ((m : ℝ) * θ) + cos θ = 2 * cos x * cos y := by simpa only [hx, hy] using Real.cos_add_cos ((m : ℝ) * θ) θ change (reciprocalResidualPoly a b m).eval (cos θ) = -2 * (v - cos θ) + (2 / ρ) * (cos x - ρ * cos y) ^ 2 rw [hR, hplus, hminus] have hmid' : cos ((m : ℝ) * θ) = 2 * cos x * cos y - cos θ := by linarith rw [hmid'] field_simp [hρ] at hsum ⊢ nlinarith [hsum]