theorem
FiniteJet.GraphKoszul.pow_smul_graphIdeal_inter_unitBall_subset
Mathematical summary.
There is an integer h_E ≥ 0 such that ϖ^{h_E}(I_E ∩ T_{E,0}) ⊆ d_{1,E}(T_{E,0}^m).
Lean interprets the two lattices as the Gauss-norm and sup-norm unit balls. Choose C such that every y∈I_E has a preimage x with ‖x‖≤C‖y‖, and then choose h_E with |ϖ|^{h_E}C≤1.
Original Lean docstring
Equation (9), lattice-inclusion form ([FJP] Lemma 5.1): literallyϖ^h (J_E ∩ P_{E,0}) ⊆ d_{1,E}(P_{E,0}^m). Here P_{E,0} = {x | ‖x‖ ≤ 1} is the unit
ball of P_E (via mem_unitBall_iff), P_{E,0}^m = {u | ‖u‖ ≤ 1} is the sup-norm unit
ball of P_E^m, J_E = Ideal.span (Set.range r), and ϖ = tP = polyToP (C t).
Used in the paper for: Lemma 5.1 (unit-ball specialization: ideal denominators)
theorem pow_smul_graphIdeal_inter_unitBall_subset [IsNoetherianRing (P E m)]
(t : E) (htu : IsUnit t) (ht1 : ‖t‖ < 1) (ht0 : 0 < ‖t‖)
(hscale : ∀ x : E, ‖t * x‖ = ‖t‖ * ‖x‖)
(hE₀P : IsNoetherianRing (unitBall (P E m)))
(r : Fin m → P E m) :
∃ h : ℕ, (fun x => polyToP (MvPolynomial.C t) ^ h * x) ''
((Ideal.span (Set.range r) : Set (P E m)) ∩ {x | ‖x‖ ≤ 1}) ⊆
(fun u => d1 r u) '' {u : Fin m → P E m | ‖u‖ ≤ 1}