How to define a norm of a ContinuousLinearMap

Stream: new members

[Hanliu Jiang]

I need do define a norm of C(\Z_[p],\Z_[p])\toL[\Z_[p]]\Z_[p],as we always define, so However Mathlib cant define this because \Z_[p] not a field , how can I solve this problem?

[Matt Diamond]

Could you provide a #mwe of what you're trying to define?

[Matt Diamond]

ℤ_[p] is a NormedRing, does that help?

[Hanliu Jiang]

/-

Copyright (c) 2025 Hanliu Jiang. All rights reserved.

Released under Apache 2.0 license as described in the file LICENSE.

Authors: Shanwen Wang, Hanliu Jiang
-/

import Mathlib.NumberTheory.Padics.MahlerBasis

import Mathlib.RingTheory.PowerSeries.Basic

/-!

The Amice Transform of p-adic measure

References

• [P. Colmez, Fonctions d'une variable p-adique][colmez2010]

Tags

Bojanic
-/

open Finset IsUltrametricDist NNReal Filter PowerSeries

open scoped fwdDiff ZeroAtInfty Topology

variable {p : ℕ} [hp : Fact p.Prime]

namespace PadicInt

section norm_1

noncomputable def to_Bound_function :

(ℕ → ℤ_[p]) →ₗ[ℤ_[p]] ( BoundedContinuousFunction ℕ ℤ_[p]) where

toFun a:= {

toFun := a

continuous_toFun :=continuous_of_discreteTopology

map_bounded' := sorry

}

map_add' _ _:=rfl

map_smul' _ _ := rfl

noncomputable def to_Bound_norm :  AddGroupNorm (ℕ → ℤ_[p])where

toFun f := ‖to_Bound_function f‖

map_zero' :=by

unfold to_Bound_function

simp

rfl

add_le' a b:=by

simp

exact norm_add_le (to_Bound_function a) (to_Bound_function b)

neg' a:=by

simp

eq_zero_of_map_eq_zero' x sx:=by

have:to_Bound_function x=0 :=by sorry

unfold to_Bound_function at this

simp at this

sorry

noncomputable instance:  SeminormedAddCommGroup (ℕ → ℤ_[p])

:=AddGroupSeminorm.toSeminormedAddCommGroup

( AddGroupNorm.toAddGroupSeminorm (to_Bound_norm))

end norm_1

section norm_2

`

noncomputable def Amice_iso :

(C(ℤ_[p],ℤ_[p]) →L[ℤ_[p]] ℤ_[p])≃ₗᵢ[ℤ_[p]]

ℕ→ ℤ_[p] :=sorry

[Hanliu Jiang]

it cant help

[Matt Diamond]

please use #backticks

[Hanliu Jiang]

/-
Copyright (c) 2025 Hanliu Jiang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shanwen Wang, Hanliu Jiang
-/

import Mathlib.NumberTheory.Padics.MahlerBasis
import Mathlib.RingTheory.PowerSeries.Basic
/-!
# The Amice Transform of p-adic measure


## References

* [P. Colmez, *Fonctions d'une variable p-adique*][colmez2010]

## Tags

Bojanic
-/

open Finset IsUltrametricDist NNReal Filter PowerSeries

open scoped fwdDiff ZeroAtInfty Topology

variable {p : ℕ} [hp : Fact p.Prime]

namespace PadicInt
section norm_1
noncomputable def to_Bound_function :
 (ℕ → ℤ_[p]) →ₗ[ℤ_[p]] ( BoundedContinuousFunction ℕ ℤ_[p]) where
  toFun a:= {
    toFun := a
    continuous_toFun :=continuous_of_discreteTopology
    map_bounded' := sorry
  }
  map_add' _ _:=rfl
  map_smul' _ _ := rfl

noncomputable def to_Bound_norm :  AddGroupNorm (ℕ → ℤ_[p])where
  toFun f := ‖to_Bound_function f‖
  map_zero' :=by

       unfold to_Bound_function
       simp
       rfl

  add_le' a b:=by
    simp
    exact norm_add_le (to_Bound_function a) (to_Bound_function b)
  neg' a:=by
    simp

  eq_zero_of_map_eq_zero' x sx:=by
       have:to_Bound_function x=0 :=by sorry
       unfold to_Bound_function at this
       simp at this
       sorry
noncomputable instance:  SeminormedAddCommGroup (ℕ → ℤ_[p])
 :=AddGroupSeminorm.toSeminormedAddCommGroup
( AddGroupNorm.toAddGroupSeminorm (to_Bound_norm))
end norm_1
section norm_2
`
noncomputable def Amice_iso :
(C(ℤ_[p],ℤ_[p]) →L[ℤ_[p]] ℤ_[p])≃ₗᵢ[ℤ_[p]]
   ℕ→ ℤ_[p] :=sorry

[Hanliu Jiang]

sorry
im a rookie

[Kevin Buzzard]

@David Loeffler have you been thinking about this sort of thing recently?

[David Loeffler]

Kevin Buzzard said:

David Loeffler have you been thinking about this sort of thing recently?

Yes, I have. At the moment Mathlib's support for normed modules over non-field base rings is a bit fragmentary; I have been working on building it up, but it's a slow job, and it's delicate to do it in a way that doesn't slow down or lose functionality for the core case of normed vector spaces over a normed field.

As for the problem at hand: you are trying to define the Amice transform as a LinearIsometryEquiv, which is a huge amount of data bundled all together – you need to define a map, define the inverse map, show it is linear, show it preserves the norm, etc. Perhaps it might be sensible to do this in stages? Try first defining

noncomputable def Amice_transform : (C(ℤ_[p], ℤ_[p]) →L[ℤ_[p]] ℤ_[p]) → (ℕ → ℤ_[p]) :=
  fun μ n ↦ μ (mahler n)

and then think about upgrading it in various ways later.

(FWIW, as a mathematician who uses p-adic function theory very often in my own research, I'm not sure the norm on the space C(ℤ_[p], ℤ_[p]) →L[ℤ_[p]] ℤ_[p] is very important anyway. This space of measures has two topologies, the "strong" topology induced by the operator norm, and the "weak" topology induced by the evaluation functionals coming from elements of C(ℤ_[p], ℤ_[p]). If you give it the strong topology it's really a pretty nasty object: it's not separable, for instance, and its dual is enormous, far bigger than C(ℤ_[p], ℤ_[p]) . But if you give it the weak topology, it's as nice a space as you could ask for – a compact Hausdorff space – and its dual is C(ℤ_[p], ℤ_[p]) again.)

[Hanliu Jiang]

ok thanks and i'm try to build p-adc l funtion with Shanwen Wang in RUC

[David Loeffler]

That's interesting! That's a goal I'd also had in mind for the future, I'd be happy to discuss and maybe work on it together. Do you mean p-adic L-functions for Dirichlet characters? Or for something fancier (modular forms etc)? Please give my regards to Shanwen, by the way; he and I know each other from the "normal maths world", since we both work on Euler systems, I didn't know he was also interested in Lean.