theorem intervalIntegral.integral_conj' {μ : MeasureTheory.Measure ℝ} {𝕜 : Type u_1} [RCLike 𝕜] {f : ℝ → 𝕜} {a b : ℝ} : ∫ (x : ℝ) in a..b, (starRingEnd 𝕜) (f x) ∂μ = (starRingEnd 𝕜) (∫ (x : ℝ) in a..b, f x ∂μ)

theorem intervalIntegrable_of_bdd {a b δ : ℝ} {g : ℝ → ℂ} (measurable_g : Measurable g) (bddg : ∀ (x : ℝ), ‖g x‖ ≤ δ) : IntervalIntegrable g MeasureTheory.volume a b

theorem IntervalIntegrable.bdd_mul {F : Type u_1} [NormedDivisionRing F] {f g : ℝ → F} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hg : IntervalIntegrable g μ a b) (hm : MeasureTheory.AEStronglyMeasurable f μ) (hfbdd : ∃ (C : ℝ), ∀ (x : ℝ), ‖f x‖ ≤ C) : IntervalIntegrable (fun (x : ℝ) => f x * g x) μ a b

theorem IntervalIntegrable.mul_bdd {F : Type u_1} [NormedField F] {f g : ℝ → F} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : IntervalIntegrable f μ a b) (hm : MeasureTheory.AEStronglyMeasurable g μ) (hgbdd : ∃ (C : ℝ), ∀ (x : ℝ), ‖g x‖ ≤ C) : IntervalIntegrable (fun (x : ℝ) => f x * g x) μ a b

theorem ConditionallyCompleteLattice.le_biSup {α : Type u_1} [ConditionallyCompleteLinearOrder α] {ι : Type u_2} {f : ι → α} {s : Set ι} {a : α} (hfs : BddAbove (f '' s)) (ha : ∃ i ∈ s, f i = a) : a ≤ ⨆ i ∈ s, f i

theorem Function.Periodic.exists_mem_Ico₀' {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x : α) : ∃ (n : ℤ), x - n • c ∈ Set.Ico 0 c ∧ f x = f (x - n • c)

theorem Function.Periodic.exists_mem_Ico' {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Periodic f c) (hc : 0 < c) (x a : α) : ∃ (n : ℤ), x - n • c ∈ Set.Ico a (a + c) ∧ f x = f (x - n • c)