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` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `modelWithCornersSelf` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UpperHalfPlane.instChartedSpaceComplex` `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` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `modelWithCornersSelf` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UpperHalfPlane.instChartedSpaceComplex` `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	6 math math: `Diffeomorph.toOpenPartialHomeomorph_mdifferentiable`, `mdifferentiable_chart`, `mdifferentiable_of_mem_atlas`, `MDifferentiable.trans`, `Bundle.Trivialization.Bundle.Trivialization.mdifferentiable`, `MDifferentiable.symm`

(root)

Definitions

Name	Category	Theorems
`MDifferentiable` 📖	MathDef	87 math math: `MDifferentiable.coordChangeL`, `UpperHalfPlane.mdifferentiable_num`, `MDifferentiable.add`, `CuspFormClass.holo`, `mdifferentiable_iff_target`, `IsLocalDiffeomorph.mdifferentiable`, `MDifferentiable.sum`, `mdifferentiable_const`, `ContinuousLinearMap.mdifferentiable`, `MDifferentiable.smul`, `MDifferentiable.clm_postcomp`, `MDifferentiable.cle_arrowCongr`, `MDifferentiable.clm_bundle_apply₂`, `mdifferentiable_of_mdifferentiableOn_union_of_isOpen`, `mdifferentiable_add_right`, `MDifferentiable.const_smul`, `UpperHalfPlane.mdifferentiable_inv_denom`, `MDifferentiable.prodMap`, `MDifferentiable.clm_bundle_apply`, `MDifferentiable.comp`, `CuspForm.holo'`, `MDifferentiable.fst`, `mdifferentiable_mulInvariantVectorField`, `mdifferentiable_mul_left`, `mdifferentiable_fst`, `MDifferentiable.coordChange`, `MDifferentiable.mpullback_vectorField`, `mdifferentiable_smul_const_section`, `ContMDiff.mdifferentiable`, `UpperHalfPlane.mdifferentiable_denom`, `mdifferentiable_iff`, `MDifferentiable.prodMk_space`, `MDifferentiable.slash`, `mdifferentiable_of_subsingleton`, `MDifferentiable.sum_section`, `ContMDiffMap.mdifferentiable'`, `MDifferentiable.sum_section_of_locallyFinite`, `MDifferentiable.clm_prodMap`, `mdifferentiable_of_mdifferentiableOn_iUnion_of_isOpen`, `MDifferentiable.mul`, `mdifferentiable_snd`, `Diffeomorph.mdifferentiable`, `MDifferentiable.prodMk`, `ContMDiffMap.mdifferentiable`, `Differentiable.comp_mdifferentiable`, `ContinuousLinearEquiv.mdifferentiable`, `mdifferentiable_addInvariantVectorField`, `Differentiable.mdifferentiable`, `MDifferentiable.sub`, `Bundle.mdifferentiable_proj`, `ModelWithCorners.mdifferentiable`, `Derivative.normalizedDerivOfComplex_mdifferentiable`, `mdifferentiable_prod_iff`, `mdifferentiable_jacobiTheta`, `mdifferentiable_sub_section`, `ModularForm.holo'`, `mdifferentiable_neg_section`, `mdifferentiableOn_univ`, `MDifferentiable.finsum_section_of_locallyFinite`, `UpperHalfPlane.mdifferentiable_coe`, `MDifferentiable.snd`, `ModularFormClass.holo`, `mdifferentiable_add_section`, `MDifferentiable.clm_apply`, `MDifferentiable.clm_precomp`, `MDifferentiable.clm_comp`, `ContMDiffSection.mdifferentiable'`, `EisensteinSeries.eisensteinSeries_SIF_MDifferentiable`, `mdifferentiable_id`, `MDifferentiableOn.smul_section_of_tsupport`, `mdifferentiable_prod_module_iff`, `ContMDiffSection.mdifferentiable`, `MDifferentiable.neg`, `mdifferentiable_smul_section`, `Bundle.mdifferentiable_zeroSection`, `mdifferentiable_mul_right`, `E2_mdifferentiable`, `EisensteinSeries.eisensteinSeriesSIF_mdifferentiable`, `UpperHalfPlane.mdifferentiable_denom_zpow`, `Derivative.serreDerivative_mdifferentiable`, `MDifferentiable.prod`, `UpperHalfPlane.mdifferentiable_iff`, `mdifferentiable_add_left`, `mdifferentiable_iff_differentiable`, `MDifferentiable.inner_bundle`, `MDifferentiable.pow`, `UpperHalfPlane.mdifferentiable_smul`

---

← Back to Index