BernsteinRationalBasis.lean

1 import Mathlib.RingTheory.Polynomial.Bernstein
2 import Mathlib.RingTheory.Polynomial.DegreeLT
3 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
4 import Mathlib.Tactic
5 
6 set_option autoImplicit false
7 namespace Komorebi.LSM.BernsteinRationalBasis
8 open Polynomial Module
9 noncomputable section
10 
11 theorem bernstein_natDegree_le (n : ℕ) (k : Fin (n+1)) :
12     (bernsteinPolynomial ℚ n k).natDegree ≤ n := by
13   have hsub : (1-(X : ℚ[X])).natDegree ≤ 1 := by
14     exact (Polynomial.natDegree_sub_le _ _).trans (by simp)
15   have hp : ((1-(X : ℚ[X]))^(n-k.val)).natDegree ≤ n-k.val := by
16     calc
17       _ ≤ (n-k.val) * (1-(X : ℚ[X])).natDegree := Polynomial.natDegree_pow_le
18       _ ≤ (n-k.val)*1 := Nat.mul_le_mul_left _ hsub
19       _ = _ := by omega
20   calc
21     _ ≤ ((n.choose k.val : ℚ[X]) * X^k.val).natDegree +
22         ((1-(X : ℚ[X]))^(n-k.val)).natDegree := Polynomial.natDegree_mul_le
23     _ ≤ k.val + (n-k.val) := by
24       apply Nat.add_le_add _ hp
25       have hm : ((n.choose k.val : ℚ[X]) * X^k.val).natDegree ≤
26           (n.choose k.val : ℚ[X]).natDegree + (X^k.val : ℚ[X]).natDegree :=
27         Polynomial.natDegree_mul_le
28       simpa using hm
29     _ = n := Nat.add_sub_of_le (by omega)
30 
31 /-- The literal rational Bernstein polynomial, in its finite degree space. -/
32 def vector (n : ℕ) (k : Fin (n+1)) : Polynomial.degreeLT ℚ (n+1) :=
33   ⟨bernsteinPolynomial ℚ n k, Polynomial.mem_degreeLT.mpr
34     (Polynomial.degree_le_natDegree.trans_lt
35       (WithBot.coe_lt_coe.mpr (Nat.lt_succ_of_le (bernstein_natDegree_le n k))))⟩
36 
37 theorem independent (n : ℕ) : LinearIndependent ℚ (vector n) := by
38   apply LinearIndependent.of_comp (Polynomial.degreeLT ℚ (n+1)).subtype
39   exact bernsteinPolynomial.linearIndependent n
40 
41 /-- Actual rational basis inversion, obtained from the independent finite family. -/
42 def basis (n : ℕ) : Basis (Fin (n+1)) ℚ (Polynomial.degreeLT ℚ (n+1)) :=
43   basisOfLinearIndependentOfCardEqFinrank (independent n) (by
44     rw [Module.finrank_eq_card_basis (Polynomial.degreeLT.basis ℚ (n+1))])
45 
46 @[simp] theorem basis_val (n : ℕ) (i : Fin (n+1)) :
47     ((basis n i : Polynomial.degreeLT ℚ (n+1)) : ℚ[X]) = bernsteinPolynomial ℚ n i := by
48   simp only [basis, coe_basisOfLinearIndependentOfCardEqFinrank]
49   rfl
50 
51 /-- Rational Bernstein coordinates of a degree-bounded polynomial. -/
52 def coordinates (n : ℕ) (p : Polynomial.degreeLT ℚ (n+1)) : Fin (n+1) → ℚ :=
53   fun i => (basis n).repr p i
54 
55 theorem reconstruct (n : ℕ) (p : Polynomial.degreeLT ℚ (n+1)) :
56     ∑ i : Fin (n+1), C (coordinates n p i) * bernsteinPolynomial ℚ n i = (p : ℚ[X]) := by
57   have h := (basis n).sum_repr p
58   have hc := congrArg (fun z : Polynomial.degreeLT ℚ (n+1) => (z : ℚ[X])) h
59   simpa only [Submodule.coe_sum, Submodule.coe_smul, coordinates,
60     Polynomial.smul_eq_C_mul, basis_val] using hc
61 
62 /-- Fixed-degree rational monomial coordinates; the constant uses partition of unity directly. -/
63 def monomialCoordinates (n k : ℕ) : Fin (n+1) → ℚ :=
64   if k=0 then fun _ => 1 else if h : k≤n then
65     coordinates n ⟨X^k, Polynomial.mem_degreeLT.mpr
66       ((Polynomial.degree_X_pow_le k).trans_lt (WithBot.coe_lt_coe.mpr (Nat.lt_succ_of_le h)))⟩
67   else fun _ => 0
68 
69 @[simp] theorem monomialCoordinates_zero (n : ℕ) (i : Fin (n+1)) :
70     monomialCoordinates n 0 i = 1 := by simp [monomialCoordinates]
71 
72 theorem monomial_reconstruct (n k : ℕ) (hk : k≤n) :
73     ∑ i : Fin (n+1), C (monomialCoordinates n k i)*bernsteinPolynomial ℚ n i = X^k := by
74   by_cases h0 : k=0
75   · subst k
76     simpa only [monomialCoordinates_zero, map_one, one_mul, pow_zero,
77       Fin.sum_univ_eq_sum_range] using bernsteinPolynomial.sum ℚ n
78   · simp only [monomialCoordinates, h0, hk, ↓reduceIte]
79     exact reconstruct n _
80 
81 /-- The exact fixed-degree Bernstein coordinates of an affine power. -/
82 def affineCoordinates (n d : ℕ) (a w : ℚ) (i : Fin (n+1)) : ℚ :=
83   ∑ k : Fin (d+1), (d.choose k : ℚ)*a^(d-k.val)*w^k.val*monomialCoordinates n k i
84 
85 theorem affine_reconstruct (n d : ℕ) (hd : d≤n) (a w : ℚ) :
86     ∑ i : Fin (n+1), C (affineCoordinates n d a w i)*bernsteinPolynomial ℚ n i =
87       (C a+C w*X)^d := by
88   calc
89     _ = ∑ k : Fin (d+1), C ((d.choose k : ℚ)*a^(d-k.val)*w^k.val) *
90         (∑ i : Fin (n+1), C (monomialCoordinates n k i)*bernsteinPolynomial ℚ n i) := by
91       simp only [affineCoordinates, map_sum, map_mul, Finset.sum_mul, Finset.mul_sum]
92       rw [Finset.sum_comm]
93       apply Finset.sum_congr rfl
94       intro k _
95       apply Finset.sum_congr rfl
96       intro i _
97       ring
98     _ = ∑ k : Fin (d+1), C ((d.choose k : ℚ)*a^(d-k.val)*w^k.val)*X^k.val := by
99       apply Finset.sum_congr rfl
100       intro k _
101       rw [monomial_reconstruct n k (by omega)]
102     _ = (C a+C w*X)^d := by
103       rw [add_comm (C a), add_pow, ← Fin.sum_univ_eq_sum_range]
104       apply Finset.sum_congr rfl
105       intro k _
106       simp only [map_mul, map_pow, mul_pow, map_natCast]
107       ring
108 
109 @[simp] theorem affineCoordinates_zero_width (n d : ℕ) (a : ℚ) (i : Fin (n+1)) :
110     affineCoordinates n d a 0 i = a^d := by
111   unfold affineCoordinates
112   rw [Finset.sum_eq_single (0 : Fin (d+1))]
113   · simp
114   · intro k _ hk
115     have hne : k.val≠0 := by
116       intro h
117       apply hk
118       exact Fin.ext h
119     simp [zero_pow hne]
120   · simp
121 
122 /-- The same finite rational coordinate expression over the real parameters. -/
123 def affineReal (n d : ℕ) (a w : ℝ) (i : Fin (n+1)) : ℝ :=
124   ∑ k : Fin (d+1), (d.choose k : ℝ)*a^(d-k.val)*w^k.val*(monomialCoordinates n k i : ℝ)
125 
126 @[simp] theorem cast_affineCoordinates (n d : ℕ) (a w : ℚ) (i : Fin (n+1)) :
127     (affineCoordinates n d a w i : ℝ) = affineReal n d a w i := by
128   simp [affineCoordinates, affineReal]
129 
130 @[simp] theorem affineReal_zero_width (n d : ℕ) (a : ℝ) (i : Fin (n+1)) :
131     affineReal n d a 0 i = a^d := by
132   unfold affineReal
133   rw [Finset.sum_eq_single (0 : Fin (d+1))]
134   · simp
135   · intro k _ hk
136     have hne : k.val≠0 := by
137       intro h
138       apply hk
139       exact Fin.ext h
140     simp [zero_pow hne]
141   · simp
142 
143 theorem continuous_affineReal (n d : ℕ) (i : Fin (n+1)) :
144     Continuous (fun aw : ℝ×ℝ => affineReal n d aw.1 aw.2 i) := by
145   unfold affineReal
146   fun_prop
147 
148 end
149 end Komorebi.LSM.BernsteinRationalBasis

Back to source controls