P-adic functional analysis

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremSerre's theorem (TauCeti.ResidueModule.isOrthonormalBasis_iff)#

For norms with values in ‖ϖ‖ ^ ℤ ∪ {0}, a family of the closed unit ball is an orthonormal basis exactly when its residues are a basis of the residue module: they are linearly independent over the residue ring and span.

TauCeti.ResidueModule.isOrthonormalBasis_iff.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2}
  {I : Type u_3} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R]
  [SeminormedAddCommGroup M] [IsUltrametricDist M] [_root_.Module R M] [IsBoundedSMul R M]
  (ϖ : TauCeti.NormedRing.PseudoUniformizer R)
  (hR : ∀ (a : R), TauCeti.zpowCeil ‖↑ϖ.unit‖ ‖a‖ = ‖a‖)
  (hM : ∀ (m : M), TauCeti.zpowCeil ‖↑ϖ.unit‖ ‖m‖ = ‖m‖)
  {e : I → ↥(TauCeti.unitClosedBallSubmodule R M)} :
  (TauCeti.IsOrthonormalBasis R fun i => ↑(e i)) ↔
    LinearIndependent (↥(Subring.unitClosedBall R) ⧸ TauCeti.unitBallIdeal R)
        (⇑TauCeti.ResidueModule.mk ∘ e) ∧
      Submodule.span (↥(Subring.unitClosedBall R) ⧸ TauCeti.unitBallIdeal R)
          (Set.range (⇑TauCeti.ResidueModule.mk ∘ e)) =
        ⊤

Lean

Formalized in Tau Ceti as TauCeti.ResidueModule.isOrthonormalBasis_iff.

Sources

• Tau Ceti documentation: TauCeti.ResidueModule.isOrthonormalBasis_iff
• Source of TauCeti.ResidueModule.isOrthonormalBasis_iff in TauCeti/Analysis/Normed/Module/Bases/ResidueBasis.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanTauCeti.ResidueModule.isOrthonormalBasis_iff

Used by 1

Used bySerre's criterion over a field

TheoremTauCeti.nonempty_continuousLinearEquiv_zeroAtInfty_nat_of_dense_span#

An infinite-dimensional ultrametric Banach space of countable type (some sequence has dense span) over a complete nontrivially normed field is continuously linearly equivalent to C₀(ℕ, K).

TauCeti.nonempty_continuousLinearEquiv_zeroAtInfty_nat_of_dense_span.{u, v} {K : Type v}
  [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E]
  [NormedSpace K E] [IsUltrametricDist E] [CompleteSpace E] (hE : ¬FiniteDimensional K E)
  {v : ℕ → E} (hv : Dense ↑(Submodule.span K (Set.range v))) :
  Nonempty (E ≃L[K] ZeroAtInftyContinuousMap ℕ K)

Lean

Formalized in Tau Ceti as TauCeti.nonempty_continuousLinearEquiv_zeroAtInfty_nat_of_dense_span.

Sources

• Tau Ceti documentation: TauCeti.nonempty_continuousLinearEquiv_zeroAtInfty_nat_of_dense_span
• Source of TauCeti.nonempty_continuousLinearEquiv_zeroAtInfty_nat_of_dense_span in TauCeti/Analysis/Normed/Module/Bases/ModelSpace.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanTauCeti.nonempty_continuousLinearEquiv_zeroAtInfty_nat_of_dense_span

Uses 1

Proof usesRiesz's lemma, translated form

DefinitionMahler duality#

Over a ring with a multiplicative pseudo-uniformiser, a measure on ℤ_p is determined by its moments μ (x ↦ x choose n), the coefficients of its Amice transform, and every bounded sequence is the moment sequence of a measure. The inverse sends a bounded sequence b to the measure f ↦ ∑ n, Δ^n f (0) * b n.

