Documentation Verification Report

ModularCharacter

📁 Source: Mathlib/MeasureTheory/Group/ModularCharacter.lean

Statistics

Metric	Count
Definitions `addModularCharacterFun`, `modularCharacter`, `modularCharacterFun`	3
Theorems `addModularCharacterFun_eq_addHaarScalarFactor`, `addModularCharacterFun_map_add`, `addModularCharacterFun_map_zero`, `addModularCharacterFun_pos`, `map_right_add_eq_addModularCharacterFun_vadd`, `map_right_mul_eq_modularCharacterFun_smul`, `modularCharacterFun_eq_haarScalarFactor`, `modularCharacterFun_map_mul`, `modularCharacterFun_map_one`, `modularCharacterFun_pos`	10
Total	13

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`addModularCharacterFun` 📖	CompOp	5 math math: `addModularCharacterFun_eq_addHaarScalarFactor`, `addModularCharacterFun_map_zero`, `addModularCharacterFun_map_add`, `addModularCharacterFun_pos`, `map_right_add_eq_addModularCharacterFun_vadd`
`modularCharacter` 📖	CompOp	—
`modularCharacterFun` 📖	CompOp	5 math math: `modularCharacterFun_map_mul`, `map_right_mul_eq_modularCharacterFun_smul`, `modularCharacterFun_map_one`, `modularCharacterFun_pos`, `modularCharacterFun_eq_haarScalarFactor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addModularCharacterFun_eq_addHaarScalarFactor` 📖	mathematical	—	`addModularCharacterFun` `addHaarScalarFactor` `map` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_map_add_right` `MeasureTheory.isMulLeftInvariant_map_add_right` `AddMonoid.toAddSemigroup` `ContinuousAdd.measurableAdd` `AddSemigroup.toAdd` `IsTopologicalAddGroup.toContinuousAdd` `IsAddHaarMeasure.toIsAddLeftInvariant`	—	`IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_map_add_right` `MeasureTheory.isMulLeftInvariant_map_add_right` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `IsAddHaarMeasure.toIsAddLeftInvariant` `exists_continuous_nonneg_pos` `IsTopologicalAddGroup.regularSpace` `ne_of_gt` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsAddHaarMeasure.toIsOpenPosMeasure` `NNReal.coe_injective` `IsScalarTower.right` `isAddHaarMeasure_addHaarMeasure` `isAddLeftInvariant_addHaarMeasure` `integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport` `Continuous.comp'` `continuous_add_right` `HasCompactSupport.comp_homeomorph` `div_self` `NNReal.coe_ne_zero` `ne_of_lt` `addHaarScalarFactor_pos_of_isAddHaarMeasure` `BorelSpace.measurable_eq` `addHaarScalarFactor_eq_integral_div` `MeasureTheory.integral_map` `AEMeasurable.add_const` `aemeasurable_id'` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `MeasureTheory.integral_smul_nnreal_measure` `mul_div_mul_comm` `one_mul`
`addModularCharacterFun_map_add` 📖	mathematical	—	`addModularCharacterFun` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`Measurable.add_const` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `isHaarMeasure_map_add_right` `isAddHaarMeasure_addHaarMeasure` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.isMulLeftInvariant_map_add_right` `isAddLeftInvariant_addHaarMeasure` `mul_comm` `IsAddHaarMeasure.toIsAddLeftInvariant` `addModularCharacterFun_eq_addHaarScalarFactor` `map_map` `comp_add_right` `addHaarScalarFactor.congr_simp` `addHaarScalarFactor_eq_mul`
`addModularCharacterFun_map_zero` 📖	mathematical	—	`addModularCharacterFun` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NNReal` `instOneNNReal`	—	`add_zero` `map_id'` `addHaarScalarFactor.congr_simp` `addHaarScalarFactor_self`
`addModularCharacterFun_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `addModularCharacterFun`	—	`isAddHaarMeasure_addHaarMeasure` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_map_add_right` `MeasureTheory.isMulLeftInvariant_map_add_right` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `IsAddHaarMeasure.toIsAddLeftInvariant` `addModularCharacterFun_eq_addHaarScalarFactor` `addHaarScalarFactor_pos_of_isAddHaarMeasure`
`map_right_add_eq_addModularCharacterFun_vadd` 📖	mathematical	—	`map` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `addModularCharacterFun`	—	`IsScalarTower.right` `IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_map_add_right` `MeasureTheory.isMulLeftInvariant_map_add_right` `ContinuousAdd.measurableAdd` `IsTopologicalAddGroup.toContinuousAdd` `IsAddHaarMeasure.toIsAddLeftInvariant` `addModularCharacterFun_eq_addHaarScalarFactor` `isAddLeftInvariant_eq_smul_of_innerRegular` `MeasureTheory.innerRegular_map_add_right`
`map_right_mul_eq_modularCharacterFun_smul` 📖	mathematical	—	`map` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `NNReal` `MeasureTheory.Measure` `instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right` `modularCharacterFun`	—	`IsScalarTower.right` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_map_mul_right` `MeasureTheory.isMulLeftInvariant_map_mul_right` `ContinuousMul.measurableMul` `IsTopologicalGroup.toContinuousMul` `IsHaarMeasure.toIsMulLeftInvariant` `modularCharacterFun_eq_haarScalarFactor` `isMulLeftInvariant_eq_smul_of_innerRegular` `MeasureTheory.innerRegular_map_mul_right`
`modularCharacterFun_eq_haarScalarFactor` 📖	mathematical	—	`modularCharacterFun` `haarScalarFactor` `map` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_map_mul_right` `MeasureTheory.isMulLeftInvariant_map_mul_right` `Monoid.toSemigroup` `ContinuousMul.measurableMul` `Semigroup.toMul` `IsTopologicalGroup.toContinuousMul` `IsHaarMeasure.toIsMulLeftInvariant`	—	`IsHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_map_mul_right` `MeasureTheory.isMulLeftInvariant_map_mul_right` `ContinuousMul.measurableMul` `IsTopologicalGroup.toContinuousMul` `IsHaarMeasure.toIsMulLeftInvariant` `exists_continuous_nonneg_pos` `IsTopologicalGroup.regularSpace` `ne_of_gt` `Continuous.integral_pos_of_hasCompactSupport_nonneg_nonzero` `BorelSpace.opensMeasurable` `IsHaarMeasure.toIsOpenPosMeasure` `NNReal.coe_injective` `IsScalarTower.right` `isHaarMeasure_haarMeasure` `isMulLeftInvariant_haarMeasure` `integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport` `Continuous.comp'` `continuous_mul_right` `HasCompactSupport.comp_homeomorph` `div_self` `NNReal.coe_ne_zero` `ne_of_lt` `haarScalarFactor_pos_of_isHaarMeasure` `BorelSpace.measurable_eq` `haarScalarFactor_eq_integral_div` `MeasureTheory.integral_map` `AEMeasurable.mul_const` `aemeasurable_id'` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `MeasureTheory.integral_smul_nnreal_measure` `mul_div_mul_comm` `one_mul`
`modularCharacterFun_map_mul` 📖	mathematical	—	`modularCharacterFun` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`Measurable.mul_const` `ContinuousMul.measurableMul` `IsTopologicalGroup.toContinuousMul` `isHaarMeasure_map_mul_right` `isHaarMeasure_haarMeasure` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `MeasureTheory.isMulLeftInvariant_map_mul_right` `isMulLeftInvariant_haarMeasure` `mul_comm` `IsHaarMeasure.toIsMulLeftInvariant` `modularCharacterFun_eq_haarScalarFactor` `map_map` `comp_mul_right` `haarScalarFactor.congr_simp`
`modularCharacterFun_map_one` 📖	mathematical	—	`modularCharacterFun` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `NNReal` `instOneNNReal`	—	`mul_one` `map_id'` `haarScalarFactor.congr_simp` `haarScalarFactor_self`
`modularCharacterFun_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `modularCharacterFun`	—	`isHaarMeasure_haarMeasure` `IsHaarMeasure.toIsFiniteMeasureOnCompacts` `isHaarMeasure_map_mul_right` `MeasureTheory.isMulLeftInvariant_map_mul_right` `ContinuousMul.measurableMul` `IsTopologicalGroup.toContinuousMul` `IsHaarMeasure.toIsMulLeftInvariant` `modularCharacterFun_eq_haarScalarFactor` `haarScalarFactor_pos_of_isHaarMeasure`

---

← Back to Index