Documentation Verification Report

MeasurableSpacePadics

📁 Source: FLT/HaarMeasure/MeasurableSpacePadics.lean

Statistics

Metric	Count
Definitions `instMeasurableSpace`, `instMeasureSpace`, `instMeasurableSpace`, `instMeasureSpace`	4
Theorems `instBorelSpace`, `instIsAddHaarMeasure`, `volume_closedBall_one`, `instBorelSpace`, `instIsAddHaarMeasure`, `instIsFiniteMeasure`, `isMeasurableEmbedding_coe`, `isMeasurableEmbedding_coeRingHom`, `volume_coe`, `volume_coe_univ`, `volume_univ`	11
Total	15

Padic

Definitions

Name	Category	Theorems
`instMeasurableSpace` 📖	CompOp	4 math math: `PadicInt.isMeasurableEmbedding_coeRingHom`, `instBorelSpace`, `MeasureTheory.ringHaarChar_padic`, `PadicInt.isMeasurableEmbedding_coe`
`instMeasureSpace` 📖	CompOp	6 math math: `volume_closedBall_one`, `PadicInt.volume_coe_univ`, `volume_padicInt_smul`, `PadicInt.volume_coe`, `instIsAddHaarMeasure`, `volume_padic_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instBorelSpace` 📖	mathematical	—	`instMeasurableSpace`	—	—
`instIsAddHaarMeasure` 📖	mathematical	—	`instMeasureSpace`	—	`instBorelSpace`
`volume_closedBall_one` 📖	mathematical	—	`instMeasureSpace`	—	`instBorelSpace`

PadicInt

Definitions

Name	Category	Theorems
`instMeasurableSpace` 📖	CompOp	3 math math: `isMeasurableEmbedding_coeRingHom`, `instBorelSpace`, `MeasureTheory.ringHaarChar_padicInt`
`instMeasureSpace` 📖	CompOp	6 math math: `volume_padicInt_smul`, `instIsAddHaarMeasure`, `volume_coe_univ`, `volume_univ`, `volume_coe`, `instIsFiniteMeasure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instBorelSpace` 📖	mathematical	—	`instMeasurableSpace`	—	`Padic.instBorelSpace`
`instIsAddHaarMeasure` 📖	mathematical	—	`instMeasureSpace`	—	`instBorelSpace`
`instIsFiniteMeasure` 📖	mathematical	—	`instMeasureSpace`	—	`volume_univ`
`isMeasurableEmbedding_coe` 📖	mathematical	—	`Padic.instMeasurableSpace`	—	`Padic.instBorelSpace`
`isMeasurableEmbedding_coeRingHom` 📖	mathematical	—	`instMeasurableSpace` `Padic.instMeasurableSpace`	—	`isMeasurableEmbedding_coe` `coe_coeRingHom`
`volume_coe` 📖	mathematical	—	`Padic.instMeasureSpace` `instMeasureSpace`	—	`volume_coe_univ` `coe_coeRingHom` `isMeasurableEmbedding_coeRingHom` `instBorelSpace` `Padic.instBorelSpace` `Padic.instIsAddHaarMeasure` `instIsAddHaarMeasure` `volume_univ`
`volume_coe_univ` 📖	mathematical	—	`Padic.instMeasureSpace` `instMeasureSpace`	—	`volume_univ` `Padic.volume_closedBall_one`
`volume_univ` 📖	mathematical	—	`instMeasureSpace`	—	`instBorelSpace`

---

← Back to Index