Padics
Results named in Tau Ceti's TauCeti.NumberTheory.Padics modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremLabute's classification of the closed subgroups of ℤ_2ˣ#
Every nontrivial closed
subgroup of ℤ_2ˣ is a principal unit group U^(f) with f ≥ 2, a subgroup
V^(f) = {±1} × U^(f) with f ≥ 2, the subgroup {±1}, or a twisted subgroup U^[f] with
f ≥ 2, generated by -1 + 2 ^ f. The four families are pairwise distinct and faithfully indexed
by f: unitsPrincipal_inj, unitsPlusMinus_inj, topologicalClosure_zpowers_two_eq_iff and
the ne lemmas above.
TauCeti.closedSubgroup_units_two_classification {A : Subgroup ℤ_[2]ˣ} (hA : IsClosed ↑A)
(hA' : A ≠ ⊥) :
(∃ f, 2 ≤ f ∧ A = TauCeti.unitsPrincipal 2 f) ∨
(∃ f, 2 ≤ f ∧ A = TauCeti.unitsPlusMinus f) ∨
A = Subgroup.zpowers (-1) ∨
∃ f u, 2 ≤ f ∧ ↑u = -1 + 2 ^ f ∧ A = (Subgroup.zpowers u).topologicalClosure
Lean
Formalized in Tau Ceti as TauCeti.closedSubgroup_units_two_classification.
Sources
TheoremLegendre's formula for (pᵏ)!#
Since pᵏ has base-p digit sum one,
(p - 1) v_p((pᵏ)!) = pᵏ - 1.
TauCeti.sub_one_mul_padicValNat_factorial_pow (p : ℕ) [hp : Fact (Nat.Prime p)] (k : ℕ) :
(p - 1) * padicValNat p (p ^ k).factorial = p ^ k - 1
Lean
Formalized in Tau Ceti as TauCeti.sub_one_mul_padicValNat_factorial_pow.
Other forms
Legendre's formula, truncated at level h. Formalized in Tau Ceti as TauCeti.padicValNat_factorial_eq_add_sum.
TauCeti.padicValNat_factorial_eq_add_sum (p : ℕ) [Fact (Nat.Prime p)] (n h : ℕ) :
padicValNat p n.factorial =
padicValNat p (n / p ^ h).factorial + ∑ k ∈ Finset.range h, n / p ^ (k + 1)
Sources
Used by 2
DefinitionMahler's theorem, scalar-linear form#
Mathlib's Mahler isometry
mahlerEquiv E : C(ℤ_[p], E) ≃ₗᵢ[ℤ_[p]] C₀(ℕ, E) is linear over any semiring S acting on the
coefficient module E.
PadicInt.mahlerLinearIsometryEquiv.{u_1, u_2} {p : ℕ} [Fact (Nat.Prime p)] (S : Type u_1)
(E : Type u_2) [Semiring S] [NormedAddCommGroup E] [_root_.Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E]
[IsUltrametricDist E] [CompleteSpace E] [_root_.Module S E] [ContinuousConstSMul S E] :
C(ℤ_[p], E) ≃ₗᵢ[S] ZeroAtInftyContinuousMap ℕ E
Used by 1
TheoremThe Schwarz lemma on a grid of p-adic integers#
Let K be a complete normed field
extension of ℚ_p and f a power series over K restricted at a radius c ≥ 1. If the Hasse
derivatives (D⁽ᵗ⁾ f)(b) vanish for t < T at every point b of a finite set s of p-adic
integers, then at every p-adic integer x
‖f(x)‖ ≤ ‖f‖_c * (‖∏_{b ∈ s} (x - b)‖ / c ^ #s) ^ T.
PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_prod.{u_1} {p : ℕ} [Fact (Nat.Prime p)]
{K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K] {c : ℝ}
{f : PowerSeries K} (hf : PowerSeries.IsRestricted c f) (hc : 1 ≤ c) {s : Finset ℤ_[p]} {T : ℕ}
(hzero : ∀ b ∈ s, ∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ((algebraMap ℚ_[p] K) ↑b) = 0)
(x : ℤ_[p]) :
‖f.evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤
PowerSeries.gaussNorm norm c f * (‖∏ b ∈ s, (x - b)‖ / c ^ s.card) ^ T
Lean
Formalized in Tau Ceti as PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_prod.
Other forms
The Schwarz lemma on a progression of p-adic integers. Formalized in Tau Ceti as PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_factorial.
PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_factorial.{u_1} {p : ℕ}
[Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K]
{c : ℝ} {f : PowerSeries K} (hf : PowerSeries.IsRestricted c f) (hc : 1 ≤ c) (a : ℤ_[p])
{d : ℤ_[p]} (hd : IsUnit d) {n T : ℕ}
(hzero :
∀ j < n,
∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ((algebraMap ℚ_[p] K) ↑(a + ↑j * d)) = 0)
(x : ℤ_[p]) :
‖f.evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤
PowerSeries.gaussNorm norm c f * (‖↑n.factorial‖ / c ^ n) ^ T
The Schwarz lemma on the integers not divisible by q. Formalized in Tau Ceti as PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_factorial_pow.
PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_factorial_pow.{u_1} {p : ℕ}
[Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K]
{c : ℝ} {f : PowerSeries K} (hf : PowerSeries.IsRestricted c f) (hc : 1 ≤ c) {q : ℕ}
(hq : p.Coprime q) {N T : ℕ}
(hzero : ∀ j < N, ¬q ∣ j → ∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ↑j = 0) (x : ℤ_[p]) :
‖f.evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤
PowerSeries.gaussNorm norm c f *
(‖↑(N / q).factorial‖ ^ (q - 1) / c ^ {x ∈ Finset.range N | ¬q ∣ x}.card) ^ T
Sources
Uses 1
TheoremVan der Put's theorem#
a continuous function on ℤ_[p] with values in an ultrametric
normed group is the uniformly convergent sum of its van der Put terms, without assuming
completeness.
PadicInt.hasSum_vanDerPut.{u_2} {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_2}
[NormedAddCommGroup E] [IsUltrametricDist E] (f : C(ℤ_[p], E)) :
HasSum (fun n => PadicInt.vanDerPutTerm (PadicInt.vanDerPutCoeff (⇑f) n) n) f
Lean
Formalized in Tau Ceti as PadicInt.hasSum_vanDerPut.
Other forms
PadicInt.vanDerPutEquiv. Formalized in Tau Ceti as PadicInt.vanDerPutEquiv.
PadicInt.vanDerPutEquiv.{u_1, u_2} {p : ℕ} [hp : Fact (Nat.Prime p)] (S : Type u_1) (E : Type u_2)
[NormedAddCommGroup E] [IsUltrametricDist E] [CompleteSpace E] [Semiring S] [_root_.Module S E]
[ContinuousConstSMul S E] : C(ℤ_[p], E) ≃ₗᵢ[S] ZeroAtInftyContinuousMap ℕ E
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.