theorem
intervalIntegral.integral_conj'
{μ : MeasureTheory.Measure ℝ}
{𝕜 : Type}
[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}
[NormedDivisionRing F]
{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}
[NormedField F]
{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}
{β : Type}
{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
Function.Periodic.exists_mem_Ico₀'
{α : Type}
{β : Type}
{f : α → β}
{c : α}
[LinearOrderedAddCommGroup α]
[Archimedean α]
(h : Function.Periodic f c)
(hc : 0 < c)
(x : α)
:
theorem
Function.Periodic.exists_mem_Ico'
{α : Type}
{β : Type}
{f : α → β}
{c : α}
[LinearOrderedAddCommGroup α]
[Archimedean α]
(h : Function.Periodic f c)
(hc : 0 < c)
(x : α)
(a : α)
: