Convergence of the formal exponential

The formal exponential Exp of a formal group law (the compositional inverse of the logarithm Λ, ChabautyColeman.FormalGroupLaw.exp) converges on (pO)ⁿ when p is odd.

The classical estimate is v_p(coeff_d Exp) ≥ -(deg d - 1)/(p-1) (ChabautyColeman.FormalGroupLaw.exp_bounded), proved by strong induction on deg d through the recursion Exp = X - (Λ - X) ∘ Exp. The bookkeeping is organised around:

• Dexp p n = (n-1)/(p-1), the denominator-exponent bound, with the elementary inequality (p-1) · v_p(M) ≤ M - 1 and the partition inequality Dexp M + ∑ Dexp kᵢ ≤ Dexp (∑ kᵢ);
• ChabautyColeman.IntLevel f p x k, meaning f(p)^k · x is integral (in the image of f), which is additive, multiplicative (adding the levels) and monotone in k.

In the induction step the product ∏ᵢ Expᵢ^{mᵢ} gains a slack Dexp (deg m) (partition inequality) that exactly cancels the logarithm's 1/deg m denominator; (p-1) v_p(m) ≤ m-1 closes the estimate. Scaling by p^{deg d} and using deg d - Dexp(deg d) → ∞ (which needs p ≥ 3) gives the integral, coefficient-decaying descent ChabautyColeman.FormalGroupLaw.exp_converges.

Blueprint node: lem:exp-converge.

theorem MvPowerSeries.invSubst_eq_sub {σ : Type u_1} {R : Type u_2} [CommRing R] [Finite σ] {a : σ → MvPowerSeries σ R} (ha : ∀ (i : σ) (e : σ →₀ ℕ), Finsupp.degree e ≤ 1 → (coeff e) (a i - X i) = 0) (i : σ) : invSubst a i = X i - subst (invSubst a) (a i - X i)

The compositional inverse satisfies the defining recursion E = X - (a - X) ∘ E.

The denominator-exponent bound Dexp

def ChabautyColeman.Dexp (p n : ℕ) : ℕ

Dexp p n = (n-1)/(p-1) (natural-number division, i.e. ⌊(n-1)/(p-1)⌋): an integer upper bound for v_p(n!) that bounds the p-power denominators of the formal exponential.

Equations

• ChabautyColeman.Dexp p n = (n - 1) / (p - 1)

theorem ChabautyColeman.Dexp_eq (p n : ℕ) : Dexp p n = (n - 1) / (p - 1)

theorem ChabautyColeman.pred_mul_padicValNat_le {p : ℕ} (hp : Nat.Prime p) {M : ℕ} (hM : 1 ≤ M) : (p - 1) * padicValNat p M ≤ M - 1

The key elementary inequality behind the exponential estimate: (p-1) · v_p(M) ≤ M - 1.

theorem ChabautyColeman.pred_mul_Dexp_le {p : ℕ} (n : ℕ) : (p - 1) * Dexp p n ≤ n - 1

theorem ChabautyColeman.Dexp_mono {p n m : ℕ} (h : n ≤ m) : Dexp p n ≤ Dexp p m

theorem ChabautyColeman.Dexp_le {p n : ℕ} : Dexp p n ≤ n

theorem ChabautyColeman.padicValNat_le_Dexp {p : ℕ} (hp : Nat.Prime p) {M : ℕ} (hM : 1 ≤ M) : padicValNat p M ≤ Dexp p M

theorem ChabautyColeman.Dexp_card_add_sum_le {p : ℕ} (hp : 2 ≤ p) {ι : Type u_1} (s : Finset ι) (k : ι → ℕ) (hk : ∀ i ∈ s, 1 ≤ k i) : Dexp p s.card + ∑ i ∈ s, Dexp p (k i) ≤ Dexp p (∑ i ∈ s, k i)

The partition inequality: parts k i ≥ 1 summing to N over s.card parts satisfy Dexp s.card + ∑ Dexp (k i) ≤ Dexp N. This absorbs the logarithm's 1/deg denominator into the product slack.

theorem ChabautyColeman.tendsto_sub_Dexp_atTop {p : ℕ} (hp : 3 ≤ p) : Filter.Tendsto (fun (n : ℕ) => n - Dexp p n) Filter.atTop Filter.atTop

For p ≥ 3, the gap n - Dexp p n → ∞ (this is where p odd enters).

p-integrality levels

def ChabautyColeman.IntLevel {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] (f : O →+* K) (p : ℕ) (x : K) (k : ℕ) : Prop

x : K is p-integral of level k (via f : O →+* K) if f(p)^k · x lies in the image of f. It is monotone in k, additive, and multiplicative (adding levels).

Equations

• ChabautyColeman.IntLevel f p x k = ∃ (c : O), f ↑p ^ k * x = f c

theorem ChabautyColeman.IntLevel.zero {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} (k : ℕ) : IntLevel f p 0 k

theorem ChabautyColeman.IntLevel.of_f {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} (c : O) : IntLevel f p (f c) 0

theorem ChabautyColeman.IntLevel.add {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} {x y : K} {k : ℕ} (hx : IntLevel f p x k) (hy : IntLevel f p y k) : IntLevel f p (x + y) k

theorem ChabautyColeman.IntLevel.neg {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} {x : K} {k : ℕ} (hx : IntLevel f p x k) : IntLevel f p (-x) k

theorem ChabautyColeman.IntLevel.mul {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} {x y : K} {j k : ℕ} (hx : IntLevel f p x j) (hy : IntLevel f p y k) : IntLevel f p (x * y) (j + k)

theorem ChabautyColeman.IntLevel.mono {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} {x : K} {j k : ℕ} (hx : IntLevel f p x j) (hjk : j ≤ k) : IntLevel f p x k

theorem ChabautyColeman.IntLevel.sum {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} {ι : Type u_3} {s : Finset ι} {g : ι → K} {k : ℕ} (h : ∀ i ∈ s, IntLevel f p (g i) k) : IntLevel f p (∑ i ∈ s, g i) k

theorem ChabautyColeman.IntLevel.prod {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} {ι : Type u_3} {s : Finset ι} {g : ι → K} {k : ι → ℕ} (h : ∀ i ∈ s, IntLevel f p (g i) (k i)) : IntLevel f p (∏ i ∈ s, g i) (∑ i ∈ s, k i)

theorem ChabautyColeman.IntLevel.finsum {O : Type u_1} {K : Type u_2} [CommRing O] [CommRing K] {f : O →+* K} {p : ℕ} {ι : Type u_3} {g : ι → K} {k : ℕ} (hfin : Function.HasFiniteSupport g) (h : ∀ (i : ι), IntLevel f p (g i) k) : IntLevel f p (∑ᶠ (i : ι), g i) k

theorem ChabautyColeman.FormalGroupLaw.log_coeff_level {O : Type u_1} {K : Type u_2} [CommRing O] [Field K] {ι : Type u_3} {f : O →+* K} {p : ℕ} [IsLocalRing O] [Fintype ι] [DecidableEq ι] (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal O) (hfp : f ↑p ≠ 0) (Φ : FormalGroupLaw O ι) (i : ι) (m : ι →₀ ℕ) (hm : 1 ≤ Finsupp.degree m) : IntLevel f p ((MvPowerSeries.coeff m) ((map f Φ).log i)) (Dexp p (Finsupp.degree m))

The coefficients of the logarithm are Dexp-bounded: f(p)^{Dexp(deg m)} · coeff_m Λ is integral. This relaxes coeff_log_map_padic (denominator p^{v_p(deg m)}) via v_p(deg m) ≤ Dexp(deg m).

theorem ChabautyColeman.FormalGroupLaw.exp_bounded {O : Type u_1} {K : Type u_2} [CommRing O] [Field K] {ι : Type u_3} {f : O →+* K} {p : ℕ} [IsLocalRing O] [Fintype ι] [DecidableEq ι] (hp : Nat.Prime p) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal O) (hfp : f ↑p ≠ 0) (Φ : FormalGroupLaw O ι) (i : ι) (d : ι →₀ ℕ) : IntLevel f p ((MvPowerSeries.coeff d) ((map f Φ).exp i)) (Dexp p (Finsupp.degree d))

The exponential coefficient bound: f(p)^{Dexp(deg d)} · coeff_d Exp is integral, i.e. v_p(coeff_d Exp) ≥ -(deg d - 1)/(p-1). Proved by strong induction on deg d through the recursion Exp = X - (Λ - X) ∘ Exp; the product slack Dexp(deg m) cancels the logarithm's 1/deg m, and (p-1)·v_p(m) ≤ m - 1 closes the step.

theorem ChabautyColeman.FormalGroupLaw.exp_converges {O : Type u_1} {K : Type u_2} [CommRing O] [Field K] {ι : Type u_3} {f : O →+* K} {p : ℕ} [IsLocalRing O] [Fintype ι] [DecidableEq ι] [UniformSpace O] [Fact (IsAdic (IsLocalRing.maximalIdeal O))] (hp : Nat.Prime p) (hp2 : p ≠ 2) (hpmem : ↑p ∈ IsLocalRing.maximalIdeal O) (hfp : f ↑p ≠ 0) (Φ : FormalGroupLaw O ι) (i : ι) : ∃ (H : MvPowerSeries ι O), (∀ (d : ι →₀ ℕ), f ((MvPowerSeries.coeff d) H) = f ↑p ^ Finsupp.degree d * (MvPowerSeries.coeff d) ((map f Φ).exp i)) ∧ Filter.Tendsto (fun (d : ι →₀ ℕ) => (MvPowerSeries.coeff d) H) Filter.cofinite (nhds 0)

Convergence of the exponential on (pO)ⁿ (p odd). After scaling the variables by p, the exponential of the base change f_*Φ descends to H ∈ O⟦U⟧ whose base change is the p-scaled exponential (f (coeff_d H) = f(p)^{deg d} · coeff_d Exp) and whose coefficients tend to 0. Here p ≥ 3 is essential: deg d - Dexp(deg d) → ∞ needs p - 1 ≥ 2.