mk_all and remove options

BonnAnalysis.lean

@@ -1,8 +1,15 @@
 import BonnAnalysis.ComplexInterpolation
+import BonnAnalysis.ConvergingSequences
+import BonnAnalysis.ConvolutionTendsToUniformly
+import BonnAnalysis.Distributions
+import BonnAnalysis.DistributionsExamples
+import BonnAnalysis.DistributionsOfVEndo
 import BonnAnalysis.Dual
 import BonnAnalysis.Examples
+import BonnAnalysis.Hadamard
 import BonnAnalysis.LorentzSpace
 import BonnAnalysis.Plancherel
 import BonnAnalysis.RealInterpolation
 import BonnAnalysis.StrongType
 import BonnAnalysis.Test
+import BonnAnalysis.UniformConvergenceSequences

BonnAnalysis/Dual.lean

@@ -7,12 +7,6 @@ import Mathlib.Analysis.NormedSpace.LinearIsometry
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Data.Real.Sign
 
-
-set_option linter.setOption false
-set_option trace.profiler true
-set_option profiler true
-
-
 /-! We show that the dual space of `L^p` for `1 ≤ p < ∞`.
 
 See [Stein-Shakarchi, Functional Analysis, section 1.4] -/