Documentation

LeanAPAP

source

Imports

Init
LeanAPAP.FiniteField.Basic
LeanAPAP.FiniteField.HoelderLifting
LeanAPAP.Integer.HoelderLifting
LeanAPAP.Physics.AlmostPeriodicity
LeanAPAP.Physics.DRC
LeanAPAP.Physics.Unbalancing
LeanAPAP.Prereqs.Chang
LeanAPAP.Prereqs.Cut
LeanAPAP.Prereqs.DFT
LeanAPAP.Prereqs.Dissociation
LeanAPAP.Prereqs.Energy
LeanAPAP.Prereqs.Indicator
LeanAPAP.Prereqs.LpNorm
LeanAPAP.Prereqs.MarcinkiewiczZygmund
LeanAPAP.Prereqs.Misc
LeanAPAP.Prereqs.Multinomial
LeanAPAP.Prereqs.Rudin
LeanAPAP.Prereqs.SalemSpencer
LeanAPAP.Prereqs.Translate
LeanAPAP.Mathlib.Algebra.Support
LeanAPAP.Mathlib.Analysis.MeanInequalities
LeanAPAP.Mathlib.Analysis.MeanInequalitiesPow
LeanAPAP.Mathlib.GroupTheory.FiniteAbelian
LeanAPAP.Mathlib.GroupTheory.OrderOfElement
LeanAPAP.Mathlib.LinearAlgebra.FiniteDimensional
LeanAPAP.Mathlib.LinearAlgebra.Ray
LeanAPAP.Mathlib.Logic.Basic
LeanAPAP.Mathlib.Order.Disjoint
LeanAPAP.Mathlib.Tactic.Binop
LeanAPAP.Mathlib.Tactic.Positivity
LeanAPAP.Prereqs.Convolution.Basic
LeanAPAP.Prereqs.Convolution.Norm
LeanAPAP.Prereqs.Convolution.Order
LeanAPAP.Prereqs.Convolution.WithConv
LeanAPAP.Mathlib.Algebra.BigOperators.Basic
LeanAPAP.Mathlib.Algebra.BigOperators.Expect
LeanAPAP.Mathlib.Algebra.BigOperators.Order
LeanAPAP.Mathlib.Algebra.BigOperators.Pi
LeanAPAP.Mathlib.Algebra.BigOperators.Ring
LeanAPAP.Mathlib.Algebra.DirectSum.Basic
LeanAPAP.Mathlib.Algebra.Group.Basic
LeanAPAP.Mathlib.Algebra.Group.TypeTags
LeanAPAP.Mathlib.Algebra.GroupPower.Basic
LeanAPAP.Mathlib.Algebra.GroupPower.Hom
LeanAPAP.Mathlib.Algebra.GroupPower.Order
LeanAPAP.Mathlib.Algebra.Hom.Group
LeanAPAP.Mathlib.Algebra.Hom.GroupInstances
LeanAPAP.Mathlib.Algebra.Module.Basic
LeanAPAP.Mathlib.Algebra.Order.LatticeGroup
LeanAPAP.Mathlib.Algebra.Order.SMul
LeanAPAP.Mathlib.Algebra.Star.Basic
LeanAPAP.Mathlib.Algebra.Star.Order
LeanAPAP.Mathlib.Algebra.Star.Pi
LeanAPAP.Mathlib.Algebra.Star.SelfAdjoint
LeanAPAP.Mathlib.Analysis.Complex.Basic
LeanAPAP.Mathlib.Analysis.Complex.Circle
LeanAPAP.Mathlib.Analysis.InnerProductSpace.PiL2
LeanAPAP.Mathlib.Analysis.NormedSpace.PiLp
LeanAPAP.Mathlib.Analysis.NormedSpace.Ray
LeanAPAP.Mathlib.Data.Complex.Basic
LeanAPAP.Mathlib.Data.Complex.Exponential
LeanAPAP.Mathlib.Data.Finset.Basic
LeanAPAP.Mathlib.Data.Finset.Card
LeanAPAP.Mathlib.Data.Finset.Image
LeanAPAP.Mathlib.Data.Finset.NatAntidiagonal
LeanAPAP.Mathlib.Data.Finset.Pointwise
LeanAPAP.Mathlib.Data.Finset.Powerset
LeanAPAP.Mathlib.Data.Fintype.Basic
LeanAPAP.Mathlib.Data.Fintype.Card
LeanAPAP.Mathlib.Data.Fintype.Lattice
LeanAPAP.Mathlib.Data.Fintype.Pi
LeanAPAP.Mathlib.Data.FunLike.Basic
LeanAPAP.Mathlib.Data.IsROrC.Basic
LeanAPAP.Mathlib.Data.Nat.Parity
LeanAPAP.Mathlib.Data.Pi.Algebra
LeanAPAP.Mathlib.Data.Rat.Order
LeanAPAP.Mathlib.Data.Real.Basic
LeanAPAP.Mathlib.Data.Real.ENNReal
LeanAPAP.Mathlib.Data.Real.NNReal
LeanAPAP.Mathlib.Data.Real.Sqrt
LeanAPAP.Mathlib.Data.ZMod.Basic
LeanAPAP.Mathlib.GroupTheory.GroupAction.BigOperators
LeanAPAP.Mathlib.GroupTheory.Submonoid.Basic
LeanAPAP.Mathlib.GroupTheory.Submonoid.Operations
LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Finset
LeanAPAP.Mathlib.Order.Heyting.Basic
LeanAPAP.Mathlib.Order.Partition.Finpartition
LeanAPAP.Mathlib.Algebra.Hom.Equiv.Basic
LeanAPAP.Mathlib.Algebra.Order.Ring.Canonical
LeanAPAP.Mathlib.Analysis.Normed.Field.Basic
LeanAPAP.Mathlib.Analysis.Normed.Group.Basic
LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
LeanAPAP.Mathlib.Data.Nat.Cast.Field
LeanAPAP.Mathlib.Data.Nat.Choose.Multinomial
LeanAPAP.Mathlib.Data.Nat.Factorial.Basic
LeanAPAP.Mathlib.Data.Nat.Factorial.BigOperators
LeanAPAP.Mathlib.Data.Nat.Factorial.DoubleFactorial
LeanAPAP.Mathlib.Data.Nat.Order.Basic
LeanAPAP.Mathlib.NumberTheory.LegendreSymbol.AddChar.Basic
LeanAPAP.Mathlib.NumberTheory.LegendreSymbol.AddChar.Duality

Imported by