AbstractMeasure.mahlerMomentsEquiv.{u_1} (p : ℕ) [Fact (Nat.Prime p)] (R : Type u_1)
  [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [Algebra ℤ_[p] R] [IsBoundedSMul ℤ_[p] R]
  [IsUltrametricDist R] [CompleteSpace R] : AbstractMeasure ℤ_[p] R R ≃ₗ[R] ↥(lp (fun x => R) ⊤)

Lean

Formalized in Tau Ceti as AbstractMeasure.mahlerMomentsEquiv.

Sources

• Tau Ceti documentation: AbstractMeasure.mahlerMomentsEquiv
• Source of AbstractMeasure.mahlerMomentsEquiv in TauCeti/NumberTheory/Padics/Measure/MahlerDuality.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanAbstractMeasure.mahlerMomentsEquiv

Uses 2

Statement usesMahler's theorem, scalar-linear form · The universal property of C₀(I, R)

TheoremMahler duality for field coefficients#

Over a complete ultrametric nontrivially normed field with a contractive ℤ_[p]-algebra structure, such as a complete extension of ℚ_p, the operator norm of a measure on ℤ_p is the supremum of the norms of the coefficients of its Amice transform.

AbstractMeasure.norm_toCLMEquiv_eq_iSup_coeff.{u_1} {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1}
  [NontriviallyNormedField K] [Algebra ℤ_[p] K] [IsBoundedSMul ℤ_[p] K] [IsUltrametricDist K]
  [CompleteSpace K] (μ : AbstractMeasure ℤ_[p] K K) :
  ‖AbstractMeasure.toCLMEquiv μ‖ = ⨆ n, ‖(PowerSeries.coeff n) (AbstractMeasure.amiceTransform μ)‖

Lean

Formalized in Tau Ceti as AbstractMeasure.norm_toCLMEquiv_eq_iSup_coeff.

Sources

• Tau Ceti documentation: AbstractMeasure.norm_toCLMEquiv_eq_iSup_coeff
• Source of AbstractMeasure.norm_toCLMEquiv_eq_iSup_coeff in TauCeti/NumberTheory/Padics/Measure/MahlerDuality.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanAbstractMeasure.norm_toCLMEquiv_eq_iSup_coeff

TheoremThe integral dual unit ball#

A ℚ_p-valued measure on ℤ_p has operator norm at most 1 exactly when there is a unique ℤ_p-valued measure μ with ν (f) = μ (f) for every ℤ_p-valued test function f.

AbstractMeasure.existsUnique_integral_iff_norm_le_one {p : ℕ} [Fact (Nat.Prime p)]
  (ν : AbstractMeasure ℤ_[p] ℚ_[p] ℚ_[p]) :
  (∃! μ,
      ∀ (f : C(ℤ_[p], ℤ_[p])),
        ν ({ toFun := fun x => ↑x, continuous_toFun := ⋯ }.comp f) = ↑(μ f)) ↔
    ‖AbstractMeasure.toCLMEquiv ν‖ ≤ 1

Lean

Formalized in Tau Ceti as AbstractMeasure.existsUnique_integral_iff_norm_le_one.

Sources

• Tau Ceti documentation: AbstractMeasure.existsUnique_integral_iff_norm_le_one
• Source of AbstractMeasure.existsUnique_integral_iff_norm_le_one in TauCeti/NumberTheory/Padics/Measure/IntegralUnitBall.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanAbstractMeasure.existsUnique_integral_iff_norm_le_one

Uses 1

Proof usesExtension of coefficients from the unit ball

TheoremS_h ≤ D_h#

The Gauss norm at the radius r_h is at most the dual stage norm at level h, provided the latter is the supremum of a bounded family.

TauCeti.gaussNorm_amiceRadius_le_amiceDualNorm.{u_1} {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedRing K] {F : PowerSeries K} {h : ℕ}
  (hF : BddAbove (Set.range fun n => ‖(PowerSeries.coeff n) F‖ * ‖↑(n / p ^ h).factorial‖)) :
  PowerSeries.gaussNorm norm (TauCeti.amiceRadius p h) F ≤ TauCeti.amiceDualNorm p h F

Lean

Formalized in Tau Ceti as TauCeti.gaussNorm_amiceRadius_le_amiceDualNorm.

Sources

• Tau Ceti documentation: TauCeti.gaussNorm_amiceRadius_le_amiceDualNorm
• Source of TauCeti.gaussNorm_amiceRadius_le_amiceDualNorm in TauCeti/NumberTheory/Padics/Distribution/Amice/Norm.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanTauCeti.gaussNorm_amiceRadius_le_amiceDualNorm

TheoremD_h ≤ p S_{h+1}#

The dual stage norm at level h is at most p times the Gauss norm at the radius r_{h+1}, provided the latter is the supremum of a bounded family.

TauCeti.amiceDualNorm_le_mul_gaussNorm_amiceRadius_succ.{u_1} {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedRing K] {F : PowerSeries K} {h : ℕ}
  (hF : PowerSeries.HasGaussNorm norm (TauCeti.amiceRadius p (h + 1)) F) :
  TauCeti.amiceDualNorm p h F ≤ ↑p * PowerSeries.gaussNorm norm (TauCeti.amiceRadius p (h + 1)) F

Lean

Formalized in Tau Ceti as TauCeti.amiceDualNorm_le_mul_gaussNorm_amiceRadius_succ.

Sources

• Tau Ceti documentation: TauCeti.amiceDualNorm_le_mul_gaussNorm_amiceRadius_succ
• Source of TauCeti.amiceDualNorm_le_mul_gaussNorm_amiceRadius_succ in TauCeti/NumberTheory/Padics/Distribution/Amice/Norm.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanTauCeti.amiceDualNorm_le_mul_gaussNorm_amiceRadius_succ

TheoremTauCeti.Huber.exists_tateSeminorm#

A ring with separately continuous multiplication in which the sets ϖ ^ n A₀, n ≥ 0, form a neighbourhood basis of zero carries an ultrametric ring seminorm, equal to the Tate gauge, whose open balls about zero form a neighbourhood basis of zero.

TauCeti.Huber.exists_tateSeminorm.{u_1} {A : Type u_1} [CommRing A] {A₀ : Subring A} {ϖ : Aˣ}
  {a : ℝ} [TopologicalSpace A]
  (hb : (nhds 0).HasBasis (fun x => True) fun n => {x | ↑(ϖ ^ (-↑n)) * x ∈ A₀})
  [SeparatelyContinuousMul A] (ha : 1 < a) (hϖ : ↑ϖ ∈ A₀) :
  ∃ α,
    (∀ (x : A), α x = TauCeti.Huber.tateGauge A₀ ϖ a x) ∧
      IsNonarchimedean ⇑α ∧ (nhds 0).HasBasis (fun ε => 0 < ε) fun ε => {x | α x < ε}

Lean

Formalized in Tau Ceti as TauCeti.Huber.exists_tateSeminorm.

Sources

• Tau Ceti documentation: TauCeti.Huber.exists_tateSeminorm
• Source of TauCeti.Huber.exists_tateSeminorm in TauCeti/RingTheory/Huber/TateGauge/Basic.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanTauCeti.Huber.exists_tateSeminorm

DefinitionThe universal property of C₀(I, R)#

Over a commutative ring admitting a multiplicative pseudo-uniformiser, bounded families I → M in a complete ultrametric module correspond to continuous linear maps C₀(I, R) →L[R] M, isometrically for the sup norm and the operator norm. A family e is sent to its linear combination map a ↦ ∑' i, a i • e i, and a map u to its values u (single i 1) at the unit coordinate vectors.

ZeroAtInftyContinuousMap.linearCombinationEquiv.{u_1, u_2, u_3} {I : Type u_1} (R : Type u_2)
  (M : Type u_3) [TopologicalSpace I] [DiscreteTopology I] [NormedCommRing R]
  [TauCeti.NormedRing.IsTate R] [NormedAddCommGroup M] [_root_.Module R M] [IsBoundedSMul R M]
  [IsUltrametricDist M] [CompleteSpace M] [DecidableEq I] :
  ↥(lp (fun x => M) ⊤) ≃ₗᵢ[R] ZeroAtInftyContinuousMap I R →L[R] M

Lean

Formalized in Tau Ceti as ZeroAtInftyContinuousMap.linearCombinationEquiv.

Sources

• Tau Ceti documentation: ZeroAtInftyContinuousMap.linearCombinationEquiv
• Source of ZeroAtInftyContinuousMap.linearCombinationEquiv in TauCeti/Topology/ContinuousMap/ZeroAtInfty/LinearCombination.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanZeroAtInftyContinuousMap.linearCombinationEquiv

Used by 1

Used byMahler duality

DefinitionTauCeti.AnalyticStage.transition#

The transition LA_h(E) → LA_{h+1}(E). The disc of a ∈ ZMod (pʰ) is the union of the discs of the classes a' = a + pʰ b, 0 ≤ b < p, in ZMod (p ^ (h + 1)), where b = ⌊a'.val / pʰ⌋. On the disc of a' the coordinates are related by w = b + p v, and the transition re-expands ∑ₖ c(a, k) wᵏ in powers of v:

d(a', j) = ∑ₖ (k choose j) b^(k - j) pʲ • c(a, k).

TauCeti.AnalyticStage.transition.{u_1, u_2} {p : ℕ} [hp : Fact (Nat.Prime p)] {h : ℕ} {E : Type u_1}
  [NormedAddCommGroup E] [_root_.Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E]
  [CompleteSpace E] (S : Type u_2) [Semiring S] [_root_.Module S E] [ContinuousConstSMul S E]
  [SMulCommClass ℤ_[p] S E] : TauCeti.AnalyticStage p h E →L[S] TauCeti.AnalyticStage p (h + 1) E

Lean

Formalized in Tau Ceti as TauCeti.AnalyticStage.transition.

Sources

• Tau Ceti documentation: TauCeti.AnalyticStage.transition
• Source of TauCeti.AnalyticStage.transition in TauCeti/NumberTheory/Padics/Distribution/AnalyticStage.lean
• Tau Ceti roadmap status: P-adic functional analysis

LeanTauCeti.AnalyticStage.transition

TheoremAmice's basis theorem#

The disc expansions amiceTerm p h n 1 of Amice's polynomials e_{h,n}(x) = ⌊n / pʰ⌋! (x choose n) form an orthonormal basis of LA_h(ℤ_p).

TauCeti.AnalyticStage.isOrthonormalBasis_amiceTerm (p : ℕ) [hp : Fact (Nat.Prime p)] (h : ℕ) :
  TauCeti.IsOrthonormalBasis ℤ_[p] fun n => TauCeti.AnalyticStage.amiceTerm p h n 1

Lean

Formalized in Tau Ceti as TauCeti.AnalyticStage.isOrthonormalBasis_amiceTerm.

Sources

• Tau Ceti documentation: TauCeti.AnalyticStage.isOrthonormalBasis_amiceTerm
• Source of TauCeti.AnalyticStage.isOrthonormalBasis_amiceTerm in TauCeti/NumberTheory/Padics/Distribution/Amice/Isometry.lean

LeanTauCeti.AnalyticStage.isOrthonormalBasis_amiceTerm

Uses 2

Proof usesAmice's theorem · Legendre's formula for (pᵏ)!

DefinitionAmice's theorem#

Amice's map (cₙ) ↦ ∑ₙ e_{h,n} • cₙ, where e_{h,n}(x) = ⌊n / pʰ⌋! (x choose n), is an isometric isomorphism from the null sequences in E onto the analytic stage LA_h(E).

TauCeti.AnalyticStage.amiceEquiv.{u_1, u_2} (p : ℕ) [hp : Fact (Nat.Prime p)] (h : ℕ) {E : Type u_1}
  [NormedAddCommGroup E] [_root_.Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E]
  [CompleteSpace E] (S : Type u_2) [Semiring S] [_root_.Module S E] [ContinuousConstSMul S E]
  [SMulCommClass ℤ_[p] S E] : ZeroAtInftyContinuousMap ℕ E ≃ₗᵢ[S] TauCeti.AnalyticStage p h E

Lean

Formalized in Tau Ceti as TauCeti.AnalyticStage.amiceEquiv.

Other forms

Amice's theorem. Formalized in Tau Ceti as TauCeti.AnalyticStage.norm_amiceMap.

TauCeti.AnalyticStage.norm_amiceMap.{u_1, u_2} {p : ℕ} [hp : Fact (Nat.Prime p)] {h : ℕ}
  {E : Type u_1} [NormedAddCommGroup E] [_root_.Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E]
  [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [_root_.Module S E]
  [ContinuousConstSMul S E] [SMulCommClass ℤ_[p] S E] (c : ZeroAtInftyContinuousMap ℕ E) :
  ‖(TauCeti.AnalyticStage.amiceMap p h S) c‖ = ‖c‖

Amice's theorem: surjectivity. Formalized in Tau Ceti as TauCeti.AnalyticStage.amiceMap_surjective.

TauCeti.AnalyticStage.amiceMap_surjective.{u_1, u_2} (p : ℕ) [hp : Fact (Nat.Prime p)] (h : ℕ)
  {E : Type u_1} [NormedAddCommGroup E] [_root_.Module ℤ_[p] E] [IsBoundedSMul ℤ_[p] E]
  [IsUltrametricDist E] [CompleteSpace E] (S : Type u_2) [Semiring S] [_root_.Module S E]
  [ContinuousConstSMul S E] [SMulCommClass ℤ_[p] S E] :
  Function.Surjective ⇑(TauCeti.AnalyticStage.amiceMap p h S)

Sources

• Tau Ceti documentation: TauCeti.AnalyticStage.amiceEquiv
• Source of TauCeti.AnalyticStage.amiceEquiv in TauCeti/NumberTheory/Padics/Distribution/Amice/Isometry.lean

LeanTauCeti.AnalyticStage.amiceEquiv · TauCeti.AnalyticStage.norm_amiceMap · TauCeti.AnalyticStage.amiceMap_surjective

Uses 1 · Used by 1

Proof usesLegendre's formula for (pᵏ)!

Used byAmice's basis theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.