3.5. A measure-theoretic toolbox🔗

Natural operations on measures correspond, under the Mahler transform, to operators on power series. We henceforth freely conflate \sM(G, \OL) with \Lam(G), writing \mu \in \Lam(G) for a measure.

Proposition3.5.1

uses 1used by 1✓L∃∀N

For a measure \mu on \Zp, define x\mu by \int_{\Zp} f \cdot x\mu = \int_{\Zp} xf \cdot \mu. Then \Am_{x\mu} = \partial\, \Am_\mu, \qquad \partial := (1+T)\tfrac{d}{dT}. This uses Definition 3.4.3.

Lean code for Proposition3.5.1●1 theorem

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.mahlerTransform_cmul_X (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.mahlerTransform p
      (PadicMeasure.cmul p (ContinuousMap.id ℤ_[p]) μ) =
    PadicMeasure.del p (PadicMeasure.mahlerTransform p μ)

theorem PadicMeasure.mahlerTransform_cmul_X
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.mahlerTransform p
      (PadicMeasure.cmul p
        (ContinuousMap.id ℤ_[p]) μ) =
    PadicMeasure.del p
      (PadicMeasure.mahlerTransform p μ)

Multiplication by `x` on measures corresponds to `∂` on Mahler transforms:
`𝓐_{xμ} = ∂ 𝓐_μ`. Proof: `x·binom(x,n) = (n+1)·binom(x,n+1) + n·binom(x,n)`.

Source: RJW Lem. 3.24 (`LemmaMultiplicationbyx`, TeX lines 1066–1075).

Proof for Proposition 3.5.1

uses 0

It suffices to compute the action on the Mahler basis. From the Pascal-type identity x\binomc{x}{n} = (x-n)\binomc{x}{n} + n\binomc{x}{n} = (n+1)\binomc{x}{n+1} + n\binomc{x}{n}, multiplication by x sends the coefficient sequence of \mu to that obtained by applying \partial, since \partial acts on T^n exactly as T^n \mapsto (1+T)\,nT^{n-1} = nT^{n-1} + nT^n, matching the two terms above.

Corollary3.5.2

uses 1used by 0✓L∃∀N

For \mu \in \Lam(\Zp) and k \geq 0, \int_{\Zp} x^k \cdot \mu = (\partial^k \Am_\mu)(0). This is immediate from Proposition 3.5.1.

Lean code for Corollary3.5.2●1 theorem

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.apply_powCM (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) (k : ℕ) :
  μ (PadicMeasure.powCM p k) =
    PowerSeries.constantCoeff
      ((PadicMeasure.del p)^[k] (PadicMeasure.mahlerTransform p μ))

theorem PadicMeasure.apply_powCM (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) (k : ℕ) :
  μ (PadicMeasure.powCM p k) =
    PowerSeries.constantCoeff
      ((PadicMeasure.del p)^[k]
        (PadicMeasure.mahlerTransform p
          μ))

`∫_{ℤ_p} xᵏ dμ = (∂ᵏ 𝓐_μ)(0)`.

Source: RJW Cor. 3.25 (`cor:eval at x^k`, TeX lines 1079–1082).

Proof for Corollary 3.5.2

Proof uses 2

Proof dependency previews

Preview

Definition 3.4.5

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

Iterating Proposition 3.5.1 gives \Am_{x^k\mu} = \partial^k \Am_\mu, and evaluating the moment formula \int_{\Zp} \mu_g = g(0) at g = \Am_{x^k\mu} (see Definition 3.4.5) yields \int_{\Zp} x^k \cdot \mu = \Am_{x^k\mu}(0) = (\partial^k \Am_\mu)(0).

Definition3.5.3

uses 1used by 1✓L∃∀N

For g \in \cC(\Zp, L) define g(x)\mu by \int_{\Zp} f \cdot g(x)\mu := \int_{\Zp} fg \cdot \mu. In particular, for z \in \OL with \abs{z-1} < 1, \Am_{z^x \mu}(T) = \Am_\mu\big((1+T)z - 1\big), since \Am_\mu((1+T)z - 1) = \int_{\Zp}((1+T)z)^x \cdot \mu is by definition the Mahler transform of z^x\mu. Uses Definition 3.4.3.

In the formalisation the multiplication is MeasureR.cmul (over the general coefficient ring of the §5 widening) and the displayed substitution identity is mahlerTransform_charTwist, stated coefficientwise — the right-hand side read off as the convergent sum over Mahler coefficients, with z = 1 + r for topologically nilpotent r.

Lean code for Definition3.5.3●2 declarations

defdefined in PadicLFunctions/MeasureR/Toolbox.lean

complete

def PadicLFunctions.MeasureR.cmul.{u_1} (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K] [IsUltrametricDist K]
  (g : C(ℤ_[p], ↥(PadicLFunctions.integerRing K)))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  PadicLFunctions.MeasureR K ℤ_[p]

def PadicLFunctions.MeasureR.cmul.{u_1}
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (K : Type u_1) [NormedField K]
  [IsUltrametricDist K]
  (g :
    C(ℤ_[p],
      ↥(PadicLFunctions.integerRing K)))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  PadicLFunctions.MeasureR K ℤ_[p]

Multiplication of a measure by a continuous function: `(g·μ)(f) = μ(gf)`
(RJW §3.5.2, TeX 1086–1089).

theoremdefined in PadicLFunctions/Interpolation/Twist.lean

complete

theorem PadicLFunctions.MeasureR.mahlerTransform_charTwist.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  (r : ↥(PadicLFunctions.integerRing K))
  (hr : Filter.Tendsto (fun x ↦ r ^ x) Filter.atTop (nhds 0))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) (n : ℕ) :
  (PowerSeries.coeff n)
      (PadicLFunctions.MeasureR.mahlerTransform p K
        (PadicLFunctions.MeasureR.twist p K
          (PadicLFunctions.MeasureR.charCM r hr) μ)) =
    ∑' (m : ℕ),
      (PowerSeries.coeff n)
          (((1 + PowerSeries.X) * PowerSeries.C (1 + r) - 1) ^ m) *
        μ (PadicLFunctions.MeasureR.mahlerCM p K m)

