theoremroutineinferred_depstructure_uncertainunresolved_ref

Interpolation with separated weights

Separated weights make the jet map at KK points surjective for large HH
lets the main argument prescribe jets at several approximations
Theorem·geom:interpolation·§2 Interpolation with separated weights

Statement (paper)

Fix integers m,K≥1m,K\ge1 and positive rational numbers w0,v0,θw_0,v_0,\theta such that 0<θ<10<\theta<1 and Kθm<1,Kw0v0θm<1. K\theta^m<1, \qquad K\frac{w_0}{v_0}\theta^m<1. There are successive lower thresholds for positive rational numbers w1,…,wmw_1,\ldots,w_m, depending only on these fixed data and the previously chosen weights, with the following property. Put W=(w0,w1,…,wm),V=(v0,w1/θ,…,wm/θ). W=(w_0,w_1,\ldots,w_m),\qquad V=(v_0,w_1/\theta,\ldots,w_m/\theta). For any points aj=(1,cj1,…,cjm)∈Cm+1,0≤j<K, a_j=(1,c_{j1},\ldots,c_{jm})\in\CC^{m+1},\qquad 0\le j<K, whose coordinates c0i,…,cK−1,ic_{0i},\ldots,c_{K-1,i} are pairwise distinct for each ii, the map PW(H)⟶⨁j=0K−1JV(H),P⟼(P(1+t,(cji+ui+log⁡(1+t))i=1m))j=0K−1. \begin{aligned} \mathcal P_W(H)&\longrightarrow\bigoplus_{j=0}^{K-1}\mathcal J_V(H),\\ P&\longmapsto \left(P\bigl(1+t,(c_{ji}+u_i+\log(1+t))_{i=1}^m\bigr)\right)_{j=0}^{K-1}. \end{aligned} is surjective for all sufficiently large, sufficiently divisible integers HH. The divisibility requirement can be chosen using only the weights. The remaining lower threshold for HH may depend on the points.

In plain English

Fix m,Km,K and rationals w0,v0,θ∈(0,1)w_0,v_0,\theta\in(0,1) with Kθm<1K\theta^m<1 and K(w0/v0)θm<1K(w_0/v_0)\theta^m<1. Then weights w1,…,wmw_1,\ldots,w_m can be chosen successively, depending only on the fixed data and earlier weights, so that for any KK points with pairwise distinct coordinates in each position, the map sending a polynomial in PW(H)\mathcal P_W(H) to its jets in JV(H)\mathcal J_V(H) at the KK points along the curve (1+t,cji+ui+log⁡(1+t))(1+t, c_{ji}+u_i+\log(1+t)) is surjective for all large, sufficiently divisible HH.

Why it's here

This is the geometric interpolation result that lets the main argument prescribe jet data at several approximation points. It is proved by blowing up along the weighted-jet ideal and showing a suitable divisor is ample. Nefness comes from the curve inequality, which the separated weights make independent of the points and centers, and the resulting vanishing of H1H^1 gives surjectivity onto jets. Only the final threshold on HH depends on the points, so the weight thresholds can be fixed in advance.
Classified routine:
The surjectivity follows from the earlier curve inequality: separated weights give the needed positivity on the blow-up, and standard ampleness and cohomology-vanishing arguments then yield surjectivity onto jets.

Uses

propCurve inequality for weighted degree

Used by

thmIrrationality exponent of pi is 2claimApproximants chosen with center-independent weight thresholdsclaimSimplex counts calibrate expanded determinant

Inside the proof

claimSeparated weights avoid center dependenceclaimProjective degree equals weighted curve degreeclaimIdeal order along a branch equals weighted contactclaimCurve inequality makes blowup class nefclaimNef margin makes target divisor ampleclaimVanishing and projective sections generate jets

Sources

PaperOpen
Section
§2 Interpolation with separated weights
Page
—
Label
geom:interpolation
Line
sections/interpolation.tex:24
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The interpolation theorem’s blowup argument invokes the curve inequality to prove its nef bound (sections/interpolation.tex:499–517). An internal claim has this edge, but the theorem node does not.
  • info
    structure_uncertain
    Its proof has no proof environment: center-independent weights are constructed at interpolation.tex:180–214, and §2.3 completes the argument at lines 429–584.
  • warn
    unresolved_ref
    The passage from curve positivity to jets invokes external blowup, ampleness, eventual Rees pushdown, and vanishing results.