Documentation Verification Report

Measure

📁 Source: Mathlib/Analysis/Complex/UpperHalfPlane/Measure.lean

Statistics

Metric	Count
Definitions `instMeasurableSpace`, `instMeasureSpace`, `instMeasureSpaceComplex`	3
Theorems `instBorelSpace`, `instIsFiniteMeasureOnCompactsComapComplexCoeVolume`, `instIsFiniteMeasureOnCompactsVolume`, `instIsLocallyFiniteMeasureComapComplexCoeVolume`, `instIsLocallyFiniteMeasureVolume`, `instSFiniteComapComplexCoeVolume`, `instSFiniteVolume`, `instSMulInvariantMeasureGeneralLinearGroupFinOfNatNatRealVolume`, `instSigmaFiniteComapComplexCoeVolume`, `instSigmaFiniteVolume`, `measurableEmbedding_coe`, `measurable_coe`, `volume_def`, `volume_eq_lintegral`, `instFiniteDimensionalRealComplex`	15
Total	18

UpperHalfPlane

Definitions

Name	Category	Theorems
`instMeasurableSpace` 📖	CompOp	8 math math: `instSFiniteComapComplexCoeVolume`, `instSigmaFiniteComapComplexCoeVolume`, `volume_def`, `instIsFiniteMeasureOnCompactsComapComplexCoeVolume`, `instBorelSpace`, `measurableEmbedding_coe`, `instIsLocallyFiniteMeasureComapComplexCoeVolume`, `measurable_coe`
`instMeasureSpace` 📖	CompOp	7 math math: `instSMulInvariantMeasureGeneralLinearGroupFinOfNatNatRealVolume`, `volume_def`, `volume_eq_lintegral`, `instSFiniteVolume`, `instIsLocallyFiniteMeasureVolume`, `instSigmaFiniteVolume`, `instIsFiniteMeasureOnCompactsVolume`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instBorelSpace` 📖	mathematical	—	`BorelSpace` `UpperHalfPlane` `instTopologicalSpace` `instMeasurableSpace`	—	`borel_comap`
`instIsFiniteMeasureOnCompactsComapComplexCoeVolume` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasureOnCompacts` `UpperHalfPlane` `instMeasurableSpace` `instTopologicalSpace` `MeasureTheory.Measure.comap` `Complex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpaceComplex` `coe` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.IsFiniteMeasureOnCompacts.comap'` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `instIsAddHaarMeasureVolume` `Complex.instFiniteDimensionalReal` `Complex.borelSpace` `continuous_coe` `measurableEmbedding_coe`
`instIsFiniteMeasureOnCompactsVolume` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasureOnCompacts` `UpperHalfPlane` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpace` `instTopologicalSpace` `MeasureTheory.MeasureSpace.volume`	—	`isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure` `instIsLocallyFiniteMeasureVolume`
`instIsLocallyFiniteMeasureComapComplexCoeVolume` 📖	mathematical	—	`MeasureTheory.IsLocallyFiniteMeasure` `UpperHalfPlane` `instMeasurableSpace` `instTopologicalSpace` `MeasureTheory.Measure.comap` `Complex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpaceComplex` `coe` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.isLocallyFiniteMeasure_of_isFiniteMeasureOnCompacts` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `instLocallyCompactSpace` `instIsFiniteMeasureOnCompactsComapComplexCoeVolume`
`instIsLocallyFiniteMeasureVolume` 📖	mathematical	—	`MeasureTheory.IsLocallyFiniteMeasure` `UpperHalfPlane` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpace` `instTopologicalSpace` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.IsLocallyFiniteMeasure.withDensity_coe` `BorelSpace.opensMeasurable` `instBorelSpace` `instIsLocallyFiniteMeasureComapComplexCoeVolume` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `NNReal.instIsTopologicalSemiring` `Continuous.div₀` `NNReal.instContinuousInv₀` `continuous_const` `continuous_im` `NNReal.ne_iff` `im_ne_zero`
`instSFiniteComapComplexCoeVolume` 📖	mathematical	—	`MeasureTheory.SFinite` `UpperHalfPlane` `instMeasurableSpace` `MeasureTheory.Measure.comap` `Complex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpaceComplex` `coe` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.instSFiniteOfSigmaFinite` `instSigmaFiniteComapComplexCoeVolume`
`instSFiniteVolume` 📖	mathematical	—	`MeasureTheory.SFinite` `UpperHalfPlane` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpace` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.instSFiniteOfSigmaFinite` `instSigmaFiniteVolume`
`instSMulInvariantMeasureGeneralLinearGroupFinOfNatNatRealVolume` 📖	mathematical	—	`MeasureTheory.SMulInvariantMeasure` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `MulAction.toSemigroupAction` `glAction` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpace` `MeasureTheory.MeasureSpace.volume`	—	`List.TFAE.out` `MeasureTheory.smulInvariantMeasure_tfae` `ContinuousConstSMul.toMeasurableConstSMul` `instBorelSpace` `instContinuousGLSMul` `volume_eq_lintegral` `Set.image_smul` `Set.image_image` `Set.InjOn.image_of_comp` `ofComplex_apply` `MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul` `instFiniteDimensionalRealComplex` `Complex.borelSpace` `instIsAddHaarMeasureVolume` `Complex.instFiniteDimensionalReal` `MeasurableEmbedding.measurableSet_image` `measurableEmbedding_coe` `Set.forall_mem_image` `HasFDerivAt.hasFDerivWithinAt` `HasStrictFDerivAt.hasFDerivAt` `hasStrictFDerivAt_smul` `one_div` `inv_pow` `Set.image_congr` `MeasureTheory.setLIntegral_congr_fun` `Ne.lt_or_gt` `Matrix.GeneralLinearGroup.det_ne_zero` `Real.instNontrivial` `sign_neg` `SignType.coe_neg` `nnnorm_neg` `nnnorm_one` `NormedDivisionRing.to_normOneClass` `sign_pos` `denom_ne_zero` `Nat.cast_one` `NNReal.eq` `sq_abs` `det_smulFDeriv` `nnnorm_div` `nnnorm_mul` `NormedDivisionRing.toNormMulClass` `nnnorm_pow` `one_mul` `nnnorm_norm` `im_smul_eq_div_normSq` `Complex.normSq_eq_norm_sq` `Real.nnnorm_abs` `inv_div` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `abs_pos_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `im_pos` `Mathlib.Meta.Positivity.abs_pos_of_ne_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `norm_pos_iff` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁`
`instSigmaFiniteComapComplexCoeVolume` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `UpperHalfPlane` `instMeasurableSpace` `MeasureTheory.Measure.comap` `Complex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpaceComplex` `coe` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.sigmaFinite_of_locallyFinite` `instSecondCountableTopology` `instIsLocallyFiniteMeasureComapComplexCoeVolume`
`instSigmaFiniteVolume` 📖	mathematical	—	`MeasureTheory.SigmaFinite` `UpperHalfPlane` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpace` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.sigmaFinite_of_locallyFinite` `instSecondCountableTopology` `instIsLocallyFiniteMeasureVolume`
`measurableEmbedding_coe` 📖	mathematical	—	`MeasurableEmbedding` `UpperHalfPlane` `Complex` `instMeasurableSpace` `Complex.measurableSpace` `coe`	—	`Topology.IsOpenEmbedding.measurableEmbedding` `instBorelSpace` `Complex.borelSpace` `isOpenEmbedding_coe`
`measurable_coe` 📖	mathematical	—	`Measurable` `UpperHalfPlane` `Complex` `instMeasurableSpace` `Complex.measurableSpace` `coe`	—	`MeasurableEmbedding.measurable` `measurableEmbedding_coe`
`volume_def` 📖	mathematical	—	`MeasureTheory.MeasureSpace.volume` `UpperHalfPlane` `instMeasureSpace` `MeasureTheory.Measure.withDensity` `instMeasurableSpace` `MeasureTheory.Measure.comap` `Complex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpaceComplex` `coe` `ENNReal.ofNNReal` `NNReal` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NNReal.instSemiring` `NNReal.instDiv` `NNReal.instOne` `Real` `Real.instLE` `Real.instZero` `im` `LT.lt.le` `Real.instPreorder` `im_pos`	—	—
`volume_eq_lintegral` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `UpperHalfPlane` `MeasureTheory.MeasureSpace.toMeasurableSpace` `instMeasureSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.MeasureSpace.volume` `MeasureTheory.lintegral` `Complex` `instMeasureSpaceComplex` `MeasureTheory.Measure.restrict` `Set.image` `coe` `ENNReal.ofNNReal` `NNReal` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NNReal.instSemiring` `NNReal.instDiv` `NNReal.instOne` `NNNorm.nnnorm` `Real` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Complex.im`	—	`measurable_coe` `MeasurableEmbedding.map_comap` `measurableEmbedding_coe` `LT.lt.le` `im_pos` `volume_def` `MeasureTheory.withDensity_apply'` `instSFiniteComapComplexCoeVolume` `Set.inter_eq_self_of_subset_left` `Set.image_subset_range` `MeasureTheory.Measure.restrict_restrict'` `MeasurableEmbedding.measurableSet_range` `MeasureTheory.MeasurePreserving.setLIntegral_comp_emb` `one_div` `inv_pow` `Real.nnnorm_of_nonneg`

(root)

Definitions

Name	Category	Theorems
`instMeasureSpaceComplex` 📖	CompOp	6 math math: `UpperHalfPlane.instSFiniteComapComplexCoeVolume`, `UpperHalfPlane.instSigmaFiniteComapComplexCoeVolume`, `UpperHalfPlane.volume_def`, `UpperHalfPlane.instIsFiniteMeasureOnCompactsComapComplexCoeVolume`, `UpperHalfPlane.volume_eq_lintegral`, `UpperHalfPlane.instIsLocallyFiniteMeasureComapComplexCoeVolume`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteDimensionalRealComplex` 📖	mathematical	—	`FiniteDimensional` `Real` `Complex` `Real.instDivisionRing` `Complex.addCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex`	—	`Complex.instFiniteDimensionalReal`

---

← Back to Index