BernsteinCellPositivity.lean

1 import KomorebiLSM.BernsteinRationalBasis
2 import KomorebiLSM.TensorBernsteinCertificate
3 import Mathlib.Topology.MetricSpace.Thickening
4 import Mathlib.Algebra.MvPolynomial.Degrees
5 
6 set_option autoImplicit false
7 namespace Komorebi.LSM.BernsteinCellPositivity
8 open scoped BigOperators
9 open MvPolynomial
10 open TensorBernsteinCertificate BernsteinRationalBasis
11 noncomputable section
12 
13 theorem affine_axis_reconstruct (n d : ℕ) (hd : d≤n) (a w : ℚ) (axis : Fin 2) :
14     ∑ i : Fin (n+1), C (affineCoordinates n d a w i)*basisPolynomial n i axis =
15       (C a+C w*X axis)^d := by
16   have h := congrArg (Polynomial.eval₂RingHom (C : ℚ →+* Polynomial₂) (X axis))
17     (affine_reconstruct n d hd a w)
18   simpa [basisPolynomial, bernsteinPolynomial, Polynomial.eval₂_pow, Polynomial.eval₂_sub] using h
19 
20 /-- The submitted coefficients are rational, with one fixed degree for all cells. -/
21 def coefficients (p : Polynomial₂) (a w : Fin 2 → ℚ) :
22     Fin (p.totalDegree+1) → Fin (p.totalDegree+1) → ℚ := fun i j =>
23   ∑ d ∈ p.support, p.coeff d *
24     affineCoordinates p.totalDegree (d 0) (a 0) (w 0) i *
25     affineCoordinates p.totalDegree (d 1) (a 1) (w 1) j
26 
27 /-- The real extension of the same finite rational formula. -/
28 def realCoefficients (p : Polynomial₂) (a w : Fin 2 → ℝ) :
29     Fin (p.totalDegree+1) → Fin (p.totalDegree+1) → ℝ := fun i j =>
30   ∑ d ∈ p.support, (p.coeff d : ℝ) *
31     affineReal p.totalDegree (d 0) (a 0) (w 0) i *
32     affineReal p.totalDegree (d 1) (a 1) (w 1) j
33 
34 @[simp] theorem cast_coefficients (p : Polynomial₂) (a w : Fin 2 → ℚ)
35     (i j : Fin (p.totalDegree+1)) :
36     (coefficients p a w i j : ℝ) =
37       realCoefficients p (fun k => (a k : ℝ)) (fun k => (w k : ℝ)) i j := by
38   simp [coefficients, realCoefficients]
39 
40 theorem support_degree (p : Polynomial₂) (d : Fin 2 →₀ ℕ) (hd : d∈p.support) (i : Fin 2) :
41     d i≤p.totalDegree :=
42   (MvPolynomial.monomial_le_degreeOf i hd).trans (MvPolynomial.degreeOf_le_totalDegree p i)
43 
44 theorem rational_reconstruction (p : Polynomial₂) (a w : Fin 2 → ℚ) :
45     MvPolynomial.bind₁ (fun axis => C (a axis)+C (w axis)*X axis) p =
46       tensorPolynomial (coefficients p a w) := by
47   have hexpand : MvPolynomial.bind₁ (fun axis => C (a axis)+C (w axis)*X axis) p =
48       ∑ d ∈ p.support, C (p.coeff d) *
49         (C (a 0)+C (w 0)*X 0)^(d 0) * (C (a 1)+C (w 1)*X 1)^(d 1) := by
50     change MvPolynomial.eval₂ C (fun axis => C (a axis)+C (w axis)*X axis) p = _
51     rw [MvPolynomial.eval₂_eq']
52     simp [Fin.prod_univ_two, mul_assoc]
53   rw [hexpand]
54   have hterm (d : Fin 2 →₀ ℕ) (hd : d∈p.support) :
55       C (p.coeff d) * (C (a 0)+C (w 0)*X 0)^(d 0) *
56         (C (a 1)+C (w 1)*X 1)^(d 1) =
57       ∑ i : Fin (p.totalDegree+1), ∑ j : Fin (p.totalDegree+1),
58         C (p.coeff d * affineCoordinates p.totalDegree (d 0) (a 0) (w 0) i *
59           affineCoordinates p.totalDegree (d 1) (a 1) (w 1) j) *
60           basisPolynomial p.totalDegree i 0 * basisPolynomial p.totalDegree j 1 := by
61     rw [← affine_axis_reconstruct p.totalDegree (d 0) (support_degree p d hd 0),
62       ← affine_axis_reconstruct p.totalDegree (d 1) (support_degree p d hd 1)]
63     simp only [Finset.mul_sum, Finset.sum_mul, map_mul]
64     rw [Finset.sum_comm]
65     apply Finset.sum_congr rfl
66     intro i _
67     apply Finset.sum_congr rfl
68     intro j _
69     ring
70   have hsum := Finset.sum_congr rfl hterm
71   rw [hsum]
72   unfold tensorPolynomial coefficients
73   simp only [map_sum, map_mul, Finset.sum_mul]
74   rw [Finset.sum_comm]
75   apply Finset.sum_congr rfl
76   intro i _
77   rw [Finset.sum_comm]
78 
79 theorem continuous_realCoefficients (p : Polynomial₂) (i j : Fin (p.totalDegree+1)) :
80     Continuous (fun aw : (Fin 2 → ℝ) × (Fin 2 → ℝ) => realCoefficients p aw.1 aw.2 i j) := by
81   unfold realCoefficients affineReal
82   fun_prop
83 
84 @[simp] theorem realCoefficients_zero_width (p : Polynomial₂) (a : Fin 2 → ℝ)
85     (i j : Fin (p.totalDegree+1)) : realCoefficients p a 0 i j = value p a := by
86   simp only [realCoefficients, Pi.zero_apply, affineReal_zero_width]
87   rw [value, MvPolynomial.eval₂_eq']
88   simp [Fin.prod_univ_two, mul_assoc]
89 
90 theorem square_compact : IsCompact square.domain := by
91   convert (isCompact_Icc : IsCompact (Set.Icc (fun _ : Fin 2 => (-1 : ℝ)) (fun _ => (1 : ℝ)))) using 1
92   ext a
93   simp [Rectangle.domain, square, Set.mem_Icc, Pi.le_def, forall_and]
94 
95 /-- Uniformity follows from a genuine compact zero-width set and continuity of the actual coefficients. -/
96 theorem positive_coefficients_near_zero (p : Polynomial₂)
97     (hp : ∀ a∈square.domain, 0<value p a) :
98     ∃ δ>0, ∀ a∈square.domain, ∀ w : Fin 2 → ℝ,
99       (∀ axis, |w axis|<δ) → ∀ i j, 0<realCoefficients p a w i j := by
100   let K : Set ((Fin 2 → ℝ) × (Fin 2 → ℝ)) := square.domain ×ˢ {0}
101   let U : Set ((Fin 2 → ℝ) × (Fin 2 → ℝ)) :=
102     {aw | ∀ i j, 0<realCoefficients p aw.1 aw.2 i j}
103   have hK : IsCompact K := square_compact.prod isCompact_singleton
104   have hU : IsOpen U := by
105     simp only [U, Set.ofPred_forall]
106     exact isOpen_iInter_of_finite (fun i => isOpen_iInter_of_finite (fun j =>
107       isOpen_lt continuous_const (continuous_realCoefficients p i j)))
108   have hKU : K⊆U := by
109     rintro ⟨a,w⟩ ⟨ha,hw⟩
110     have hw0 : w=0 := Set.mem_singleton_iff.mp hw
111     subst w
112     intro i j
113     rw [realCoefficients_zero_width]
114     exact hp a ha
115   obtain ⟨δ,hδ,hsub⟩ := hK.exists_thickening_subset_open hU hKU
116   refine ⟨δ,hδ,?_⟩
117   intro a ha w hw
118   have hwn : ‖w‖<δ := (pi_norm_lt_iff hδ).mpr (fun axis => by
119     simpa only [Real.norm_eq_abs] using hw axis)
120   change (a,w)∈U
121   apply hsub
122   apply Metric.mem_thickening_iff.mpr
123   refine ⟨(a,0),⟨ha,by simp⟩,?_⟩
124   simpa only [Prod.dist_eq, dist_self, dist_zero_right, max_eq_right (norm_nonneg w)] using hwn
125 
126 /-- Strict positivity on the square produces actual rational tensor witnesses on every sufficiently small cell. -/
127 theorem exists_small_positive (p : Polynomial₂) (hp : ∀ x∈square.domain, 0<value p x) :
128     ∃ δ>0, ∀ R : Rectangle, R.domain⊆square.domain →
129       (∀ axis, (R.width axis : ℝ)<δ) → Nonempty (LocalCertificate p R) := by
130   obtain ⟨δ,hδ,hcoeff⟩ := positive_coefficients_near_zero p hp
131   refine ⟨δ,hδ,?_⟩
132   intro R hR hw
133   have ha : (fun axis => (R.lo axis : ℝ))∈square.domain := by
134     apply hR
135     intro axis
136     refine ⟨le_rfl,?_⟩
137     change (R.lo axis : ℝ) ≤ (R.hi axis : ℝ)
138     exact_mod_cast (R.proper axis).le
139   have hc := hcoeff (fun axis => (R.lo axis : ℝ)) ha (fun axis => (R.width axis : ℝ))
140     (fun axis => by rw [abs_of_pos (R.width_pos axis)]; exact hw axis)
141   refine ⟨{
142     degreeX := p.totalDegree
143     degreeY := p.totalDegree
144     coefficient := coefficients p R.lo R.width
145     nonneg := ?_
146     identity := ?_ }⟩
147   · intro i j
148     have hreal : 0<(coefficients p R.lo R.width i j : ℝ) := by
149       rw [cast_coefficients]
150       exact hc i j
151     exact le_of_lt (by exact_mod_cast hreal)
152   · exact rational_reconstruction p R.lo R.width
153 
154 end
155 end Komorebi.LSM.BernsteinCellPositivity

Back to source controls