theorem Asymptotics.IsBigOWith.atTop_integral_Iic_of_nonneg_of_tendsto_integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [Nonempty α] [OrderClosedTopology α] {f : α → E} {g : α → ℝ} {μ : MeasureTheory.Measure α} {c : ℝ} (hfg : IsBigOWith c Filter.atTop f g) (hf : ∀ (a : α), MeasureTheory.IntegrableOn f (Set.Iic a) μ) (hg : ∀ (a : α), MeasureTheory.IntegrableOn g (Set.Iic a) μ) (h_nonneg : ∀ᶠ (x : α) in Filter.atTop, 0 ≤ g x) (h_tendsto : Filter.Tendsto (fun (a : α) => ∫ (x : α) in Set.Iic a, g x ∂μ) Filter.atTop Filter.atTop) (c' : ℝ) : c' > c → IsBigOWith c' Filter.atTop (fun (a : α) => ∫ (x : α) in Set.Iic a, f x ∂μ) fun (a : α) => ∫ (x : α) in Set.Iic a, g x ∂μ

theorem Asymptotics.IsBigO.atTop_integral_Iic_of_nonneg_of_tendsto_integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [Nonempty α] [OrderClosedTopology α] {f : α → E} {g : α → ℝ} {μ : MeasureTheory.Measure α} (hfg : f =O[Filter.atTop] g) (hf : ∀ (a : α), MeasureTheory.IntegrableOn f (Set.Iic a) μ) (hg : ∀ (a : α), MeasureTheory.IntegrableOn g (Set.Iic a) μ) (h_nonneg : ∀ᶠ (x : α) in Filter.atTop, 0 ≤ g x) (h_tendsto : Filter.Tendsto (fun (a : α) => ∫ (x : α) in Set.Iic a, g x ∂μ) Filter.atTop Filter.atTop) : (fun (a : α) => ∫ (x : α) in Set.Iic a, f x ∂μ) =O[Filter.atTop] fun (a : α) => ∫ (x : α) in Set.Iic a, g x ∂μ

theorem Asymptotics.IsLittleO.atTop_integral_Iic_of_nonneg_of_tendsto_integral {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [Nonempty α] [OrderClosedTopology α] {f : α → E} {g : α → ℝ} {μ : MeasureTheory.Measure α} (hfg : f =o[Filter.atTop] g) (hf : ∀ (a : α), MeasureTheory.IntegrableOn f (Set.Iic a) μ) (hg : ∀ (a : α), MeasureTheory.IntegrableOn g (Set.Iic a) μ) (h_nonneg : ∀ᶠ (x : α) in Filter.atTop, 0 ≤ g x) (h_tendsto : Filter.Tendsto (fun (a : α) => ∫ (x : α) in Set.Iic a, g x ∂μ) Filter.atTop Filter.atTop) : (fun (a : α) => ∫ (x : α) in Set.Iic a, f x ∂μ) =o[Filter.atTop] fun (a : α) => ∫ (x : α) in Set.Iic a, g x ∂μ

theorem Asymptotics.IsEquivalent.atTop_integral_Iic_of_nonneg_of_tendsto_integral {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] [LinearOrder α] [Nonempty α] [OrderClosedTopology α] {g : α → ℝ} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hfg : IsEquivalent Filter.atTop f g) (hf : ∀ (a : α), MeasureTheory.IntegrableOn f (Set.Iic a) μ) (hg : ∀ (a : α), MeasureTheory.IntegrableOn g (Set.Iic a) μ) (h_nonneg : ∀ᶠ (x : α) in Filter.atTop, 0 ≤ g x) (h_tendsto : Filter.Tendsto (fun (a : α) => ∫ (x : α) in Set.Iic a, g x ∂μ) Filter.atTop Filter.atTop) : IsEquivalent Filter.atTop (fun (a : α) => ∫ (x : α) in Set.Iic a, f x ∂μ) fun (a : α) => ∫ (x : α) in Set.Iic a, g x ∂μ

theorem Asymptotics.IsEquivalent.integral_real_Ioc {f g : ℝ → ℝ} (hfg : IsEquivalent Filter.atTop f g) {a : ℝ} (hf : ∀ x ≥ a, MeasureTheory.IntegrableOn f (Set.Ioc a x) MeasureTheory.volume) (hg : ∀ x ≥ a, MeasureTheory.IntegrableOn g (Set.Ioc a x) MeasureTheory.volume) (h_tendsto : Filter.Tendsto g Filter.atTop Filter.atTop) : IsEquivalent Filter.atTop (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc a x, f t) fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioc a x, g t