-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathLeanModularForms.lean
More file actions
49 lines (49 loc) · 3.3 KB
/
Copy pathLeanModularForms.lean
File metadata and controls
49 lines (49 loc) · 3.3 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
import LeanModularForms.Modularforms.AtImInfty
import LeanModularForms.Modularforms.DimensionFormulas
import LeanModularForms.Modularforms.ForMathlib_Cusps
import LeanModularForms.Modularforms.IsCuspForm
import LeanModularForms.Modularforms.ResToImagAxis
import LeanModularForms.Modularforms.SlashActionAuxil
import LeanModularForms.ForMathlib.ContourIntegral.CrossingLimit
import LeanModularForms.ForMathlib.ContourIntegral.PVSplit
import LeanModularForms.ForMathlib.ContourIntegral.SegmentFTC
import LeanModularForms.ForMathlib.ClassicalCPV
import LeanModularForms.ForMathlib.EllipticPoints
import LeanModularForms.ForMathlib.FDBoundaryH
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.ArcCalculus
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.CauchyPrimitive
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.Homotopy.Integrality
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.Homotopy.Invariance
import LeanModularForms.ForMathlib.SegmentFTC
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.OnCurvePV.Basic
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.PVInfrastructure.AnnulusBounds
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.PVInfrastructure.SingularAnnulus
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.PVInfrastructure.GammaAnalysis
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.PVInfrastructure.RemainderAnalysis
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.PVInfrastructure.StepBounds
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.PVInfrastructure.UniformStepBound
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.Residue
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.Residue.GeneralizedTheoremBase
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.Residue.MeasureHelpers
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.Residue.MultipointPV
import LeanModularForms.ForMathlib.GeneralizedResidueTheory.Residue.MultipointPV.DominatedConvergence
import LeanModularForms.ForMathlib.ValenceFormula.Boundary.Bounds
import LeanModularForms.ForMathlib.ValenceFormula.Boundary.Smooth
import LeanModularForms.ForMathlib.ModularInvariance
import LeanModularForms.ForMathlib.ValenceFormula.OnCurvePV.Basic
import LeanModularForms.ForMathlib.ValenceFormula.OnCurvePV.EndpointCorner
import LeanModularForms.ForMathlib.ValenceFormula.OnCurvePV.Main
import LeanModularForms.ForMathlib.ValenceFormula.PVChain.ArcContribution
import LeanModularForms.ForMathlib.ValenceFormula.PVChain.Assembly
import LeanModularForms.ForMathlib.ValenceFormula.PVChain.Assembly.ResidueSide
import LeanModularForms.ForMathlib.ValenceFormula.PVChain.Helpers
import LeanModularForms.ForMathlib.ValenceFormula.PVChain.OnCurveCapture
import LeanModularForms.ForMathlib.ValenceFormula.PVChain.ResidueSideInfra
import LeanModularForms.ForMathlib.ValenceFormula.PVChain.Seg5CuspIntegral
import LeanModularForms.ForMathlib.TrigLemmas
import LeanModularForms.ForMathlib.ValenceFormula.WindingWeights.Common
import LeanModularForms.ForMathlib.ValenceFormula.WindingWeights.I
import LeanModularForms.ForMathlib.ValenceFormula.WindingWeights.Rho
import LeanModularForms.ForMathlib.ValenceFormula.WindingWeights.RhoPlusOne
import LeanModularForms.ForMathlib.ValenceFormulaFinal
import LeanModularForms.ForMathlib.HW33Clean