5.6 Separated Koornwinder systems
Separation of variables reduces parts of the conversion problem to one-dimensional polynomial families. The results specify the scale function and basis ordering on which the connection support depends.
Reference details: Vertical coefficient truncation and related results
For \(p\in R[X]\) over a commutative ring and \(n\in \mathbb {N}\), define
Lean Formalisation
def MvPolynomial.verticalTruncation.{u_1} {R : Type u_1} [CommRing R] (n : ℕ) (p : Polynomial R) : MvPolynomial (Fin 2) RLean definition
/-- Truncate a univariate coefficient expansion and regard it as a polynomial in `y`.
This is the classical polynomial content of the zero-step separated lift. -/
noncomputable def verticalTruncation (n : ℕ) (p : Polynomial R) : MvPolynomial (Fin 2) R :=
∑ j ∈ Finset.range (n + 1), C (p.coeff j) * X 1 ^ jThis construction has no scaling parameter.
The total degree of \(V_n(p)\) is at most \(n\). If \(\deg p\le n\), then \(V_n(p)(x,y)=p(y)\). If in addition every nonzero coefficient \(p_j\) with \(j\le n\) has \(j=n\), then \(V_n(p)(x,\rho z)=\rho ^n p(z)\) for every \(\rho ,z\), including \(\rho =0\).
Lean Formalisation
theorem MvPolynomial.eval_verticalTruncation.{u_1} {R : Type u_1} [CommRing R] (n : ℕ) (p : Polynomial R) (hp : p.natDegree ≤ n)
(v : Fin 2 → R) : (MvPolynomial.eval v) (MvPolynomial.verticalTruncation n p) = Polynomial.eval (v 1) pLean proof
/-- Truncation retains evaluation when the degree is within the cutoff. -/
theorem eval_verticalTruncation (n : ℕ) (p : Polynomial R) (hp : p.natDegree ≤ n)
(v : Fin 2 → R) : eval v (verticalTruncation n p) = p.eval (v 1) := by
rw [verticalTruncation, map_sum, Polynomial.eval_eq_sum_range' (by omega : p.natDegree < n+1)]
simpFor \(b\in R[x]\), a step \(s\ge 1\) and \(n\in \mathbb {N}\), define
Lean Formalisation
def MvPolynomial.scaledLift.{u_1} {R : Type u_1} [CommRing R] (a : Polynomial R) (step : ℕ+) (n : ℕ) (p : Polynomial R) :
MvPolynomial (Fin 2) RLean definition
/-- Division-free lift for a scale whose specified power is polynomial. -/
noncomputable def scaledLift (a : Polynomial R) (step : ℕ+) (n : ℕ) (p : Polynomial R) :
MvPolynomial (Fin 2) R :=
∑ j ∈ Finset.range (n+1), C (p.coeff j) * X 1 ^ j *
a.eval₂ C (X 0) ^ ((n-j)/(step : ℕ))If \(\deg q\le n\), every nonzero \(q_j\) has \(s\mid n-j\), \(b(x)=\rho ^s\) and \(y=\rho z\), then \(L_{s,n}(q)(x,y)=\rho ^nq(z)\); no condition \(\rho \ne 0\) is needed. If \(\deg b\le s\), then \(L_{s,n}(q)\) has total degree at most \(n\). For \(s=2\) and \(b=1-x^2\) it is the disk lift of Definition 5.3.30.
Lean Formalisation
theorem MvPolynomial.eval_scaledLift.{u_1} {R : Type u_1} [CommRing R] (a : Polynomial R) (step : ℕ+) (n : ℕ) (p : Polynomial R)
(hp : p.natDegree ≤ n) (hpar : ∀ j ≤ n, p.coeff j ≠ 0 → ↑step ∣ n - j) (v : Fin 2 → R) (s z : R)
(hs : Polynomial.eval (v 0) a = s ^ ↑step) (hy : v 1 = s * z) :
(MvPolynomial.eval v) (MvPolynomial.scaledLift a step n p) = s ^ n * Polynomial.eval z pLean proof
/-- The scaled-coordinate evaluation formula, including zero-scale boundary points. -/
theorem eval_scaledLift (a : Polynomial R) (step : ℕ+) (n : ℕ) (p : Polynomial R)
(hp : p.natDegree ≤ n)
(hpar : ∀ j ≤ n, p.coeff j ≠ 0 → (step : ℕ) ∣ n-j)
(v : Fin 2 → R) (s z : R) (hs : a.eval (v 0) = s^(step : ℕ)) (hy : v 1 = s*z) :
eval v (scaledLift a step n p) = s^n * p.eval z := by
rw [scaledLift, map_sum, Polynomial.eval_eq_sum_range' (by omega : p.natDegree < n+1),
Finset.mul_sum]
apply Finset.sum_congr rfl
intro j hj
simp only [map_mul, map_pow, eval_C, eval_X, eval_eval₂_C_X, hs, hy]
by_cases hz : p.coeff j = 0
· simp [hz]
have hjn : j ≤ n := by simpa only [Finset.mem_range, Nat.lt_succ_iff] using hj
have he : j+(step : ℕ)*((n-j)/(step : ℕ)) = n := by
rw [Nat.mul_div_cancel' (hpar j hjn hz)]
omega
rw [mul_pow, ← pow_mul]
calc
p.coeff j * (s^j*z^j) * s^((step : ℕ)*((n-j)/(step : ℕ))) =
(s^j*s^((step : ℕ)*((n-j)/(step : ℕ)))) * (p.coeff j*z^j) := by ring
_ = s^n * (p.coeff j*z^j) := by rw [← pow_add, he]For a real polynomial \(a\) and \(k\in \mathbb N\), let \(D_{a,k}=\{ x\in \mathbb R:a(x)^k\ge 0\} \). For a source measure \(\eta \) on this domain, the \(k\)th outer measure is the polynomial density measure \(a^k\, d\eta \), transported to real coordinates. For even \(k\), the source domain is all of \(\mathbb R\).
Lean Formalisation
def Polynomial.koornwinderOuterMeasure (a : Polynomial ℝ) (k : ℕ)
(μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval x (a ^ k) }) : MeasureTheory.Measure ℝLean definition
/-- The degree-k measure lives on the nonnegative locus of the degree-k density. -/
noncomputable def koornwinderOuterMeasure (a : ℝ[X]) (k : ℕ)
(μ : Measure {x : ℝ // 0 ≤ (a^k).eval x}) : Measure ℝ :=
polynomialDensityMeasure (a^k) μFor a measurable set \(E\), the \(k\)th outer measure assigns \(\int _{\iota ^{-1}(E)}a(x)^k\, d\eta (x)\) as a nonnegative integral. At degree zero, transporting any real source measure to \(D_{a,0}=\mathbb R\) and applying this construction recovers that measure.
Lean Formalisation
theorem Polynomial.koornwinderOuterMeasure_apply (a : Polynomial ℝ) (k : ℕ)
(μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval x (a ^ k) }) {s : Set ℝ} (hs : MeasurableSet s) :
(a.koornwinderOuterMeasure k μ) s =
∫⁻ (x : { x // 0 ≤ Polynomial.eval x (a ^ k) }) in Subtype.val ⁻¹' s,
↑(NNReal.mk (Polynomial.eval (↑x) (a ^ k)) ⋯) ∂μLean proof
/-- The shifted measure is characterized by its nonnegative source integral. -/
theorem koornwinderOuterMeasure_apply (a : ℝ[X]) (k : ℕ)
(μ : Measure {x : ℝ // 0 ≤ (a^k).eval x}) {s : Set ℝ} (hs : MeasurableSet s) :
koornwinderOuterMeasure a k μ s =
∫⁻ x in Subtype.val ⁻¹' s,
ENNReal.ofNNReal (NNReal.mk ((a^k).eval (x : ℝ)) x.property) ∂μ :=
polynomialDensityMeasure_apply (a^k) μ hsLet \(D\subseteq \mathbb R\) be an outer domain, \(\mu \) a measure on \(D\), \(\nu \) a measure on \(\mathbb R\), \(\rho :D\to \mathbb R\) a scale and \(a\) a polynomial. Write \(\bar\mu =\iota _*\mu \), where \(\iota :D\hookrightarrow \mathbb R\) is the real coordinate map. When \(a\ge 0\) almost everywhere for \(\bar\mu \), transport \(\bar\mu \) to \(D_{a,k}\) and let \(\mu _k\) be its degree-dependent outer measure from Definition 5.6.5. Let \(\omega \) be the pushforward of \(\mu \otimes \nu \) by \((x,z)\mapsto (\iota (x),\rho (x)z)\). The input includes almost-everywhere measurability certificates for both the product kernel \(x\mapsto (z\mapsto (x,z))_*\nu \) and the coordinate map \((x,z)\mapsto (x,\rho (x)z)\) under \(\mu \otimes \nu \). The scale may be discontinuous, and no interval support condition is imposed. Global scales use \(D=\mathbb R\). A real measure supported almost everywhere in a measurable \(D\) is represented by its restriction to that domain; its coordinate pushforward recovers the original measure.
Lean Formalisation
def MvPolynomial.koornwinderCoordinates {D : Set ℝ} (ρ : ↑D → ℝ) (v : ↑D × ℝ) : Fin 2 → ℝLean definition
/-- Separated coordinates with an arbitrary continuous scale. -/
def koornwinderCoordinates (ρ : D → ℝ) (v : D × ℝ) : Fin 2 → ℝ := ![(v.1 : ℝ), ρ v.1*v.2]Theorem 5.6.9 assumes \(\rho \) continuous with \(\rho ^2=a\) almost everywhere for \(\mu \).
Write \(\Phi (x,z)=(\iota (x),\rho (x)z)\) for the separated coordinate map and \(\omega =\Phi _*(\mu \otimes \nu )\) for the measure of Definition 5.6.7. An s-finite inner measure makes the product kernel almost-everywhere measurable; if \(\rho \) is continuous, \(\Phi \) is also almost-everywhere measurable. In particular, finite polynomial moments of the inner measure suffice. For every measurable set \(A\), \(\omega (A)=(\mu \otimes \nu )(\Phi ^{-1}(A))\). If \(f\) is \(\omega \)-integrable, then \(f\circ \Phi \) is \(\mu \otimes \nu \)-integrable and
Lean Formalisation
theorem MvPolynomial.KoornwinderMeasureInput.ofContinuous {D : Set ℝ} {ρ : ↑D → ℝ} (μ : MeasureTheory.Measure ↑D)
(ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] (hρ : Continuous ρ) :
MvPolynomial.KoornwinderMeasureInput ρ μ νLean proof
/-- Continuous scales and s-finite inner factors supply both certificates. -/
theorem KoornwinderMeasureInput.ofContinuous {ρ : D → ℝ} (μ : Measure D) (ν : Measure ℝ)
[SFinite ν] (hρ : Continuous ρ) : KoornwinderMeasureInput ρ μ ν :=
⟨Measurable.map_prodMk_left.aemeasurable,
(continuous_koornwinderCoordinates hρ).measurable.aemeasurable⟩If \(\bar\mu \) and \(\nu \) have finite polynomial moments, so does \(\omega \). The scale is continuous and its square agrees \(\mu \)-almost everywhere with the polynomial \(a\).
Lean Formalisation
theorem MvPolynomial.hasFiniteMoments_koornwinderMeasure {D : Set ℝ} {μ : MeasureTheory.Measure ↑D}
{ν : MeasureTheory.Measure ℝ} {ρ : ↑D → ℝ}
(hμ : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ)) (hν : Polynomial.HasFiniteMoments ν)
(hρ : Continuous ρ) (a : Polynomial ℝ) (ha : ∀ᵐ (x : ↑D) ∂μ, ρ x ^ 2 = Polynomial.eval (↑x) a) :
MvPolynomial.HasFiniteMoments (MvPolynomial.koornwinderMeasure ρ μ ν ⋯)Lean proof
/-- Finite moments of both factors give finite moments after separated transport. -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasFiniteMoments_koornwinderMeasure {D : Set ℝ} {μ : Measure D} {ν : Measure ℝ} {ρ : D → ℝ}
(hμ : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ)) (hν : Polynomial.HasFiniteMoments ν)
(hρ : Continuous ρ) (a : ℝ[X]) (ha : ∀ᵐ x ∂μ, ρ x^2 = a.eval (x : ℝ)) :
HasFiniteMoments (koornwinderMeasure ρ μ ν) := by
let := hμ.isFiniteMeasure
let := Measure.isFiniteMeasure_of_map (μ := μ) measurable_subtype_coe.aemeasurable
let := hν.isFiniteMeasure
have hall (p : MvPolynomial (Fin 2) ℝ) :
MemLp (fun v => eval v p) 2 (koornwinderMeasure ρ μ ν) := by
induction p using MvPolynomial.induction_on' with
| add p q hp hq =>
exact MemLp.ae_eq (Filter.Eventually.of_forall (fun v => (map_add (eval v) p q).symm))
(hp.add hq)
| monomial d c =>
apply (memLp_two_iff_integrable_sq (monomial d c).continuous_eval.aestronglyMeasurable).mpr
change Integrable ((fun v => eval v (monomial d c))^2) _
rw [koornwinderMeasure, integrable_map_measure
((monomial d c).continuous_eval.pow 2).aestronglyMeasurable
(continuous_koornwinderCoordinates hρ).measurable.aemeasurable]
have hx := hμ.integrable_mul
(Polynomial.C (c^2)*Polynomial.X^(2*d 0)*a^(d 1)) 1
have hx' : Integrable (fun x : D =>
(Polynomial.C (c^2)*Polynomial.X^(2*d 0)*a^(d 1)).eval (x : ℝ) *
(1 : ℝ[X]).eval (x : ℝ)) μ :=
(integrable_map_measure
(((Polynomial.C (c^2)*Polynomial.X^(2*d 0)*a^(d 1)).continuous.mul
(1 : ℝ[X]).continuous).aestronglyMeasurable)
measurable_subtype_coe.aemeasurable).mp hx
have hz := hν (Polynomial.X^(d 1))
have hi := hx'.mul_prod hz
apply hi.congr
filter_upwards [Measure.quasiMeasurePreserving_fst.ae ha] with v hv
simp only [Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow,
Polynomial.eval_X, Polynomial.eval_one, mul_one] at *
simp only [Function.comp_def, Pi.pow_apply, eval_monomial]
rw [Finsupp.prod_fintype _ _ (by simp)]
simp only [
Fin.prod_univ_two, koornwinderCoordinates, Matrix.cons_val_zero, Matrix.cons_val_one]
rw [← hv]
simp only [mul_pow, ← pow_mul, Nat.mul_comm]
ring
intro p
exact (memLp_two_iff_integrable_sq p.continuous_eval.aestronglyMeasurable).mp (hall p)Require \(a(\iota (x))\ge 0\) almost everywhere for \(\mu \). Choose positive-leading orthonormal sequences \(q_k\) for \(\nu \) and \(p_r^{[k]}\) for \(\mu _k\), together with polynomial lifts \(L_k\) satisfying \(L_k(x,\rho (x)z)=\rho (x)^kq_k(z)\) almost everywhere in \(x\). Set \(P_{n,k}=p_{n-k}^{[k]}L_k\) for \(0\le k\le n\). Two constructions of such systems are defined, under finite moments and positive definite polynomial pairings for \(\bar\mu \) and \(\nu \): one for a nonzero polynomial scale \(c\) restricted to \(D\) (\(a=c^2\)), and one for \(\rho (x)=\sqrt{a(\iota (x))}\) on \(D=\{ x\in \mathbb R:a(x)\ge 0\} \) when \(a\ne 0\) and \(\nu \) is even. The square-root scale has no values outside \(D\). The label \(n\) is the separated index.
Lean Formalisation
inductive MvPolynomial.KoornwinderSystem {D : Set ℝ} (a : Polynomial ℝ) (ρ : ↑D → ℝ) (μ : MeasureTheory.Measure ↑D)
(ν : MeasureTheory.Measure ℝ) : TypeLean definition
/-- Normalized separated data with polynomial inner lifts. -/
structure KoornwinderSystem {D : Set ℝ} (a : ℝ[X]) (ρ : D → ℝ) (μ : Measure D) (ν : Measure ℝ) where
/-- The squared scale is nonnegative on the outer source. -/
scale_nonneg : ∀ᵐ x : D ∂μ, 0 ≤ a.eval (x : ℝ)
/-- One outer sequence for each inner degree. -/
outer : ℕ → Polynomial.Sequence ℝ
/-- The common inner sequence. -/
inner : Polynomial.Sequence ℝ
/-- A division-free polynomial realization of each scaled inner member. -/
lift : ℕ → MvPolynomial (Fin 2) ℝ
/-- The lift realizes the separated expression on the outer measure. -/
lift_eval : ∀ k, ∀ᵐ x ∂μ, ∀ z, eval (koornwinderCoordinates ρ (x,z)) (lift k) =
ρ x^k * (inner k).eval z
/-- Orthogonality of the inner sequence. -/
inner_orthogonal : inner.IsOrthogonal ν
/-- Orthogonality in each shifted outer measure. -/
outer_orthogonal : ∀ k, (outer k).IsOrthogonal (koornwinderOuterMeasure a k ((Measure.map Subtype.val μ).comap Subtype.val))
/-- Positive inner leading coefficients fix orientation. -/
inner_leadingCoeff_pos : ∀ k, 0 < (inner k).leadingCoeff
/-- Positive outer leading coefficients fix orientation. -/
outer_leadingCoeff_pos : ∀ k n, 0 < (outer k n).leadingCoeff
/-- Inner squared norms are one. -/
inner_norm : ∀ k, Polynomial.integralInner ν (Polynomial.IntegrablePair.of ν (inner k) (inner k)) = 1
/-- Outer squared norms are one. -/
outer_norm : ∀ k n, Polynomial.integralInner (koornwinderOuterMeasure a k ((Measure.map Subtype.val μ).comap Subtype.val)) (Polynomial.IntegrablePair.of (koornwinderOuterMeasure a k ((Measure.map Subtype.val μ).comap Subtype.val)) (outer k n) (outer k n)) = 1The separated label \(n\) is not asserted to equal total degree in these general cases.
Reference details: Separated evaluation of a Koornwinder system and related results
For every pair of natural indices \(n,k\), almost every \(x\in D\) and every \(z\in \mathbb R\),
where \(n-k\) is natural-number subtraction. In particular this is the separated expression for every valid index \(0\le k\le n\).
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.eval_polynomial {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν) (n k : ℕ) :
∀ᵐ (x : ↑D) ∂μ,
∀ (z : ℝ),
(MvPolynomial.eval (MvPolynomial.koornwinderCoordinates ρ (x, z))) (S.polynomial n k) =
Polynomial.eval (↑x) (↑(S.outer k) (n - k)) * ρ x ^ k * Polynomial.eval z (↑S.inner k)Lean proof
/-- The separated evaluation identity holds almost everywhere in the outer factor. -/
theorem eval_polynomial (n k : ℕ) :
∀ᵐ x ∂μ, ∀ z, eval (koornwinderCoordinates ρ (x,z)) (S.polynomial n k) =
(S.outer k (n-k)).eval (x : ℝ) * ρ x^k * (S.inner k).eval z := by
filter_upwards [S.lift_eval k] with x hx
intro z
rw [polynomial, map_mul, hx z, eval_eval₂_C_X]
simp [koornwinderCoordinates, mul_assoc]A generalised Koornwinder system supplies all moments of its inner measure and each shifted outer measure. If its scale is continuous and \(\rho ^2=a\) almost everywhere, the separated measure also has all polynomial moments. In particular this holds for a polynomial scale \(\rho =c\) with \(a=c^2\).
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.hasFiniteMoments_inner {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν) :
Polynomial.HasFiniteMoments νLean proof
/-- The inner orthogonal sequence supplies every inner moment. -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasFiniteMoments_inner (S : KoornwinderSystem a ρ μ ν) : Polynomial.HasFiniteMoments ν :=
S.inner_orthogonal.hasFiniteMomentsFor a Koornwinder system of Definition 5.6.10, with continuous scale \(\rho \) satisfying \(\rho ^2=a\) almost everywhere for the outer measure, \(\langle P_{n,k},P_{m,j}\rangle _\omega =\delta _{nm}\delta _{kj}\) for valid separated indices.
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.integralInner_polynomial {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν)
[MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (hρ : Continuous ρ) (n k m j : ℕ)
(hi :
MeasureTheory.Integrable
(fun x =>
Polynomial.eval (↑x) (↑(S.outer k) (n - k)) * Polynomial.eval (↑x) (↑(S.outer j) (m - j)) * ρ x ^ (k + j))
μ) :
MvPolynomial.integralInner (MvPolynomial.koornwinderMeasure ρ μ ν ⋯)
(MvPolynomial.IntegrablePair.of (MvPolynomial.koornwinderMeasure ρ μ ν ⋯) (S.polynomial n k) (S.polynomial m j)
⋯) =
(∫ (x : ↑D),
Polynomial.eval (↑x) (↑(S.outer k) (n - k)) * Polynomial.eval (↑x) (↑(S.outer j) (m - j)) * ρ x ^ (k + j) ∂μ) *
Polynomial.integralInner ν (Polynomial.IntegrablePair.of ν (↑S.inner k) (↑S.inner j) ⋯)Lean proof
/-- Products of separated members factor into one-dimensional pairings. -/
theorem integralInner_polynomial [SFinite μ] [SFinite ν] (hρ : Continuous ρ)
(n k m j : ℕ)
(hi : Integrable (fun x : D => (S.outer k (n-k)).eval (x : ℝ) *
(S.outer j (m-j)).eval (x : ℝ) * ρ x^(k+j)) μ) :
integralInner (koornwinderMeasure ρ μ ν) (IntegrablePair.of (koornwinderMeasure ρ μ ν) (S.polynomial n k) (S.polynomial m j)
(h := S.integrable_polynomial_mul hρ n k m j hi)) =
(∫ x, (S.outer k (n-k)).eval (x : ℝ) * (S.outer j (m-j)).eval (x : ℝ) * ρ x^(k+j) ∂μ) *
Polynomial.integralInner ν (Polynomial.IntegrablePair.of ν (S.inner k) (S.inner j)
(h := S.inner_orthogonal.integrable k j)) := by
have he := (koornwinderMeasure_integral
(KoornwinderMeasureInput.ofContinuous μ ν hρ)
⟨fun v ↦ eval v (S.polynomial n k*S.polynomial m j), by simpa only [map_mul] using S.integrable_polynomial_mul hρ n k m j hi⟩).2
simp only [map_mul] at he
rw [integralInner, he, Polynomial.integralInner, ← integral_prod_mul]
apply integral_congr_ae
filter_upwards [Measure.quasiMeasurePreserving_fst.ae (S.eval_polynomial n k),
Measure.quasiMeasurePreserving_fst.ae (S.eval_polynomial m j)] with v hv hw
rw [hv v.2, hw v.2, pow_add]
ringReference details: Bases of separated finite spans
Let \(V_N=\operatorname {span}\{ P_{n,k}:0\le k\le n\le N\} \). These indexed polynomials form an orthonormal basis of \(V_N\); the coordinate of \(p\in V_N\) at \((n,k)\) is \(\langle p,P_{n,k}\rangle _\omega \).
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.integralGram_sectionBasis {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν)
(hμ : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ)) (hν : Polynomial.HasFiniteMoments ν)
(hρ : Continuous ρ) (ha : ∀ᵐ (x : ↑D) ∂μ, ρ x ^ 2 = Polynomial.eval (↑x) a) (N : ℕ) :
MvPolynomial.integralGram (MvPolynomial.koornwinderMeasure ρ μ ν ⋯) (fun i => ↑((S.sectionBasis hμ hν hρ ha N) i)) ⋯ =
1Lean proof
/-- Each finite separated basis has identity Gram matrix. -/
theorem integralGram_sectionBasis (N : ℕ) :
integralGram (koornwinderMeasure ρ μ ν)
(fun i => (S.sectionBasis hμ hν hρ ha N i : MvPolynomial (Fin 2) ℝ)) = 1 := by
classical
let := hμ.isFiniteMeasure_subtype
let := hν.isFiniteMeasure
ext i j
simp only [integralGram, sectionBasis_apply, Matrix.one_apply]
by_cases hij : i=j
· subst j
rw [S.integralInner_polynomial_self hρ ha, ite_eq_left rfl]
· rw [ite_eq_right hij]
apply S.integralInner_polynomial_eq_zero hρ ha (by omega) (by omega)
intro he
apply hij
have hn : i.1=j.1 := Fin.ext (congrArg Prod.fst he)
rcases i with ⟨n,k⟩
rcases j with ⟨m,l⟩
dsimp at hn
subst m
congr 1
exact Fin.ext (congrArg Prod.snd he)This statement does not identify \(V_N\) with a total-degree space.
If every \(L_k\) has total degree at most \(k\), then \(V_N\) is exactly the space of bivariate polynomials of total degree at most \(N\). The lift bound holds for affine polynomial scales and for square-root quadratic scales with even inner measure.
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.sectionSpan_eq_restrictTotalDegree {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν)
(hμ : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ)) (hν : Polynomial.HasFiniteMoments ν)
(hρ : Continuous ρ) (ha : ∀ᵐ (x : ↑D) ∂μ, ρ x ^ 2 = Polynomial.eval (↑x) a)
(hlift : ∀ (k : ℕ), (S.lift k).totalDegree ≤ k) (N : ℕ) :
S.sectionSpan N = MvPolynomial.restrictTotalDegree (Fin 2) ℝ NLean proof
/-- Degree-compatible lifts identify separated finite spans with total-degree spaces. -/
theorem sectionSpan_eq_restrictTotalDegree
(hμ : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ)) (hν : Polynomial.HasFiniteMoments ν)
(hρ : Continuous ρ) (ha : ∀ᵐ x ∂μ, ρ x^2 = a.eval (x : ℝ))
(hlift : ∀ k, (S.lift k).totalDegree ≤ k) (N : ℕ) :
S.sectionSpan N = restrictTotalDegree (Fin 2) ℝ N := by
have hle : S.sectionSpan N ≤ restrictTotalDegree (Fin 2) ℝ N := by
apply Submodule.span_le.mpr
rintro p ⟨i,rfl⟩
apply (mem_restrictTotalDegree (Fin 2) N _).mpr
exact (S.totalDegree_polynomial_le hlift (by exact Nat.le_of_lt_succ i.2.isLt)).trans
(Nat.le_of_lt_succ i.1.isLt)
let b : Basis (KoornwinderIndex N) ℝ (restrictTotalDegree (Fin 2) ℝ N) :=
(basisRestrictSupport ℝ _).reindex (separatedIndexEquiv N).symm
apply Submodule.eq_of_le_of_finrank_eq hle
rw [Module.finrank_eq_card_basis (S.sectionBasis hμ hν hρ ha N),
Module.finrank_eq_card_basis b]Formal details: Polynomial density within an outer domain and related results
Let \(D\subseteq \mathbb R\) and \(p\in \mathbb R[X]\). A measure \(\eta \) on \(\{ x\in D:p(x)\ge 0\} \) defines a measure on \(D\) by weighting by \(p\) and pushing forward along the inclusion into \(D\).
Lean Formalisation
def Polynomial.subtypeDensityMeasure {D : Set ℝ} (p : Polynomial ℝ)
(μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval (↑x) p }) : MeasureTheory.Measure ↑DLean definition
/-- A nonnegative polynomial density on a source inside the fixed outer domain. -/
noncomputable def subtypeDensityMeasure (p : ℝ[X])
(μ : Measure {x : D // 0 ≤ p.eval (x : ℝ)}) : Measure D :=
Measure.map Subtype.val (μ.withDensity (fun x =>
ENNReal.ofNNReal (NNReal.mk (p.eval (x.val : ℝ)) x.property)))For every measurable subset \(E\) of \(D\), the resulting measure assigns the nonnegative integral \(\int _{\iota ^{-1}(E)}p(x)\, d\eta (x)\).
Lean Formalisation
theorem Polynomial.subtypeDensityMeasure_apply {D : Set ℝ} (p : Polynomial ℝ)
(μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval (↑x) p }) {s : Set ↑D} (hs : MeasurableSet s) :
(p.subtypeDensityMeasure μ) s =
∫⁻ (x : { x // 0 ≤ Polynomial.eval (↑x) p }) in Subtype.val ⁻¹' s, ↑(NNReal.mk (Polynomial.eval (↑↑x) p) ⋯) ∂μLean proof
/-- Values on measurable sets are the nonnegative weighted source integrals. -/
theorem subtypeDensityMeasure_apply (p : ℝ[X])
(μ : Measure {x : D // 0 ≤ p.eval (x : ℝ)}) {s : Set D} (hs : MeasurableSet s) :
subtypeDensityMeasure p μ s = ∫⁻ x in Subtype.val ⁻¹' s,
ENNReal.ofNNReal (NNReal.mk (p.eval (x.val : ℝ)) x.property) ∂μ := by
rw [subtypeDensityMeasure, Measure.map_apply measurable_subtype_coe hs,
withDensity_apply _ (measurable_subtype_coe hs)]Under finite moments and positive definite pairings, and for a nonzero scale polynomial \(a\ge 0\) almost everywhere, modify \(\mu \) by a nonzero polynomial \(u\ge 0\) almost everywhere, using the density measure of Definition 5.6.16 after transporting the source to \(\{ u\ge 0\} \), and keeping the inner sequence and lifts fixed. The old and new separated spans \(V_N\) coincide. If moreover \(\nu \) has finite moments, \(\rho \) is continuous and \(\rho ^2=a\) almost everywhere for \(\mu \), the connection coefficient from \((n,k)\) to \((m,j)\) vanishes unless \(j=k\) and \(0\le n-m\le \deg u\). No degree restriction on the scale is needed.
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.sectionSpan_eq_of_lift_eq {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} {μ' : MeasureTheory.Measure ↑D}
{ν' : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν)
(T : MvPolynomial.KoornwinderSystem a ρ μ' ν')
(hμ : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ))
(hpos : Polynomial.HasPositiveDefiniteIntegral (MeasureTheory.Measure.map Subtype.val μ))
(hμ' : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ'))
(hpos' : Polynomial.HasPositiveDefiniteIntegral (MeasureTheory.Measure.map Subtype.val μ')) (ha0 : a ≠ 0)
(ha : ∀ᵐ (x : ↑D) ∂μ, 0 ≤ Polynomial.eval (↑x) a) (ha' : ∀ᵐ (x : ↑D) ∂μ', 0 ≤ Polynomial.eval (↑x) a)
(hL : S.lift = T.lift) (N : ℕ) : S.sectionSpan N = T.sectionSpan NLean proof
/-- Every finite separated span is unchanged when only the outer sequences change. -/
theorem sectionSpan_eq_of_lift_eq
(hμ : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ)) (hpos : Polynomial.HasPositiveDefiniteIntegral (Measure.map Subtype.val μ))
(hμ' : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ')) (hpos' : Polynomial.HasPositiveDefiniteIntegral (Measure.map Subtype.val μ'))
(ha0 : a ≠ 0) (ha : ∀ᵐ (x : D) ∂μ, 0 ≤ a.eval (x : ℝ)) (ha' : ∀ᵐ (x : D) ∂μ', 0 ≤ a.eval (x : ℝ))
(hL : S.lift=T.lift) (N : ℕ) : S.sectionSpan N = T.sectionSpan N := by
apply le_antisymm
· apply Submodule.span_le.mpr
rintro p ⟨i,rfl⟩
exact S.polynomial_mem_sectionSpan_of_lift_eq T hμ' hpos' ha0 ha' hL
(by exact Nat.le_of_lt_succ i.1.isLt) (by exact Nat.le_of_lt_succ i.2.isLt)
· apply Submodule.span_le.mpr
rintro p ⟨i,rfl⟩
exact T.polynomial_mem_sectionSpan_of_lift_eq S hμ hpos ha0 ha hL.symm
(by exact Nat.le_of_lt_succ i.1.isLt) (by exact Nat.le_of_lt_succ i.2.isLt)Reference details: Separated modification polynomial and related results
For real polynomials \(b,h,g\), a positive integer \(s\) and \(\ell \in \mathbb {N}\), define
Reference: [DX14, §2.6.1].
Lean Formalisation
def MvPolynomial.koornwinderModificationPolynomial (b h g : Polynomial ℝ) (step : ℕ+) (l : ℕ) : MvPolynomial (Fin 2) ℝLean definition
/-- A separated modification as a genuine bivariate polynomial. -/
noncomputable def koornwinderModificationPolynomial (b h g : ℝ[X]) (step : ℕ+) (l : ℕ) :
MvPolynomial (Fin 2) ℝ := h.eval₂ C (X 0) * scaledLift b step ((step : ℕ)*l) gFor real polynomials \(b,h,g\), let \(u(x,y)=h(x)V_0(g)(x,y)=h(x)g_0\). Its total degree is at most \(\deg h\). If \(\deg g\le 0\) and \(b(x)=1\), then \(u(x,y)=b(x)^\ell h(x)g(z)\) for every \(y,z\) and \(\ell \in \mathbb {N}\).
Lean Formalisation
theorem MvPolynomial.eval_zeroStepKoornwinderModification (b h g : Polynomial ℝ) (l : ℕ) (hg : g.natDegree ≤ 0) (v : Fin 2 → ℝ)
(z : ℝ) (hb : Polynomial.eval (v 0) b = 1) :
(MvPolynomial.eval v) (Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X 0) h * MvPolynomial.verticalTruncation 0 g) =
Polynomial.eval (v 0) (b ^ l * h) * Polynomial.eval z gLean proof
/-- The former zero-step modification is an ordinary constant vertical factor.
This statement uses coefficient truncation, with no division by a scale step. -/
theorem eval_zeroStepKoornwinderModification (b h g : ℝ[X]) (l : ℕ)
(hg : g.natDegree ≤ 0) (v : Fin 2 → ℝ) (z : ℝ) (hb : b.eval (v 0) = 1) :
eval v (h.eval₂ C (X 0) * verticalTruncation 0 g) =
(b^l*h).eval (v 0) * g.eval z := by
have hgval : g.eval z = g.coeff 0 := by
rw [Polynomial.eval_eq_sum_range' (by omega : g.natDegree < 0+1)]
simp
simp [verticalTruncation, eval_eval₂_C_X, hgval, hb]For a positive integer \(s\), suppose \(\rho ^s=b\) and \(\deg g\le s\ell \), with nonzero coefficients of \(g\) only at indices congruent to \(s\ell \) modulo \(s\). The polynomial \(u=h(x)L_{s,s\ell }(g)\) pulls back to \(b(x)^\ell h(x)g(z)\). If \(\rho \) is continuous, \(\nu \) is s-finite and both factor densities are nonnegative almost everywhere, replacing \((\mu ,\nu )\) by \((b^\ell h\mu ,g\nu )\) gives the same polynomial integrals as multiplying \(\omega \) by \(u\): for a polynomial \(p\) with \(up\in L^1(\omega )\), the modified integral of \(p\) exists and equals \(\int up\, d\omega \). For \(\ell =1\), \(h=1\), the affine factor is \(\alpha c(x)+\beta y\); the square-root factor is \(\alpha a(x)+\beta y^2\).
Lean Formalisation
theorem MvPolynomial.eval_koornwinderModificationPolynomial {D : Set ℝ} (b h g : Polynomial ℝ) (step : ℕ+) (l : ℕ)
(hg : g.natDegree ≤ ↑step * l) (hpar : ∀ j ≤ ↑step * l, g.coeff j ≠ 0 → ↑step ∣ ↑step * l - j) (ρ : ↑D → ℝ) (x : ↑D)
(z : ℝ) (hb : ρ x ^ ↑step = Polynomial.eval (↑x) b) :
(MvPolynomial.eval (MvPolynomial.koornwinderCoordinates ρ (x, z)))
(MvPolynomial.koornwinderModificationPolynomial b h g step l) =
Polynomial.eval (↑x) (b ^ l * h) * Polynomial.eval z gLean proof
/-- Evaluation of the modification in separated coordinates. -/
theorem eval_koornwinderModificationPolynomial (b h g : ℝ[X]) (step : ℕ+) (l : ℕ)
(hg : g.natDegree ≤ (step : ℕ)*l)
(hpar : ∀ j ≤ (step : ℕ)*l, g.coeff j ≠ 0 → (step : ℕ) ∣ (step : ℕ)*l-j)
(ρ : D → ℝ) (x : D) (z : ℝ) (hb : ρ x^(step : ℕ) = b.eval (x : ℝ)) :
eval (koornwinderCoordinates ρ (x,z)) (koornwinderModificationPolynomial b h g step l) =
(b^l*h).eval (x : ℝ) * g.eval z := by
rw [koornwinderModificationPolynomial, map_mul, eval_eval₂_C_X,
eval_scaledLift b step ((step : ℕ)*l) g hg hpar _ (ρ x) z
(by simpa [koornwinderCoordinates] using hb.symm) rfl,
pow_mul, hb]
simp only [koornwinderCoordinates, Matrix.cons_val_zero, Polynomial.eval_mul, Polynomial.eval_pow]
ringAssume finite moments and positive-leading normalised source and target systems. For an affine scale \(c\ge 0\), modify the factor measures by \(c^\ell h\) and \(g\), where \(h,g\ge 0\) almost everywhere and \(\deg g\le \ell \). A nonzero connection coefficient requires
For a continuous scale with square \(a\), \(\deg a\le 2\), assume additionally that \(\nu \) is even with positive definite polynomial pairing, and \(g\) is nonzero, even, nonnegative and of degree at most \(2\ell \). Modifying by \(a^\ell h\) and \(g\) permits only
These are containing supports: individual permitted entries may also vanish.
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.connectionEntry_affine_support {D : Set ℝ} {μ : MeasureTheory.Measure ↑D}
{ν : MeasureTheory.Measure ℝ} (c h g : Polynomial ℝ) (l : ℕ)
(S : MvPolynomial.KoornwinderSystem (c ^ 2) (fun x => Polynomial.eval (↑x) c) μ ν)
(T :
MvPolynomial.KoornwinderSystem (c ^ 2) (fun x => Polynomial.eval (↑x) c)
((c ^ l * h).subtypeDensityMeasure (MeasureTheory.Measure.comap Subtype.val μ))
(g.polynomialDensityMeasure (MeasureTheory.Measure.comap Subtype.val ν)))
(hμ : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ)) (hν : Polynomial.HasFiniteMoments ν)
(hc : ∀ᵐ (x : ↑D) ∂μ, 0 ≤ Polynomial.eval (↑x) c) (hh : ∀ᵐ (x : ↑D) ∂μ, 0 ≤ Polynomial.eval (↑x) h)
(hg : ∀ᵐ (x : ℝ) ∂ν, 0 ≤ Polynomial.eval x g) (hcdeg : c.natDegree ≤ 1) (hgdeg : g.natDegree ≤ l) {n k m j : ℕ}
(hk : k ≤ n) (hj : j ≤ m) (hout : ¬∃ s r, s ≤ h.natDegree + l ∧ r ≤ l ∧ n = m + s ∧ k = j + r) :
S.connectionEntry T n k m j ⋯ ⋯ = 0Lean proof
/-- Affine scales give a finite rectangular support, without an inner parity assumption. -/
theorem connectionEntry_affine_support {μ : Measure D} {ν : Measure ℝ} (c h g : ℝ[X]) (l : ℕ)
(S : KoornwinderSystem (c^2) (fun x => c.eval (x : ℝ)) μ ν)
(T : KoornwinderSystem (c^2) (fun x => c.eval (x : ℝ))
(Polynomial.subtypeDensityMeasure ((c^l*h)) ((μ).comap Subtype.val))
(Polynomial.polynomialDensityMeasure (g) ((ν).comap Subtype.val)))
(hμ : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ)) (hν : Polynomial.HasFiniteMoments ν)
(hc : ∀ᵐ (x : D) ∂μ, 0 ≤ c.eval (x : ℝ)) (hh : ∀ᵐ (x : D) ∂μ, 0 ≤ h.eval (x : ℝ))
(hg : ∀ᵐ x ∂ν, 0 ≤ g.eval (x : ℝ)) (hcdeg : c.natDegree ≤ 1) (hgdeg : g.natDegree ≤ l)
{n k m j : ℕ} (hk : k ≤ n) (hj : j ≤ m)
(hout : ¬ ∃ s r : ℕ, s ≤ h.natDegree+l ∧ r ≤ l ∧ n=m+s ∧ k=j+r) :
S.connectionEntry T n k m j = 0 := by
have ha : ∀ᵐ (x : D) ∂μ, c.eval (x : ℝ)^2 = (c^2).eval (x : ℝ) := by simp
have hb : ∀ᵐ (x : D) ∂μ, c.eval (x : ℝ)^1 = c.eval (x : ℝ) := by simp
by_cases hi : k < j ∨ j+g.natDegree < k
· exact S.connectionEntry_eq_zero_of_inner_modification h g l T hμ hν (c.continuous.comp continuous_subtype_val) hc hh hg hi
have hkj : k=j+1*(k-j) := by omega
have hr : k-j ≤ l := by omega
by_cases ho : n < m ∨ m+h.natDegree+l < n
· exact S.connectionEntry_eq_zero_of_outer_band h g l T hμ hν (c.continuous.comp continuous_subtype_val) ha 1 hb hc hh hg
hcdeg hk hj hkj hr (by simpa using ho)
exfalso
apply hout
exact ⟨n-m,k-j,by omega,hr,by omega,by omega⟩Suppose the source section lies in the target section and the target factor measures are absolutely continuous with respect to the source ones. Mixed pairings are the actual conversion coordinates \(C\), and the source Gram matrix in the target measure is \(C^{\mathsf T}C\). Section compatibility holds for ordinary systems, and for Type 1 modifications. Using a degree-then-inner ordered enumeration, the preceding support bounds make \(C\) upper triangular; its diagonal is positive. It is the unique positive upper triangular Gram factor. Any exact unpivoted unit-lower LU factorisation of that Gram matrix has upper factor with exactly the same zero entries as \(C\).
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.connectionEntry_eq_sectionBasis_repr {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} {μ' : MeasureTheory.Measure ↑D}
{ν' : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν)
(T : MvPolynomial.KoornwinderSystem a ρ μ' ν')
(hμ' : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ')) (hν' : Polynomial.HasFiniteMoments ν')
(hρ : Continuous ρ) (ha : ∀ᵐ (x : ↑D) ∂μ', ρ x ^ 2 = Polynomial.eval (↑x) a) (N n k : ℕ)
(hp : S.polynomial n k ∈ T.sectionSpan N) (i : MvPolynomial.KoornwinderIndex N) :
S.connectionEntry T n k ↑i.fst ↑i.snd ⋯ ⋯ = ((T.sectionBasis hμ' hν' hρ ha N).repr ⟨S.polynomial n k, hp⟩) iLean proof
/-- A mixed pairing is the actual finite-span coordinate whenever the source lies in that span. -/
theorem connectionEntry_eq_sectionBasis_repr
{a : ℝ[X]} {ρ : D → ℝ} {μ : Measure D} {ν : Measure ℝ} {μ' : Measure D} {ν' : Measure ℝ}
(S : KoornwinderSystem a ρ μ ν) (T : KoornwinderSystem a ρ μ' ν')
(hμ' : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ')) (hν' : Polynomial.HasFiniteMoments ν')
(hρ : Continuous ρ) (ha : ∀ᵐ x ∂μ', ρ x^2 = a.eval (x : ℝ))
(N n k : ℕ) (hp : S.polynomial n k ∈ T.sectionSpan N) (i : KoornwinderIndex N) :
S.connectionEntry T n k i.1 i.2 =
(T.sectionBasis hμ' hν' hρ ha N).repr ⟨S.polynomial n k,hp⟩ i := by
rw [T.sectionBasis_repr hμ' hν' hρ ha]
exact integralInner_comm _ _ _For successive systems \(S,T,U\), if the source section lies in the intermediate section, mixed-pairing conversion matrices satisfy \(C_{SU}=C_{TU}C_{ST}\). Under compatible finite spans these are actual coordinate conversions. Their containing offset supports add by Minkowski sum.
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.connectionEntry_comp {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} {μ' : MeasureTheory.Measure ↑D}
{ν' : MeasureTheory.Measure ℝ} {μ'' : MeasureTheory.Measure ↑D} {ν'' : MeasureTheory.Measure ℝ}
(S : MvPolynomial.KoornwinderSystem a ρ μ ν) (T : MvPolynomial.KoornwinderSystem a ρ μ' ν')
(U : MvPolynomial.KoornwinderSystem a ρ μ'' ν'')
(hμ' : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ')) (hν' : Polynomial.HasFiniteMoments ν')
(hμ'' : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ''))
(hν'' : Polynomial.HasFiniteMoments ν'') (hρ : Continuous ρ) (ha' : ∀ᵐ (x : ↑D) ∂μ', ρ x ^ 2 = Polynomial.eval (↑x) a)
(ha'' : ∀ᵐ (x : ↑D) ∂μ'', ρ x ^ 2 = Polynomial.eval (↑x) a) (N : ℕ)
(hspan : ∀ (i : MvPolynomial.KoornwinderIndex N), S.polynomial ↑i.fst ↑i.snd ∈ T.sectionSpan N) :
(Matrix.of fun i j => S.connectionEntry U ↑j.fst ↑j.snd ↑i.fst ↑i.snd ⋯ ⋯) =
(Matrix.of fun i j => T.connectionEntry U ↑j.fst ↑j.snd ↑i.fst ↑i.snd ⋯ ⋯) *
Matrix.of fun i j => S.connectionEntry T ↑j.fst ↑j.snd ↑i.fst ↑i.snd ⋯ ⋯Lean proof
/-- Separated connection sections compose exactly through an intermediate span. -/
theorem connectionEntry_comp
{a : ℝ[X]} {ρ : D → ℝ} {μ : Measure D} {ν : Measure ℝ} {μ' : Measure D} {ν' : Measure ℝ} {μ'' : Measure D} {ν'' : Measure ℝ}
(S : KoornwinderSystem a ρ μ ν) (T : KoornwinderSystem a ρ μ' ν')
(U : KoornwinderSystem a ρ μ'' ν'')
(hμ' : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ')) (hν' : Polynomial.HasFiniteMoments ν')
(hμ'' : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ'')) (hν'' : Polynomial.HasFiniteMoments ν'')
(hρ : Continuous ρ) (ha' : ∀ᵐ x ∂μ', ρ x^2 = a.eval (x : ℝ))
(ha'' : ∀ᵐ x ∂μ'', ρ x^2 = a.eval (x : ℝ)) (N : ℕ)
(hspan : ∀ i : KoornwinderIndex N, S.polynomial i.1 i.2 ∈ T.sectionSpan N) :
Matrix.of (fun i j : KoornwinderIndex N => S.connectionEntry U j.1 j.2 i.1 i.2) =
Matrix.of (fun i j : KoornwinderIndex N => T.connectionEntry U j.1 j.2 i.1 i.2) *
Matrix.of (fun i j : KoornwinderIndex N => S.connectionEntry T j.1 j.2 i.1 i.2) := by
classical
ext i j
let v : T.sectionSpan N := ⟨S.polynomial j.1 j.2,hspan j⟩
let L := ((integralBilinForm (koornwinderMeasure ρ μ'' ν'')
(hasFiniteMoments_koornwinderMeasure hμ'' hν'' hρ a ha''))
(U.polynomial i.1 i.2)).comp (T.sectionSpan N).subtype
have he := congrArg L ((T.sectionBasis hμ' hν' hρ ha' N).sum_repr v)
simp only [map_sum,map_smul,smul_eq_mul] at he
have hc (k : KoornwinderIndex N) :
(T.sectionBasis hμ' hν' hρ ha' N).repr v k =
S.connectionEntry T j.1 j.2 k.1 k.2 :=
(S.connectionEntry_eq_sectionBasis_repr T hμ' hν' hρ ha' N _ _ (hspan j) k).symm
have ht (k : KoornwinderIndex N) : L (T.sectionBasis hμ' hν' hρ ha' N k) =
T.connectionEntry U k.1 k.2 i.1 i.2 := by
change integralInner (koornwinderMeasure ρ μ'' ν'') (IntegrablePair.of (koornwinderMeasure ρ μ'' ν'') (U.polynomial i.1 i.2) (T.sectionBasis hμ' hν' hρ ha' N k)) = _
rw [T.sectionBasis_apply]
exact integralInner_comm _ _ _
have hv : L v = S.connectionEntry U j.1 j.2 i.1 i.2 := integralInner_comm _ _ _
simp_rw [hc,ht,hv] at he
simp only [Matrix.mul_apply, Matrix.of_apply]
exact he.symm.trans (Finset.sum_congr rfl (fun k _ => mul_comm _ _))No additional sparsity or construction-cost assertion is implied.
Reference details: Coordinate multiplication support
Let multiplication entries be \(\langle x_iP_{n,k},P_{m,j}\rangle _\omega \). For continuous \(\rho \) with \(\rho ^2=a\) almost everywhere for \(\mu \), multiplication by \(x\) requires \(j=k\) and \(|n-m|\le 1\). For polynomial scale \(c\), multiplication by \(y\) requires \(|k-j|\le 1\), \(|n-m|\le B\) whenever \(B\ge 1\), \(\deg c\le B\) and \(\deg (c^2)\le B+1\). For an even inner measure with positive definite pairing, the same bounds hold for continuous scale \(\rho \) with \(\rho ^2=a\) and \(\deg a\le B+1\). Thus ordinary affine and square-root-quadratic cases have \(B=1\). Finite moments are assumed throughout. For unrestricted scales these statements concern pairing entries, without asserting completeness in the entire polynomial algebra.
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.multiplicationEntry_x_eq_zero {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν)
[MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (hρ : Continuous ρ)
(ha : ∀ᵐ (x : ↑D) ∂μ, ρ x ^ 2 = Polynomial.eval (↑x) a)
(hμ : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ)) {n k m j : ℕ} (hk : k ≤ n) (hj : j ≤ m)
(hout : k ≠ j ∨ n + 1 < m ∨ m + 1 < n) : S.multiplicationEntry 0 n k m j ⋯ ⋯ = 0Lean proof
/-- Multiplication by x has block bandwidth one and no off-diagonal inner indices. -/
theorem multiplicationEntry_x_eq_zero (hμ : Polynomial.HasFiniteMoments (Measure.map Subtype.val μ))
{n k m j : ℕ} (hk : k ≤ n) (hj : j ≤ m)
(hout : k ≠ j ∨ n+1 < m ∨ m+1 < n) : S.multiplicationEntry 0 n k m j = 0 := by
rw [S.multiplicationEntry_x hρ n k m j (hi := (S.hasFiniteMoments hρ ha).integrable_mul _ _)]
by_cases hkj : k=j
· subst j
rw [S.inner_norm, mul_one]
have he : (∫ x : D, (x : ℝ)*(S.outer k (n-k)).eval (x : ℝ)*(S.outer k (m-k)).eval (x : ℝ)*ρ x^(k+k) ∂μ) =
Polynomial.integralInner (koornwinderOuterMeasure a k ((Measure.map Subtype.val μ).comap Subtype.val)) (Polynomial.IntegrablePair.of (koornwinderOuterMeasure a k ((Measure.map Subtype.val μ).comap Subtype.val)) (Polynomial.X*S.outer k (n-k)) (S.outer k (m-k))) := by
simp only [Polynomial.integralInner]
have hpos := ha.mono (fun x hx => hx ▸ sq_nonneg (ρ x))
have hpair := (hμ.koornwinderOuterMeasure a
(ae_nonneg_eval_map_subtype hpos) k).integrable_mul
(Polynomial.X*S.outer k (n-k)) (S.outer k (m-k))
have ht := integral_koornwinderOuterMeasure_map_subtype μ a hpos k
⟨fun x : ℝ => (Polynomial.X*S.outer k (n-k)).eval x *
(S.outer k (m-k)).eval x, hpair⟩
dsimp only at ht
rw [ht]
apply integral_congr_ae
filter_upwards [ha] with x hx
rw [show k+k=2*k by omega, pow_mul, hx]
simp only [Polynomial.eval_mul,Polynomial.eval_X]
ring
rw [he]
exact (S.outer_orthogonal k).integralInner_X_mul_eq_zero
(hμ.koornwinderOuterMeasure a (ae_nonneg_eval_map_subtype (ha.mono (fun x hx => hx ▸ sq_nonneg (ρ x)))) k)
(by omega)
· rw [show Polynomial.integralInner ν (Polynomial.IntegrablePair.of ν (S.inner k) (S.inner j)) = 0 from
S.inner_orthogonal.orthogonal k j hkj, mul_zero]If \(\deg L_k\le k\), multiplying a member of the section \(V_N\) by either coordinate lies in \(V_{N+1}\) and has the exact finite expansion with the multiplication entries above as coefficients. Consequently the support bounds describe the actual coordinate multiplication operators for ordinary systems.
Lean Formalisation
theorem MvPolynomial.KoornwinderSystem.coordinate_mul_mem_sectionSpan {D : Set ℝ} {a : Polynomial ℝ} {ρ : ↑D → ℝ}
{μ : MeasureTheory.Measure ↑D} {ν : MeasureTheory.Measure ℝ} (S : MvPolynomial.KoornwinderSystem a ρ μ ν)
(hμ : Polynomial.HasFiniteMoments (MeasureTheory.Measure.map Subtype.val μ)) (hν : Polynomial.HasFiniteMoments ν)
(hρ : Continuous ρ) (ha : ∀ᵐ (x : ↑D) ∂μ, ρ x ^ 2 = Polynomial.eval (↑x) a)
(hlift : ∀ (k : ℕ), (S.lift k).totalDegree ≤ k) (coord : Fin 2) (N : ℕ) (i : MvPolynomial.KoornwinderIndex N) :
MvPolynomial.X coord * S.polynomial ↑i.fst ↑i.snd ∈ S.sectionSpan (N + 1)Lean proof
/-- Ordinary coordinate multiplication lands in the section with one extra degree. -/
theorem coordinate_mul_mem_sectionSpan (coord : Fin 2) (N : ℕ) (i : KoornwinderIndex N) :
X coord*S.polynomial i.1 i.2 ∈ S.sectionSpan (N+1) := by
rw [S.sectionSpan_eq_restrictTotalDegree hμ hν hρ ha hlift]
apply (mem_restrictTotalDegree (Fin 2) (N+1) _).mpr
have hp := S.totalDegree_polynomial_le hlift (Nat.le_of_lt_succ i.2.isLt)
have hm := totalDegree_mul (X coord : MvPolynomial (Fin 2) ℝ) (S.polynomial i.1 i.2)
rw [totalDegree_X] at hm
have := i.1.isLt
omegaEvery existing Cartesian disk system whose outer measure \(\mu \) is supported in \([-1,1]\) almost everywhere supplies a separated Koornwinder system with \(a=1-x^2\) and \(\rho =\sqrt{1-x^2}\). Its polynomials are exactly the existing disk polynomials, with the same indices and normalisation.
Lean Formalisation
theorem MvPolynomial.CartesianDiskSystem.toKoornwinderSystem_polynomial {μ ν : MeasureTheory.Measure ℝ}
(S : MvPolynomial.CartesianDiskSystem (MeasureTheory.Measure.comap Subtype.val μ) ν)
(hx : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.Icc (-1) 1) (n k : ℕ) : (S.toKoornwinderSystem hx).polynomial n k = S.polynomial n kLean proof
/-- The bridge uses exactly the existing Cartesian disk polynomial. -/
theorem toKoornwinderSystem_polynomial (hx : ∀ᵐ x ∂μ, x ∈ Icc (-1 : ℝ) 1) (n k : ℕ) :
(S.toKoornwinderSystem hx).polynomial n k = S.polynomial n k := rfl