forked from YaelDillies/LeanAPAP
-
Notifications
You must be signed in to change notification settings - Fork 0
/
LeanAPAP.lean
101 lines (101 loc) · 4.44 KB
/
LeanAPAP.lean
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
import LeanAPAP.FiniteField.Basic
import LeanAPAP.FiniteField.HoelderLifting
import LeanAPAP.Integer.HoelderLifting
import LeanAPAP.Mathlib.Algebra.BigOperators.Basic
import LeanAPAP.Mathlib.Algebra.BigOperators.Expect
import LeanAPAP.Mathlib.Algebra.BigOperators.Order
import LeanAPAP.Mathlib.Algebra.BigOperators.Pi
import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
import LeanAPAP.Mathlib.Algebra.DirectSum.Basic
import LeanAPAP.Mathlib.Algebra.Group.Basic
import LeanAPAP.Mathlib.Algebra.GroupPower.Basic
import LeanAPAP.Mathlib.Algebra.GroupPower.Hom
import LeanAPAP.Mathlib.Algebra.GroupPower.Order
import LeanAPAP.Mathlib.Algebra.Group.TypeTags
import LeanAPAP.Mathlib.Algebra.Hom.Equiv.Basic
import LeanAPAP.Mathlib.Algebra.Hom.Group
import LeanAPAP.Mathlib.Algebra.Hom.GroupInstances
import LeanAPAP.Mathlib.Algebra.Module.Basic
import LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
import LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical
import LeanAPAP.Mathlib.Algebra.Order.SMul
import LeanAPAP.Mathlib.Algebra.Star.Basic
import LeanAPAP.Mathlib.Algebra.Star.Order
import LeanAPAP.Mathlib.Algebra.Star.Pi
import LeanAPAP.Mathlib.Algebra.Star.SelfAdjoint
import LeanAPAP.Mathlib.Algebra.Support
import LeanAPAP.Mathlib.Analysis.Complex.Basic
import LeanAPAP.Mathlib.Analysis.Complex.Circle
import LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
import LeanAPAP.Mathlib.Analysis.MeanInequalities
import LeanAPAP.Mathlib.Analysis.MeanInequalitiesPow
import LeanAPAP.Mathlib.Analysis.Normed.Field.Basic
import LeanAPAP.Mathlib.Analysis.Normed.Group.Basic
import LeanAPAP.Mathlib.Analysis.NormedSpace.PiLp
import LeanAPAP.Mathlib.Analysis.NormedSpace.Ray
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
import LeanAPAP.Mathlib.Data.Complex.Basic
import LeanAPAP.Mathlib.Data.Complex.Exponential
import LeanAPAP.Mathlib.Data.Finset.Basic
import LeanAPAP.Mathlib.Data.Finset.Card
import LeanAPAP.Mathlib.Data.Finset.Image
import LeanAPAP.Mathlib.Data.Finset.NatAntidiagonal
import LeanAPAP.Mathlib.Data.Finset.Pointwise
import LeanAPAP.Mathlib.Data.Finset.Powerset
import LeanAPAP.Mathlib.Data.Fintype.Basic
import LeanAPAP.Mathlib.Data.Fintype.Card
import LeanAPAP.Mathlib.Data.Fintype.Lattice
import LeanAPAP.Mathlib.Data.Fintype.Pi
import LeanAPAP.Mathlib.Data.FunLike.Basic
import LeanAPAP.Mathlib.Data.IsROrC.Basic
import LeanAPAP.Mathlib.Data.Nat.Cast.Field
import LeanAPAP.Mathlib.Data.Nat.Choose.Multinomial
import LeanAPAP.Mathlib.Data.Nat.Factorial.Basic
import LeanAPAP.Mathlib.Data.Nat.Factorial.BigOperators
import LeanAPAP.Mathlib.Data.Nat.Factorial.DoubleFactorial
import LeanAPAP.Mathlib.Data.Nat.Order.Basic
import LeanAPAP.Mathlib.Data.Nat.Parity
import LeanAPAP.Mathlib.Data.Pi.Algebra
import LeanAPAP.Mathlib.Data.Rat.Order
import LeanAPAP.Mathlib.Data.Real.Basic
import LeanAPAP.Mathlib.Data.Real.ENNReal
import LeanAPAP.Mathlib.Data.Real.NNReal
import LeanAPAP.Mathlib.Data.Real.Sqrt
import LeanAPAP.Mathlib.Data.ZMod.Basic
import LeanAPAP.Mathlib.GroupTheory.FiniteAbelian
import LeanAPAP.Mathlib.GroupTheory.GroupAction.BigOperators
import LeanAPAP.Mathlib.GroupTheory.OrderOfElement
import LeanAPAP.Mathlib.GroupTheory.Submonoid.Basic
import LeanAPAP.Mathlib.GroupTheory.Submonoid.Operations
import LeanAPAP.Mathlib.LinearAlgebra.FiniteDimensional
import LeanAPAP.Mathlib.LinearAlgebra.Ray
import LeanAPAP.Mathlib.Logic.Basic
import LeanAPAP.Mathlib.NumberTheory.LegendreSymbol.AddChar.Basic
import LeanAPAP.Mathlib.NumberTheory.LegendreSymbol.AddChar.Duality
import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Finset
import LeanAPAP.Mathlib.Order.Disjoint
import LeanAPAP.Mathlib.Order.Heyting.Basic
import LeanAPAP.Mathlib.Order.Partition.Finpartition
import LeanAPAP.Mathlib.Tactic.Binop
import LeanAPAP.Mathlib.Tactic.Positivity
import LeanAPAP.Physics.AlmostPeriodicity
import LeanAPAP.Physics.DRC
import LeanAPAP.Physics.Unbalancing
import LeanAPAP.Prereqs.Chang
import LeanAPAP.Prereqs.Convolution.Basic
import LeanAPAP.Prereqs.Convolution.Norm
import LeanAPAP.Prereqs.Convolution.Order
import LeanAPAP.Prereqs.Convolution.WithConv
import LeanAPAP.Prereqs.Cut
import LeanAPAP.Prereqs.DFT
import LeanAPAP.Prereqs.Dissociation
import LeanAPAP.Prereqs.Energy
import LeanAPAP.Prereqs.Indicator
import LeanAPAP.Prereqs.LpNorm
import LeanAPAP.Prereqs.MarcinkiewiczZygmund
import LeanAPAP.Prereqs.Misc
import LeanAPAP.Prereqs.Multinomial
import LeanAPAP.Prereqs.Rudin
import LeanAPAP.Prereqs.SalemSpencer
import LeanAPAP.Prereqs.Translate