Documentation
LeanAPAP
Search
Google site search
return to top
source
Imports
Init
LeanAPAP.FiniteField
LeanAPAP.Integer
LeanAPAP.Extras.BSG
LeanAPAP.Physics.AlmostPeriodicity
LeanAPAP.Physics.DRC
LeanAPAP.Physics.Unbalancing
LeanAPAP.Prereqs.Chang
LeanAPAP.Prereqs.Energy
LeanAPAP.Prereqs.LargeSpec
LeanAPAP.Prereqs.MarcinkiewiczZygmund
LeanAPAP.Prereqs.NNLpNorm
LeanAPAP.Prereqs.Rudin
LeanAPAP.Mathlib.Tactic.Positivity
LeanAPAP.Prereqs.Bohr.Arc
LeanAPAP.Prereqs.Bohr.Basic
LeanAPAP.Prereqs.Bohr.Regular
LeanAPAP.Prereqs.Convolution.Compact
LeanAPAP.Prereqs.Convolution.Norm
LeanAPAP.Prereqs.Convolution.Order
LeanAPAP.Prereqs.Convolution.ThreeAP
LeanAPAP.Prereqs.FourierTransform.Compact
LeanAPAP.Prereqs.FourierTransform.Convolution
LeanAPAP.Prereqs.FourierTransform.Discrete
LeanAPAP.Prereqs.Inner.Function
LeanAPAP.Prereqs.LpNorm.Compact
LeanAPAP.Prereqs.LpNorm.Weighted
LeanAPAP.Prereqs.Convolution.Discrete.Basic
LeanAPAP.Prereqs.Convolution.Discrete.Defs
LeanAPAP.Prereqs.Function.Indicator.Basic
LeanAPAP.Prereqs.Function.Indicator.Complex
LeanAPAP.Prereqs.Function.Indicator.Defs
LeanAPAP.Prereqs.Inner.Hoelder.Compact
LeanAPAP.Prereqs.Inner.Hoelder.Discrete
LeanAPAP.Prereqs.LpNorm.Discrete.Basic
LeanAPAP.Prereqs.LpNorm.Discrete.Defs
LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Imported by