5.8 Cartesian disk connections
We identify the separated construction with the normalized Dunkl–Xu basis. The connection support and degree-padding results determine which finite matrix sections give the exact coefficients.
Let \(\mu \) be a measure on \([-1,1]\) and \(\nu \) a real measure. Write \(\bar\mu =\iota _*\mu \) for the real-coordinate measure. The \(k\)th outer measure is the shifted disk measure of Definition 5.3.37, using the transport of \(\bar\mu \) to \(D_k\). Its geometric Cartesian measure is the pushforward in Definition 5.3.42. A real source supported on \([-1,1]\) is transported to the interval without loss. A Cartesian disk system for \((\mu ,\nu )\) consists of an inner polynomial sequence \((q_k)\) and, for each \(k\), an outer polynomial sequence \((p_r^{[k]})\) such that \((q_k)\) is orthogonal for \(\nu \) and \((p_r^{[k]})\) for the \(k\)th outer measure, each \(q_k\) has the parity of \(k\), all leading coefficients are positive, and all squared norms are one. Its polynomials are
with \(L_k\) the parity lift of Definition 5.3.30; on the disk with \(|x|{\lt}1\) this is \(p_{n-k}^{[k]}(x)(1-x^2)^{k/2}q_k(y/\sqrt{1-x^2})\). At the tips \((\pm 1,0)\), the values are given by the polynomial lift \(L_kq_k\).
Lean Formalisation
def MvPolynomial.cartesianDiskPolynomial (p q : Polynomial ℝ) (k : ℕ) : MvPolynomial (Fin 2) ℝLean definition
/-- The polynomial Cartesian product of an outer factor and a parity-lifted inner factor. -/
noncomputable def cartesianDiskPolynomial (p q : ℝ[X]) (k : ℕ) :
MvPolynomial (Fin 2) ℝ := p.eval₂ C (X 0) * diskLift k qLet \(\mu \) and \(\nu \) be measures on \(\mathbb R\) with all polynomial moments finite and positive definite polynomial pairings. Suppose \(\mu \) assigns zero mass to \(\mathbb R\setminus [-1,1]\) and \(\nu \) is invariant under \(x\mapsto -x\). Then there exists a Cartesian disk system for the restriction of \(\mu \) to \([-1,1]\) and the inner measure \(\nu \).
Lean Formalisation
def MvPolynomial.cartesianDiskSystem (μ ν : MeasureTheory.Measure ℝ) [ν.IsNegInvariant] (hμ : Polynomial.HasFiniteMoments μ)
(hμpos : Polynomial.HasPositiveDefiniteIntegral μ) (hν : Polynomial.HasFiniteMoments ν)
(hνpos : Polynomial.HasPositiveDefiniteIntegral ν) (hx : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Icc (-1) 1) :
MvPolynomial.CartesianDiskSystem (MeasureTheory.Measure.comap Subtype.val μ) νLean definition
/-- Such systems exist for nondegenerate factors with even inner measure. -/
noncomputable def cartesianDiskSystem (μ ν : Measure ℝ) [ν.IsNegInvariant]
(hμ : Polynomial.HasFiniteMoments μ) (hμpos : Polynomial.HasPositiveDefiniteIntegral μ)
(hν : Polynomial.HasFiniteMoments ν) (hνpos : Polynomial.HasPositiveDefiniteIntegral ν)
(hx : ∀ᵐ x ∂μ, x ∈ Icc (-1 : ℝ) 1) : CartesianDiskSystem (Measure.comap (Subtype.val : Set.Icc (-1 : ℝ) 1 → ℝ) μ) ν := by
classical
choose Q hQ hQl hQn using exists_positive_orthonormal_sequence ν hν hνpos
have he (k : ℕ) := exists_positive_orthonormal_sequence (diskOuterMeasure k (μ.comap Subtype.val))
(hμ.diskOuterMeasure hx k) (hμpos.diskOuterMeasure hμ hx k)
choose P hP hPl hPn using he
refine ⟨P,Q,hQ,?_,hQ.coeff_eq_zero_of_parity hν hνpos,hQl,hPl,hQn,?_⟩
· simpa only [map_comap_subtype_coe measurableSet_Icc,
Measure.restrict_eq_self_of_ae_mem hx] using hP
· simpa only [map_comap_subtype_coe measurableSet_Icc,
Measure.restrict_eq_self_of_ae_mem hx] using hPnReference details: Moments supplied by a Cartesian disk system
A Cartesian disk system supplies all moments of both one-dimensional factors. If the outer measure is supported almost everywhere on \([-1,1]\), its Cartesian measure has all polynomial moments. More generally, finite moments of the two factors and this outer support condition suffice; no support condition on the inner factor is needed for this conclusion.
Lean Formalisation
theorem MvPolynomial.CartesianDiskSystem.hasFiniteMoments_inner {μ : MeasureTheory.Measure ↑(Set.Icc (-1) 1)}
{ν : MeasureTheory.Measure ℝ} (S : MvPolynomial.CartesianDiskSystem μ ν) : Polynomial.HasFiniteMoments νLean proof
/-- The inner family supplies all inner moments. -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem CartesianDiskSystem.hasFiniteMoments_inner {μ : Measure (Icc (-1 : ℝ) 1)} {ν : Measure ℝ}
(S : CartesianDiskSystem μ ν) : Polynomial.HasFiniteMoments ν :=
S.inner_orthogonal.hasFiniteMomentsAssume also that the inner measure \(\nu \) is supported in \([-1,1]\). The Cartesian polynomials are orthonormal and form a basis of every complete finite total-degree space. Their measure is positive definite on the polynomial algebra. No Jacobi formula is assumed for the one-dimensional factors.
Lean Formalisation
theorem MvPolynomial.integralInner_cartesianDiskPolynomial {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ]
[MeasureTheory.SFinite ν] (hx : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Icc (-1) 1) (p q r s : Polynomial ℝ) (k j : ℕ)
(hr : r.natDegree ≤ k) (hs : s.natDegree ≤ j) (hpr : ∀ (i : ℕ), i % 2 ≠ k % 2 → r.coeff i = 0)
(hps : ∀ (i : ℕ), i % 2 ≠ j % 2 → s.coeff i = 0)
(ho :
MeasureTheory.Integrable (fun x => Polynomial.eval (↑x) p * Polynomial.eval (↑x) q * √(1 - ↑x ^ 2) ^ (k + j))
(MeasureTheory.Measure.comap Subtype.val μ) := by
aesop (config := { enableSimp := false }) (rule_sets := [PolynomialIntegrability]))
(hi : MeasureTheory.Integrable (fun z => Polynomial.eval z r * Polynomial.eval z s) ν := by
aesop (config := { enableSimp := false }) (rule_sets := [PolynomialIntegrability])) :
MvPolynomial.integralInner
(MvPolynomial.cartesianDiskMeasure (MeasureTheory.Measure.comap Subtype.val μ)
(MeasureTheory.ProductMeasureInput.ofSFinite (MeasureTheory.Measure.comap Subtype.val μ) ν))
(MvPolynomial.IntegrablePair.of
(MvPolynomial.cartesianDiskMeasure (MeasureTheory.Measure.comap Subtype.val μ)
(MeasureTheory.ProductMeasureInput.ofSFinite (MeasureTheory.Measure.comap Subtype.val μ) ν))
(MvPolynomial.cartesianDiskPolynomial p r k) (MvPolynomial.cartesianDiskPolynomial q s j) ⋯) =
(∫ (x : ↑(Set.Icc (-1) 1)),
Polynomial.eval (↑x) p * Polynomial.eval (↑x) q *
√(1 - ↑x ^ 2) ^ (k + j) ∂MeasureTheory.Measure.comap Subtype.val μ) *
Polynomial.integralInner ν (Polynomial.IntegrablePair.of ν r s hi)Lean proof
/-- Arbitrary Cartesian polynomial pairings separate into two one-dimensional integrals. -/
theorem integralInner_cartesianDiskPolynomial {μ ν : Measure ℝ}
[SFinite μ] [SFinite ν] (hx : ∀ᵐ x ∂μ, x ∈ Icc (-1 : ℝ) 1)
(p q r s : ℝ[X]) (k j : ℕ) (hr : r.natDegree ≤ k) (hs : s.natDegree ≤ j)
(hpr : ∀ i, i % 2 ≠ k % 2 → r.coeff i = 0)
(hps : ∀ i, i % 2 ≠ j % 2 → s.coeff i = 0)
(ho : Integrable (fun x : Icc (-1 : ℝ) 1 => p.eval (x : ℝ)*q.eval (x : ℝ)*Real.sqrt (1-(x : ℝ)^2)^(k+j)) (μ.comap Subtype.val) := by
aesop (config := { enableSimp := false }) (rule_sets := [PolynomialIntegrability]))
(hi : Integrable (fun z => r.eval z*s.eval z) ν := by
aesop (config := { enableSimp := false }) (rule_sets := [PolynomialIntegrability])) :
integralInner (cartesianDiskMeasure (Measure.comap (Subtype.val : Set.Icc (-1 : ℝ) 1 → ℝ) μ) (ProductMeasureInput.ofSFinite (Measure.comap (Subtype.val : Set.Icc (-1 : ℝ) 1 → ℝ) μ) ν)) (IntegrablePair.of (cartesianDiskMeasure (Measure.comap (Subtype.val : Set.Icc (-1 : ℝ) 1 → ℝ) μ) (ProductMeasureInput.ofSFinite (Measure.comap (Subtype.val : Set.Icc (-1 : ℝ) 1 → ℝ) μ) ν)) (cartesianDiskPolynomial p r k) (cartesianDiskPolynomial q s j)
(h := by
exact integrable_cartesianDiskPolynomial_mul (μ := μ) (ν := ν) hx p q r s k j hr hs hpr hps ho hi)) =
(∫ x : Icc (-1 : ℝ) 1, p.eval (x : ℝ) * q.eval (x : ℝ) * Real.sqrt (1-(x : ℝ)^2)^(k+j) ∂μ.comap Subtype.val) *
Polynomial.integralInner ν (Polynomial.IntegrablePair.of ν r s (h := hi)) := by
let : SFinite (μ.comap (Subtype.val : Icc (-1 : ℝ) 1 → ℝ)) := by
refine ⟨⟨fun n => (sfiniteSeq μ n).comap Subtype.val, fun n => inferInstance, ?_⟩⟩
ext t ht
rw [Measure.sum_apply _ ht]
simp only [comap_subtype_coe_apply measurableSet_Icc]
rw [← Measure.sum_apply _ ((MeasurableEmbedding.subtype_coe measurableSet_Icc).measurableSet_image.mpr ht),
sum_sfiniteSeq]
simp only [integralInner, Polynomial.integralInner]
change (∫ v, eval v (cartesianDiskPolynomial p r k) *
eval v (cartesianDiskPolynomial q s j)
∂Measure.map diskCoordinates ((μ.comap Subtype.val).prod ν)) = _
erw [integral_map continuous_diskCoordinates.measurable.aemeasurable
((cartesianDiskPolynomial p r k).continuous_eval.mul
(cartesianDiskPolynomial q s j).continuous_eval).aestronglyMeasurable,
← integral_prod_mul]
apply integral_congr_ae
filter_upwards [] with v
dsimp only [diskCoordinates, Pi.mul_apply]
rw [eval_cartesianDiskPolynomial p r k hr hpr v.1 v.2 v.1.property,
eval_cartesianDiskPolynomial q s j hs hps v.1 v.2 v.1.property, pow_add]
ringWrite \(A(x)=1-x^2\). Let \(h,g\) be nonzero nonnegative polynomial densities for \(\mu ,\nu \), with \(g\) even and \(\deg g\le 2\ell \). The actual bivariate polynomial
changes the Cartesian measure to the pushforward of \(A^\ell h\, d\mu \otimes g\, d\nu \), provided the inner measure \(\nu \) is supported in \([-1,1]\). Under this support assumption the identity holds against all continuous real-valued test functions on \(\mathbb R^2\), in particular for polynomial pairings. The modified positive-leading orthonormal Cartesian system exists even when the density vanishes in the interior.
Lean Formalisation
theorem MvPolynomial.eval_cartesianDiskModification (h g : Polynomial ℝ) (l : ℕ) (hgdeg : g.natDegree ≤ 2 * l)
(hgpar : ∀ (i : ℕ), i % 2 ≠ 0 → g.coeff i = 0) (x z : ℝ) (hx : x ∈ Set.Icc (-1) 1) :
(MvPolynomial.eval ((fun v => ![v.1, √(1 - v.1 ^ 2) * v.2]) (x, z))) (MvPolynomial.cartesianDiskModification h g l) =
Polynomial.eval x (h.diskModificationWeight l) * Polynomial.eval z gLean proof
/-- The separated density formula, valid even at the vertical boundary. -/
theorem eval_cartesianDiskModification (h g : ℝ[X]) (l : ℕ)
(hgdeg : g.natDegree ≤ 2*l) (hgpar : ∀ i, i % 2 ≠ 0 → g.coeff i = 0)
(x z : ℝ) (hx : x ∈ Icc (-1 : ℝ) 1) :
eval ((fun v : ℝ × ℝ ↦ (![v.1, Real.sqrt (1-v.1^2)*v.2] : Fin 2 → ℝ)) (x,z)) (cartesianDiskModification h g l) =
(diskModificationWeight h l).eval x * g.eval z := by
rw [cartesianDiskModification, eval_cartesianDiskPolynomial h g (2*l) hgdeg
(by simpa using hgpar) x z hx, pow_mul,
Real.sq_sqrt (by nlinarith [hx.1,hx.2] : 0 ≤ 1-x^2)]
simp [diskModificationWeight,mul_comm]For the separated polynomial disk modification of Theorem 5.8.5, the coefficient from source \((n,k)\) to target \((m,j)\) can be nonzero only if
If \(\mu \) and \(h\) are also even and \(\deg h\le 2a\), this sharpens to
The unchanged-index coefficient is positive. These are support containments, not assertions that every permitted entry is nonzero.
Lean Formalisation
theorem MvPolynomial.CartesianDiskSystem.connectionEntry_eq_zero_of_outside_band {μ ν : MeasureTheory.Measure ℝ}
(S : MvPolynomial.CartesianDiskSystem (MeasureTheory.Measure.comap Subtype.val μ) ν) (h g : Polynomial ℝ) (l : ℕ)
(T :
MvPolynomial.CartesianDiskSystem
(MeasureTheory.Measure.comap Subtype.val (h.diskOuterModification l (MeasureTheory.Measure.comap Subtype.val μ)))
(g.polynomialDensityMeasure (MeasureTheory.Measure.comap Subtype.val ν)))
(hμ : Polynomial.HasFiniteMoments μ) (hν : Polynomial.HasFiniteMoments ν) (hx : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Icc (-1) 1)
(hh : ∀ᵐ (x : ℝ) ∂μ, 0 ≤ Polynomial.eval x h) (hg : ∀ᵐ (x : ℝ) ∂ν, 0 ≤ Polynomial.eval x g) [ν.IsNegInvariant]
(hgpar : ∀ (x : ℝ), Polynomial.eval (-x) g = Polynomial.eval x g) (hgdeg : g.natDegree ≤ 2 * l) {n k m j : ℕ}
(hk : k ≤ n) (hj : j ≤ m) (hout : ¬∃ s r, s ≤ h.natDegree + 2 * l ∧ r ≤ l ∧ n = m + s ∧ k = j + 2 * r) :
S.connectionEntry T n k m j ⋯ = 0Lean proof
/-- Without outer reflection symmetry, the same mechanism bounds all total-degree
steps while retaining the even inner-degree steps. -/
theorem connectionEntry_eq_zero_of_outside_band [ν.IsNegInvariant]
(hgpar : ∀ x, g.eval (-x) = g.eval x) (hgdeg : g.natDegree ≤ 2*l)
{n k m j : ℕ} (hk : k ≤ n) (hj : j ≤ m)
(hout : ¬ ∃ s r : ℕ, s ≤ h.natDegree+2*l ∧ r ≤ l ∧ n=m+s ∧ k=j+2*r) :
S.connectionEntry T n k m j = 0 := by
by_cases hb : k < j ∨ j+g.natDegree < k
· exact S.connectionEntry_eq_zero_of_inner_band h g l T hμ hν hx hh hg hb
by_cases hp : k % 2 ≠ j % 2
· exact S.connectionEntry_eq_zero_of_inner_parity h g l T hμ hν hx hh hg hgpar hp
have hkj : k=j+2*((k-j)/2) := by omega
have hr : (k-j)/2 ≤ l := by omega
by_cases ho : n < m ∨ m+h.natDegree+2*l < n
· exact S.connectionEntry_eq_zero_of_outer_band h g l T hμ hν hx hh hg hk hj hkj hr ho
exfalso
apply hout
exact ⟨n-m,(k-j)/2,by omega,hr,by omega,hkj⟩Assume the source and target factor measures are supported in \([-1,1]\). On every complete degree space, the connection matrix consists of the mixed integral coefficients of Theorem 5.8.6 and factors the modified Gram matrix as \(R^\top R\). The support bounds of Theorem 5.8.6 therefore apply to these finite matrices uniformly in the truncation degree.
Lean Formalisation
theorem MvPolynomial.CartesianDiskSystem.connectionMatrix_apply {μ ν μ' ν' : MeasureTheory.Measure ℝ}
[MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure μ']
[MeasureTheory.IsFiniteMeasure ν']
(S : MvPolynomial.CartesianDiskSystem (MeasureTheory.Measure.comap Subtype.val μ) ν)
(T : MvPolynomial.CartesianDiskSystem (MeasureTheory.Measure.comap Subtype.val μ') ν')
(hx : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Icc (-1) 1) (hz : ∀ᵐ (z : ℝ) ∂ν, z ∈ Set.Icc (-1) 1)
(hx' : ∀ᵐ (x : ℝ) ∂μ', x ∈ Set.Icc (-1) 1) (hz' : ∀ᵐ (z : ℝ) ∂ν', z ∈ Set.Icc (-1) 1) (N : ℕ)
(i j : { d // (d.sum fun x e => e) ≤ N }) :
S.connectionMatrix T hx hz hx' hz' N i j = S.connectionEntry T (↑j 0 + ↑j 1) (↑j 1) (↑i 0 + ↑i 1) (↑i 1) ⋯Lean proof
/-- Finite sections use the same entries as the integral connection. -/
theorem connectionMatrix_apply (N : ℕ)
(i j : {d : Fin 2 →₀ ℕ // d.sum (fun _ e => e) ≤ N}) :
S.connectionMatrix T hx hz hx' hz' N i j =
S.connectionEntry T (j.1 0+j.1 1) (j.1 1) (i.1 0+i.1 1) (i.1 1) := by
change (T.degreeBasis hx' hz' N).repr (S.degreeBasis hx hz N j) i = _
rw [T.degreeBasis_repr hx' hz']
simp only [S.degreeBasis_apply]
exact integralInner_comm _ _ _For the symmetric Jacobi factors of the standard disk weight, every positive-leading orthonormal Cartesian realization equals the existing normalized Dunkl–Xu basis. Raw Jacobi-normalized disk polynomials differ by positive scalars. Thus the support statements apply in the original total-degree and increasing inner-index convention, without changing bases within degree blocks.
Lean Formalisation
theorem MvPolynomial.dunklXuDisk_eq_pos_smul_cartesian {β : ℝ} (hβ : -1 < β)
(S :
MvPolynomial.CartesianDiskSystem
(MeasureTheory.Measure.comap Subtype.val (Polynomial.jacobiMeasure (β + 1 / 2) (β + 1 / 2)))
(Polynomial.jacobiMeasure β β))
(n k : ℕ) : ∃ c, 0 < c ∧ MvPolynomial.dunklXuDisk β n k = c • S.polynomial n kLean proof
/-- The raw Jacobi-normalized disk polynomial is a positive scalar multiple
of every positive-leading orthonormal Cartesian realization. -/
theorem dunklXuDisk_eq_pos_smul_cartesian {β : ℝ} (hβ : -1 < β)
(S : CartesianDiskSystem (Measure.comap (Subtype.val : Set.Icc (-1 : ℝ) 1 → ℝ) (jacobiMeasure (β+1/2) (β+1/2))) (jacobiMeasure β β))
(n k : ℕ) : ∃ c : ℝ, 0 < c ∧ dunklXuDisk β n k = c • S.polynomial n k := by
have ha : -1 < β+1/2 := by linarith
have hak : -1 < (β+1/2)+(k : ℝ) := by have := Nat.cast_nonneg (α := ℝ) k; linarith
let J := jacobiSequence hβ hβ
let K := jacobiSequence hak hak
have hJ : J.IsOrthogonal (jacobiMeasure β β) := isOrthogonal_jacobiSequence hβ hβ
have hK : K.IsOrthogonal (diskOuterMeasure k ((jacobiMeasure (β+1/2) (β+1/2)).comap Subtype.val)) :=
isOrthogonal_jacobiSequence_diskOuterMeasure ha k
have hjpos : 0 < (J k).leadingCoeff := by
change 0 < (J k).coeff (J k).natDegree
rw [J.natDegree_eq]
exact coeff_jacobi_self_pos hβ hβ k
have hkpos : 0 < (K (n-k)).leadingCoeff := by
change 0 < (K (n-k)).coeff (K (n-k)).natDegree
rw [K.natDegree_eq]
exact coeff_jacobi_self_pos hak hak (n-k)
let ci := (J k).leadingCoeff/(S.inner k).leadingCoeff
let co := (K (n-k)).leadingCoeff/(S.outer k (n-k)).leadingCoeff
have hi : jacobi β β k = ci • S.inner k :=
S.inner_orthogonal.eq_leadingCoeff_div_smul
(hasFiniteMoments_jacobiMeasure hβ hβ)
(hasPositiveDefiniteIntegral_jacobiMeasure hβ hβ) hJ k
have ho : jacobi ((β+1/2)+k) ((β+1/2)+k) (n-k) = co • S.outer k (n-k) :=
(S.outer_orthogonal_real k (ae_mem_Icc_jacobiMeasure _ _)).eq_leadingCoeff_div_smul
((hasFiniteMoments_jacobiMeasure ha ha).diskOuterMeasure
(ae_mem_Icc_jacobiMeasure _ _) k)
((hasPositiveDefiniteIntegral_jacobiMeasure ha ha).diskOuterMeasure
(hasFiniteMoments_jacobiMeasure ha ha) (ae_mem_Icc_jacobiMeasure _ _) k) hK (n-k)
refine ⟨co*ci,mul_pos (div_pos hkpos (S.outer_leadingCoeff_pos k (n-k)))
(div_pos hjpos (S.inner_leadingCoeff_pos k)),?_⟩
rw [dunklXuDisk,show β+(k : ℝ)+1/2=(β+1/2)+k by ring,ho,hi,diskLift_smul]
simp only [Polynomial.smul_eq_C_mul,Polynomial.eval₂_mul,Polynomial.eval₂_C,
CartesianDiskSystem.polynomial,cartesianDiskPolynomial,MvPolynomial.smul_eq_C_mul,map_mul]
ringFor every \(\beta {\gt}-1\) and every complete finite degree section, multiplying the disk weight by \(x^2y^2\) gives normalized connection support contained in
Multiplication by \((1-x^2-y^2)(2-2x^2-y^2)\) gives support contained in
Both factors have positive diagonal, with at most six or nine permitted positions per column, respectively; invalid degree/inner-index pairs are omitted.
Lean Formalisation
theorem MvPolynomial.cartesianDiskModification_X_sq :
MvPolynomial.cartesianDiskModification (Polynomial.X ^ 2) (Polynomial.X ^ 2) 1 =
MvPolynomial.X 0 ^ 2 * MvPolynomial.X 1 ^ 2Lean proof
/-- The first separated modification is exactly x²y². -/
theorem cartesianDiskModification_X_sq :
cartesianDiskModification (Polynomial.X^2) (Polynomial.X^2) 1 =
(X 0)^2*(X 1)^2 := by
norm_num [cartesianDiskModification,cartesianDiskPolynomial,diskLift,Finset.sum_range_succ]Let \(W\) be the exact leading section of polynomial multiplication in the raw Dunkl–Xu basis, and let \(D\) contain the positive raw basis norms. For a separated modification as in Theorem 5.8.5 (\(h,g\) nonzero nonnegative densities, \(g\) even, \(\deg g\le 2\ell \)), its normalized connection satisfies \(R^\top R=DWD^{-1}\). If \(h\) is moreover even, then under a degree/inner-index ordered enumeration any exact unpivoted \(W=LU\) with unit lower triangular \(L\) and upper triangular \(U\) has \(U_{ij}=0\) if and only if \(R_{ij}=0\). In particular the six- and nine-position bounds transfer to the raw upper factor.
Lean Formalisation
theorem MvPolynomial.integralInner_mul_normalizedDunklXuDegreeBasis {β : ℝ} (hβ : -1 < β) (u : MvPolynomial (Fin 2) ℝ) (N : ℕ)
(i j : { d // (d.sum fun x e => e) ≤ N }) :
MvPolynomial.integralInner (MvPolynomial.dunklXuDiskMeasure β)
(MvPolynomial.IntegrablePair.of (MvPolynomial.dunklXuDiskMeasure β)
(u * ↑((MvPolynomial.normalizedDunklXuDegreeBasis hβ N) i))
↑((MvPolynomial.normalizedDunklXuDegreeBasis hβ N) j) ⋯) =
MvPolynomial.dunklXuNorm β ⟨(↑i 0 + ↑i 1, ↑i 1), ⋯⟩ * MvPolynomial.dunklXuMultiplicationSection hβ u N i j *
(MvPolynomial.dunklXuNorm β ⟨(↑j 0 + ↑j 1, ↑j 1), ⋯⟩)⁻¹Lean proof
/-- Norm scaling turns raw multiplication entries into normalized Gram entries. -/
theorem integralInner_mul_normalizedDunklXuDegreeBasis {β : ℝ} (hβ : -1 < β)
(u : MvPolynomial (Fin 2) ℝ) (N : ℕ)
(i j : {d : Fin 2 →₀ ℕ // d.sum (fun _ e => e) ≤ N}) :
integralInner (dunklXuDiskMeasure β) (IntegrablePair.of (dunklXuDiskMeasure β) (u*(normalizedDunklXuDegreeBasis hβ N i : MvPolynomial (Fin 2) ℝ)) (normalizedDunklXuDegreeBasis hβ N j)) =
dunklXuNorm β ⟨((i.1 0+i.1 1), (i.1 1)), by exact hasFiniteMoments_dunklXuDiskMeasure (by linarith) _⟩ * dunklXuMultiplicationSection hβ u N i j *
(dunklXuNorm β ⟨((j.1 0+j.1 1), (j.1 1)), by exact hasFiniteMoments_dunklXuDiskMeasure (by linarith) _⟩)⁻¹ := by
rw [integralInner_mul_left_right]
simp only [normalizedDunklXuDegreeBasis_apply]
rw [← normalizedDunklXuBasis_repr_eq_integralInner,
normalizedDunklXuBasis_repr,normalizedDunklXuBasis_apply,
mul_smul_comm,map_smul,Finsupp.smul_apply,smul_eq_mul]
unfold dunklXuMultiplicationSection
ringReference details: Symmetric polynomial degree projections
The finite orthonormal degree basis defines a polynomial projection by integral coordinates. It is symmetric for the polynomial pairing and fixes every polynomial through its degree cutoff.
Lean Formalisation
theorem MvPolynomial.integralProjection_symmetric.{u_1, u_2} {σ : Type u_1} {ι : Type u_2} [Fintype σ] [Fintype ι]
(μ : MeasureTheory.Measure (σ → ℝ)) (hμ : MvPolynomial.HasFiniteMoments μ) {V : Submodule ℝ (MvPolynomial σ ℝ)}
(b : Module.Basis ι ℝ ↥V) (p q : MvPolynomial σ ℝ) :
MvPolynomial.integralInner μ (MvPolynomial.IntegrablePair.of μ ((MvPolynomial.integralProjection μ hμ b) p) q ⋯) =
MvPolynomial.integralInner μ (MvPolynomial.IntegrablePair.of μ p ((MvPolynomial.integralProjection μ hμ b) q) ⋯)Lean proof
/-- The projection is symmetric for the integral pairing. -/
theorem integralProjection_symmetric (p q : MvPolynomial σ ℝ) :
integralInner μ (IntegrablePair.of μ (integralProjection μ hμ b p) q) =
integralInner μ (IntegrablePair.of μ p (integralProjection μ hμ b q)) := by
change integralBilinForm μ hμ (∑ i, integralBilinForm μ hμ (b i) p • (b i : MvPolynomial σ ℝ)) q =
integralBilinForm μ hμ p (∑ i, integralBilinForm μ hμ (b i) q • (b i : MvPolynomial σ ℝ))
simp only [map_sum,map_smul,LinearMap.sum_apply,LinearMap.smul_apply,smul_eq_mul]
apply Finset.sum_congr rfl
intro i _
change integralInner μ (IntegrablePair.of μ (b i) p) * integralInner μ (IntegrablePair.of μ (b i) q) =
integralInner μ (IntegrablePair.of μ (b i) q) * integralInner μ (IntegrablePair.of μ p (b i))
rw [integralInner_comm μ p]
ringCompress coordinate multiplication at degree \(N+2\). For any two quadratics \(a+bx^2+cy^2\) and \(d+ex^2+fy^2\), the leading raw Dunkl–Xu coefficients through degree \(N\) of their product, formed from those compressed coordinate operators, agree exactly with full polynomial multiplication followed by leading extraction. Equivalently, \(B\) output degree blocks require \(B+2\) coordinate blocks. This applies to both preceding quartic modifications.
Lean Formalisation
theorem MvPolynomial.compressedMul_sq_apply_eq.{u_1} {σ : Type u_1} (T : MvPolynomial σ ℝ →ₗ[ℝ] MvPolynomial σ ℝ) (N : ℕ)
(hT : ∀ (p : MvPolynomial σ ℝ), p.totalDegree ≤ N → T p = p) (u p : MvPolynomial σ ℝ)
(hp : p.totalDegree + 2 * u.totalDegree ≤ N) : (MvPolynomial.compressedMul T u ^ 2) p = u ^ 2 * pLean proof
/-- Two padded multiplication steps agree with the full polynomial product. -/
theorem compressedMul_sq_apply_eq (T : MvPolynomial σ ℝ →ₗ[ℝ] MvPolynomial σ ℝ)
(N : ℕ) (hT : ∀ p, p.totalDegree ≤ N → T p=p)
(u p : MvPolynomial σ ℝ) (hp : p.totalDegree+2*u.totalDegree ≤ N) :
((compressedMul T u)^2) p = u^2*p := by
have hp' : p.totalDegree ≤ N := by omega
have hup : (u*p).totalDegree ≤ N := (totalDegree_mul _ _).trans (by omega)
have huup : (u*(u*p)).totalDegree ≤ N := by
have h₁ := totalDegree_mul u (u*p)
have h₂ := totalDegree_mul u p
omega
rw [pow_two]
change T (u*T (T (u*T p))) = u^2*p
rw [hT p hp',hT (u*p) hup,hT (u*p) hup,hT (u*(u*p)) huup]
ringIt does not assert exactness of the entire quartic output in the padded space.