OAI/Analysis/BrownMeasure/Dirac.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.FiniteFactor.expLogPotential_dirac_zeroline 10 - lemma
OAI.FiniteFactor.dirac_zero_support_compactline 29
OAI/Analysis/BrownMeasure/Dirac.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.FiniteFactor.expLogPotential_dirac_zero line 10OAI.FiniteFactor.dirac_zero_support_compact line 29