5.3 Classical orthogonal polynomials in several variables
On squares, triangles and disks, separation of variables constructs orthogonal polynomials from one-dimensional families. The resulting bases have explicit norms and span each total-degree space, with sparse multiplication and parameter conversion. We begin with the multivariate version of the polynomial inner product from Chapter 3.1.
A measure \(\mu \) on \(\mathbb {R}^\sigma \) has finite polynomial moments when every polynomial square is \(\mu \)-integrable.
Lean Formalisation
def MvPolynomial.HasFiniteMoments.{u_1} {σ : Type u_1} (μ : MeasureTheory.Measure (σ → ℝ)) : PropLean definition
/-- Finite polynomial moments, expressed as square integrability of all polynomials
(Dunkl–Xu, Chapter 3). -/
def HasFiniteMoments (μ : Measure (σ → ℝ)) : Prop :=
∀ p : MvPolynomial σ ℝ, Integrable (fun x => eval x p ^ 2) μThe polynomial integral is positive definite when every polynomial square is integrable and every nonzero polynomial has strictly positive squared integral.
Lean Formalisation
inductive MvPolynomial.HasPositiveDefiniteIntegral.{u_1} {σ : Type u_1} (μ : MeasureTheory.Measure (σ → ℝ)) : PropLean definition
/-- Strict positivity of the polynomial integral pairing, without a support restriction
(Dunkl–Xu, Chapter 3). -/
structure HasPositiveDefiniteIntegral (μ : Measure (σ → ℝ)) : Prop where
/-- Every polynomial square has a classical finite integral. -/
moments : HasFiniteMoments μ
/-- Nonzero polynomial squares have strictly positive integrals. -/
positive : ∀ p : MvPolynomial σ ℝ, p ≠ 0 → 0 < ∫ x, eval x p ^ 2 ∂μReference details: Characterisation of positive multivariate polynomial integrals and related results
A positive-definite polynomial integral has all polynomial moments finite. Every nonzero polynomial has strictly positive squared integral.
Lean Formalisation
theorem MvPolynomial.HasPositiveDefiniteIntegral.hasFiniteMoments.{u_1} {σ : Type u_1} {μ : MeasureTheory.Measure (σ → ℝ)}
(hpos : MvPolynomial.HasPositiveDefiniteIntegral μ) : MvPolynomial.HasFiniteMoments μLean proof
/-- Positive square integrals are genuine finite integrals. -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem HasPositiveDefiniteIntegral.hasFiniteMoments {μ : Measure (σ → ℝ)}
(hpos : HasPositiveDefiniteIntegral μ) : HasFiniteMoments μ :=
hpos.momentsFor a measure \(\mu \) on \(\mathbb {R}^\sigma \), an integrable polynomial pair consists of polynomials \(p,q\) together with \(pq\in L^1(\mu )\). Its pairing is the finite integral \(\langle p,q\rangle _\mu =\int pq\, d\mu \), defined on these pairs only.
Lean Formalisation
inductive MvPolynomial.IntegrablePair.{u_1} {σ : Type u_1} (μ : MeasureTheory.Measure (σ → ℝ)) : Type u_1Lean definition
/-- A polynomial pair whose product has a finite integral (Dunkl–Xu, Chapter 3).
No moment condition is imposed on other polynomials. -/
structure IntegrablePair (μ : Measure (σ → ℝ)) where
left : MvPolynomial σ ℝ
right : MvPolynomial σ ℝ
integrable : Integrable (fun x => eval x left * eval x right) μAn integrable pair has pairing \(\int pq\, d\mu \). The pairing is symmetric; on an integrable diagonal pair it equals \(\int p^2\, d\mu \).
Lean Formalisation
theorem MvPolynomial.integralInner_eq_integral.{u_1} {σ : Type u_1} (μ : MeasureTheory.Measure (σ → ℝ))
(pq : MvPolynomial.IntegrablePair μ) :
MvPolynomial.integralInner μ pq = ∫ (x : σ → ℝ), (MvPolynomial.eval x) pq.left * (MvPolynomial.eval x) pq.right ∂μLean proof
/-- The pairing is exactly the integral of its integrable product. -/
theorem integralInner_eq_integral (μ : Measure (σ → ℝ)) (pq : IntegrablePair μ) :
integralInner μ pq = ∫ x, eval x pq.left * eval x pq.right ∂μ := rflIf every polynomial square is \(\mu \)-integrable, then \(\mu \) is a finite measure, and, for finite \(\sigma \), every product \(pq\) of polynomials is \(\mu \)-integrable.
Lean Formalisation
theorem MvPolynomial.HasFiniteMoments.integrable_mul.{u_1} {σ : Type u_1} [Fintype σ] {μ : MeasureTheory.Measure (σ → ℝ)}
(hμ : MvPolynomial.HasFiniteMoments μ) (p q : MvPolynomial σ ℝ) :
MeasureTheory.Integrable (fun x => (MvPolynomial.eval x) p * (MvPolynomial.eval x) q) μLean proof
/-- Finite polynomial moments make all polynomial products integrable
(Dunkl–Xu, Chapter 3). -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem HasFiniteMoments.integrable_mul [Fintype σ] {μ : Measure (σ → ℝ)} (hμ : HasFiniteMoments μ)
(p q : MvPolynomial σ ℝ) : Integrable (fun x => eval x p * eval x q) μ := by
have hp : MemLp (fun x => eval x p) 2 μ :=
(memLp_two_iff_integrable_sq p.continuous_eval.aestronglyMeasurable).2 (hμ p)
have hq : MemLp (fun x => eval x q) 2 μ :=
(memLp_two_iff_integrable_sq q.continuous_eval.aestronglyMeasurable).2 (hμ q)
exact hp.integrable_mul hqFor finite \(\sigma \), assume explicitly that \(\mu \) has finite polynomial moments and positive-definite polynomial integral. Equip the polynomial space with the inner product \(\langle p,q\rangle _\mu =\int pq\, d\mu \). There is no connectedness or product-support restriction.
Lean Formalisation
def MvPolynomial.HasFiniteMoments.pair.{u_1} {σ : Type u_1} [Fintype σ] {μ : MeasureTheory.Measure (σ → ℝ)}
(hμ : MvPolynomial.HasFiniteMoments μ) (p q : MvPolynomial σ ℝ) : MvPolynomial.IntegrablePair μLean definition
/-- Finite moments supply every polynomial pair (Dunkl–Xu, Chapter 3). -/
abbrev HasFiniteMoments.pair [Fintype σ] {μ : Measure (σ → ℝ)} (hμ : HasFiniteMoments μ)
(p q : MvPolynomial σ ℝ) : IntegrablePair μ := ⟨p, q, hμ.integrable_mul p q⟩Supporting results: total-degree spaces
For a variable set \(\sigma \) and \(N\in \mathbb {N}\), consider the submodule of polynomials of total degree at most \(N\).
Lean Formalisation
def MvPolynomial.restrictTotalDegree.{u, v} (σ : Type u) (R : Type v) [CommSemiring R] (m : ℕ) :
Submodule R (MvPolynomial σ R)For a finite variable set \(\sigma \), the space of real polynomials of total degree at most \(N\) is finite-dimensional.
Lean Formalisation
theorem MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite.{u, v} (σ : Type u) (R : Type v) [CommSemiring R]
[Finite σ] (N : ℕ) : Module.Finite R ↥(MvPolynomial.restrictTotalDegree σ R N)5.3.1 Tensor-product domains
Products of univariate orthogonal families are orthogonal for product measures. Multiplication by a coordinate acts on one factor only, so the univariate recurrences determine the multivariate multiplication matrices. Total degree organises the products into finite polynomial spaces, while the product measure makes their pairings factor into one-dimensional pairings.
Reference details: Product moments, bases and strict positivity
Finite polynomial moments are preserved under finite products. Orthogonal coordinate sequences with positive squared norms form a basis of every complete multivariate total-degree space. Strict positivity of every coordinate polynomial pairing implies strict positivity of the product pairing. These results impose no interval or compact-support assumption.
Lean Formalisation
theorem MvPolynomial.hasFiniteMoments_pi.{u_1} {σ : Type u_1} [Fintype σ] (μ : σ → MeasureTheory.Measure ℝ)
(hμ : ∀ (i : σ), Polynomial.HasFiniteMoments (μ i)) : MvPolynomial.HasFiniteMoments (MeasureTheory.Measure.pi μ)Lean proof
/-- Finite polynomial moments are preserved under finite products of measures. -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasFiniteMoments_pi (μ : σ → Measure ℝ)
(hμ : ∀ i, Polynomial.HasFiniteMoments (μ i)) : HasFiniteMoments (Measure.pi μ) := by
let : ∀ i, IsFiniteMeasure (μ i) := fun i ↦ (hμ i).isFiniteMeasure
have hm : ∀ p : MvPolynomial σ ℝ, MemLp (fun x ↦ eval x p) 2 (Measure.pi μ) := by
intro p
induction p using MvPolynomial.induction_on' with
| monomial d a =>
apply (memLp_two_iff_integrable_sq (monomial d a).continuous_eval.aestronglyMeasurable).2
have hi := Integrable.fintype_prod (fun i ↦ hμ i (Polynomial.X ^ d i))
convert hi.const_mul (a ^ 2) using 1
funext x
simp [eval_monomial, Finsupp.prod_fintype, mul_pow, Finset.prod_pow]
| add p q hp hq =>
apply MemLp.ae_eq (hf_Lp := hp.add hq)
filter_upwards [] with x
simp only [Pi.add_apply, eval_add]
intro p
exact (memLp_two_iff_integrable_sq p.continuous_eval.aestronglyMeasurable).1 (hm p)Multiplication by coordinate \(x_i\) is exactly multiplication by \(x\) in factor \(i\). For \(\sigma \)-finite factor measures, pairing \(x_i\) times a product with another product gives the product of the univariate pairings, with \(x\) acting in factor \(i\). If each coordinate sequence is orthogonal for its factor measure, these pairing entries vanish when any other coordinate degree changes; if each factor measure also has finite polynomial moments, they vanish when the \(i\)th degree changes by more than one.
Lean Formalisation
theorem MvPolynomial.tensorProductPolynomial_update.{u_1} {σ : Type u_1} [Fintype σ] [DecidableEq σ] (p : σ → Polynomial ℝ)
(i : σ) (q : Polynomial ℝ) :
MvPolynomial.tensorProductPolynomial (Function.update p i q) =
Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X i) q *
∏ j ∈ Finset.univ.erase i, Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X j) (p j)Lean proof
/-- Updating one factor leaves the product of all the other factors unchanged. -/
theorem tensorProductPolynomial_update (p : σ → ℝ[X]) (i : σ) (q : ℝ[X]) :
tensorProductPolynomial (Function.update p i q) =
q.eval₂ C (X i) * ∏ j ∈ Finset.univ.erase i, (p j).eval₂ C (X j) := by
unfold tensorProductPolynomial
have he : (fun j ↦ (Function.update p i q j).eval₂ C (X j)) =
Function.update (fun j ↦ (p j).eval₂ C (X j)) i (q.eval₂ C (X i)) := by
funext j
by_cases hj : j = i
· subst j; simp
· simp [Function.update_of_ne hj]
rw [he, Finset.prod_update_of_mem (Finset.mem_univ i)]
rw [show (Finset.univ \ {i} : Finset σ) = Finset.univ.erase i by
ext j
simp [ne_comm]]Orthogonal polynomials on tensor-product domains: see Theorems 5.3.10, 5.3.11 and 5.3.13.
Supporting results: factored pairings and coordinates
For a finite coordinate set, the product of univariate polynomial factors is an actual multivariate polynomial of degree at most the sum of their degrees. Under a product of sigma-finite measures, its pairing with another coordinate product is the product of the coordinate pairings. Orthogonal coordinate sequences give orthogonal multiindices; normalized factors give normalized products.
Lean Formalisation
theorem MvPolynomial.eval_tensorProductPolynomial.{u_1} {σ : Type u_1} [Fintype σ] (p : σ → Polynomial ℝ) (x : σ → ℝ) :
(MvPolynomial.eval x) (MvPolynomial.tensorProductPolynomial p) = ∏ i, Polynomial.eval (x i) (p i)Lean proof
/-- Evaluation is the pointwise product of the univariate evaluations. -/
@[simp] theorem eval_tensorProductPolynomial (p : σ → ℝ[X]) (x : σ → ℝ) :
eval x (tensorProductPolynomial p) = ∏ i, (p i).eval (x i) := by
simp [tensorProductPolynomial, eval_eval₂_C_X]If each coordinate family is normalized, every complete tensor degree basis has identity Gram matrix and its coordinates are the exact polynomial integral projections.
Lean Formalisation
theorem MvPolynomial.integralGram_tensorProductDegreeBasis.{u_1} {σ : Type u_1} [Fintype σ] [DecidableEq σ]
(μ : σ → MeasureTheory.Measure ℝ) (P : σ → Polynomial.Sequence ℝ) (hμ : ∀ (i : σ), Polynomial.HasFiniteMoments (μ i))
(hP : ∀ (i : σ), (P i).IsOrthogonal (μ i))
(hn :
∀ (i : σ) (n : ℕ), 0 < Polynomial.integralInner (μ i) (Polynomial.IntegrablePair.of (μ i) (↑(P i) n) (↑(P i) n) ⋯))
(hnorm :
∀ (i : σ) (n : ℕ), Polynomial.integralInner (μ i) (Polynomial.IntegrablePair.of (μ i) (↑(P i) n) (↑(P i) n) ⋯) = 1)
(N : ℕ) :
MvPolynomial.integralGram (MeasureTheory.Measure.pi μ)
(fun i => ↑((MvPolynomial.tensorProductDegreeBasis μ P hμ hP hn N) i)) ⋯ =
1Lean proof
/-- Normalized factors give identity Gram matrix on every complete degree section. -/
theorem integralGram_tensorProductDegreeBasis (μ : σ → Measure ℝ)
(P : σ → Polynomial.Sequence ℝ) (hμ : ∀ i, Polynomial.HasFiniteMoments (μ i))
(hP : ∀ i, (P i).IsOrthogonal (μ i))
(hn : ∀ i n, 0 < Polynomial.integralInner (μ i) (Polynomial.IntegrablePair.of (μ i) (P i n) (P i n)))
(hnorm : ∀ i n, Polynomial.integralInner (μ i) (Polynomial.IntegrablePair.of (μ i) (P i n) (P i n)) = 1) (N : ℕ) :
integralGram (Measure.pi μ)
(fun i ↦ (tensorProductDegreeBasis μ P hμ hP hn N i : MvPolynomial σ ℝ)) = 1 := by
classical
let : ∀ i, IsFiniteMeasure (μ i) := fun i ↦ (hμ i).isFiniteMeasure
ext i j
simp only [integralGram, tensorProductDegreeBasis_apply, Matrix.one_apply]
by_cases hij : i = j
· subst j
rw [ite_eq_left rfl]
exact integralInner_tensorProductPolynomial_self μ _ (fun t ↦ (hμ t).integrable_mul _ _) (fun t ↦ hnorm t (i.1 t))
· rw [ite_eq_right hij]
apply integralInner_tensorProductPolynomial_eq_zero μ P hP
intro h
exact hij (Subtype.ext (Finsupp.ext (fun t ↦ congrFun h t)))5.3.2 The triangle: Proriol polynomials
On the triangle the Proriol polynomials couple an outer Jacobi polynomial in \(x\) to an inner one in \(y/x\), scaled by \(x^k\) so the result is a polynomial. Coordinate multiplication couples only neighbouring degrees, and raising any weight parameter by an integer gives a sparse conversion with banded inner blocks.
For real \(\alpha ,\beta ,\gamma \), write \(\widetilde P_j^{(a,b)}(x)=P_j^{(a,b)}(2x-1)\), and for a polynomial \(q(z)=\sum _j c_jz^j\) of degree at most \(k\) let \(x^kq(y/x)\) denote the polynomial \(\sum _j c_jy^jx^{k-j}\). Define
used for \(0\le k\le n\).
Lean Formalisation
def MvPolynomial.proriol (α β γ : ℝ) (n k : ℕ) : MvPolynomial (Fin 2) ℝLean definition
/-- Proriol triangle polynomials in the standard Jacobi normalization (DLMF 18.37.7). -/
noncomputable def proriol (α β γ : ℝ) (n k : ℕ) : MvPolynomial (Fin 2) ℝ :=
(shiftedJacobi α (β + γ + 2 * k + 1) (n - k)).eval₂ C (X 0) *
scaledLift Polynomial.X 1 k (shiftedJacobi β γ k)For \(x\ne 0\),
the triangle polynomial of [DLMF, 18.37.7] on \(0{\lt}y{\lt}x{\lt}1\). For all real \(x,z\), including \(x=0\), \(Q_{n,k}^{\alpha ,\beta ,\gamma }(x,xz)=\widetilde P_{n-k}^{(\alpha ,\beta +\gamma +2k+1)}(x)\, x^k\, \widetilde P_k^{(\beta ,\gamma )}(z)\). If \(k\le n\), the polynomial has total degree at most \(n\).
Lean Formalisation
theorem MvPolynomial.eval_proriol (α β γ : ℝ) (n k : ℕ) (x y : ℝ) (hx : x ≠ 0) :
(MvPolynomial.eval ![x, y]) (MvPolynomial.proriol α β γ n k) =
Polynomial.eval (2 * x - 1) (Polynomial.jacobi α (β + γ + 2 * ↑k + 1) (n - k)) * x ^ k *
Polynomial.eval (2 * (y / x) - 1) (Polynomial.jacobi β γ k)Lean proof
/-- Away from x=0, this is exactly the displayed Jacobi formula in DLMF 18.37.7. -/
theorem eval_proriol (α β γ : ℝ) (n k : ℕ) (x y : ℝ) (hx : x ≠ 0) :
eval (![x, y] : Fin 2 → ℝ) (proriol α β γ n k) =
(jacobi α (β + γ + 2 * k + 1) (n - k)).eval (2 * x - 1) * x ^ k *
(jacobi β γ k).eval (2 * (y / x) - 1) := by
simpa [eval_shiftedJacobi, mul_div_cancel₀ y hx] using
eval_proriol_scaled α β γ n k x (y / x)For \(\alpha ,\beta ,\gamma {\gt}-1\), distinct valid triangular indices give orthogonal Proriol polynomials for the standard triangle measure. Write \(h_j^{(a,b)}\) for the standard Jacobi squared norm. Then
The product formula includes degree zero without introducing singular Gamma quotients.
Reference: [DLMF, 18.37.8].
Lean Formalisation
theorem MvPolynomial.integralInner_proriolMeasure_eq_zero {α β γ : ℝ} (hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) {n k m j : ℕ}
(hk : k ≤ n) (hj : j ≤ m) (hne : (n, k) ≠ (m, j)) :
MvPolynomial.integralInner (MvPolynomial.proriolMeasure α β γ)
(MvPolynomial.IntegrablePair.of (MvPolynomial.proriolMeasure α β γ) (MvPolynomial.proriol α β γ n k)
(MvPolynomial.proriol α β γ m j) ⋯) =
0Lean proof
/-- Proriol orthogonality for the standard DLMF triangle measure. -/
theorem integralInner_proriolMeasure_eq_zero {α β γ : ℝ}
(hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ)
{n k m j : ℕ} (hk : k ≤ n) (hj : j ≤ m) (hne : (n,k) ≠ (m,j)) :
integralInner (proriolMeasure α β γ) (IntegrablePair.of (proriolMeasure α β γ) (proriol α β γ n k) (proriol α β γ m j)) = 0 := by
rw [integralInner, integral_proriolMeasure _ _ _ ⟨_, (hasFiniteMoments_proriolProductMeasure hα hβ hγ).integrable_mul _ _⟩]
change _ * integralInner (proriolProductMeasure α β γ) (IntegrablePair.of (proriolProductMeasure α β γ) _ _ (h := (hasFiniteMoments_proriolProductMeasure hα hβ hγ).integrable_mul _ _)) = 0
rw [integralInner_proriol_eq_zero hα hβ hγ hk hj hne, mul_zero]For \(\alpha ,\beta ,\gamma {\gt}-1\), the polynomials \(Q_{n,k}\) with \(0\le k\le n\le N\) form a basis of the complete total-degree-\(N\) space. Coordinates are \(\langle p,Q_{n,k}\rangle /\| Q_{n,k}\| ^2\) in the standard triangle measure. This measure has finite polynomial moments and a strictly positive polynomial pairing.
Reference: [DX14, Section 2.4].
Lean Formalisation
theorem MvPolynomial.proriolDegreeBasis_apply {α β γ : ℝ} (hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) (N : ℕ)
(d : { d // (d.sum fun x e => e) ≤ N }) :
↑((MvPolynomial.proriolDegreeBasis hα hβ hγ N) d) = MvPolynomial.proriol α β γ (↑d 0 + ↑d 1) (↑d 1)Lean proof
/-- The finite basis uses the DLMF normalization, without rescaling its members. -/
@[simp] theorem proriolDegreeBasis_apply {α β γ : ℝ}
(hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) (N : ℕ)
(d : {d : Fin 2 →₀ ℕ // d.sum (fun _ e ↦ e) ≤ N}) :
(proriolDegreeBasis hα hβ hγ N d : MvPolynomial (Fin 2) ℝ) =
proriol α β γ (d.1 0+d.1 1) (d.1 1) := by
simp [proriolDegreeBasis, proriolDegreeFamily]This measure has finite polynomial moments and a strictly positive polynomial pairing, supplying the hypotheses of the general Gram/Cholesky construction.
Reference details: Classical Proriol multiplication entry and related results
For real parameters and natural indices, the multiplication-entry domain requires integrability of \(x_\ell Q_{n,k}Q_{m,j}\) and \(Q_{m,j}^2\) for the Proriol measure, together with a strictly positive target squared norm \(h_{m,j}=\int Q_{m,j}^2\, d\mu \). Define the multiplication entry by \(M^\ell _{(m,j),(n,k)}=(\int x_\ell Q_{n,k}Q_{m,j}\, d\mu )/h_{m,j}\). This local domain does not require positivity for other polynomial pairings.
Lean Formalisation
inductive MvPolynomial.ProriolMultiplicationInput (α β γ : ℝ) (coord : Fin 2) (n k m j : ℕ) : PropLean definition
/-- Classical mixed-pairing and nonzero target-norm data for one multiplication entry. -/
structure ProriolMultiplicationInput (α β γ : ℝ) (coord : Fin 2) (n k m j : ℕ) : Prop where
mixed : Integrable (fun x => eval x (X coord * proriol α β γ n k)*eval x (proriol α β γ m j))
(proriolMeasure α β γ)
square : Integrable (fun x => (eval x (proriol α β γ m j))^2) (proriolMeasure α β γ)
positive : 0 < ∫ x, (eval x (proriol α β γ m j))^2 ∂proriolMeasure α β γOn the multiplication-entry domain,
The integrand is integrable and \(h_{m,j}{\gt}0\). For \(\alpha ,\beta ,\gamma {\gt}-1\), these conditions hold for every choice of natural indices and either coordinate.
Lean Formalisation
theorem MvPolynomial.ProriolMultiplicationInput.of_neg_one_lt {α β γ : ℝ} (hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ)
(coord : Fin 2) (n k m j : ℕ) : MvPolynomial.ProriolMultiplicationInput α β γ coord n k m jLean proof
/-- The full orthogonality range supplies every classical Proriol multiplication entry. -/
theorem ProriolMultiplicationInput.of_neg_one_lt {α β γ : ℝ}
(hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) (coord : Fin 2) (n k m j : ℕ) :
ProriolMultiplicationInput α β γ coord n k m j :=
⟨(hasFiniteMoments_proriolMeasure hα hβ hγ).integrable_mul _ _,
hasFiniteMoments_proriolMeasure hα hβ hγ _, integral_sq_proriolMeasure_pos hα hβ hγ m j⟩For valid indices and \(\alpha ,\beta ,\gamma {\gt}-1\), the coefficient of \(Q_{m,j}\) in either \(xQ_{n,k}\) or \(yQ_{n,k}\) vanishes when \(|m-n|{\gt}1\). For \(x\) it also vanishes unless \(j=k\); for \(y\) it vanishes when \(|j-k|{\gt}1\). These are actual coordinates in any containing complete degree space, in the normalization of [DLMF]: both matrices are block tridiagonal, with diagonal inner blocks for \(x\) and tridiagonal inner blocks for \(y\).
Reference: [GO20, Section 2.2].
Lean Formalisation
theorem MvPolynomial.proriolMultiplicationEntry_eq_repr {α β γ : ℝ} (hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) (coord : Fin 2)
(n k N : ℕ) (p : ↥(MvPolynomial.restrictTotalDegree (Fin 2) ℝ N))
(hp : ↑p = MvPolynomial.X coord * MvPolynomial.proriol α β γ n k) (i : { d // (d.sum fun x e => e) ≤ N }) :
MvPolynomial.proriolMultiplicationEntry α β γ coord n k (↑i 0 + ↑i 1) (↑i 1) ⋯ =
((MvPolynomial.proriolDegreeBasis hα hβ hγ N).repr p) iLean proof
/-- These entries agree with coordinates in any containing complete degree space. -/
theorem proriolMultiplicationEntry_eq_repr {α β γ : ℝ}
(hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) (coord : Fin 2) (n k N : ℕ)
(p : restrictTotalDegree (Fin 2) ℝ N) (hp : (p : MvPolynomial (Fin 2) ℝ) =
X coord * proriol α β γ n k)
(i : {d : Fin 2 →₀ ℕ // d.sum (fun _ e ↦ e) ≤ N}) :
proriolMultiplicationEntry α β γ coord n k (i.1 0+i.1 1) (i.1 1) =
(proriolDegreeBasis hα hβ hγ N).repr p i := by
rw [proriolDegreeBasis_repr]
simp only [hp]
rflReference details: All integer Proriol parameter shifts
For admissible \(\alpha ,\beta ,\gamma \) and nonnegative integers \(a,b,c\), raising these parameters multiplies the weight by \(u=(1-x)^a(x-y)^b y^c\). This holds for every polynomial integral and Gram pairing; \(\deg u\le a+b+c\).
Lean Formalisation
theorem MvPolynomial.totalDegree_proriolShiftDensity_le (a b c : ℕ) :
(MvPolynomial.proriolShiftDensity a b c).totalDegree ≤ a + b + cLean proof
/-- The degree of the modifying density is bounded by the sum of the shifts. -/
theorem totalDegree_proriolShiftDensity_le (a b c : ℕ) :
(proriolShiftDensity a b c).totalDegree ≤ a+b+c := by
have hx : (1-X 0 : MvPolynomial (Fin 2) ℝ).totalDegree ≤ 1 :=
(totalDegree_sub _ _).trans (by simp)
have hy : (X 0-X 1 : MvPolynomial (Fin 2) ℝ).totalDegree ≤ 1 :=
(totalDegree_sub _ _).trans (by simp)
have ha : ((1-X 0 : MvPolynomial (Fin 2) ℝ)^a).totalDegree ≤ a :=
(totalDegree_pow _ _).trans (by simpa using Nat.mul_le_mul_left a hx)
have hb : ((X 0-X 1 : MvPolynomial (Fin 2) ℝ)^b).totalDegree ≤ b :=
(totalDegree_pow _ _).trans (by simpa using Nat.mul_le_mul_left b hy)
have hc : ((X 1 : MvPolynomial (Fin 2) ℝ)^c).totalDegree ≤ c := by simp
exact (totalDegree_mul _ _).trans
(Nat.add_le_add ((totalDegree_mul _ _).trans (Nat.add_le_add ha hb)) hc)For \(\alpha ,\beta ,\gamma {\gt}-1\) and an integer \(r\ge 0\), replacing \(\alpha \) by \(\alpha +r\) multiplies the triangle weight by \((1-x)^r\) at the level of every polynomial integral and Gram pairing. In the expansion of a source \(Q_{n,k}\) in the new Proriol basis, the coefficient of the target \(Q_{m,j}\) is zero unless \(j=k\) and \(m\le n\le m+r\).
Lean Formalisation
theorem MvPolynomial.integral_proriolMeasure_alpha_add_nat {α β γ : ℝ} (hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) (r : ℕ)
(p : MvPolynomial (Fin 2) ℝ) :
∫ (v : Fin 2 → ℝ), (MvPolynomial.eval v) p ∂MvPolynomial.proriolMeasure (α + ↑r) β γ =
∫ (v : Fin 2 → ℝ), (MvPolynomial.eval v) ((1 - MvPolynomial.X 0) ^ r * p) ∂MvPolynomial.proriolMeasure α β γLean proof
/-- Raising the outer parameter is the polynomial density change (1-x)^r. -/
theorem integral_proriolMeasure_alpha_add_nat {α β γ : ℝ}
(hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) (r : ℕ)
(p : MvPolynomial (Fin 2) ℝ) :
∫ v, eval v p ∂proriolMeasure (α+r) β γ =
∫ v, eval v ((1-X 0)^r*p) ∂proriolMeasure α β γ := by
rw [integral_proriolMeasure_density (by linarith [Nat.cast_nonneg (α := ℝ) r]) hβ hγ,
integral_proriolMeasure_density hα hβ hγ]
simp only [map_mul, map_pow, map_sub, map_one, eval_X, Matrix.cons_val_zero]
apply integral_congr_ae
filter_upwards [] with x
rw [Real.rpow_add (by linarith [x.property.2] : 0 < 1-(x : ℝ)), Real.rpow_natCast]
have he (y : Set.Ioo (0 : ℝ) (x : ℝ)) : ((x : ℝ)-(y : ℝ))^β * (y : ℝ)^γ * ((1-(x : ℝ))^r * eval (![(x : ℝ),(y : ℝ)] : Fin 2 → ℝ) p) =
(1-(x : ℝ))^r * (((x : ℝ)-(y : ℝ))^β * (y : ℝ)^γ * eval (![(x : ℝ),(y : ℝ)] : Fin 2 → ℝ) p) := by ring
simp_rw [he]
rw [integral_const_mul]
ringFor nonnegative integer parameter shifts \((a,b,c)\) as in Theorem 5.3.21, the coefficient of the target \(Q_{m,j}\) in a source \(Q_{n,k}\) vanishes unless
The statement concerns actual coordinates in every complete finite degree space.
Lean Formalisation
theorem Polynomial.integralInner_shiftedJacobi_add_nat_eq_zero {α β : ℝ} (hα : -1 < α) (hβ : -1 < β) (a b k j : ℕ)
(hgap : k < j ∨ j + (a + b) < k) :
Polynomial.integralInner (Polynomial.unitJacobiMeasure (α + ↑a) (β + ↑b))
(Polynomial.IntegrablePair.of (Polynomial.unitJacobiMeasure (α + ↑a) (β + ↑b)) (Polynomial.shiftedJacobi α β k)
(Polynomial.shiftedJacobi (α + ↑a) (β + ↑b) j) ⋯) =
0Lean proof
/-- Mixed shifted Jacobi pairings have the finite modification bandwidth. -/
theorem integralInner_shiftedJacobi_add_nat_eq_zero {α β : ℝ}
(hα : -1 < α) (hβ : -1 < β) (a b k j : ℕ) (hgap : k < j ∨ j+(a+b) < k) :
integralInner (unitJacobiMeasure (α+a) (β+b)) (IntegrablePair.of (unitJacobiMeasure (α+a) (β+b)) (shiftedJacobi α β k) (shiftedJacobi (α+a) (β+b) j) (h := (hasFiniteMoments_unitJacobiMeasure (by have := Nat.cast_nonneg (α := ℝ) a; linarith) (by have := Nat.cast_nonneg (α := ℝ) b; linarith)).integrable_mul _ _)) = 0 := by
have hαa : -1 < α+a := by linarith [Nat.cast_nonneg (α := ℝ) a]
have hβb : -1 < β+b := by linarith [Nat.cast_nonneg (α := ℝ) b]
rcases hgap with h | h
· apply (isOrthogonal_shiftedJacobiSequence hαa hβb).integralInner_eq_zero_of_degree_lt
(hasFiniteMoments_unitJacobiMeasure hαa hβb)
exact degree_le_natDegree.trans_lt (by
exact_mod_cast (natDegree_shiftedJacobi_le α β k).trans_lt h)
· rw [integralInner_comm, integralInner_unitJacobiMeasure_add_nat α β a b _ _
(hi := (hasFiniteMoments_unitJacobiMeasure hαa hβb).integrable_mul _ _)
(hj := (hasFiniteMoments_unitJacobiMeasure hα hβ).integrable_mul _ _)]
apply mul_eq_zero_of_right
apply (isOrthogonal_shiftedJacobiSequence hα hβ).integralInner_eq_zero_of_degree_lt
(hasFiniteMoments_unitJacobiMeasure hα hβ)
apply degree_le_natDegree.trans_lt
have hpow : ((1-X : ℝ[X])^a).natDegree ≤ a := by
rw [natDegree_pow]
have hd : (1-X : ℝ[X]).natDegree ≤ 1 := (natDegree_sub_le _ _).trans (by simp)
simpa using Nat.mul_le_mul_left a hd
have hd := natDegree_mul_le (p := (1-X)^a) (q := (X^b : ℝ[X]))
have hd' := natDegree_mul_le (p := (1-X)^a*X^b) (q := shiftedJacobi (α+a) (β+b) j)
have hj := natDegree_shiftedJacobi_le (α+a) (β+b) j
simp only [natDegree_X_pow] at hd
have hdeg : (((1-X)^a*X^b)*shiftedJacobi (α+a) (β+b) j).natDegree ≤ j+(a+b) := by omega
exact_mod_cast hdeg.trans_lt hSupporting results: affine Jacobi measures and the triangle measure
On the open interval \((0,1)\), set \(\widehat w_{\alpha ,\beta }(x)=2w_{\alpha ,\beta }(2x-1)\).
Lean Formalisation
def Polynomial.unitJacobiWeight (α β : ℝ) : C(↑(Set.Ioo 0 1), NNReal)Lean definition
/-- The affine Jacobi density, including its mass-preserving factor. -/
def unitJacobiWeight (α β : ℝ) : C(Ioo (0 : ℝ) 1, ℝ≥0) where
toFun x := 2 * jacobiWeight α β
⟨2 * (x : ℝ) - 1, by constructor <;> linarith [x.property.1, x.property.2]⟩
continuous_toFun := by
apply continuous_const.mul
apply (jacobiWeight α β).continuous.comp
apply Continuous.subtype_mk
fun_propFor every \(x\in (0,1)\), \(\widehat w_{\alpha ,\beta }(x)=2^{\alpha +\beta +1}(1-x)^\alpha x^\beta \).
Lean Formalisation
theorem Polynomial.unitJacobiWeight_apply (α β : ℝ) (x : ↑(Set.Ioo 0 1)) :
↑((Polynomial.unitJacobiWeight α β) x) = 2 ^ (α + β + 1) * ((1 - ↑x) ^ α * ↑x ^ β)Lean proof
/-- The affine density formula has positive bases at every typed point. -/
theorem unitJacobiWeight_apply (α β : ℝ) (x : Ioo (0 : ℝ) 1) :
(unitJacobiWeight α β x : ℝ) =
(2 : ℝ) ^ (α + β + 1) * ((1 - (x : ℝ)) ^ α * (x : ℝ) ^ β) :=
two_mul_jacobiWeight_affine α β x.propertyLet \(\widehat\mu _{\alpha ,\beta }\) be the pushforward of \(\mu _{\alpha ,\beta }\) by \(t\mapsto (t+1)/2\). Set \(\widehat P_n^{(\alpha ,\beta )}(x)=P_n^{(\alpha ,\beta )}(2x-1)\).
Lean Formalisation
def Polynomial.unitJacobiMeasure (α β : ℝ) : MeasureTheory.Measure ℝLean definition
/-- Jacobi measure transported to [0,1], with its original total mass. -/
noncomputable def unitJacobiMeasure (α β : ℝ) : Measure ℝ :=
Measure.map (fun t : ℝ ↦ (t + 1) / 2) (jacobiMeasure α β)For a measurable \(f\in \mathcal I(\widehat\mu _{\alpha ,\beta })\), the product \(\widehat w_{\alpha ,\beta }f\) is integrable on the open interval \((0,1)\), and
Lean Formalisation
theorem Polynomial.integrable_unitJacobiWeight_mul (α β : ℝ)
(f : MeasureTheory.IntegrableInput (Polynomial.unitJacobiMeasure α β)) (hf : Measurable ↑f) :
MeasureTheory.Integrable (fun x => ↑((Polynomial.unitJacobiWeight α β) x) * ↑f ↑x) MeasureTheory.volumeLean proof
/-- A measurable integrable input has an integrable subtype density product. -/
theorem integrable_unitJacobiWeight_mul (α β : ℝ)
(f : IntegrableInput (unitJacobiMeasure α β)) (hf : Measurable f.val) :
Integrable (fun x : Ioo (0 : ℝ) 1 ↦ (unitJacobiWeight α β x : ℝ) * f.val x) volume := by
have _ := hf
exact (integral_unitJacobiMeasure_subtype_data α β f).1The shifted Jacobi polynomials are orthogonal for \(\widehat\mu _{\alpha ,\beta }\) when \(\alpha ,\beta {\gt}-1\). For arbitrary real \(\alpha ,\beta \), \(r\in \mathbb {N}\) and measurable \(f\in \mathcal I(\widehat\mu _{\alpha ,\beta +r})\), the function \(x^rf(x)\) is integrable for \(\widehat\mu _{\alpha ,\beta }\) and
Lean Formalisation
theorem Polynomial.integral_pow_unitJacobiMeasure_integrable (α β : ℝ) (k : ℕ)
(f : MeasureTheory.IntegrableInput (Polynomial.unitJacobiMeasure α (β + ↑k))) (hf : Measurable ↑f) :
MeasureTheory.Integrable (fun x => x ^ k * ↑f x) (Polynomial.unitJacobiMeasure α β) ∧
∫ (x : ℝ), x ^ k * ↑f x ∂Polynomial.unitJacobiMeasure α β =
(2 ^ k)⁻¹ * ∫ (x : ℝ), ↑f x ∂Polynomial.unitJacobiMeasure α (β + ↑k)Lean proof
/-- Radial powers preserve every convergent measurable input in the shifted measure. -/
theorem integral_pow_unitJacobiMeasure_integrable (α β : ℝ) (k : ℕ)
(f : IntegrableInput (unitJacobiMeasure α (β + k))) (hf : Measurable f.val) :
Integrable (fun x ↦ x ^ k * f.val x) (unitJacobiMeasure α β) ∧
(∫ x, x ^ k * f.val x ∂unitJacobiMeasure α β) =
((2 : ℝ) ^ k)⁻¹ * ∫ x, f.val x ∂unitJacobiMeasure α (β + k) := by
rcases f with ⟨f,hfint⟩
simp only at *
have hi : Integrable (fun x ↦ x^k*f x) (unitJacobiMeasure α β) := by
rw [unitJacobiMeasure, integrable_map_measure (by fun_prop) (by fun_prop),
integrable_jacobiMeasure_iff]
have h := hfint
rw [unitJacobiMeasure, integrable_map_measure hf.aestronglyMeasurable (by fun_prop),
integrable_jacobiMeasure_iff] at h
convert h.const_mul ((2 : ℝ)^k)⁻¹ using 1
ext x
rw [jacobiWeight_beta_add_nat]
change _ * (((x+1)/2)^k*f ((x+1)/2)) = _
rw [div_pow]
dsimp only [Function.comp_def]
ring
refine ⟨hi, ?_⟩
have hx : Integrable (fun t : ℝ ↦ ((t+1)/2)^k*f ((t+1)/2)) (jacobiMeasure α β) :=
(integrable_map_measure (by fun_prop) (by fun_prop)).mp hi
have hy : Integrable (fun t : ℝ ↦ f ((t+1)/2)) (jacobiMeasure α (β+k)) :=
(integrable_map_measure hf.aestronglyMeasurable (by fun_prop)).mp hfint
rw [integral_unitJacobiMeasure α β ⟨_,hi⟩,integral_unitJacobiMeasure α (β+k) ⟨f,hfint⟩,
integral_jacobiMeasure α β ⟨_,hx⟩,integral_jacobiMeasure α (β+k) ⟨_,hy⟩,
← integral_const_mul]
apply integral_congr_ae
filter_upwards [] with x
rw [jacobiWeight_beta_add_nat]
rw [div_pow]
ringFor \(\alpha ,\beta ,\gamma {\gt}-1\), transport \(\widehat\mu _{\alpha ,\beta +\gamma +1}\otimes \widehat\mu _{\beta ,\gamma }\) by \((x,z)\mapsto (x,xz)\) and multiply by \(2^{-c}\), where \(c=\alpha +2\beta +2\gamma +3\). Polynomial integrals in the resulting measure are exactly
Thus the auxiliary affine mass has been removed from the weight of [DLMF, 18.37.8].
The standard triangle measure has all polynomial moments.
Reference: [DLMF, 18.37.8].
Lean Formalisation
theorem MvPolynomial.integral_proriolProductMeasure_density {α β γ : ℝ} (hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ)
(p : MvPolynomial (Fin 2) ℝ) :
∫ (v : Fin 2 → ℝ), (MvPolynomial.eval v) p ∂MvPolynomial.proriolProductMeasure α β γ =
2 ^ (α + 2 * β + 2 * γ + 3) *
∫ (x : ↑(Set.Ioo 0 1)),
(1 - ↑x) ^ α * ∫ (y : ↑(Set.Ioo 0 ↑x)), (↑x - ↑y) ^ β * ↑y ^ γ * (MvPolynomial.eval ![↑x, ↑y]) pLean proof
/-- Polynomial integrals have the standard triangular weight and the explicit affine mass. -/
theorem integral_proriolProductMeasure_density {α β γ : ℝ}
(hα : -1 < α) (hβ : -1 < β) (hγ : -1 < γ) (p : MvPolynomial (Fin 2) ℝ) :
∫ v, eval v p ∂proriolProductMeasure α β γ =
(2 : ℝ)^(α+2*β+2*γ+3) *
∫ x : Ioo (0 : ℝ) 1, (1-(x : ℝ))^α *
∫ y : Ioo (0 : ℝ) (x : ℝ), ((x : ℝ)-(y : ℝ))^β * (y : ℝ)^γ *
eval (![(x : ℝ),(y : ℝ)] : Fin 2 → ℝ) p := by
let μ := unitJacobiMeasure α (β+γ+1)
let ν := unitJacobiMeasure β γ
let := isFiniteMeasure_unitJacobiMeasure hα (show -1 < β+γ+1 by linarith)
let := isFiniteMeasure_unitJacobiMeasure hβ hγ
have hm : Integrable (fun v ↦ eval v p) (proriolProductMeasure α β γ) := by
simpa only [proriolProductMeasure, map_one, mul_one] using
(hasFiniteMoments_proriolProductMeasure hα hβ hγ).integrable_mul p 1
have ht := koornwinderMeasure_integral_univ (fun x ↦ x) continuous_id μ ν
⟨fun v ↦ eval v p, hm⟩
have hi := ht.1
have hc : Continuous (fun v : ℝ × ℝ ↦ eval (![v.1,v.1*v.2] : Fin 2 → ℝ) p) := by
exact p.continuous_eval.comp (by fun_prop)
have hf : Measurable (fun x ↦ ∫ z, eval (![x,x*z] : Fin 2 → ℝ) p ∂ν) :=
hc.stronglyMeasurable.integral_prod_right'.measurable
have hzi (x : ℝ) : Integrable (fun z ↦ eval (![x,x*z] : Fin 2 → ℝ) p) ν := by
have hzcont : Continuous (fun z : ℝ ↦ eval (![x,x*z] : Fin 2 → ℝ) p) :=
p.continuous_eval.comp (by fun_prop)
rw [show ν = unitJacobiMeasure β γ from rfl, unitJacobiMeasure,
integrable_map_measure hzcont.aestronglyMeasurable (by fun_prop)]
exact integrable_jacobiMeasure hβ hγ (p.continuous_eval.comp (by fun_prop)).continuousOn
have hin (x : ℝ) := integral_unitJacobiMeasure_subtype β γ
⟨(fun z ↦ eval (![x,x*z] : Fin 2 → ℝ) p), hzi x⟩
((p.continuous_eval.comp (by fun_prop)).measurable)
rw [proriolProductMeasure, ht.2, integral_prod _ hi]
change (∫ x, (∫ z, eval (![x,x*z] : Fin 2 → ℝ) p ∂ν) ∂μ) = _
rw [integral_unitJacobiMeasure_subtype _ _ ⟨_,hi.integral_prod_left⟩ hf]
simp only
simp_rw [unitJacobiWeight_apply]
rw [← integral_const_mul]
apply integral_congr_ae
filter_upwards [] with x
rw [hin x]
simp only
simp_rw [unitJacobiWeight_apply, mul_assoc]
rw [integral_const_mul]
have hzint := integrable_unitJacobiMeasure_density_input β γ
⟨(fun z ↦ eval (![(x : ℝ),(x : ℝ)*z] : Fin 2 → ℝ) p),hzi x⟩
have hd := integral_duffy_jacobi β γ x.property.1
⟨(fun y ↦ eval (![(x : ℝ),y] : Fin 2 → ℝ) p),hzint⟩
simp only [mul_assoc] at hd
rw [← hd]
have htwo : (2 : ℝ)^(α+(β+γ+1)+1) * (2 : ℝ)^(β+γ+1) =
(2 : ℝ)^(α+2*β+2*γ+3) := by
rw [← Real.rpow_add (by norm_num : (0 : ℝ) < 2)]
congr 1
ring
rw [← htwo]
ring5.3.3 The disk: Dunkl–Xu and Zernike polynomials
The disk has two classical bases. The Cartesian Dunkl–Xu polynomials separate \(x\) from \(y/\sqrt{1-x^2}\); a parity lift keeps them polynomial, even on the boundary. Raising the weight parameter multiplies the measure by \(1-x^2-y^2\) and gives a four-term connection with explicit coefficients. The Zernike polynomials instead separate radius and angle, which makes them natural for the Laplacian and for annuli.
Reference details: Polynomial lift for Cartesian disk families
For \(p(x)=\sum _j c_jx^j\) define the bivariate polynomial \(L_np(x,y)=\sum _{j=0}^n c_j y^j(1-x^2)^{\lfloor (n-j)/2\rfloor }\).
Lean Formalisation
def MvPolynomial.diskLift.{u_1} {R : Type u_1} [CommRing R] (n : ℕ) (p : Polynomial R) : MvPolynomial (Fin 2) RLean definition
/-- The parity lift used by Cartesian disk polynomials. Its separated-function
interpretation requires the input polynomial to have parity `n`. -/
noncomputable def diskLift (n : ℕ) (p : Polynomial R) : MvPolynomial (Fin 2) R :=
∑ j ∈ Finset.range (n + 1),
C (p.coeff j) * X 1 ^ j * (1 - X 0 ^ 2) ^ ((n - j) / 2)Its evaluation on the disk, for \(p\) of degree at most \(n\) and parity \(n\), is Theorem 5.3.100.
The definition uses no division or square roots.
Set \(D_{n,k}^{\beta }(x,y)=P_{n-k}^{(\beta +k+1/2,\beta +k+1/2)}(x) L_kP_k^{(\beta ,\beta )}(x,y)\), using \(0\le k\le n\) in the degree-\(n\) block. This is the Cartesian Jacobi normalization, with increasing \(k\) within a block; it is not yet orthonormally scaled.
Reference: [DX14, Section 2.3].
Lean Formalisation
def MvPolynomial.dunklXuDisk (β : ℝ) (n k : ℕ) : MvPolynomial (Fin 2) ℝLean definition
/-- Cartesian Dunkl–Xu polynomials in Jacobi normalization. The degree-indexed
family uses `k ≤ n`; the formula is defined for all natural indices. -/
noncomputable def dunklXuDisk (β : ℝ) (n k : ℕ) : MvPolynomial (Fin 2) ℝ :=
(Polynomial.jacobi (β + k + 1 / 2) (β + k + 1 / 2) (n - k)).eval₂ C (X 0) *
diskLift k (Polynomial.jacobi β β k)For \(x^2{\lt}1\), put \(s=\sqrt{1-x^2}\). Then \(D_{n,k}^{\beta }(x,y)=P_{n-k}^{(\beta +k+1/2,\beta +k+1/2)}(x)s^kP_k^{(\beta ,\beta )}(y/s)\). The defining polynomial has total degree at most \(n\) when \(k\le n\) and is well defined on the boundary too. Its constant member is one; the \(k=0\) subfamily is the symmetric Jacobi family in \(x\).
Reference: [DX14, Section 2.3].
Lean Formalisation
theorem MvPolynomial.eval_dunklXuDisk (β : ℝ) (n k : ℕ) (v : Fin 2 → ℝ) (hv : v 0 ^ 2 < 1) :
(MvPolynomial.eval v) (MvPolynomial.dunklXuDisk β n k) =
Polynomial.eval (v 0) (Polynomial.jacobi (β + ↑k + 1 / 2) (β + ↑k + 1 / 2) (n - k)) *
(√(1 - v 0 ^ 2) ^ k * Polynomial.eval (v 1 / √(1 - v 0 ^ 2)) (Polynomial.jacobi β β k))Lean proof
/-- The standard separated Jacobi formula holds throughout the open vertical
strip, in particular on the disk interior. -/
theorem eval_dunklXuDisk (β : ℝ) (n k : ℕ) (v : Fin 2 → ℝ)
(hv : v 0 ^ 2 < 1) :
eval v (dunklXuDisk β n k) =
(Polynomial.jacobi (β + k + 1 / 2) (β + k + 1 / 2) (n - k)).eval (v 0) *
(Real.sqrt (1 - v 0 ^ 2) ^ k *
(Polynomial.jacobi β β k).eval (v 1 / Real.sqrt (1 - v 0 ^ 2))) := by
have hs : Real.sqrt (1 - v 0 ^ 2) ≠ 0 :=
ne_of_gt (Real.sqrt_pos.mpr (by linarith))
rw [dunklXuDisk, map_mul, eval_eval₂_C_X,
eval_diskLift_scaled k _ (Polynomial.natDegree_jacobi_le β β k)
(Polynomial.coeff_jacobi_symmetric_eq_zero_of_parity β k) v
(Real.sqrt (1 - v 0 ^ 2)) (v 1 / Real.sqrt (1 - v 0 ^ 2))]
· rw [Real.sq_sqrt (by linarith)]
· field_simpReference details: Measurability domain of the product measure and related results
For an outer measure \(\mu \), the admissible inner measures \(\nu \) are those for which the measure-valued map \(x\mapsto (y\mapsto (x,y))_*\nu \) is \(\mu \)-almost-everywhere measurable. This is the measurability condition used to form the product measure \(\mu \otimes \nu \).
Lean Formalisation
inductive MeasureTheory.ProductMeasureInput.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
(μ : MeasureTheory.Measure α) : Type u_2Lean definition
/-- Inner measures with a certified product kernel over the outer measure. -/
structure ProductMeasureInput {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
(μ : Measure α) where
inner : Measure β
measurable : AEMeasurable (fun x : α ↦ Measure.map (Prod.mk x) inner) μFor every measurable set \(A\), the product measure satisfies \((\mu \otimes \nu )(A)=\int \nu (\{ y:(x,y)\in A\} )\, d\mu (x)\), where the integral is nonnegative and may be infinite.
Lean Formalisation
theorem MeasureTheory.ProductMeasureInput.prod_apply.{u_1, u_2} {α : Type u_1} {β : Type u_2} [MeasurableSpace α]
[MeasurableSpace β] {μ : MeasureTheory.Measure α} (ν : MeasureTheory.ProductMeasureInput μ) {s : Set (α × β)}
(hs : MeasurableSet s) : (μ.prod ν.inner) s = ∫⁻ (x : α), ν.inner (Prod.mk x ⁻¹' s) ∂μLean proof
theorem ProductMeasureInput.prod_apply {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
{μ : Measure α} (ν : ProductMeasureInput (β := β) μ) {s : Set (α × β)}
(hs : MeasurableSet s) :
(μ.prod ν.inner) s = ∫⁻ x, ν.inner ((Prod.mk x) ⁻¹' s) ∂μ := by
rw [Measure.prod, Measure.bind_apply hs ν.measurable]
apply lintegral_congr
intro x
exact Measure.map_apply measurable_prodMk_left hsFor a real polynomial \(p\), write \(D_p=\{ x\in \mathbb R:p(x)\ge 0\} \). For a measure \(\eta \) on \(D_p\), its polynomial density measure is the real-coordinate pushforward of \(p\, d\eta \). The density has values in \([0,\infty )\) on its entire domain.
Lean Formalisation
def Polynomial.polynomialDensityMeasure (p : Polynomial ℝ) (μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval x p }) :
MeasureTheory.Measure ℝLean definition
/-- Weight a measure on the nonnegative locus of a polynomial and return its real-coordinate measure. -/
noncomputable def polynomialDensityMeasure (p : ℝ[X])
(μ : Measure {x : ℝ // 0 ≤ p.eval x}) : Measure ℝ :=
Measure.map Subtype.val
(μ.withDensity (fun x => ENNReal.ofNNReal (NNReal.mk (p.eval (x : ℝ)) x.property)))For every measurable \(E\subseteq \mathbb R\), the polynomial density measure assigns \(\int _{\iota ^{-1}(E)}p(x)\, d\eta (x)\), interpreted as a nonnegative integral, where \(\iota :D_p\hookrightarrow \mathbb R\) is the coordinate inclusion.
Lean Formalisation
theorem Polynomial.polynomialDensityMeasure_apply (p : Polynomial ℝ)
(μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval x p }) {s : Set ℝ} (hs : MeasurableSet s) :
(p.polynomialDensityMeasure μ) s =
∫⁻ (x : { x // 0 ≤ Polynomial.eval x p }) in Subtype.val ⁻¹' s, ↑(NNReal.mk (Polynomial.eval (↑x) p) ⋯) ∂μLean proof
/-- Evaluation on measurable sets is the nonnegative weighted source measure. -/
theorem polynomialDensityMeasure_apply (p : ℝ[X])
(μ : Measure {x : ℝ // 0 ≤ p.eval x}) {s : Set ℝ} (hs : MeasurableSet s) :
polynomialDensityMeasure p μ s =
∫⁻ x in Subtype.val ⁻¹' s, ENNReal.ofNNReal (NNReal.mk (p.eval (x : ℝ)) x.property) ∂μ := by
rw [polynomialDensityMeasure, Measure.map_apply measurable_subtype_coe hs,
withDensity_apply _ (measurable_subtype_coe hs)]For \(k\in \mathbb N\), let \(D_k=\{ x\in \mathbb R:(1-x^2)^k\ge 0\} \). For a measure \(\eta \) on \(D_k\), the shifted disk outer measure is the real-coordinate pushforward of \((1-x^2)^k\, d\eta (x)\). The domain is all of \(\mathbb R\) for even \(k\) and \([-1,1]\) for odd \(k\).
Lean Formalisation
def Polynomial.diskOuterMeasure (k : ℕ)
(μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval x ((1 - Polynomial.X ^ 2) ^ k) }) : MeasureTheory.Measure ℝLean definition
/-- The outer density is defined on its full nonnegative locus at degree k. -/
noncomputable def diskOuterMeasure (k : ℕ)
(μ : Measure {x : ℝ // 0 ≤ ((1-X^2 : ℝ[X])^k).eval x}) : Measure ℝ :=
polynomialDensityMeasure ((1-X^2)^k) μFor every measurable \(E\subseteq \mathbb R\), the shifted measure assigns the nonnegative integral \(\int _{\iota ^{-1}(E)}(1-x^2)^k\, d\eta (x)\). At degree zero, a real measure transported to \(D_0=\mathbb R\) is recovered unchanged.
Lean Formalisation
theorem Polynomial.diskOuterMeasure_apply (k : ℕ)
(μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval x ((1 - Polynomial.X ^ 2) ^ k) }) {s : Set ℝ}
(hs : MeasurableSet s) :
(Polynomial.diskOuterMeasure k μ) s =
∫⁻ (x : { x // 0 ≤ Polynomial.eval x ((1 - Polynomial.X ^ 2) ^ k) }) in Subtype.val ⁻¹' s,
↑(NNReal.mk (Polynomial.eval (↑x) ((1 - Polynomial.X ^ 2) ^ k)) ⋯) ∂μLean proof
/-- Values on measurable sets are the nonnegative weighted source integrals. -/
theorem diskOuterMeasure_apply (k : ℕ)
(μ : Measure {x : ℝ // 0 ≤ ((1-X^2 : ℝ[X])^k).eval x})
{s : Set ℝ} (hs : MeasurableSet s) :
diskOuterMeasure k μ s = ∫⁻ x in Subtype.val ⁻¹' s,
ENNReal.ofNNReal (NNReal.mk (((1-X^2 : ℝ[X])^k).eval (x : ℝ)) x.property) ∂μ :=
polynomialDensityMeasure_apply _ μ hsFor every real \(\alpha \) and \(k\in \mathbb N\), transport the symmetric Jacobi measure \(\mu _{\alpha ,\alpha }\) to \(D_k=\{ x:(1-x^2)^k\ge 0\} \). Its outer degree-\(k\) shift equals \(\mu _{\alpha +k,\alpha +k}\).
Lean Formalisation
theorem Polynomial.diskOuterMeasure_jacobi (α : ℝ) (k : ℕ) :
Polynomial.diskOuterMeasure k (MeasureTheory.Measure.comap Subtype.val (Polynomial.jacobiMeasure α α)) =
Polynomial.jacobiMeasure (α + ↑k) (α + ↑k)Lean proof
/-- The outer Cartesian shift equals the integer symmetric Jacobi measure shift,
including parameters with infinite mass. Reference: Dunkl–Xu, disk families. -/
theorem diskOuterMeasure_jacobi (α : ℝ) (k : ℕ) :
diskOuterMeasure k ((jacobiMeasure α α).comap Subtype.val) =
jacobiMeasure (α+k) (α+k) := by
obtain ⟨w, hw, hwval, _, he⟩ := exists_polynomialDensityMeasure_extension ((1-X^2 : ℝ[X])^k)
rw [diskOuterMeasure, he]
apply Measure.ext_of_lintegral
intro φ hφ
rw [lintegral_withDensity_eq_lintegral_mul _ hw.coe_nnreal_ennreal hφ]
simp only [jacobiMeasure, openIntervalWeightMeasure,
(MeasurableEmbedding.subtype_coe measurableSet_Ioo).lintegral_map]
erw [lintegral_withDensity_eq_lintegral_mul _
(jacobiWeight α α).continuous.measurable.coe_nnreal_ennreal
((hw.coe_nnreal_ennreal.mul hφ).comp measurable_subtype_coe),
lintegral_withDensity_eq_lintegral_mul _
(jacobiWeight (α+k) (α+k)).continuous.measurable.coe_nnreal_ennreal
(hφ.comp measurable_subtype_coe)]
apply lintegral_congr
intro x
have hx : 0 ≤ ((1-X^2 : ℝ[X])^k).eval (x : ℝ) := by
simp only [eval_pow, eval_sub, eval_one, eval_X]
exact pow_nonneg (by nlinarith [x.property.1, x.property.2]) _
simp only [Pi.mul_apply, Function.comp_apply]
rw [hwval x hx]
have hew : jacobiWeight (α+k) (α+k) x =
jacobiWeight α α x * NNReal.mk (((1-X^2 : ℝ[X])^k).eval (x : ℝ)) hx := by
apply NNReal.eq
simp only [NNReal.coe_mul, NNReal.coe_mk, eval_pow, eval_sub, eval_one, eval_X]
rw [jacobiWeight_add_nat]
ring
rw [hew, ENNReal.coe_mul, mul_assoc]For \(h\in \mathbb R[X]\) and \(l\in \mathbb N\), put \(w(x)=(1-x^2)^l h(x)\). A measure \(\eta \) on \(\{ x:w(x)\ge 0\} \) has modified outer measure given by the real-coordinate pushforward of \(w\, d\eta \). All source points lie in the nonnegative-density domain.
Lean Formalisation
def Polynomial.diskModificationWeight (h : Polynomial ℝ) (l : ℕ) : Polynomial ℝLean definition
/-- The outer factor required by a polynomially separated disk modification. -/
noncomputable def diskModificationWeight (h : ℝ[X]) (l : ℕ) : ℝ[X] := (1-X^2)^l*hFor every measurable \(E\subseteq \mathbb R\), the modified measure assigns \(\int _{\iota ^{-1}(E)}(1-x^2)^l h(x)\, d\eta (x)\) as a nonnegative integral.
Lean Formalisation
theorem Polynomial.diskOuterModification_apply (h : Polynomial ℝ) (l : ℕ)
(μ : MeasureTheory.Measure { x // 0 ≤ Polynomial.eval x (h.diskModificationWeight l) }) {s : Set ℝ}
(hs : MeasurableSet s) :
(h.diskOuterModification l μ) s =
∫⁻ (x : { x // 0 ≤ Polynomial.eval x (h.diskModificationWeight l) }) in Subtype.val ⁻¹' s,
↑(NNReal.mk (Polynomial.eval (↑x) (h.diskModificationWeight l)) ⋯) ∂μLean proof
/-- Values on measurable sets are the nonnegative polynomial-density integrals. -/
theorem diskOuterModification_apply (h : ℝ[X]) (l : ℕ)
(μ : Measure {x : ℝ // 0 ≤ (diskModificationWeight h l).eval x})
{s : Set ℝ} (hs : MeasurableSet s) :
diskOuterModification h l μ s = ∫⁻ x in Subtype.val ⁻¹' s,
ENNReal.ofNNReal (NNReal.mk ((diskModificationWeight h l).eval (x : ℝ)) x.property) ∂μ :=
polynomialDensityMeasure_apply _ μ hsThe Cartesian chart \((x,z)\mapsto (x,\sqrt{1-x^2}z)\) has domain \([-1,1]\times \mathbb {R}\). For a measure \(\mu \) on \([-1,1]\) and a real inner measure \(\nu \) with the product-kernel measurability condition of Definition 5.3.33, its pushforward of \(\mu \otimes \nu \) is the Cartesian measure. Real outer measures supported on \([-1,1]\) are transported to this domain. The disk measure uses the Jacobi factors \(\mu _{\beta +1/2,\beta +1/2}\) and \(\mu _{\beta ,\beta }\) in this construction. The disk orthogonality range is \(\beta {\gt}-1\).
Lean Formalisation
def MvPolynomial.diskCoordinates (v : ↑(Set.Icc (-1) 1) × ℝ) : Fin 2 → ℝLean definition
/-- Cartesian coordinates on the full classical strip. -/
noncomputable def diskCoordinates (v : Icc (-1 : ℝ) 1 × ℝ) : Fin 2 → ℝ :=
![(v.1 : ℝ), Real.sqrt (1-(v.1 : ℝ)^2)*v.2]Reference details: Characterisation of the Cartesian chart and pushforward and related results
The Cartesian disk chart \(\Phi (x,z)=(x,\sqrt{1-x^2}\, z)\) on \([-1,1]\times \mathbb {R}\) is continuous, including at \(x=\pm 1\), and \(1-x^2\ge 0\) on this domain. If \(f\) is integrable for the Cartesian measure \(\omega =\Phi _*(\mu \otimes \nu )\), then \(f\circ \Phi \) is integrable for \(\mu \otimes \nu \), and
Lean Formalisation
theorem MvPolynomial.continuous_diskCoordinates : Continuous MvPolynomial.diskCoordinatesLean proof
theorem continuous_diskCoordinates : Continuous diskCoordinates := by
unfold diskCoordinates
fun_propFor \(\beta {\gt}-1\), every continuous real-valued function on the plane is integrable for the Cartesian disk measure. All polynomial moments exist, and the measure is finite.
Lean Formalisation
theorem MvPolynomial.integrable_dunklXuDiskMeasure {β : ℝ} (hβ : -1 < β) {f : (Fin 2 → ℝ) → ℝ} (hf : Continuous f) :
MeasureTheory.Integrable f (MvPolynomial.dunklXuDiskMeasure β)Lean proof
/-- A continuous function on the plane is integrable for the disk measure. -/
theorem integrable_dunklXuDiskMeasure {β : ℝ} (hβ : -1 < β)
{f : (Fin 2 → ℝ) → ℝ} (hf : Continuous f) :
Integrable f (dunklXuDiskMeasure β) := by
let := isFiniteMeasure_jacobiMeasure hβ hβ
let := isFiniteMeasure_jacobiMeasure
(show -1 < β + 1 / 2 by linarith) (show -1 < β + 1 / 2 by linarith)
change Integrable f (Measure.map diskCoordinates
((Measure.comap (Subtype.val : Icc (-1 : ℝ) 1 → ℝ)
(jacobiMeasure (β + 1/2) (β + 1/2))).prod (jacobiMeasure β β)))
rw [integrable_map_measure hf.aestronglyMeasurable
continuous_diskCoordinates.measurable.aemeasurable]
have hi := (hf.comp continuous_diskCoordinates).continuousOn.integrableOn_compact
(μ := (Measure.comap (Subtype.val : Icc (-1 : ℝ) 1 → ℝ)
(jacobiMeasure (β + 1/2) (β + 1/2))).prod (jacobiMeasure β β))
(isCompact_univ.prod isCompact_Icc :
IsCompact (univ ×ˢ Icc (-1 : ℝ) 1 : Set (Icc (-1 : ℝ) 1 × ℝ)))
have ha : ∀ᵐ v ∂(Measure.comap (Subtype.val : Icc (-1 : ℝ) 1 → ℝ)
(jacobiMeasure (β + 1/2) (β + 1/2))).prod (jacobiMeasure β β),
v ∈ (univ ×ˢ Icc (-1 : ℝ) 1 : Set (Icc (-1 : ℝ) 1 × ℝ)) := by
filter_upwards [Measure.quasiMeasurePreserving_snd.ae
(ae_mem_Ioo_jacobiMeasure β β)] with v hz
exact ⟨mem_univ _, hz.1.le, hz.2.le⟩
rwa [IntegrableOn, Measure.restrict_eq_self_of_ae_mem ha] at hiFor \(\beta \in \mathbb {R}\) and \(x,z\in (-1,1)\), put \(r_x=\sqrt{1-x^2}\). Writing \(w_{a,b}\) for the Jacobi weight,
Lean Formalisation
theorem MvPolynomial.diskCoordinates_weight (β : ℝ) (x z : ↑(Set.Ioo (-1) 1)) :
↑((Polynomial.jacobiWeight (β + 1 / 2) (β + 1 / 2)) x) * ↑((Polynomial.jacobiWeight β β) z) =
√(1 - ↑x ^ 2) * (1 - ↑x ^ 2 - (√(1 - ↑x ^ 2) * ↑z) ^ 2) ^ βLean proof
/-- The disk Jacobian identity for domain-typed Jacobi weights. -/
theorem diskCoordinates_weight (β : ℝ) (x z : Ioo (-1 : ℝ) 1) :
(jacobiWeight (β + 1 / 2) (β + 1 / 2) x : ℝ) * (jacobiWeight β β z : ℝ) =
Real.sqrt (1 - (x : ℝ) ^ 2) *
(1 - (x : ℝ) ^ 2 - (Real.sqrt (1 - (x : ℝ) ^ 2) * (z : ℝ)) ^ 2) ^ β := by
have hx0 : 0 < 1 - (x : ℝ)^2 := by nlinarith [x.property.1,x.property.2]
have hz0 : 0 ≤ 1 - (z : ℝ)^2 := by nlinarith [z.property.1,z.property.2]
change ((1-(x : ℝ))^(β+1/2)*(1+(x : ℝ))^(β+1/2)) *
((1-(z : ℝ))^β*(1+(z : ℝ))^β) = _
rw [symmetricWeight _ _ x.property, symmetricWeight _ _ z.property]
rw [show 1-(x : ℝ)^2-(Real.sqrt (1-(x : ℝ)^2)*(z : ℝ))^2 =
(1-(x : ℝ)^2)*(1-(z : ℝ)^2) by rw [mul_pow, Real.sq_sqrt hx0.le]; ring,
Real.mul_rpow hx0.le hz0, Real.rpow_add hx0, Real.sqrt_eq_rpow]
ringFor \(\beta {\gt}-1\), continuous \(f:\mathbb {R}^2\to \mathbb {R}\), and \(x\in (-1,1)\), put \(r_x=\sqrt{1-x^2}\). The function
is denoted by \(F_{\beta ,f,x}\). Its domain is the open slice \((-r_x,r_x)\).
Lean Formalisation
def MvPolynomial.diskSliceInput (β : ↑(Set.Ioi (-1))) (f : C(Fin 2 → ℝ, ℝ)) (x : ↑(Set.Ioo (-1) 1)) :
MeasureTheory.IntegrableInput MeasureTheory.volumeLean definition
/-- The classical weighted integrand on a vertical open disk slice.
Reference: Dunkl–Xu, disk measures and Cartesian coordinates. -/
noncomputable def diskSliceInput (β : Ioi (-1 : ℝ))
(f : C((Fin 2 → ℝ), ℝ)) (x : Ioo (-1 : ℝ) 1) :
IntegrableInput (volume : Measure (Ioo (-Real.sqrt (1-(x : ℝ)^2))
(Real.sqrt (1-(x : ℝ)^2)))) :=
⟨fun y ↦ (1-(x : ℝ)^2-(y : ℝ)^2)^(β : ℝ) * f ![(x : ℝ),(y : ℝ)], by
exact integrable_diskSlice β.property x f.continuous⟩For \(\beta {\gt}-1\), continuous \(f:\mathbb {R}^2\to \mathbb {R}\), \(x\in (-1,1)\) and \(y\in (-\sqrt{1-x^2},\sqrt{1-x^2})\), the base \(1-x^2-y^2\) is positive. The function \(F_{\beta ,f,x}(y)=(1-x^2-y^2)^\beta f(x,y)\) is Lebesgue-integrable on that open slice, including when \(-1{\lt}\beta {\lt}0\).
Lean Formalisation
theorem MvPolynomial.diskSlice_radical_pos (x : ↑(Set.Ioo (-1) 1)) (y : ↑(Set.Ioo (-√(1 - ↑x ^ 2)) √(1 - ↑x ^ 2))) :
0 < 1 - ↑x ^ 2 - ↑y ^ 2Lean proof
theorem diskSlice_radical_pos (x : Ioo (-1 : ℝ) 1)
(y : Ioo (-Real.sqrt (1-(x : ℝ)^2)) (Real.sqrt (1-(x : ℝ)^2))) :
0 < 1-(x : ℝ)^2-(y : ℝ)^2 := by
have hA : 0 < 1-(x : ℝ)^2 := by nlinarith [x.property.1,x.property.2]
have hr := Real.sqrt_pos.2 hA
have hr2 := Real.sq_sqrt hA.le
nlinarith [y.property.1,y.property.2]For \(\beta {\gt}-1\) and continuous \(f:\mathbb {R}^2\to \mathbb {R}\), set \(r_x=\sqrt{1-x^2}\) for \(x\in (-1,1)\) and define
The integrand is the slice function of Definition 5.3.46.
Lean Formalisation
def MvPolynomial.diskSlicesInput (β : ↑(Set.Ioi (-1))) (f : C(Fin 2 → ℝ, ℝ)) :
MeasureTheory.IntegrableInput MeasureTheory.volumeLean definition
/-- The integrable outer function formed from the classical vertical slices. -/
noncomputable def diskSlicesInput (β : Ioi (-1 : ℝ))
(f : C((Fin 2 → ℝ), ℝ)) : IntegrableInput (volume : Measure (Ioo (-1 : ℝ) 1)) :=
⟨fun x ↦ ∫ y, (diskSliceInput β f x).val y, by
apply (integrable_integral_dunklXuDiskMeasure_iterated β f).1.congr
exact Filter.Eventually.of_forall (fun x ↦ (diskSliceInput_integral β f x).symm)⟩For \(\beta {\gt}-1\) and continuous \(f:\mathbb {R}^2\to \mathbb {R}\), the function
is Lebesgue-integrable on \((-1,1)\).
Lean Formalisation
theorem MvPolynomial.diskSlicesInput_integrable (β : ↑(Set.Ioi (-1))) (f : C(Fin 2 → ℝ, ℝ)) :
MeasureTheory.Integrable (↑(MvPolynomial.diskSlicesInput β f)) MeasureTheory.volumeLean proof
/-- The iterated slice integral has an integrable outer input. -/
theorem diskSlicesInput_integrable (β : Ioi (-1 : ℝ))
(f : C((Fin 2 → ℝ), ℝ)) :
Integrable (diskSlicesInput β f).val volume := (diskSlicesInput β f).integrableFor \(\beta {\gt}-1\) and continuous \(f\), integration against the disk measure is
Both integrals use the open-slice inputs of Definitions 5.3.46 and 5.3.48; all their integrands are classically integrable. There is no additional normalization constant.
Lean Formalisation
theorem MvPolynomial.integral_dunklXuDiskMeasure_eq_slices (β : ↑(Set.Ioi (-1))) (f : C(Fin 2 → ℝ, ℝ)) :
∫ (v : Fin 2 → ℝ), f v ∂MvPolynomial.dunklXuDiskMeasure ↑β =
∫ (x : ↑(Set.Ioo (-1) 1)), ↑(MvPolynomial.diskSlicesInput β f) xLean proof
theorem integral_dunklXuDiskMeasure_eq_slices (β : Ioi (-1 : ℝ))
(f : C((Fin 2 → ℝ), ℝ)) :
(∫ v, f v ∂dunklXuDiskMeasure β) = ∫ x, (diskSlicesInput β f).val x := by
rw [(integrable_integral_dunklXuDiskMeasure_iterated β f).2]
change _ = ∫ x : Ioo (-1 : ℝ) 1, ∫ y, (diskSliceInput β f x).val y
simp_rw [diskSliceInput_integral]Integrability and finiteness of moments are given by Theorem 5.3.44.
For \(\beta {\gt}-1\), distinct valid pairs \((n,k)\) are orthogonal. Writing \(h_r^{\alpha ,\alpha }\) for the usual Jacobi squared norm,
Reference: [DX14, Section 2.3].
Lean Formalisation
theorem MvPolynomial.integral_mul_dunklXuDisk_eq_zero {β : ℝ} (hβ : -1 < β) {n k m j : ℕ} (hk : k ≤ n) (hj : j ≤ m)
(hne : (n, k) ≠ (m, j)) :
∫ (v : Fin 2 → ℝ),
(MvPolynomial.eval v) (MvPolynomial.dunklXuDisk β n k) *
(MvPolynomial.eval v) (MvPolynomial.dunklXuDisk β m j) ∂MvPolynomial.dunklXuDiskMeasure β =
0Lean proof
/-- Distinct valid disk indices are orthogonal. -/
theorem integral_mul_dunklXuDisk_eq_zero {β : ℝ} (hβ : -1 < β)
{n k m j : ℕ} (hk : k ≤ n) (hj : j ≤ m) (hne : (n, k) ≠ (m, j)) :
∫ v, eval v (dunklXuDisk β n k) * eval v (dunklXuDisk β m j)
∂dunklXuDiskMeasure β = 0 := by
by_cases hkj : k = j
· subst j
rw [integral_mul_dunklXuDisk_same_inner hβ,
integral_mul_jacobi_eq_zero
(show -1 < β + k + 1 / 2 by have := Nat.cast_nonneg (α := ℝ) k; linarith)
(show -1 < β + k + 1 / 2 by have := Nat.cast_nonneg (α := ℝ) k; linarith)
(show n - k ≠ m - k by intro h; apply hne; congr 1; omega), zero_mul]
· exact integral_mul_dunklXuDisk_eq_zero_of_inner_ne hβ n k m j hkjThe disk polynomials through degree \(N\) form a basis of the full bivariate polynomial space of degree at most \(N\). The full family, indexed by \(n\ge 0\) and \(0\le k\le n\), is a basis of the polynomial algebra. Every nonzero polynomial has strictly positive squared integral for \(\beta {\gt}-1\).
Lean Formalisation
theorem MvPolynomial.linearIndependent_dunklXuDisk {β : ℝ} (hβ : -1 < β) :
LinearIndependent ℝ fun i => MvPolynomial.dunklXuDisk β i.fst ↑i.sndLean proof
/-- The degree blocks with increasing inner index form a linearly independent family. -/
theorem linearIndependent_dunklXuDisk {β : ℝ} (hβ : -1 < β) :
LinearIndependent ℝ (fun i : Σ n : ℕ, Fin (n + 1) => dunklXuDisk β i.1 i.2) := by
apply LinearMap.BilinForm.linearIndependent_of_iIsOrtho
(B := integralBilinForm (dunklXuDiskMeasure β) (hasFiniteMoments_dunklXuDiskMeasure hβ))
· intro i j hij
apply integral_mul_dunklXuDisk_eq_zero hβ (by omega) (by omega)
intro h
apply hij
have hn := congrArg Prod.fst h
have hk := congrArg Prod.snd h
rcases i with ⟨n, k⟩
rcases j with ⟨m, l⟩
dsimp at hn hk
subst m
congr 1
exact Fin.ext hk
· intro i
change integralInner (dunklXuDiskMeasure β) (IntegrablePair.of (dunklXuDiskMeasure β) _ _) ≠ 0
rw [integralInner_self]
exact (integral_sq_dunklXuDisk_pos hβ i.1 i.2).ne'Reference details: Classical Dunkl–Xu polynomial norm and related results
For every parameter and index choice for which \((D_{n,k}^{\beta })^2\) is integrable with respect to \(\mu _\beta \), define
The domain consists of all such square-integrable polynomials; no additional parameter restrictions are imposed.
Lean Formalisation
def MvPolynomial.dunklXuNorm (β : ℝ)
(i :
{ i //
MeasureTheory.Integrable (fun v => (MvPolynomial.eval v) (MvPolynomial.dunklXuDisk β i.1 i.2) ^ 2)
(MvPolynomial.dunklXuDiskMeasure β) }) :
ℝLean definition
/-- The finite norm of a square-integrable Cartesian disk polynomial. -/
noncomputable def dunklXuNorm (β : ℝ)
(i : {i : ℕ × ℕ // Integrable (fun v ↦ eval v (dunklXuDisk β i.1 i.2)^2)
(dunklXuDiskMeasure β)}) : ℝ :=
Real.sqrt (∫ v, eval v (dunklXuDisk β i.val.1 i.val.2)^2 ∂dunklXuDiskMeasure β)Whenever \((D_{n,k}^{\beta })^2\) is \(\mu _\beta \)-integrable,
Lean Formalisation
theorem MvPolynomial.dunklXuNorm_nonneg (β : ℝ)
(i :
{ i //
MeasureTheory.Integrable (fun v => (MvPolynomial.eval v) (MvPolynomial.dunklXuDisk β i.1 i.2) ^ 2)
(MvPolynomial.dunklXuDiskMeasure β) }) :
0 ≤ MvPolynomial.dunklXuNorm β iLean proof
/-- The classical polynomial norm is nonnegative. -/
theorem dunklXuNorm_nonneg (β : ℝ)
(i : {i : ℕ × ℕ // Integrable (fun v ↦ eval v (dunklXuDisk β i.1 i.2)^2)
(dunklXuDiskMeasure β)}) : 0 ≤ dunklXuNorm β i :=
Real.sqrt_nonneg _Dividing by the positive square root of the product norm gives orthonormal polynomial bases, both globally and in each finite degree space. Coordinates are integral pairings; normalization multiplies raw coordinates by positive norm factors.
Lean Formalisation
theorem MvPolynomial.integralInner_normalizedDunklXuBasis {β : ℝ} (hβ : -1 < β) (i j : (n : ℕ) × Fin (n + 1)) :
MvPolynomial.integralInner (MvPolynomial.dunklXuDiskMeasure β)
(MvPolynomial.IntegrablePair.of (MvPolynomial.dunklXuDiskMeasure β) ((MvPolynomial.normalizedDunklXuBasis hβ) i)
((MvPolynomial.normalizedDunklXuBasis hβ) j) ⋯) =
if i = j then 1 else 0Lean proof
/-- The normalized disk basis is orthonormal for the integral pairing. -/
theorem integralInner_normalizedDunklXuBasis {β : ℝ} (hβ : -1 < β)
(i j : Σ n : ℕ, Fin (n + 1)) :
integralInner (dunklXuDiskMeasure β) (IntegrablePair.of (dunklXuDiskMeasure β) (normalizedDunklXuBasis hβ i) (normalizedDunklXuBasis hβ j)) = if i = j then 1 else 0 := by
classical
have hM := hasFiniteMoments_dunklXuDiskMeasure hβ
have he := congrArg₂ (fun p q => integralInner (dunklXuDiskMeasure β) (hM.pair p q))
(normalizedDunklXuBasis_apply hβ i) (normalizedDunklXuBasis_apply hβ j)
rw [he, integralInner_smul_left (h := hM.integrable_mul _ _), integralInner_comm,
integralInner_smul_left (h := hM.integrable_mul _ _), integralInner_comm]
by_cases hij : i = j
· subst j
rw [ite_eq_left rfl, integralInner_self]
have hp := integral_sq_dunklXuDisk_pos hβ i.1 i.2
have hs := Real.sq_sqrt hp.le
have hn := (Real.sqrt_pos.mpr hp).ne'
dsimp [dunklXuNorm]
field_simp
nlinarith
· rw [ite_eq_right hij]
have ho : integralInner (dunklXuDiskMeasure β) (IntegrablePair.of (dunklXuDiskMeasure β) (dunklXuDisk β i.1 i.2) (dunklXuDisk β j.1 j.2)) = 0 := by
apply integral_mul_dunklXuDisk_eq_zero hβ (by omega) (by omega)
intro h
apply hij
have hn := congrArg Prod.fst h
have hk := congrArg Prod.snd h
rcases i with ⟨n, k⟩
rcases j with ⟨m, l⟩
dsimp at hn hk
subst m
congr 1
exact Fin.ext hk
rw [ho]
ringThe next results describe how raising the disk weight changes coordinates: they give the support of the conversion matrix and the values and signs of its coefficients.
Reference details: Disk measure raising and related results
For \(\beta {\gt}-1\), increasing \(\beta \) by one multiplies the disk measure by \(1-x^2-y^2\), as an identity against every continuous real-valued test function on \(\mathbb R^2\) and in particular for all polynomial pairings.
Lean Formalisation
theorem MvPolynomial.integral_dunklXuDiskMeasure_add_one {β : ℝ} (hβ : -1 < β) {f : (Fin 2 → ℝ) → ℝ} (hf : Continuous f) :
∫ (v : Fin 2 → ℝ), f v ∂MvPolynomial.dunklXuDiskMeasure (β + 1) =
∫ (v : Fin 2 → ℝ), (MvPolynomial.eval v) MvPolynomial.diskBoundary * f v ∂MvPolynomial.dunklXuDiskMeasure βLean proof
/-- The unit disk parameter shift is precisely a boundary-polynomial density
change, stated for every continuous test function. -/
theorem integral_dunklXuDiskMeasure_add_one {β : ℝ} (hβ : -1 < β)
{f : (Fin 2 → ℝ) → ℝ} (hf : Continuous f) :
∫ v, f v ∂dunklXuDiskMeasure (β + 1) =
∫ v, eval v diskBoundary * f v ∂dunklXuDiskMeasure β := by
have hα : -1 < β+1/2 := by linarith
have hu : cartesianDiskModification 1 (1-Polynomial.X^2) 1 = diskBoundary := by
norm_num [cartesianDiskModification, cartesianDiskPolynomial, diskBoundary,
diskLift, Finset.sum_range_succ, Polynomial.coeff_one]
ring
have houter : diskOuterModification 1 1
((jacobiMeasure (β+1/2) (β+1/2)).comap Subtype.val) =
jacobiMeasure ((β+1/2)+1) ((β+1/2)+1) := by
exact (congrArg (fun p : ℝ[X] ↦ polynomialDensityMeasure p
((jacobiMeasure (β+1/2) (β+1/2)).comap Subtype.val))
(mul_one ((1-Polynomial.X^2)^1))).trans (by simpa only [diskOuterMeasure, Nat.cast_one] using diskOuterMeasure_jacobi (β+1/2) 1)
have hinner : Polynomial.polynomialDensityMeasure (1-Polynomial.X^2)
((jacobiMeasure β β).comap Subtype.val) = jacobiMeasure (β+1) (β+1) := by
exact (congrArg (fun p : ℝ[X] ↦ polynomialDensityMeasure p
((jacobiMeasure β β).comap Subtype.val))
(pow_one (1-Polynomial.X^2)).symm).trans (by simpa only [diskOuterMeasure, Nat.cast_one] using diskOuterMeasure_jacobi β 1)
have hg : ∀ᵐ x ∂jacobiMeasure β β, 0 ≤ (1-Polynomial.X^2 : ℝ[X]).eval x := by
filter_upwards [ae_mem_Icc_jacobiMeasure β β] with x hx
simp only [Polynomial.eval_sub, Polynomial.eval_one, Polynomial.eval_pow, Polynomial.eval_X]
nlinarith [hx.1,hx.2]
have hdeg : (1-Polynomial.X^2 : ℝ[X]).natDegree ≤ 2*1 := by compute_degree
have hpar : ∀ i, i%2 ≠ 0 → (1-Polynomial.X^2 : ℝ[X]).coeff i = 0 := by
intro i hi
have h0 : i ≠ 0 := by omega
have h2 : i ≠ 2 := by omega
simp [Polynomial.coeff_sub, Polynomial.coeff_one, h0, h2]
have he := integral_cartesianDiskModification
(hasFiniteMoments_jacobiMeasure hα hα) (hasFiniteMoments_jacobiMeasure hβ hβ)
(ae_mem_Icc_jacobiMeasure _ _) (ae_mem_Icc_jacobiMeasure _ _)
1 (1-Polynomial.X^2) 1 (by filter_upwards [] with x; simp) hg hdeg hpar hf
simp only [cartesianDiskMeasure] at he
simp only [houter, hinner, hu] at he
simpa only [dunklXuDiskMeasure, cartesianDiskMeasure, show β+1/2+1 = β+1+1/2 by ring] using heFor \(\beta \in \mathbb R\) and natural degrees, define
The domain at each degree requires exactly the displayed denominator to be nonzero; degree zero admits every real parameter.
Lean Formalisation
inductive Polynomial.JacobiSymmetricRaiseAInput (β : ℝ) (n : ℕ) : PropLean definition
/-- The index-dependent classical denominator domain for symmetric RaiseA coefficients. -/
structure JacobiSymmetricRaiseAInput (β : ℝ) (n : ℕ) : Prop where
nonzero : (match n with
| 0 => (1 : ℝ)
| 1 => β + 2
| m+2 => (2*(m : ℝ)+2*β+5)*(2*m+2*β+6)*(2*m+2*β+4)) ≠ 0The coefficient \(A_n(\beta )\) equals the expression in Definition 5.3.57 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem Polynomial.JacobiSymmetricRaiseAInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
Polynomial.JacobiSymmetricRaiseAInput β nLean proof
/-- The full orthogonality range lies in this classical coefficient domain. -/
theorem JacobiSymmetricRaiseAInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
JacobiSymmetricRaiseAInput β n := by
constructor
rcases n with _ | _ | n
· norm_num
· dsimp; linarith
· dsimp
have hn := Nat.cast_nonneg (α := ℝ) n
exact mul_ne_zero (mul_ne_zero (ne_of_gt (by linarith))
(ne_of_gt (by linarith))) (ne_of_gt (by linarith))Define \(B_0(\beta )=B_1(\beta )=0\) for every real \(\beta \), and
when its displayed denominator is nonzero.
Lean Formalisation
inductive Polynomial.JacobiSymmetricRaiseBInput (β : ℝ) (n : ℕ) : PropLean definition
/-- The index-dependent classical denominator domain for symmetric RaiseB coefficients. -/
structure JacobiSymmetricRaiseBInput (β : ℝ) (n : ℕ) : Prop where
nonzero : (match n with
| 0 => (1 : ℝ)
| 1 => 1
| m+2 => (2*(m : ℝ)+2*β+5)*(2*m+2*β+6)*(2*m+2*β+4)) ≠ 0The coefficient \(B_n(\beta )\) equals the expression in Definition 5.3.59 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem Polynomial.JacobiSymmetricRaiseBInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
Polynomial.JacobiSymmetricRaiseBInput β nLean proof
/-- The full orthogonality range lies in this classical coefficient domain. -/
theorem JacobiSymmetricRaiseBInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
JacobiSymmetricRaiseBInput β n := by
constructor
rcases n with _ | _ | n
· norm_num
· norm_num
· dsimp
have hn := Nat.cast_nonneg (α := ℝ) n
exact mul_ne_zero (mul_ne_zero (ne_of_gt (by linarith))
(ne_of_gt (by linarith))) (ne_of_gt (by linarith))Write \(D_n(\beta )=(2n+2\beta +2)(n+2\beta +2)(2n+2\beta +3)(2n+2\beta +4)\). For \(D_n(\beta )\ne 0\), define
Lean Formalisation
inductive Polynomial.JacobiSymmetricLowerInput (β : ℝ) (n : ℕ) : PropLean definition
/-- The index-dependent classical denominator domain for symmetric Lower coefficients. -/
structure JacobiSymmetricLowerInput (β : ℝ) (n : ℕ) : Prop where
nonzero : (2*(n : ℝ)+2*β+2)*((n : ℝ)+2*β+2)*(2*n+2*β+3)*(2*n+2*β+4) ≠ 0The coefficient \(E_n(\beta )\) equals the expression in Definition 5.3.61 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem Polynomial.JacobiSymmetricLowerInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
Polynomial.JacobiSymmetricLowerInput β nLean proof
/-- The full orthogonality range lies in this classical coefficient domain. -/
theorem JacobiSymmetricLowerInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
JacobiSymmetricLowerInput β n := by
constructor
have hn := Nat.cast_nonneg (α := ℝ) n
exact mul_ne_zero (mul_ne_zero (mul_ne_zero (ne_of_gt (by linarith))
(ne_of_gt (by linarith))) (ne_of_gt (by linarith))) (ne_of_gt (by linarith))With \(D_n(\beta )=(2n+2\beta +2)(n+2\beta +2)(2n+2\beta +3)(2n+2\beta +4)\), define
on the same domain \(D_n(\beta )\ne 0\).
Lean Formalisation
def Polynomial.jacobiSymmetricLowerB (β : ℝ) (n : ℕ)
(_d : Polynomial.JacobiSymmetricLowerInput β n := by
exact Polynomial.JacobiSymmetricLowerInput.of_neg_one_lt (by linarith) _) :
ℝLean definition
/-- The unchanged-degree coefficient for multiplication by the boundary polynomial. -/
noncomputable def jacobiSymmetricLowerB (β : ℝ) (n : ℕ)
(_d : JacobiSymmetricLowerInput β n := by exact Polynomial.JacobiSymmetricLowerInput.of_neg_one_lt (by linarith) _) : ℝ :=
((2 * n + 2 * β + 2) * (n + 2 * β + 2) *
(2 * n + 2 * β + 3) * (2 * n + 2 * β + 4))⁻¹ *
(4 * (n + β + 1) ^ 2 * (2 * n + 2 * β + 4) * (n + 2 * β + 2))The coefficient \(F_n(\beta )\) equals the expression in Definition 5.3.63 whenever its denominator conditions hold, including the separate low-degree cases specified there. The domain is the same as that of the degree-plus-two lowering coefficient.
Lean Formalisation
theorem Polynomial.jacobiSymmetricLowerB_apply (β : ℝ) (n : ℕ) (input : Polynomial.JacobiSymmetricLowerInput β n) :
Polynomial.jacobiSymmetricLowerB β n input =
((2 * ↑n + 2 * β + 2) * (↑n + 2 * β + 2) * (2 * ↑n + 2 * β + 3) * (2 * ↑n + 2 * β + 4))⁻¹ *
(4 * (↑n + β + 1) ^ 2 * (2 * ↑n + 2 * β + 4) * (↑n + 2 * β + 2))Lean proof
/-- Evaluation on the full classical coefficient domain. -/
theorem jacobiSymmetricLowerB_apply (β : ℝ) (n : ℕ) (input : JacobiSymmetricLowerInput β n) :
jacobiSymmetricLowerB β n input =
((2 * n + 2 * β + 2) * (n + 2 * β + 2) *
(2 * n + 2 * β + 3) * (2 * n + 2 * β + 4))⁻¹ *
(4 * (n + β + 1) ^ 2 * (2 * n + 2 * β + 4) * (n + 2 * β + 2)) := rflFor \(n\in \mathbb N\) and \(\beta \in \mathbb R\), when every constituent coefficient below is defined, set \(\widehat A_n(\beta )=A_n(\beta )A_n(\beta +1)\).
Lean Formalisation
inductive Polynomial.JacobiSymmetricDoubleRaiseAInput (β : ℝ) (n : ℕ) : PropLean definition
/-- Local classical inputs for the composed A coefficient. -/
structure JacobiSymmetricDoubleRaiseAInput (β : ℝ) (n : ℕ) : Prop where
a : JacobiSymmetricRaiseAInput β n
b : JacobiSymmetricRaiseAInput (β + 1) nThe coefficient \(\widehat A_n(\beta )\) equals the expression in Definition 5.3.65 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem Polynomial.JacobiSymmetricDoubleRaiseAInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
Polynomial.JacobiSymmetricDoubleRaiseAInput β nLean proof
/-- Admissible Jacobi parameters supply all constituent coefficient domains. -/
theorem JacobiSymmetricDoubleRaiseAInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
JacobiSymmetricDoubleRaiseAInput β n :=
⟨JacobiSymmetricRaiseAInput.of_neg_one_lt (by linarith) _, JacobiSymmetricRaiseAInput.of_neg_one_lt (by linarith) _⟩For \(n\in \mathbb N\) and \(\beta \in \mathbb R\), when every constituent coefficient below is defined, set \(\widehat B_n(\beta )=A_n(\beta )B_n(\beta +1)+B_n(\beta )A_{\max (n-2,0)}(\beta +1)\).
Lean Formalisation
inductive Polynomial.JacobiSymmetricDoubleRaiseBInput (β : ℝ) (n : ℕ) : PropLean definition
/-- Local classical inputs for the composed B coefficient. -/
structure JacobiSymmetricDoubleRaiseBInput (β : ℝ) (n : ℕ) : Prop where
a : JacobiSymmetricRaiseAInput β n
b : JacobiSymmetricRaiseBInput (β + 1) n
c : JacobiSymmetricRaiseBInput β n
d : JacobiSymmetricRaiseAInput (β + 1) (n - 2)The coefficient \(\widehat B_n(\beta )\) equals the expression in Definition 5.3.67 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem Polynomial.JacobiSymmetricDoubleRaiseBInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
Polynomial.JacobiSymmetricDoubleRaiseBInput β nLean proof
/-- Admissible Jacobi parameters supply all constituent coefficient domains. -/
theorem JacobiSymmetricDoubleRaiseBInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
JacobiSymmetricDoubleRaiseBInput β n :=
⟨JacobiSymmetricRaiseAInput.of_neg_one_lt (by linarith) _, JacobiSymmetricRaiseBInput.of_neg_one_lt (by linarith) _, JacobiSymmetricRaiseBInput.of_neg_one_lt (by linarith) _, JacobiSymmetricRaiseAInput.of_neg_one_lt (by linarith) _⟩For \(n\in \mathbb N\) and \(\beta \in \mathbb R\), when every constituent coefficient below is defined, set \(\widehat C_n(\beta )=B_n(\beta )B_{\max (n-2,0)}(\beta +1)\).
Lean Formalisation
inductive Polynomial.JacobiSymmetricDoubleRaiseCInput (β : ℝ) (n : ℕ) : PropLean definition
/-- Local classical inputs for the composed C coefficient. -/
structure JacobiSymmetricDoubleRaiseCInput (β : ℝ) (n : ℕ) : Prop where
a : JacobiSymmetricRaiseBInput β n
b : JacobiSymmetricRaiseBInput (β + 1) (n - 2)The coefficient \(\widehat C_n(\beta )\) equals the expression in Definition 5.3.69 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem Polynomial.JacobiSymmetricDoubleRaiseCInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
Polynomial.JacobiSymmetricDoubleRaiseCInput β nLean proof
/-- Admissible Jacobi parameters supply all constituent coefficient domains. -/
theorem JacobiSymmetricDoubleRaiseCInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n : ℕ) :
JacobiSymmetricDoubleRaiseCInput β n :=
⟨JacobiSymmetricRaiseBInput.of_neg_one_lt (by linarith) _, JacobiSymmetricRaiseBInput.of_neg_one_lt (by linarith) _⟩For \(n,k\in \mathbb N\) and \(\beta \in \mathbb R\), when every constituent coefficient is defined, set \(\mathcal A_{n,k}(\beta )=A_k(\beta )A_{\max (n-k,0)}(\beta +k+1/2)\).
Lean Formalisation
inductive MvPolynomial.DunklXuDiskRaiseAInput (β : ℝ) (n k : ℕ) : PropLean definition
/-- Constituent coefficient domains for the Cartesian A entry. -/
structure DunklXuDiskRaiseAInput (β : ℝ) (n k : ℕ) : Prop where
inner : JacobiSymmetricRaiseAInput β k
outer : JacobiSymmetricRaiseAInput (β + k + 1 / 2) (n-k)The coefficient \(\mathcal A_{n,k}(\beta )\) equals the expression in Definition 5.3.71 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem MvPolynomial.DunklXuDiskRaiseAInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
MvPolynomial.DunklXuDiskRaiseAInput β n kLean proof
/-- The full disk orthogonality range supplies the local coefficient inputs. -/
theorem DunklXuDiskRaiseAInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
DunklXuDiskRaiseAInput β n k := by
have hk := Nat.cast_nonneg (α := ℝ) k
have hk2 := Nat.cast_nonneg (α := ℝ) (k-2)
refine ⟨JacobiSymmetricRaiseAInput.of_neg_one_lt hβ _, ?_⟩
exact JacobiSymmetricRaiseAInput.of_neg_one_lt (by linarith) _For \(n,k\in \mathbb N\) and \(\beta \in \mathbb R\), when every constituent coefficient is defined, set \(\mathcal B_{n,k}(\beta )=A_k(\beta )B_{\max (n-k,0)}(\beta +k+1/2)\).
Lean Formalisation
inductive MvPolynomial.DunklXuDiskRaiseBInput (β : ℝ) (n k : ℕ) : PropLean definition
/-- Constituent coefficient domains for the Cartesian B entry. -/
structure DunklXuDiskRaiseBInput (β : ℝ) (n k : ℕ) : Prop where
inner : JacobiSymmetricRaiseAInput β k
outer : JacobiSymmetricRaiseBInput (β + k + 1 / 2) (n-k)The coefficient \(\mathcal B_{n,k}(\beta )\) equals the expression in Definition 5.3.73 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem MvPolynomial.DunklXuDiskRaiseBInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
MvPolynomial.DunklXuDiskRaiseBInput β n kLean proof
/-- The full disk orthogonality range supplies the local coefficient inputs. -/
theorem DunklXuDiskRaiseBInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
DunklXuDiskRaiseBInput β n k := by
have hk := Nat.cast_nonneg (α := ℝ) k
have hk2 := Nat.cast_nonneg (α := ℝ) (k-2)
refine ⟨JacobiSymmetricRaiseAInput.of_neg_one_lt hβ _, ?_⟩
exact JacobiSymmetricRaiseBInput.of_neg_one_lt (by linarith) _Let \(n,k\in \mathbb N\). For \(k{\lt}2\) the coefficient is zero for every real \(\beta \). For \(k\ge 2\), when every constituent coefficient is defined, set \(\mathcal C_{n,k}(\beta )=B_k(\beta )E_{\max (n-k,0)}(\beta +1+(k-2)+1/2)\).
Lean Formalisation
inductive MvPolynomial.DunklXuDiskRaiseCInput (β : ℝ) (n k : ℕ) : PropLean definition
/-- Constituent coefficient domains for the Cartesian C entry. -/
structure DunklXuDiskRaiseCInput (β : ℝ) (n k : ℕ) : Prop where
inner : JacobiSymmetricRaiseBInput β k
outer : 2 ≤ k → JacobiSymmetricLowerInput (β + 1 + (k - 2 : ℕ) + 1 / 2) (n-k)The coefficient \(\mathcal C_{n,k}(\beta )\) equals the expression in Definition 5.3.75 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem MvPolynomial.DunklXuDiskRaiseCInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
MvPolynomial.DunklXuDiskRaiseCInput β n kLean proof
/-- The full disk orthogonality range supplies the local coefficient inputs. -/
theorem DunklXuDiskRaiseCInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
DunklXuDiskRaiseCInput β n k := by
have hk := Nat.cast_nonneg (α := ℝ) k
have hk2 := Nat.cast_nonneg (α := ℝ) (k-2)
refine ⟨JacobiSymmetricRaiseBInput.of_neg_one_lt hβ _, ?_⟩
intro _
exact JacobiSymmetricLowerInput.of_neg_one_lt (by linarith) _Let \(n,k\in \mathbb N\). For \(k{\lt}2\) the coefficient is zero for every real \(\beta \). For \(k\ge 2\), when every constituent coefficient is defined, set \(\mathcal D_{n,k}(\beta )=B_k(\beta )F_{\max (n-k,0)}(\beta +1+(k-2)+1/2)\).
Lean Formalisation
inductive MvPolynomial.DunklXuDiskRaiseDInput (β : ℝ) (n k : ℕ) : PropLean definition
/-- Constituent coefficient domains for the Cartesian D entry. -/
structure DunklXuDiskRaiseDInput (β : ℝ) (n k : ℕ) : Prop where
inner : JacobiSymmetricRaiseBInput β k
outer : 2 ≤ k → JacobiSymmetricLowerInput (β + 1 + (k - 2 : ℕ) + 1 / 2) (n-k)The coefficient \(\mathcal D_{n,k}(\beta )\) equals the expression in Definition 5.3.77 whenever its denominator conditions hold, including the separate low-degree cases specified there. Every \(\beta {\gt}-1\) lies in this domain for every natural index.
Lean Formalisation
theorem MvPolynomial.DunklXuDiskRaiseDInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
MvPolynomial.DunklXuDiskRaiseDInput β n kLean proof
/-- The full disk orthogonality range supplies the local coefficient inputs. -/
theorem DunklXuDiskRaiseDInput.of_neg_one_lt {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
DunklXuDiskRaiseDInput β n k := by
have hk := Nat.cast_nonneg (α := ℝ) k
have hk2 := Nat.cast_nonneg (α := ℝ) (k-2)
refine ⟨JacobiSymmetricRaiseBInput.of_neg_one_lt hβ _, ?_⟩
intro _
exact JacobiSymmetricLowerInput.of_neg_one_lt (by linarith) _For \(\beta {\gt}-1\) and \(0\le k\le n\), the polynomial \(D_{n,k}^{\beta }\) belongs to the real span of \(D_{m,j}^{\beta +1}\) with
Omit indices that become negative; subtraction here is integer subtraction. For \(\beta {\gt}-1\) and natural indices \(k\le n\), put \(q=n-k\) and \(\gamma =\beta +k+1/2\). Define the four coefficients, in the displayed index order, by
Here \(A,B,E,F\) are the symmetric Jacobi coefficients on the domains specified in Theorem 5.3.101. When \(\beta {\gt}-1\), the unchanged-index coefficient is strictly positive. This is the ordinary unit parameter shift of the Cartesian disk family.
References: [DX14, Section 2.3]; the Cartesian disk raising operator in MultivariateOrthogonalPolynomials.jl [MOP].
Lean Formalisation
theorem MvPolynomial.dunklXuDisk_raise {β : ℝ} (hβ : -1 < β) (n k : ℕ) (hk : k ≤ n) :
0 < MvPolynomial.dunklXuDiskRaiseA β n k ⋯ ∧
MvPolynomial.dunklXuDisk β n k =
MvPolynomial.dunklXuDiskRaiseA β n k ⋯ • MvPolynomial.dunklXuDisk (β + 1) n k +
MvPolynomial.dunklXuDiskRaiseB β n k ⋯ • MvPolynomial.dunklXuDisk (β + 1) (n - 2) k +
MvPolynomial.dunklXuDiskRaiseC β n k ⋯ • MvPolynomial.dunklXuDisk (β + 1) n (k - 2) +
MvPolynomial.dunklXuDiskRaiseD β n k ⋯ • MvPolynomial.dunklXuDisk (β + 1) (n - 2) (k - 2) ∧
(n < k + 2 → MvPolynomial.dunklXuDiskRaiseB β n k ⋯ = 0) ∧
(k < 2 → MvPolynomial.dunklXuDiskRaiseC β n k ⋯ = 0 ∧ MvPolynomial.dunklXuDiskRaiseD β n k ⋯ = 0)Lean proof
/-- Raising the disk parameter has four-term support. Coefficients at indices
which would have negative degree or invalid inner index vanish explicitly. -/
theorem dunklXuDisk_raise {β : ℝ} (hβ : -1 < β) (n k : ℕ) (hk : k ≤ n) :
0 < dunklXuDiskRaiseA β n k ∧ dunklXuDisk β n k =
dunklXuDiskRaiseA β n k • dunklXuDisk (β + 1) n k +
dunklXuDiskRaiseB β n k • dunklXuDisk (β + 1) (n - 2) k +
dunklXuDiskRaiseC β n k • dunklXuDisk (β + 1) n (k - 2) +
dunklXuDiskRaiseD β n k • dunklXuDisk (β + 1) (n - 2) (k - 2) ∧
(n < k + 2 → dunklXuDiskRaiseB β n k = 0) ∧
(k < 2 → dunklXuDiskRaiseC β n k = 0 ∧ dunklXuDiskRaiseD β n k = 0) := by
have ha : -1 < β + k + 1 / 2 := by
have := Nat.cast_nonneg (α := ℝ) k
linarith
let a := jacobiSymmetricRaiseA β k
let b := jacobiSymmetricRaiseB β k
let c := jacobiSymmetricRaiseA (β + k + 1 / 2) (n - k)
let d := jacobiSymmetricRaiseB (β + k + 1 / 2) (n - k)
have ha₀ := jacobiSymmetricRaiseA_pos hβ k
have hc₀ := jacobiSymmetricRaiseA_pos ha (n - k)
obtain ⟨hi, hb⟩ := jacobi_symmetric_raise_all hβ k
obtain ⟨ho, hd⟩ := jacobi_symmetric_raise_all ha (n - k)
change jacobi β β k = a • _ + b • _ at hi
change jacobi _ _ (n - k) = c • _ + d • _ at ho
change k < 2 → b = 0 at hb
change n - k < 2 → d = 0 at hd
have hp : β + k + 1 / 2 + 1 = β + 1 + k + 1 / 2 := by ring
rw [hp] at ho
have ho' := congrArg (fun p : ℝ[X] => p.eval₂ C (X 0 : MvPolynomial (Fin 2) ℝ)) ho
simp only [Polynomial.smul_eq_C_mul, Polynomial.eval₂_add, Polynomial.eval₂_mul,
Polynomial.eval₂_C] at ho'
have hi' := congrArg (diskLift k) hi
rw [diskLift_add, diskLift_smul, diskLift_smul] at hi'
by_cases hsmall : k < 2
· rw [hb hsmall, zero_smul, add_zero] at hi'
simp only [dunklXuDiskRaiseA, dunklXuDiskRaiseB, dunklXuDiskRaiseC,
dunklXuDiskRaiseD, dite_eq_left hsmall]
refine ⟨mul_pos ha₀ hc₀, ?_, ?_, by simp⟩
· simp only [zero_smul, add_zero, dunklXuDisk, smul_eq_C_mul]
rw [hi', ho']
simp only [smul_eq_C_mul, map_mul]
rw [show n - 2 - k = n - k - 2 by omega]
ring
· intro hn
change a * d = 0
rw [hd (by omega), mul_zero]
· have hk2 : 2 ≤ k := by omega
have hkcast : ((k - 2 : ℕ) : ℝ) = (k : ℝ) - 2 := by
rw [Nat.cast_sub hk2, Nat.cast_ofNat]
have hl : -1 < β + 1 + (k - 2 : ℕ) + 1 / 2 := by
have := Nat.cast_nonneg (α := ℝ) (k - 2)
linarith
let e := jacobiSymmetricLowerA (β + 1 + (k - 2 : ℕ) + 1 / 2) (n - k)
let f := jacobiSymmetricLowerB (β + 1 + (k - 2 : ℕ) + 1 / 2) (n - k)
have hlower := jacobi_symmetric_weight_lower hl (n - k)
change (1 - Polynomial.X ^ 2) * jacobi _ _ (n - k) = e • _ + f • _ at hlower
rw [show β + 1 + (k - 2 : ℕ) + 1 / 2 + 1 = β + k + 1 / 2 by
rw [hkcast]; ring] at hlower
have hlower' := congrArg
(fun p : ℝ[X] => p.eval₂ C (X 0 : MvPolynomial (Fin 2) ℝ)) hlower
simp only [Polynomial.smul_eq_C_mul, Polynomial.eval₂_add, Polynomial.eval₂_mul,
Polynomial.eval₂_C, Polynomial.eval₂_sub, Polynomial.eval₂_one,
Polynomial.eval₂_pow, Polynomial.eval₂_X] at hlower'
have hLift : diskLift k (jacobi (β + 1) (β + 1) (k - 2)) =
(1 - X 0 ^ 2) * diskLift (k - 2) (jacobi (β + 1) (β + 1) (k - 2)) := by
convert diskLift_add_two (k - 2) (jacobi (β + 1) (β + 1) (k - 2))
(natDegree_jacobi_le _ _ _) using 1
congr 1
omega
rw [hLift] at hi'
simp only [dunklXuDiskRaiseA, dunklXuDiskRaiseB, dunklXuDiskRaiseC,
dunklXuDiskRaiseD, dite_eq_right hsmall]
change 0 < a * c ∧ _ = (a * c) • _ + (a * d) • _ + (b * e) • _ + (b * f) • _ ∧ _
refine ⟨mul_pos ha₀ hc₀, ?_, ?_, ?_⟩
· simp only [dunklXuDisk, smul_eq_C_mul]
rw [hi']
simp only [smul_eq_C_mul]
rw [show n - 2 - k = n - k - 2 by omega,
show n - (k - 2) = n - k + 2 by omega,
show n - 2 - (k - 2) = n - k by omega]
calc
_ = (C a * ((jacobi (β + k + 1 / 2) (β + k + 1 / 2) (n - k)).eval₂ C (X 0)) *
diskLift k (jacobi (β + 1) (β + 1) k)) +
C b * (((1 - X 0 ^ 2) *
(jacobi (β + k + 1 / 2) (β + k + 1 / 2) (n - k)).eval₂ C (X 0)) *
diskLift (k - 2) (jacobi (β + 1) (β + 1) (k - 2))) := by ring
_ = _ := by rw [hlower', ho']; simp only [map_mul]; ring
· intro hn
change a * d = 0
rw [hd (by omega), mul_zero]
· intro h
exact False.elim (hsmall h)Reference details: Explicit disk raising coefficients and signs and related results
For \(\beta {\gt}-1\) and \(0\le k\le n\), let \(q=n-k\) and \(\gamma =\beta +k+1/2\). In the four-term connection, the coefficients at \((n,k),(n-2,k),(n,k-2),(n-2,k-2)\) are
The last two are defined to be zero when \(k{\lt}2\). The first is strictly positive; the second is zero for \(q{\lt}2\) and strictly negative for \(q\ge 2\). When \(k\ge 2\), the third is strictly positive and the fourth strictly negative.
Reference: [DX14, Section 2.3].
Lean Formalisation
theorem MvPolynomial.dunklXuDiskRaiseA_pos {β : ℝ} (hβ : -1 < β) (n k : ℕ) : 0 < MvPolynomial.dunklXuDiskRaiseA β n k ⋯Lean proof
/-- The diagonal coefficient is positive for the full disk parameter range. -/
theorem dunklXuDiskRaiseA_pos {β : ℝ} (hβ : -1 < β) (n k : ℕ) :
0 < dunklXuDiskRaiseA β n k :=
mul_pos (jacobiSymmetricRaiseA_pos hβ k)
(jacobiSymmetricRaiseA_pos (outerParameter_gt_neg_one hβ k) (n - k))Zernike polynomials separate radial factors from sine and cosine angular modes. The Laplacian preserves these angular sectors, which we use in the annular construction of the next chapter.
For \(s\in [0,\infty )\) and \(\theta \in \mathbb R\), set \(\Phi (s,\theta )=\sqrt{s}(\cos \theta ,\sin \theta )\).
Lean Formalisation
def MvPolynomial.zernikeCoordinates (v : NNReal × ℝ) : Fin 2 → ℝLean definition
/-- Polar coordinates on the full nonnegative squared-radius domain. -/
noncomputable def zernikeCoordinates (v : ℝ≥0 × ℝ) : Fin 2 → ℝ :=
![Real.sqrt (v.1 : ℝ)*Real.cos v.2, Real.sqrt (v.1 : ℝ)*Real.sin v.2]The map \(\Phi :[0,\infty )\times \mathbb R\to \mathbb R^2\) is continuous, including at \(s=0\).
Lean Formalisation
theorem MvPolynomial.continuous_zernikeCoordinates : Continuous MvPolynomial.zernikeCoordinatesLean proof
/-- The polar coordinate map is continuous at the disk center as well. -/
theorem continuous_zernikeCoordinates : Continuous zernikeCoordinates := by
unfold zernikeCoordinates
simp_rw [← Real.coe_sqrt]
fun_propFor real \(a,b\), let \(\eta _{b,a}\) be the affine Jacobi measure on \([0,1]\), regarded as a measure on \([0,\infty )\). Define \(\omega ^{\rm aux}_{a,b}=\Phi _*(\eta _{b,a}\otimes d\theta |_{(-\pi ,\pi )})\).
Lean Formalisation
def MvPolynomial.zernikeProductMeasure (a b : ℝ) : MeasureTheory.Measure (Fin 2 → ℝ)Lean definition
/-- The auxiliary squared-radius/angle pushforward, before removing the Jacobi mass factor. -/
noncomputable def zernikeProductMeasure (a b : ℝ) : Measure (Fin 2 → ℝ) :=
let μ := Measure.comap NNReal.toReal (unitJacobiMeasure b a)
let ν := ProductMeasureInput.ofSFinite μ (volume.restrict (Ioo (-Real.pi) Real.pi))
Measure.map zernikeCoordinates (μ.prod ν.inner)If \(a,b{\gt}-1\), every continuous real-valued function on \(\mathbb R^2\) is integrable for \(\omega ^{\rm aux}_{a,b}\). In particular, all polynomial moments are finite.
Lean Formalisation
theorem MvPolynomial.integrable_zernikeProductMeasure {a b : ℝ} (ha : -1 < a) (hb : -1 < b) {f : (Fin 2 → ℝ) → ℝ}
(hf : Continuous f) : MeasureTheory.Integrable f (MvPolynomial.zernikeProductMeasure a b)Lean proof
/-- Continuous disk functions pull back to integrable functions on the compact parameter support. -/
theorem integrable_zernikeProductMeasure {a b : ℝ} (ha : -1 < a) (hb : -1 < b)
{f : (Fin 2 → ℝ) → ℝ} (hf : Continuous f) :
Integrable f (zernikeProductMeasure a b) := by
let := isFiniteMeasure_unitJacobiMeasure hb ha
rw [zernikeProductMeasure, integrable_map_measure hf.aestronglyMeasurable
continuous_zernikeCoordinates.measurable.aemeasurable]
have hi := (hf.comp continuous_zernikeCoordinates).continuousOn.integrableOn_compact
(μ := (Measure.comap NNReal.toReal (unitJacobiMeasure b a)).prod
(volume.restrict (Ioo (-Real.pi) Real.pi)))
(isCompact_Icc.prod isCompact_Icc : IsCompact (Icc (0 : NNReal) 1 ×ˢ Icc (-Real.pi) Real.pi))
have hr : ∀ᵐ r ∂Measure.comap NNReal.toReal (unitJacobiMeasure b a), r ∈ Icc (0 : NNReal) 1 := by
have hh := ae_of_ae_map (μ := Measure.comap NNReal.toReal (unitJacobiMeasure b a))
(f := NNReal.toReal) (by fun_prop)
(show ∀ᵐ x ∂(Measure.comap NNReal.toReal (unitJacobiMeasure b a)).map NNReal.toReal,
x ∈ Icc (0 : ℝ) 1 by rw [map_comap_nonnegative_unitJacobiMeasure]; exact ae_mem_Icc_unitJacobiMeasure b a)
exact hh.mono (fun r hr ↦ ⟨bot_le, hr.2⟩)
have hs : ∀ᵐ v ∂(Measure.comap NNReal.toReal (unitJacobiMeasure b a)).prod
(volume.restrict (Ioo (-Real.pi) Real.pi)),
v ∈ Icc (0 : NNReal) 1 ×ˢ Icc (-Real.pi) Real.pi := by
filter_upwards [Measure.quasiMeasurePreserving_fst.ae hr,
Measure.quasiMeasurePreserving_snd.ae (ae_restrict_mem measurableSet_Ioo)] with v hv hθ
exact ⟨hv, hθ.1.le, hθ.2.le⟩
rwa [IntegrableOn, Measure.restrict_eq_self_of_ae_mem hs] at hiFor real \(a,b\), define \(\omega _{a,b}=2^{-(a+b+2)}\omega ^{\rm aux}_{a,b}\).
Lean Formalisation
def MvPolynomial.zernikeMeasure (a b : ℝ) : MeasureTheory.Measure (Fin 2 → ℝ)Lean definition
/-- The disk measure with radial weight (r²)^a (1-r²)^b, including the area Jacobian. -/
noncomputable def zernikeMeasure (a b : ℝ) : Measure (Fin 2 → ℝ) :=
ENNReal.ofReal (((2 : ℝ)^(a+b+2))⁻¹) • zernikeProductMeasure a bFormal details: Finite moments of the weighted disk measure and related results
For \(a,b{\gt}-1\), the measure \(\omega _{a,b}\) has all polynomial moments finite.
Lean Formalisation
theorem MvPolynomial.hasFiniteMoments_zernikeMeasure {a b : ℝ} (ha : -1 < a) (hb : -1 < b) :
MvPolynomial.HasFiniteMoments (MvPolynomial.zernikeMeasure a b)Lean proof
/-- Every polynomial has finite square integral for the standard disk measure. -/
@[aesop (rule_sets := [PolynomialIntegrability]) unsafe 80% apply]
theorem hasFiniteMoments_zernikeMeasure {a b : ℝ} (ha : -1 < a) (hb : -1 < b) :
HasFiniteMoments (zernikeMeasure a b) := by
intro p
exact (hasFiniteMoments_zernikeProductMeasure ha hb p).smul_measure ENNReal.ofReal_ne_topFor a Cartesian polynomial \(p\) and \(s\ge 0\), let \(A_p(s)\) be the function \(\theta \mapsto p(\Phi (s,\theta ))\) on \((-\pi ,\pi )\). Write \(J_p(s)=\int _{-\pi }^{\pi }A_p(s)(\theta )\, d\theta \).
Lean Formalisation
def MvPolynomial.zernikeAngularInput (p : MvPolynomial (Fin 2) ℝ) (r : NNReal) :
MeasureTheory.IntegrableInput (MeasureTheory.volume.restrict (Set.Ioo (-Real.pi) Real.pi))Lean definition
/-- An integrable angular slice at a nonnegative squared radius. -/
noncomputable def zernikeAngularInput (p : MvPolynomial (Fin 2) ℝ) (r : NNReal) :
IntegrableInput (volume.restrict (Ioo (-Real.pi) Real.pi)) :=
⟨fun θ => eval (zernikeCoordinates (r,θ)) p, by
have hc : Continuous (fun θ => eval (zernikeCoordinates (r,θ)) p) :=
p.continuous_eval.comp (continuous_zernikeCoordinates.comp (by fun_prop))
exact (hc.integrableOn_Icc (a := -Real.pi) (b := Real.pi)).mono_set Ioo_subset_Icc_self⟩For every Cartesian polynomial \(p\) and \(s\ge 0\), the function \(\theta \mapsto A_p(s)(\theta )=p(\Phi (s,\theta ))\) is Lebesgue-integrable on \((-\pi ,\pi )\).
Lean Formalisation
theorem MvPolynomial.zernikeAngularInput_integrable (p : MvPolynomial (Fin 2) ℝ) (r : NNReal) :
MeasureTheory.Integrable (↑(p.zernikeAngularInput r)) (MeasureTheory.volume.restrict (Set.Ioo (-Real.pi) Real.pi))Lean proof
/-- Every angular slice has its classical integral. -/
theorem zernikeAngularInput_integrable (p : MvPolynomial (Fin 2) ℝ) (r : NNReal) :
Integrable (zernikeAngularInput p r).val (volume.restrict (Ioo (-Real.pi) Real.pi)) :=
(zernikeAngularInput p r).integrableFor \(a,b{\gt}-1\) and a Cartesian polynomial \(p\), define the function \(S_{a,b,p}(s)=(1-s)^bs^aJ_p(s)\) on \(s\in (0,1)\).
Lean Formalisation
def MvPolynomial.zernikeSquaredRadiusInput (a b : ↑(Set.Ioi (-1))) (p : MvPolynomial (Fin 2) ℝ) :
MeasureTheory.IntegrableInput MeasureTheory.volumeLean definition
/-- The integrable squared-radius density, with all power bases strictly positive. -/
noncomputable def zernikeSquaredRadiusInput (a b : Ioi (-1 : ℝ))
(p : MvPolynomial (Fin 2) ℝ) : IntegrableInput (volume : Measure (Ioo (0 : ℝ) 1)) :=
⟨fun r : Ioo (0 : ℝ) 1 => (1-(r : ℝ))^(b : ℝ)*(r : ℝ)^(a : ℝ) *
∫ θ, (zernikeAngularInput p (NNReal.mk r r.property.1.le)).val θ
∂volume.restrict (Ioo (-Real.pi) Real.pi), integrable_zernikeSquaredRadius_formula a b p⟩The function \(S_{a,b,p}\) is integrable on \((0,1)\), including when its weight has endpoint singularities.
Lean Formalisation
theorem MvPolynomial.zernikeSquaredRadiusInput_integrable (a b : ↑(Set.Ioi (-1))) (p : MvPolynomial (Fin 2) ℝ) :
MeasureTheory.Integrable (↑(MvPolynomial.zernikeSquaredRadiusInput a b p)) MeasureTheory.volumeLean proof
/-- The weighted squared-radius input is integrable even for singular admissible weights. -/
theorem zernikeSquaredRadiusInput_integrable (a b : Ioi (-1 : ℝ))
(p : MvPolynomial (Fin 2) ℝ) : Integrable (zernikeSquaredRadiusInput a b p).val volume :=
(zernikeSquaredRadiusInput a b p).integrableFor \(a,b{\gt}-1\) and a Cartesian polynomial \(p\), define the function \(R_{a,b,p}(r)=r(r^2)^a(1-r^2)^bJ_p(r^2)\) on \(r\in (0,1)\).
Lean Formalisation
def MvPolynomial.zernikePolarInput (a b : ↑(Set.Ioi (-1))) (p : MvPolynomial (Fin 2) ℝ) :
MeasureTheory.IntegrableInput MeasureTheory.volumeLean definition
/-- The ordinary polar-radius density with its area Jacobian and integrability certificate. -/
noncomputable def zernikePolarInput (a b : Ioi (-1 : ℝ))
(p : MvPolynomial (Fin 2) ℝ) : IntegrableInput (volume : Measure (Ioo (0 : ℝ) 1)) :=
⟨fun r : Ioo (0 : ℝ) 1 => (r : ℝ)*((r : ℝ)^2)^(a : ℝ)*(1-(r : ℝ)^2)^(b : ℝ) *
∫ θ, (zernikeAngularInput p (NNReal.mk ((r : ℝ)^2) (sq_nonneg _))).val θ
∂volume.restrict (Ioo (-Real.pi) Real.pi), integrable_zernikePolar_formula a b p⟩The function \(R_{a,b,p}\) is integrable on \((0,1)\), including admissible endpoint singularities.
Lean Formalisation
theorem MvPolynomial.zernikePolarInput_integrable (a b : ↑(Set.Ioi (-1))) (p : MvPolynomial (Fin 2) ℝ) :
MeasureTheory.Integrable (↑(MvPolynomial.zernikePolarInput a b p)) MeasureTheory.volumeLean proof
/-- The polar-radius input is classically integrable throughout the admissible parameter range. -/
theorem zernikePolarInput_integrable (a b : Ioi (-1 : ℝ))
(p : MvPolynomial (Fin 2) ℝ) : Integrable (zernikePolarInput a b p).val volume :=
(zernikePolarInput a b p).integrableLet \(H^c_m\) and \(H^s_m\) be the real polynomials with \(H^c_m+iH^s_m=(x+iy)^m\). For real \(a,b\) and the shifted Jacobi polynomials \(\widetilde P_k^{(a,b)}(s)=P_k^{(a,b)}(2s-1)\), set
In total degree \(n\), the \(j\)th polynomial, \(0\le j\le n\), is the sine mode with frequency \(m=j+1\) when \(n+j\) is odd and the cosine mode with frequency \(m=j\) otherwise, with radial degree \(k=(n-m)/2\).
Reference: [DLMF, 18.37(i)].
Lean Formalisation
def MvPolynomial.diskHarmonics : ℕ → MvPolynomial (Fin 2) ℝ × MvPolynomial (Fin 2) ℝLean definition
/-- The cosine and sine solid harmonics, as a polynomial pair. -/
noncomputable def diskHarmonics : ℕ → MvPolynomial (Fin 2) ℝ × MvPolynomial (Fin 2) ℝ
| 0 => (1,0)
| m+1 => (X 0*(diskHarmonics m).1-X 1*(diskHarmonics m).2,
X 1*(diskHarmonics m).1+X 0*(diskHarmonics m).2)In polar coordinates,
and both have total degree at most \(2k+m\). For \(0\le j\le n\), the indices of the \(j\)th polynomial in degree \(n\) satisfy \(2k+m=n\), and a sine mode has \(m\ne 0\).
Reference: [DLMF, 18.37(i)].
Lean Formalisation
theorem MvPolynomial.eval_zernikeCos_polar (a b : ℝ) (k m : ℕ) (r θ : ℝ) :
(MvPolynomial.eval ![r * Real.cos θ, r * Real.sin θ]) (MvPolynomial.zernikeCos a b k m) =
Polynomial.eval (2 * r ^ 2 - 1) (Polynomial.jacobi b (a + ↑m) k) * r ^ m * Real.cos (↑m * θ)Lean proof
/-- The actual Cartesian polynomial has the conventional real Zernike polar expression. -/
theorem eval_zernikeCos_polar (a b : ℝ) (k m : ℕ) (r θ : ℝ) :
eval (![r*Real.cos θ,r*Real.sin θ] : Fin 2 → ℝ) (zernikeCos a b k m) =
(Polynomial.jacobi b (a+m) k).eval (2*r^2-1)*r^m*Real.cos (m*θ) := by
rw [zernikeCos, map_mul, eval_zernikeRadialPolynomial_polar,
(eval_diskHarmonics_polar m r θ).1, Polynomial.eval_shiftedJacobi, mul_assoc]Within each degree the modes are thus ordered \(1,\sin (2\theta ),\cos (2\theta ),\ldots \) for even degree and \(\sin \theta ,\cos \theta ,\sin (3\theta ),\cos (3\theta ),\ldots \) for odd degree, the real ordering in MultivariateOrthogonalPolynomials.jl [MOP]. For \(a=0\), [DLMF, 18.37.1] combines these real modes into a complex mode and divides by \(P_k^{(b,m)}(1)\); these raw real polynomials do not include that endpoint-normalizing factor. Positive \(L^2\) normalization is a separate operation.
Reference details: Classical Zernike polynomial norm and related results
For every parameter and index choice for which \((Z_{n,j}^{a,b})^2\) is integrable with respect to \(\omega _{a,b}\), define
The domain consists of all such square-integrable polynomials; no additional parameter restrictions are imposed.
Lean Formalisation
def MvPolynomial.zernikeNorm (a b : ℝ)
(i :
{ i //
MeasureTheory.Integrable (fun v => (MvPolynomial.eval v) (MvPolynomial.zernike a b i.1 i.2) ^ 2)
(MvPolynomial.zernikeMeasure a b) }) :
ℝLean definition
/-- Positive standard norm in total-degree order. -/
noncomputable def zernikeNorm (a b : ℝ)
(i : {i : ℕ × ℕ // Integrable (fun v ↦ eval v (zernike a b i.1 i.2)^2)
(zernikeMeasure a b)}) : ℝ :=
Real.sqrt (∫ v, eval v (zernike a b i.val.1 i.val.2)^2 ∂zernikeMeasure a b)Whenever \((Z_{n,j}^{a,b})^2\) is \(\omega _{a,b}\)-integrable,
Lean Formalisation
theorem MvPolynomial.zernikeNorm_nonneg (a b : ℝ)
(i :
{ i //
MeasureTheory.Integrable (fun v => (MvPolynomial.eval v) (MvPolynomial.zernike a b i.1 i.2) ^ 2)
(MvPolynomial.zernikeMeasure a b) }) :
0 ≤ MvPolynomial.zernikeNorm a b iLean proof
/-- The classical polynomial norm is nonnegative. -/
theorem zernikeNorm_nonneg (a b : ℝ)
(i : {i : ℕ × ℕ // Integrable (fun v ↦ eval v (zernike a b i.1 i.2)^2)
(zernikeMeasure a b)}) : 0 ≤ zernikeNorm a b i :=
Real.sqrt_nonneg _For \(a,b{\gt}-1\), the retained real Zernike modes are mutually orthogonal for the standard radial disk measure and form complete bases of every finite total-degree polynomial space. Writing \(h_k^{(b,a+m)}\) for the standard Jacobi squared norm, their squared norms are
Dividing by the positive square roots gives identity Gram matrices. If \(H_m\) is either solid angular harmonic, the Cartesian polynomial Laplacian satisfies
In particular the Laplacian preserves each angular sector, including at the origin.
Reference: [DLMF, 18.37(i)].
Lean Formalisation
theorem MvPolynomial.integralInner_zernikeMode_eq_zero {a b : ℝ} (ha : -1 < a) (hb : -1 < b) {s t : Bool} {k m l n : ℕ}
(hne : (s, k, m) ≠ (t, l, n)) :
MvPolynomial.integralInner (MvPolynomial.zernikeMeasure a b)
(MvPolynomial.IntegrablePair.of (MvPolynomial.zernikeMeasure a b) (MvPolynomial.zernikeMode s a b k m)
(MvPolynomial.zernikeMode t a b l n) ⋯) =
0Lean proof
/-- Orthogonality of all distinct retained real modes in the standard disk measure. -/
theorem integralInner_zernikeMode_eq_zero {a b : ℝ} (ha : -1 < a) (hb : -1 < b)
{s t : Bool} {k m l n : ℕ} (hne : (s,k,m) ≠ (t,l,n)) :
integralInner (zernikeMeasure a b) (IntegrablePair.of (zernikeMeasure a b) (zernikeMode s a b k m) (zernikeMode t a b l n)) = 0 := by
rw [integralInner_zernikeMeasure a b _ _
(hi := (hasFiniteMoments_zernikeMeasure ha hb).integrable_mul _ _)
(hj := (hasFiniteMoments_zernikeProductMeasure ha hb).integrable_mul _ _)]
by_cases hs : s=t
· subst t
by_cases hm : m=n
· subst n
rw [integralInner_zernikeMode_eq_zero_of_radial ha hb s (by aesop) m, mul_zero]
· rw [integralInner_zernikeMode_eq_zero_of_angular ha hb (Or.inr hm), mul_zero]
· rw [integralInner_zernikeMode_eq_zero_of_angular ha hb (Or.inl hs), mul_zero]Reference details: Classical real-mode Zernike normalization and related results
For an individual real Zernike mode \(Z\), with \(Z^2\) integrable against \(\omega _{a,b}\), define its norm by \(\sqrt{\int Z^2\, d\omega _{a,b}}\). The normalized polynomial \(Z/\| Z\| \) additionally requires a strictly positive squared integral.
Lean Formalisation
inductive MvPolynomial.ZernikeModeNormInput (s : Bool) (a b : ℝ) (k m : ℕ) : PropLean definition
/-- Classical finite-square input for a real Zernike mode (DLMF 18.37). -/
structure ZernikeModeNormInput (s : Bool) (a b : ℝ) (k m : ℕ) : Prop where
integrable : Integrable (fun v => (eval v (zernikeMode s a b k m))^2) (zernikeMeasure a b)The square of the norm equals the convergent squared integral. For \(a,b{\gt}-1\), every mode has a finite norm and every retained mode has positive norm; its normalized polynomial has squared integral one.
Lean Formalisation
theorem MvPolynomial.ZernikeModeNormInput.of_parameters {a b : ℝ} (ha : -1 < a) (hb : -1 < b) (s : Bool) (k m : ℕ) :
MvPolynomial.ZernikeModeNormInput s a b k mLean proof
/-- The full integrable parameter range supplies every finite mode norm. -/
theorem ZernikeModeNormInput.of_parameters {a b : ℝ} (ha : -1 < a) (hb : -1 < b)
(s : Bool) (k m : ℕ) : ZernikeModeNormInput s a b k m :=
⟨hasFiniteMoments_zernikeMeasure ha hb _⟩Supporting results: parity lifts, symmetric Jacobi conversions, radial measure
The lift is linear in \(p\) and has total degree at most \(n\). If \(\deg p\le n\) and \(p\) has parity \(n\), then \(L_np(x,sz)=s^np(z)\) whenever \(s^2=1-x^2\). This is a polynomial identity and does not require \(s\ne 0\). Also \(L_{n+2}p=(1-x^2)L_np\) when \(\deg p\le n\).
Lean Formalisation
theorem MvPolynomial.eval_diskLift_scaled.{u_1} {R : Type u_1} [CommRing R] (n : ℕ) (p : Polynomial R) (hp : p.natDegree ≤ n)
(hpar : ∀ (j : ℕ), j % 2 ≠ n % 2 → p.coeff j = 0) (v : Fin 2 → R) (s z : R) (hs : 1 - v 0 ^ 2 = s ^ 2)
(hy : v 1 = s * z) : (MvPolynomial.eval v) (MvPolynomial.diskLift n p) = s ^ n * Polynomial.eval z pLean proof
/-- Evaluating the lift after a squared-radius substitution is exactly the
scaled univariate polynomial, with no invertibility assumption on the radius. -/
theorem eval_diskLift_scaled (n : ℕ) (p : Polynomial R)
(hp : p.natDegree ≤ n) (hpar : ∀ j, j % 2 ≠ n % 2 → p.coeff j = 0)
(v : Fin 2 → R) (s z : R) (hs : 1 - v 0 ^ 2 = s ^ 2) (hy : v 1 = s * z) :
eval v (diskLift n p) = s ^ n * p.eval z := by
rw [diskLift, 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, map_sub, map_one, eval_C, eval_X, hs, hy]
by_cases hjpar : j % 2 = n % 2
· have hjn : j ≤ n := by simpa only [Finset.mem_range, Nat.lt_succ_iff] using hj
have he : j + 2 * ((n - j) / 2) = n := by omega
rw [mul_pow, ← pow_mul]
calc
p.coeff j * (s ^ j * z ^ j) * s ^ (2 * ((n - j) / 2)) =
(s ^ j * s ^ (2 * ((n - j) / 2))) * (p.coeff j * z ^ j) := by ring
_ = s ^ n * (p.coeff j * z ^ j) := by rw [← pow_add, he]
· simp [hpar j hjpar]Let \(A_j,B_j,E_j,F_j\) be the coefficients on the degree-dependent domains of Definitions 5.3.57, 5.3.59, 5.3.61, and 5.3.63. Every \(\beta {\gt}-1\) belongs to these domains. For real \(\beta {\gt}-1\) and \(n\ge 0\), there exist real coefficients giving
The range includes \(\beta =-1/2\). The raising coefficients are \(A_{n+2},B_{n+2}\) and the weighted-lowering coefficients are \(E_n,F_n\), respectively.
Reference: [DLMF, 18.9(ii)].
Lean Formalisation
theorem Polynomial.exists_jacobi_symmetric_raise {β : ℝ} (hβ : -1 < β) (n : ℕ) :
∃ a b,
Polynomial.jacobi β β (n + 2) =
a • Polynomial.jacobi (β + 1) (β + 1) (n + 2) + b • Polynomial.jacobi (β + 1) (β + 1) nLean proof
/-- Existential wrapper for the explicit symmetric raising coefficients. -/
theorem exists_jacobi_symmetric_raise {β : ℝ} (hβ : -1 < β) (n : ℕ) :
∃ a b : ℝ, jacobi β β (n + 2) =
a • jacobi (β + 1) (β + 1) (n + 2) + b • jacobi (β + 1) (β + 1) n :=
⟨_, _, jacobi_symmetric_raise hβ n⟩The signs of these coefficients are stated in Theorem 5.3.102.
Write \(A_m,B_m\) for the coefficients at degrees \(m,m-2\) in symmetric raising, and \(E_n,F_n\) for the coefficients at degrees \(n+2,n\) in weighted lowering. For \(\beta {\gt}-1\), put \(d_j=2n+2\beta +j\). The explicit formulas are
The initial values are \(A_0=1\), \(A_1=(\beta +1)/(\beta +2)\) and \(B_0=B_1=0\). In particular, no removable singularity is introduced at \(\beta =-1/2\).
Reference: [DLMF, 18.9(ii)].
Lean Formalisation
theorem Polynomial.jacobiSymmetricRaiseA_pos {β : ℝ} (hβ : -1 < β) (n : ℕ) : 0 < Polynomial.jacobiSymmetricRaiseA β n ⋯Lean proof
/-- The unchanged-degree raising coefficient is strictly positive. -/
theorem jacobiSymmetricRaiseA_pos {β : ℝ} (hβ : -1 < β) (n : ℕ) :
0 < jacobiSymmetricRaiseA β n := by
rcases n with _ | _ | n
· norm_num [jacobiSymmetricRaiseA]
· exact div_pos (by linarith) (by linarith)
· have hn := Nat.cast_nonneg (α := ℝ) n
have h₀ : 0 < 2 * (n : ℝ) + 2 * β + 5 := by linarith
have h₁ : 0 < 2 * (n : ℝ) + 2 * β + 6 := by linarith
have h₂ : 0 < 2 * (n : ℝ) + 2 * β + 4 := by linarith
have h₃ : 0 < (n : ℝ) + 2 * β + 3 := by linarith
have h₄ : 0 < (n : ℝ) + 2 * β + 4 := by linarith
dsimp [jacobiSymmetricRaiseA]
positivityFor \(\alpha ,\beta \in \mathbb {R}\), \(k\in \mathbb {N}\) and \(x\in (-1,1)\),
For \(f\in \mathcal I(\mu _{\alpha +k,\beta +k})\), the function \((1-x^2)^kf(x)\) is \(\mu _{\alpha ,\beta }\)-integrable and
Lean Formalisation
theorem Polynomial.jacobiWeight_add_nat (α β : ℝ) (k : ℕ) (x : ↑(Set.Ioo (-1) 1)) :
↑((Polynomial.jacobiWeight (α + ↑k) (β + ↑k)) x) = (1 - ↑x ^ 2) ^ k * ↑((Polynomial.jacobiWeight α β) x)Lean proof
/-- Integer parameter shifts on the classical weight domain. -/
theorem jacobiWeight_add_nat (α β : ℝ) (k : ℕ) (x : Ioo (-1 : ℝ) 1) :
(jacobiWeight (α + k) (β + k) x : ℝ) =
(1 - (x : ℝ) ^ 2) ^ k * (jacobiWeight α β x : ℝ) := by
induction k with
| zero => simp
| succ k ih =>
have ha : α + ((k + 1 : ℕ) : ℝ) = (α + k) + 1 := by push_cast; ring
have hb : β + ((k + 1 : ℕ) : ℝ) = (β + k) + 1 := by push_cast; ring
rw [ha, hb, jacobiWeight_add_one, ih, pow_succ]
ringFor \(a,b{\gt}-1\), polynomial integration against the constructed disk measure is
All polynomial moments are finite. In squared-radius coordinates, the area factor is \(1/2\); relative to the affine Jacobi product measure, the mass factor is \(2^{-(a+b+2)}\).
Lean Formalisation
theorem MvPolynomial.integral_zernikeMeasure_squaredRadius {a b : ℝ} (ha : -1 < a) (hb : -1 < b) (p : MvPolynomial (Fin 2) ℝ) :
∫ (v : Fin 2 → ℝ), (MvPolynomial.eval v) p ∂MvPolynomial.zernikeMeasure a b =
1 / 2 * ∫ (r : ↑(Set.Ioo 0 1)), ↑(MvPolynomial.zernikeSquaredRadiusInput ⟨a, ha⟩ ⟨b, hb⟩ p) rLean proof
/-- Squared-radius integration with its area factor, entirely within the classical domain. -/
theorem integral_zernikeMeasure_squaredRadius {a b : ℝ} (ha : -1 < a) (hb : -1 < b)
(p : MvPolynomial (Fin 2) ℝ) :
∫ v, eval v p ∂zernikeMeasure a b =
(1/2 : ℝ) * ∫ r : Ioo (0 : ℝ) 1,
(zernikeSquaredRadiusInput ⟨a,ha⟩ ⟨b,hb⟩ p).val r := by
let := isFiniteMeasure_unitJacobiMeasure hb ha
have hp := integrable_zernikeProductMeasure ha hb p.continuous_eval
change Integrable (fun v ↦ eval v p) (Measure.map zernikeCoordinates
((Measure.comap NNReal.toReal (unitJacobiMeasure b a)).prod
(volume.restrict (Ioo (-Real.pi) Real.pi)))) at hp
have hi := (integrable_map_measure p.continuous_eval.aestronglyMeasurable
continuous_zernikeCoordinates.measurable.aemeasurable).mp hp
have he := (radial_data a b ⟨_,integrable_zernikeRadialIntegral ⟨a,ha⟩ ⟨b,hb⟩ p⟩ (measurable_zernikeRadialIntegral p)).2
rw [zernikeMeasure, integral_smul_measure, ENNReal.toReal_ofReal (by positivity), smul_eq_mul,
zernikeProductMeasure, integral_map continuous_zernikeCoordinates.measurable.aemeasurable
p.continuous_eval.aestronglyMeasurable]
change ((2 : ℝ)^(a+b+2))⁻¹ *
(∫ v : NNReal × ℝ, eval (zernikeCoordinates v) p
∂(Measure.comap NNReal.toReal (unitJacobiMeasure b a)).prod
(volume.restrict (Ioo (-Real.pi) Real.pi))) = _
change Integrable (fun v : NNReal × ℝ ↦ eval (zernikeCoordinates v) p)
((Measure.comap NNReal.toReal (unitJacobiMeasure b a)).prod
(volume.restrict (Ioo (-Real.pi) Real.pi))) at hi
rw [integral_prod _ hi]
change ((2 : ℝ)^(a+b+2))⁻¹ *
(∫ r : NNReal, ∫ θ, (zernikeAngularInput p r).val θ
∂volume.restrict (Ioo (-Real.pi) Real.pi)
∂Measure.comap NNReal.toReal (unitJacobiMeasure b a)) = _
rw [he, ← integral_const_mul, ← integral_const_mul]
apply integral_congr_ae
filter_upwards [] with r
rw [unitJacobiWeight_apply]
change ((2 : ℝ)^(a+b+2))⁻¹ * ((2 : ℝ)^(b+a+1) * _ * _) = (1/2 : ℝ) * (_ * _)
rw [show a+b+2 = (b+a+1)+1 by ring,
Real.rpow_add (by norm_num : (0 : ℝ) < 2), Real.rpow_one]
field_simp
rflThe disk provides the angular description. Removing an inner disk changes the radial measure and brings in the semiclassical Jacobi family of Chapter 5.2.