Documentation Verification Report

MDifferentiable

📁 Source: Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean

Statistics

Metric	Count
Definitions `MDifferentiable`, `MDifferentiable`	2
Theorems `div_linear_zpow_differentiableOn`, `eisSummand_extension_differentiableOn`, `eisensteinSeriesSIF_mdifferentiable`, `eisensteinSeries_SIF_MDifferentiable`	4
Total	6

EisensteinSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_linear_zpow_differentiableOn` 📖	mathematical	—	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `Complex.instAdd` `Complex.instMul` `Complex.instIntCast` `setOf` `Real` `Real.instLT` `Real.instZero` `Complex.im`	—	`ne_or_eq` `DifferentiableOn.zpow` `DifferentiableOn.add_const` `DifferentiableOn.const_mul` `differentiableOn_id` `UpperHalfPlane.linear_ne_zero` `Function.comp_ne_zero_iff` `Int.cast_injective` `RCLike.charZero_rclike` `Int.cast_zero` `MulZeroClass.zero_mul` `add_zero` `differentiableOn_const`
`eisSummand_extension_differentiableOn` 📖	mathematical	—	`DifferentiableOn` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `UpperHalfPlane` `eisSummand` `OpenPartialHomeomorph.toFun'` `UpperHalfPlane.instTopologicalSpace` `UpperHalfPlane.ofComplex` `setOf` `Real` `Real.instLT` `Real.instZero` `Complex.im`	—	`DifferentiableOn.congr` `div_linear_zpow_differentiableOn` `CanLift.prf` `UpperHalfPlane.canLift` `UpperHalfPlane.comp_ofComplex`
`eisensteinSeriesSIF_mdifferentiable` 📖	mathematical	—	`MDifferentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UpperHalfPlane.instChartedSpaceComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `chartedSpaceSelf` `DFunLike.coe` `SlashInvariantForm` `Subgroup.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.instGroup` `Matrix.GeneralLinearGroup` `Real` `Real.semiring` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Matrix.SpecialLinearGroup.mapGL` `Real.commRing` `Ring.toIntAlgebra` `Real.instRing` `CongruenceSubgroup.Gamma` `SlashInvariantForm.funLike` `eisensteinSeriesSIF`	—	`DifferentiableOn.differentiableAt` `TendstoLocallyUniformlyOn.differentiableOn` `Complex.instCompleteSpace` `Filter.atTop_neBot` `Finset.isDirected_le` `eisensteinSeries_tendstoLocallyUniformlyOn` `Filter.Eventually.of_forall` `DifferentiableOn.fun_sum` `eisSummand_extension_differentiableOn` `UpperHalfPlane.isOpen_upperHalfPlaneSet` `IsOpen.mem_nhds` `UpperHalfPlane.coe_im_pos` `UpperHalfPlane.comp_ofComplex` `MDifferentiableAt.comp` `DifferentiableAt.mdifferentiableAt` `UpperHalfPlane.mdifferentiable_coe`
`eisensteinSeries_SIF_MDifferentiable` 📖	mathematical	—	`MDifferentiable` `Complex` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Complex.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.innerProductSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UpperHalfPlane.instChartedSpaceComplex` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `chartedSpaceSelf` `DFunLike.coe` `SlashInvariantForm` `Subgroup.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.instGroup` `Matrix.GeneralLinearGroup` `Real` `Real.semiring` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Matrix.SpecialLinearGroup.mapGL` `Real.commRing` `Ring.toIntAlgebra` `Real.instRing` `CongruenceSubgroup.Gamma` `SlashInvariantForm.funLike` `eisensteinSeriesSIF`	—	`eisensteinSeriesSIF_mdifferentiable`

OpenPartialHomeomorph

Definitions

Name	Category	Theorems
`MDifferentiable` 📖	MathDef	5 math math: `Diffeomorph.toPartialHomeomorph_mdifferentiable`, `Diffeomorph.toOpenPartialHomeomorph_mdifferentiable`, `mdifferentiable_chart`, `mdifferentiable_of_mem_atlas`, `Trivialization.mdifferentiable`

(root)

Definitions

Name	Category	Theorems
`MDifferentiable` 📖	MathDef	47 math math: `UpperHalfPlane.mdifferentiable_num`, `CuspFormClass.holo`, `mdifferentiable_iff_target`, `IsLocalDiffeomorph.mdifferentiable`, `mdifferentiable_const`, `ContinuousLinearMap.mdifferentiable`, `mdifferentiable_of_mdifferentiableOn_union_of_isOpen`, `mdifferentiable_add_right`, `UpperHalfPlane.mdifferentiable_inv_denom`, `CuspForm.holo'`, `mdifferentiable_mulInvariantVectorField`, `mdifferentiable_mul_left`, `mdifferentiable_fst`, `ContMDiff.mdifferentiable`, `UpperHalfPlane.mdifferentiable_denom`, `mdifferentiable_iff`, `mdifferentiable_of_subsingleton`, `ContMDiffMap.mdifferentiable'`, `mdifferentiable_of_mdifferentiableOn_iUnion_of_isOpen`, `mdifferentiable_snd`, `Diffeomorph.mdifferentiable`, `ContMDiffMap.mdifferentiable`, `ContinuousLinearEquiv.mdifferentiable`, `mdifferentiable_addInvariantVectorField`, `Differentiable.mdifferentiable`, `Bundle.mdifferentiable_proj`, `ModelWithCorners.mdifferentiable`, `mdifferentiable_prod_iff`, `mdifferentiable_jacobiTheta`, `ModularForm.holo'`, `mdifferentiableOn_univ`, `UpperHalfPlane.mdifferentiable_coe`, `ModularFormClass.holo`, `ContMDiffSection.mdifferentiable'`, `EisensteinSeries.eisensteinSeries_SIF_MDifferentiable`, `mdifferentiable_id`, `MDifferentiableOn.smul_section_of_tsupport`, `mdifferentiable_prod_module_iff`, `ContMDiffSection.mdifferentiable`, `Bundle.mdifferentiable_zeroSection`, `mdifferentiable_mul_right`, `EisensteinSeries.eisensteinSeriesSIF_mdifferentiable`, `UpperHalfPlane.mdifferentiable_denom_zpow`, `UpperHalfPlane.mdifferentiable_iff`, `mdifferentiable_add_left`, `mdifferentiable_iff_differentiable`, `UpperHalfPlane.mdifferentiable_smul`

---

← Back to Index