Measurability of p-adics

Stream: Is there code for X?

[Yaël Dillies]

We don't have the MeasurableSpace ℚ_[p] instance in mathlib:

import Mathlib

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

#synth MeasurableSpace ℚ_[p]

[Yaël Dillies]

Does anyone have it in their project somewhere? We need it for FLT.

[Johan Commelin]

I guess you first want it for $\Z_p$... which is also missing.

[David Loeffler]

It's trivial to add, isn't it? The only natural measure-space structure on ℚ_[p] is the Borel one, so we should just add

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

instance : MeasurableSpace ℚ_[p] := borel _
instance : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace

We should probably also add BorelSpace instances

instance : BorelSpace ℚ_[p] := ⟨rfl⟩
instance : BorelSpace ℤ_[p] := Subtype.borelSpace _

[David Loeffler]

Do you need some actual properties of this measurable-space structure, or are you really just wanting an instance?

[Yaël Dillies]

Yes sure, it's trivial to add, but there is a bunch of API around the trivial definition and I want the things around it

[David Loeffler]

Then can you be more precise about what you're actually asking for?

I'm going to tag @Yakov Pechersky @María Inés de Frutos Fernández @Jou Glasheen since they have all worked on related stuff recently.

[Yakov Pechersky]

Do you even need p prime? Is Z_p as a comm ring measurable?

[Adam Topaz]

Does $\Z_p$ mean something (in mathlib I mean) when p is not prime?

[Johan Commelin]

I guess we want to know that it is a Haar measure

[Yaël Dillies]

Yes, I think I can do everything from there

[David Loeffler]

Are we talking about measurable space structure, or measure space structure (which amounts to choosing a specific measure)? If we want a measure space structure then it seems natural to just define the measure to be the Haar measure giving measure 1 to Z_p.

[David Loeffler]

Something like this should do it, I guess:

import Mathlib

open Topology TopologicalSpace MeasureTheory Measure

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

instance : MeasurableSpace ℚ_[p] := borel _
instance : BorelSpace ℚ_[p] := ⟨rfl⟩

instance : MeasurableSpace ℤ_[p] := Subtype.instMeasurableSpace
instance : BorelSpace ℤ_[p] := Subtype.borelSpace _

lemma PadicInt.isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
  refine IsOpen.isOpenEmbedding_subtypeVal (?_ : IsOpen {y : ℚ_[p] | ‖y‖ ≤ 1})
  simpa only [Metric.closedBall, dist_eq_norm_sub, sub_zero] using
    IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero

lemma PadicInt.isMeasurableEmbedding_coe : MeasurableEmbedding ((↑) : ℤ_[p] → ℚ_[p]) := by
  convert PadicInt.isOpenEmbedding_coe.measurableEmbedding
  exact inferInstanceAs (BorelSpace ℤ_[p])

noncomputable instance : MeasureSpace ℤ_[p] := ⟨addHaarMeasure ⊤⟩

instance : IsAddHaarMeasure (volume : Measure ℤ_[p]) := isAddHaarMeasure_addHaarMeasure _

lemma PadicInt.volume_univ : volume (Set.univ : Set ℤ_[p]) = 1 := addHaarMeasure_self

-- should we more generally make a map from `CompactOpens` to `PositiveCompacts`?
private def Padic.unitBall_positiveCompact : PositiveCompacts ℚ_[p] where
  carrier := {y | ‖y‖ ≤ 1}
  isCompact' := by simpa only [Metric.closedBall, dist_zero_right] using
    isCompact_closedBall (0 : ℚ_[p]) 1
  interior_nonempty' := by
    rw [IsOpen.interior_eq]
    · exact ⟨0, by simp⟩
    · simpa only [Metric.closedBall, dist_zero_right] using
        IsUltrametricDist.isOpen_closedBall (0 : ℚ_[p]) one_ne_zero

noncomputable instance : MeasureSpace ℚ_[p] := ⟨addHaarMeasure Padic.unitBall_positiveCompact⟩

instance : IsAddHaarMeasure (volume : Measure ℚ_[p]) := isAddHaarMeasure_addHaarMeasure _

lemma Padic.volume_closedBall : volume {x : ℚ_[p] | ‖x‖ ≤ 1} = 1 := addHaarMeasure_self

[David Loeffler]

Sadly I couldn't quite find a simple proof that (volume : Measure ℤ_[p]) is the comap of (volume : Measure ℚ_[p]). Is this something you want? I feel this is a bit of a guessing-game here, since you still haven't said what kind of API you're actually looking for.

[Yaël Dillies]

Thanks David! But as stated in the first message I wasn't looking for anything specific. I was asking whether anyone had it in their project

[David Loeffler]

I was asking whether anyone had it in their project

That's kind of a hard question to answer since you are repeatedly refusing to specify what "it" might be.

[Yaël Dillies]

I know where you want to get to, David, but my question was deliberately vague so that people could broadly mention what they had in their personal projects and branches.

[Kevin Buzzard]

I don't know why Yael isn't adding the information that I asked them this afternoon whether they could prove that the "canonical" norm on Qp (saying how multiplication scales Haar measure) is the usual p-adic norm. More generally I want that the canonical norm on a the fraction field of a complete DVR with finite residue field is what it is