-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathLeanAPAP.lean
82 lines (82 loc) · 3.57 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
import LeanAPAP.Extras.BSG
import LeanAPAP.FiniteField
import LeanAPAP.Integer
import LeanAPAP.Mathlib.Algebra.BigOperators.Group.Finset
import LeanAPAP.Mathlib.Algebra.Group.AddChar
import LeanAPAP.Mathlib.Algebra.Group.Basic
import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset
import LeanAPAP.Mathlib.Algebra.Order.Field.Defs
import LeanAPAP.Mathlib.Algebra.Order.Floor
import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
import LeanAPAP.Mathlib.Algebra.Order.Module.Rat
import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
import LeanAPAP.Mathlib.Algebra.Order.Ring.Cast
import LeanAPAP.Mathlib.Algebra.Order.Ring.Defs
import LeanAPAP.Mathlib.Algebra.Star.Rat
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
import LeanAPAP.Mathlib.Data.Complex.Basic
import LeanAPAP.Mathlib.Data.ENNReal.Basic
import LeanAPAP.Mathlib.Data.ENNReal.Operations
import LeanAPAP.Mathlib.Data.ENNReal.Real
import LeanAPAP.Mathlib.Data.Finset.Density
import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
import LeanAPAP.Mathlib.Data.Finset.Preimage
import LeanAPAP.Mathlib.Data.Real.ConjExponents
import LeanAPAP.Mathlib.Data.ZMod.Module
import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
import LeanAPAP.Mathlib.Order.CompleteLattice
import LeanAPAP.Mathlib.Order.Filter.Basic
import LeanAPAP.Mathlib.Order.Hom.Basic
import LeanAPAP.Mathlib.Order.LiminfLimsup
import LeanAPAP.Mathlib.Tactic.Positivity
import LeanAPAP.Physics.AlmostPeriodicity
import LeanAPAP.Physics.DRC
import LeanAPAP.Physics.Unbalancing
import LeanAPAP.Prereqs.AddChar.Basic
import LeanAPAP.Prereqs.AddChar.MeasurableSpace
import LeanAPAP.Prereqs.AddChar.PontryaginDuality
import LeanAPAP.Prereqs.Balance
import LeanAPAP.Prereqs.Bohr.Arc
import LeanAPAP.Prereqs.Bohr.Basic
import LeanAPAP.Prereqs.Bohr.Regular
import LeanAPAP.Prereqs.Chang
import LeanAPAP.Prereqs.Convolution.Compact
import LeanAPAP.Prereqs.Convolution.Discrete.Basic
import LeanAPAP.Prereqs.Convolution.Discrete.Defs
import LeanAPAP.Prereqs.Convolution.Norm
import LeanAPAP.Prereqs.Convolution.Order
import LeanAPAP.Prereqs.Convolution.ThreeAP
import LeanAPAP.Prereqs.Convolution.WithConv
import LeanAPAP.Prereqs.Energy
import LeanAPAP.Prereqs.Expect.Basic
import LeanAPAP.Prereqs.Expect.Complex
import LeanAPAP.Prereqs.Expect.MeanInequalities
import LeanAPAP.Prereqs.Expect.Order
import LeanAPAP.Prereqs.FourierTransform.Compact
import LeanAPAP.Prereqs.FourierTransform.Convolution
import LeanAPAP.Prereqs.FourierTransform.Discrete
import LeanAPAP.Prereqs.Function.Indicator.Basic
import LeanAPAP.Prereqs.Function.Indicator.Complex
import LeanAPAP.Prereqs.Function.Indicator.Defs
import LeanAPAP.Prereqs.Function.Translate
import LeanAPAP.Prereqs.Inner.Compact
import LeanAPAP.Prereqs.Inner.Discrete.Basic
import LeanAPAP.Prereqs.Inner.Discrete.Defs
import LeanAPAP.Prereqs.Inner.Function
import LeanAPAP.Prereqs.LargeSpec
import LeanAPAP.Prereqs.LpNorm.Compact
import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
import LeanAPAP.Prereqs.LpNorm.Weighted
import LeanAPAP.Prereqs.MarcinkiewiczZygmund
import LeanAPAP.Prereqs.NNLpNorm
import LeanAPAP.Prereqs.PointwiseDensity
import LeanAPAP.Prereqs.Randomisation
import LeanAPAP.Prereqs.Rudin