16 lines
586 B
Lean4
16 lines
586 B
Lean4
import Mathlib
|
||
|
||
|
||
theorem intervalIntegrable_iff_intervalIntegrable_smul
|
||
{E : Type*} [NormedAddCommGroup E]
|
||
{a b : ℝ} {μ : MeasureTheory.Measure ℝ}
|
||
{R : Type*} [NormedAddCommGroup R] [SMulZeroClass R E] [IsBoundedSMul R E]
|
||
{f : ℝ → E} {r : R} (hr : r ≠ 0) :
|
||
IntervalIntegrable f μ a b ↔ IntervalIntegrable (r • f) μ a b := by
|
||
sorry
|
||
|
||
theorem IntervalIntegrable.abs'
|
||
{a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} (hf : Measurable f) :
|
||
IntervalIntegrable f μ a b ↔ IntervalIntegrable (fun x => |f x|) μ a b := by
|
||
sorry
|