English
For a<b, the comap of polynomialFunctions on the unit interval I under the affine homeomorphism iccHomeoI a b h, corresponds to polynomialFunctions on the closed interval [a,b]: (polynomialFunctions I).comap (compRightAlgHom ...).symm = polynomialFunctions (Set.Icc a b).
Русский
Пусть a<b. По аффинному гомоморфизму iccHomeoI, соответствующему отображению x↦(b−a)^{-1}x + a, предобраз полином-функций на I равен полином-функциям на [a,b].
LaTeX
$$$ (polynomialFunctions I).comap (compRightAlgHom \\; \\mathbb{R}\\; \\mathbb{R} (iccHomeoI a b h).symm) = polynomialFunctions (Set.Icc a b) $$$
Lean4
/-- The preimage of polynomials on `[0,1]` under the pullback map by `x ↦ (b-a) * x + a`
is the polynomials on `[a,b]`. -/
theorem comap_compRightAlgHom_iccHomeoI (a b : ℝ) (h : a < b) :
(polynomialFunctions I).comap (compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm) = polynomialFunctions (Set.Icc a b) :=
by
ext f
fconstructor
· rintro ⟨p, ⟨-, w⟩⟩
rw [DFunLike.ext_iff] at w
dsimp at w
let q := p.comp ((b - a)⁻¹ • Polynomial.X + Polynomial.C (-a * (b - a)⁻¹))
refine ⟨q, ⟨?_, ?_⟩⟩
· simp
· ext x
simp only [q, neg_mul, RingHom.map_neg, RingHom.map_mul, AlgHom.coe_toRingHom, Polynomial.eval_X,
Polynomial.eval_neg, Polynomial.eval_C, Polynomial.eval_smul, smul_eq_mul, Polynomial.eval_mul,
Polynomial.eval_add, Polynomial.eval_comp, Polynomial.toContinuousMapOnAlgHom_apply,
Polynomial.toContinuousMapOn_apply, Polynomial.toContinuousMap_apply]
convert w ⟨_, _⟩
· ext
simp only [iccHomeoI_symm_apply_coe]
replace h : b - a ≠ 0 := sub_ne_zero_of_ne h.ne.symm
field_simp
ring
· change _ + _ ∈ I
rw [mul_comm (b - a)⁻¹, ← neg_mul, ← add_mul, ← sub_eq_add_neg]
have w₁ : 0 < (b - a)⁻¹ := inv_pos.mpr (sub_pos.mpr h)
have w₂ : 0 ≤ (x : ℝ) - a := sub_nonneg.mpr x.2.1
have w₃ : (x : ℝ) - a ≤ b - a := sub_le_sub_right x.2.2 a
fconstructor
· exact mul_nonneg w₂ (le_of_lt w₁)
· rw [← div_eq_mul_inv, div_le_one (sub_pos.mpr h)]
exact w₃
· rintro ⟨p, ⟨-, rfl⟩⟩
let q := p.comp ((b - a) • Polynomial.X + Polynomial.C a)
refine ⟨q, ⟨?_, ?_⟩⟩
· simp
· ext x
simp [q, mul_comm]