theorem PadicLFunctions.MeasureR.mahlerTransform_charTwist.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  (r : ↥(PadicLFunctions.integerRing K))
  (hr :
    Filter.Tendsto (fun x ↦ r ^ x)
      Filter.atTop (nhds 0))
  (μ : PadicLFunctions.MeasureR K ℤ_[p])
  (n : ℕ) :
  (PowerSeries.coeff n)
      (PadicLFunctions.MeasureR.mahlerTransform
        p K
        (PadicLFunctions.MeasureR.twist p
          K
          (PadicLFunctions.MeasureR.charCM
            r hr)
          μ)) =
    ∑' (m : ℕ),
      (PowerSeries.coeff n)
          (((1 + PowerSeries.X) *
                PowerSeries.C (1 + r) -
              1) ^
            m) *
        μ
          (PadicLFunctions.MeasureR.mahlerCM
            p K m)

L5.1.6: the `z`-twist transform formula, coefficientwise form (recorded
fallback of the decomposition's eval₂ form — both routes recorded at L5.1.6
attack [3]): the Mahler coefficients of the twist of `μ` by the character
`κ_r = (1+r)^x` (mathlib `PadicInt.addChar_of_value_at_one`) are
`∑_{m} binom(n+m choose stuff)`-convolutions; equivalently, for every `n`,
`𝓐(κ_r·μ)_n = ∑' m, (coeff of the expansion) — here stated in the form the
§5.1 proofs consume: the twisted transform evaluated through `(1+T)(1+r)−1`.

Source (TeX 1084–1090): "the measure `z^x μ` has Mahler transform
`𝓐_μ((1+T)z − 1)`".

Definition3.5.4

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 3.5.5

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

For an open compact X \subseteq \Zp with characteristic function \one_X, the restriction \Res_X(\mu) is the measure with \int_{\Zp} f \cdot \Res_X(\mu) := \int_{\Zp} f\one_X \cdot \mu, also written \int_X f \cdot \mu; one says \mu is supported on X if \mu = \Res_X(\mu). For X = b + p^n\Zp the characteristic function is the finite Fourier expansion \one_{b+p^n\Zp}(x) = \tfrac{1}{p^n}\sum_{\xi \in \mu_{p^n}} \xi^{x-b} over the p^n-th roots of unity (the sum being 1 when p^n \mid x - b and 0 otherwise). Multiplying \mu by each character x \mapsto \xi^x via Definition 3.5.3 and summing gives \Am_{\Res_{b+p^n\Zp}(\mu)}(T) = \frac{1}{p^n}\sum_{\xi \in \mu_{p^n}} \xi^{-b}\, \Am_\mu\big((1+T)\xi - 1\big). The case b = 0, n = 1 gives the restriction to \Zpx: \Am_{\Res_{\Zpx}(\mu)}(T) = \Am_\mu(T) - \frac{1}{p}\sum_{\xi \in \mu_p}\Am_\mu\big((1+T)\xi - 1\big). An arbitrary open compact X (or its complement, as here for \Zpx) is a finite disjoint union of such balls, so its restriction formula is obtained by summing.

The displayed Fourier-expansion formula (deferred during §3) is realised in the §5 coefficient layer as MeasureR.res_class_eq_sum_twists, stated as an identity of measures multiplied through by p^n and with ξ^{-b} written with a positive exponent — the source's identity divided by p^n.

Lean code for Definition3.5.4●3 declarations

defdefined in PadicLFunctions/Measure/Toolbox.lean

complete

def PadicMeasure.res (p : ℕ) [hp : Fact (Nat.Prime p)] {U : Set ℤ_[p]}
  (hU : IsClopen U) (μ : PadicMeasure p ℤ_[p]) : PadicMeasure p ℤ_[p]

def PadicMeasure.res (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  {U : Set ℤ_[p]} (hU : IsClopen U)
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure p ℤ_[p]

Restriction of a measure to a clopen subset `U ⊆ ℤ_p`:
`(Res_U μ)(f) = μ(𝟙_U · f)`, viewed as a measure on `ℤ_p`.

Source: RJW §3.5.3 (TeX lines 1100–1103).

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.res_union (p : ℕ) [hp : Fact (Nat.Prime p)]
  {U V : Set ℤ_[p]} (hU : IsClopen U) (hV : IsClopen V)
  (hUV : Disjoint U V) (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.res p ⋯ μ =
    PadicMeasure.res p hU μ + PadicMeasure.res p hV μ

theorem PadicMeasure.res_union (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  {U V : Set ℤ_[p]} (hU : IsClopen U)
  (hV : IsClopen V) (hUV : Disjoint U V)
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.res p ⋯ μ =
    PadicMeasure.res p hU μ +
      PadicMeasure.res p hV μ

Restriction is additive over a disjoint clopen decomposition.

Source: RJW §3.5.4 (TeX line 1129): "we can write X ... as a disjoint union".

theoremdefined in PadicLFunctions/Interpolation/Twist.lean

complete

theorem PadicLFunctions.MeasureR.res_class_eq_sum_twists.{u_1} {p : ℕ}
  [hp : Fact (Nat.Prime p)] {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K] [IsUltrametricDist K] [CompleteSpace K]
  {n : ℕ} (_hn : 1 ≤ n) {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n)) (b : ZMod (p ^ n))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  ↑p ^ n • PadicLFunctions.MeasureR.res p K ⋯ μ =
    ∑ c ∈ Finset.range (p ^ n),
      ζ ^ (c * (p ^ n - b.val % p ^ n)) •
        PadicLFunctions.MeasureR.twist p K
          (PadicLFunctions.MeasureR.charCM (ζ ^ c - 1) ⋯) μ

theorem PadicLFunctions.MeasureR.res_class_eq_sum_twists.{u_1}
  {p : ℕ} [hp : Fact (Nat.Prime p)]
  {K : Type u_1} [NormedField K]
  [NormedAlgebra ℚ_[p] K]
  [IsUltrametricDist K] [CompleteSpace K]
  {n : ℕ} (_hn : 1 ≤ n)
  {ζ : ↥(PadicLFunctions.integerRing K)}
  (hζ : IsPrimitiveRoot ζ (p ^ n))
  (b : ZMod (p ^ n))
  (μ : PadicLFunctions.MeasureR K ℤ_[p]) :
  ↑p ^ n •
      PadicLFunctions.MeasureR.res p K ⋯
        μ =
    ∑ c ∈ Finset.range (p ^ n),
      ζ ^ (c * (p ^ n - b.val % p ^ n)) •
        PadicLFunctions.MeasureR.twist p K
          (PadicLFunctions.MeasureR.charCM
            (ζ ^ c - 1) ⋯)
          μ

L5.1.7 (`EqRestrictionFormula`, cleared per R5-CLEAR): for a primitive
`p^n`-th root of unity `ζ` and `b : ZMod (p^n)`,
`p^n · Res_{b+p^nℤ_p}(μ) = ∑_{c} ζ^{-bc} · (κ_{ζ^c−1}-twist of μ)` as
measures (`ζ^{-bc}` realised with the positive exponent `c·(p^n − b.val)`).

Source (verbatim, TeX 1126–1131): the display `EqRestrictionFormula`,
multiplied through by `p^n`.

Definition3.5.5

Statement uses 2

Statement dependency previews

Preview

Definition 3.4.3

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

For a \in \Zpx define \sigma_a(\mu) by \int_{\Zp} f(x) \cdot \sigma_a(\mu) = \int_{\Zp} f(ax) \cdot \mu. Testing against f(x) = (1+T)^x (so f(ax) = ((1+T)^a)^x) shows \Am_{\sigma_a(\mu)} = \Am_\mu((1+T)^a - 1): this is the substitution 1+T \mapsto (1+T)^a. Write \varphi := \sigma_p, so \int_{\Zp} f(x) \cdot \varphi(\mu) = \int_{\Zp} f(px) \cdot \mu and \Am_{\varphi(\mu)} = \Am_\mu((1+T)^p - 1). Define the partial inverse \psi(\mu) by \int_{\Zp} f(x) \cdot \psi(\mu) = \int_{p\Zp} f(p^{-1}x) \cdot \mu. These use Definition 3.5.4 and Definition 3.4.3.

Lean code for Definition3.5.5●5 declarations

defdefined in PadicLFunctions/Measure/Toolbox.lean

complete

def PadicMeasure.sigma (p : ℕ) [hp : Fact (Nat.Prime p)] (a : ℤ_[p]ˣ) :
  PadicMeasure p ℤ_[p] →ₗ[ℤ_[p]] PadicMeasure p ℤ_[p]

def PadicMeasure.sigma (p : ℕ)
  [hp : Fact (Nat.Prime p)] (a : ℤ_[p]ˣ) :
  PadicMeasure p ℤ_[p] →ₗ[ℤ_[p]]
    PadicMeasure p ℤ_[p]

The `ℤ_p^×`-action on measures: `∫ f d(σ_a μ) = ∫ f(ax) dμ`.

Source: RJW §3.5.5 (TeX lines 1135–1136).

defdefined in PadicLFunctions/Measure/Toolbox.lean

complete

def PadicMeasure.phi (p : ℕ) [hp : Fact (Nat.Prime p)] :
  PadicMeasure p ℤ_[p] →ₗ[ℤ_[p]] PadicMeasure p ℤ_[p]

def PadicMeasure.phi (p : ℕ)
  [hp : Fact (Nat.Prime p)] :
  PadicMeasure p ℤ_[p] →ₗ[ℤ_[p]]
    PadicMeasure p ℤ_[p]

The operator `φ` ("`σ_p`"): `∫ f d(φμ) = ∫ f(px) dμ`.

Source: RJW §3.5.5 (TeX lines 1141–1142).

defdefined in PadicLFunctions/Measure/Toolbox.lean

complete

def PadicMeasure.psi (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) : PadicMeasure p ℤ_[p]

def PadicMeasure.psi (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure p ℤ_[p]

The operator `ψ`: `∫ f d(ψμ) = ∫_{pℤ_p} f(p⁻¹x) dμ`.

Source: RJW §3.5.5 (TeX lines 1147–1148).

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.mahlerTransform_sigma (p : ℕ) [hp : Fact (Nat.Prime p)]
  (a : ℤ_[p]ˣ) (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.mahlerTransform p ((PadicMeasure.sigma p a) μ) =
    PowerSeries.subst (PowerSeries.binomialSeries ℤ_[p] ↑a - 1)
      (PadicMeasure.mahlerTransform p μ)

theorem PadicMeasure.mahlerTransform_sigma (p : ℕ)
  [hp : Fact (Nat.Prime p)] (a : ℤ_[p]ˣ)
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.mahlerTransform p
      ((PadicMeasure.sigma p a) μ) =
    PowerSeries.subst
      (PowerSeries.binomialSeries ℤ_[p]
          ↑a -
        1)
      (PadicMeasure.mahlerTransform p μ)

`𝓐_{σ_a μ} = 𝓐_μ((1+T)^a − 1)`: the `ℤ_p^×`-action on power series is substitution
into the binomial series.

Source: RJW §3.5.5 (TeX line 1138).

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.mahlerTransform_phi (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.mahlerTransform p ((PadicMeasure.phi p) μ) =
    PowerSeries.subst ((1 + PowerSeries.X) ^ p - 1)
      (PadicMeasure.mahlerTransform p μ)

theorem PadicMeasure.mahlerTransform_phi (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.mahlerTransform p
      ((PadicMeasure.phi p) μ) =
    PowerSeries.subst
      ((1 + PowerSeries.X) ^ p - 1)
      (PadicMeasure.mahlerTransform p μ)

`𝓐_{φ(μ)} = 𝓐_μ((1+T)^p − 1)` — Eq. (3.9) (`eq:varphi power series`).

Source: RJW TeX lines 1144–1146.

Proposition3.5.6

uses 1

Used by 2

Reverse dependency previews

Preview

Corollary 3.5.7

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

The operators of Definition 3.5.5 satisfy \psi \circ \varphi = \mathrm{id} and \varphi \circ \psi(\mu) = \Res_{p\Zp}(\mu), whence \Res_{\Zpx}(\mu) = (1 - \varphi\circ\psi)(\mu). On power series, \psi is the unique operator with \varphi\circ\psi(F)(T) = \tfrac{1}{p}\sum_{\xi \in \mu_p} F((1+T)\xi - 1).

Lean code for Proposition3.5.6●3 theorems

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.psi_phi (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.psi p ((PadicMeasure.phi p) μ) = μ

theorem PadicMeasure.psi_phi (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.psi p
      ((PadicMeasure.phi p) μ) =
    μ

`ψ ∘ φ = id`. Source: RJW TeX lines 1149–1150, first display.

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.phi_psi (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  (PadicMeasure.phi p) (PadicMeasure.psi p μ) = PadicMeasure.res p ⋯ μ

theorem PadicMeasure.phi_psi (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  (PadicMeasure.phi p)
      (PadicMeasure.psi p μ) =
    PadicMeasure.res p ⋯ μ

`φ ∘ ψ = Res_{pℤ_p}`. Source: RJW TeX lines 1149–1151, second display.

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.res_units_eq (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.res p ⋯ μ =
    μ - (PadicMeasure.phi p) (PadicMeasure.psi p μ)

theorem PadicMeasure.res_units_eq (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.res p ⋯ μ =
    μ -
      (PadicMeasure.phi p)
        (PadicMeasure.psi p μ)

Proof for Proposition 3.5.6

uses 1

Both relations are direct computations against a test function f. For \psi\circ\varphi, insert \one_{p\Zp}(px) = 1 to get \int f \cdot \psi\varphi(\mu) = \int \one_{p\Zp}(px) f(x) \cdot \varphi(\mu) = \int f(x) \cdot \mu. For \varphi\circ\psi, \int f \cdot \varphi\psi(\mu) = \int f(px) \cdot \psi(\mu) = \int_{p\Zp} f \cdot \mu = \int f \cdot \Res_{p\Zp}(\mu). Subtracting from the identity gives \Res_{\Zpx} = 1 - \varphi\psi, matching the b=0,n=1 restriction formula of Definition 3.5.4; transporting through \Am yields the stated power-series formula.

Corollary3.5.7

uses 0

Used by 2

Reverse dependency previews

Preview

Proposition 3.5.8

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

A measure \mu \in \Lam(\Zp) is supported on \Zpx iff \psi(\Am_\mu) = 0.

Lean code for Corollary3.5.7●1 theorem

theoremdefined in PadicLFunctions/Measure/Toolbox.lean

complete

theorem PadicMeasure.isSupportedOn_units_iff_psi_eq_zero (p : ℕ)
  [hp : Fact (Nat.Prime p)] (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.IsSupportedOn p ⋯ μ ↔ PadicMeasure.psi p μ = 0

theorem PadicMeasure.isSupportedOn_units_iff_psi_eq_zero
  (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  PadicMeasure.IsSupportedOn p ⋯ μ ↔
    PadicMeasure.psi p μ = 0

Proof for Corollary 3.5.7

uses 1

By Proposition 3.5.6, \mu = \Res_{\Zpx}(\mu) iff \Am_\mu = \Am_\mu - \varphi\psi(\Am_\mu), i.e. \varphi\psi(\Am_\mu) = 0. As \varphi is injective on power series this is equivalent to \psi(\Am_\mu) = 0.

Proposition3.5.8

Statement uses 2

Statement dependency previews

Preview

Definition 3.3.4

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

There is an injection \iota : \Lam(\Zpx) \hookrightarrow \Lam(\Zp) with \int_{\Zp} \phi \cdot \iota(\mu) = \int_{\Zpx} \phi|_{\Zpx} \cdot \mu, identifying \Lam(\Zpx) with the measures supported on \Zpx, i.e. those with \psi(\mu) = 0 (by Corollary 3.5.7). This is not a subalgebra: convolution on \Zpx uses the multiplicative structure, \int_{\Zpx} f(x) \cdot (\mu *_{\Zpx} \lambda) = \int_{\Zpx}\left(\int_{\Zpx} f(xy) \cdot \mu(x)\right) \cdot \lambda(y), whereas convolution on \Zp is additive (cf. Definition 3.3.4).

Lean code for Proposition3.5.8●3 declarations

defdefined in PadicLFunctions/Measure/UnitsZp.lean

complete

def PadicMeasure.iota (p : ℕ) [hp : Fact (Nat.Prime p)] :
  PadicMeasure p ℤ_[p]ˣ →ₗ[ℤ_[p]] PadicMeasure p ℤ_[p]

def PadicMeasure.iota (p : ℕ)
  [hp : Fact (Nat.Prime p)] :
  PadicMeasure p ℤ_[p]ˣ →ₗ[ℤ_[p]]
    PadicMeasure p ℤ_[p]

The embedding `ι : Λ(ℤ_p^×) → Λ(ℤ_p)`:
`∫_{ℤ_p} φ d(ιμ) = ∫_{ℤ_p^×} φ|_{ℤ_p^×} dμ`.

Source: RJW Rem. 3.33 (TeX lines 1170–1171).

theoremdefined in PadicLFunctions/Measure/UnitsZp.lean

complete

theorem PadicMeasure.iota_injective (p : ℕ) [hp : Fact (Nat.Prime p)] :
  Function.Injective ⇑(PadicMeasure.iota p)

theorem PadicMeasure.iota_injective (p : ℕ)
  [hp : Fact (Nat.Prime p)] :
  Function.Injective
    ⇑(PadicMeasure.iota p)

`ι` is injective (restriction `C(ℤ_p, ℤ_p) → C(ℤ_p^×, ℤ_p)` is surjective, via
extension by zero). Source: RJW Rem. 3.33: "we can identify `Λ(ℤ_p^×)` with its
image".

theoremdefined in PadicLFunctions/Measure/UnitsZp.lean

complete

theorem PadicMeasure.mem_range_iota_iff (p : ℕ) [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  μ ∈ Set.range ⇑(PadicMeasure.iota p) ↔ PadicMeasure.psi p μ = 0

theorem PadicMeasure.mem_range_iota_iff (p : ℕ)
  [hp : Fact (Nat.Prime p)]
  (μ : PadicMeasure p ℤ_[p]) :
  μ ∈ Set.range ⇑(PadicMeasure.iota p) ↔
    PadicMeasure.psi p μ = 0

**The image of `ι` is `ker ψ`**: `μ ∈ range ι ↔ ψ(μ) = 0`.

Source: RJW Rem. 3.33 (TeX lines 1171–1172): "By Corollary 3.32, a measure
`μ ∈ Λ(ℤ_p)` lies in `Λ(ℤ_p^×)` if and only if `ψ(μ) = 0`."

Proof for Proposition 3.5.8

uses 1

Since \Res_{\Zpx} \circ \iota is the identity on \Lam(\Zpx), the map \iota is injective and its image is exactly the measures fixed by \Res_{\Zpx}, which by Corollary 3.5.7 are those with \psi = 0. That the multiplicative and additive convolutions differ is immediate from their defining formulas, so the inclusion is only \OL-linear, not multiplicative.