fix root

leanprover-community · Feb 4, 2024 · d6a651f · d6a651f
1 parent 6ff7862
commit d6a651f
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/Mathlib/MeasureTheory/Integral/Asymptotics.lean b/Mathlib/MeasureTheory/Integral/Asymptotics.lean
@@ -15,12 +15,12 @@ noncomputable section
 
 open Asymptotics MeasureTheory Set Filter
 
-variable {α E : Type*} [MeasurableSpace α] {f g : α → E} {a b : α} {μ : Measure α} {l : Filter α}
+variable {α E : Type*} [MeasurableSpace α] [NormedDivisionRing E] [NormedSpace ℝ E]
+ [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
+ {f g : α → E} {a b : α} {μ : Measure α} {l : Filter α}
 
-theorem __root__.Asymptotics.IsBigO.integrableAtFilter [NormedDivisionRing E] [NormedSpace ℝ E]
-    [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
-    (hfm : Measurable f) (hgm : Measurable g) (hf : f =O[l] g) (hg : IntegrableAtFilter g l μ) :
-    IntegrableAtFilter f l μ := by
+theorem _root_.Asymptotics.IsBigO.integrableAtFilter (hfm : Measurable f) (hgm : Measurable g)
+    (hf : f =O[l] g) (hg : IntegrableAtFilter g l μ) : IntegrableAtFilter f l μ := by
   obtain ⟨C, hC⟩ := hf.bound
   obtain ⟨C', hC'⟩ := exists_norm_eq E <| le_max_right C 0
   obtain ⟨s, hsl, hs⟩ := hC.exists_mem