theorem
intervalIntegrable_of_bdd
{a b δ : ℝ}
{g : ℝ → ℂ}
(measurable_g : Measurable g)
(bddg : ∀ (x : ℝ), ‖g x‖ ≤ δ)
:
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
IntegrableOn.sub
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[NormedAddCommGroup β]
{s : Set α}
{f g : α → β}
(hf : MeasureTheory.IntegrableOn f s μ)
(hg : MeasureTheory.IntegrableOn g s μ)
:
MeasureTheory.IntegrableOn (f - g) s μ
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)
: