ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>f : α × β → E<VAR>h1f : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)<GOAL>MeasureTheory.Integrable f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y => f (x, y)) ν) ∧ MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>h1f : MeasureTheory.AEStronglyMeasurable f (μ.prod ν)<GOAL>MeasureTheory.Integrable f (μ.prod ν) ↔ (∀ᵐ (y : β) ∂ν, MeasureTheory.Integrable (fun x => f (x, y)) μ) ∧ MeasureTheory.Integrable (fun y => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>∀ᵐ (y : β) ∂ν, MeasureTheory.Integrable (fun x => f (x, y)) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y => f (x, y)) ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>MeasureTheory.Integrable (fun y => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>𝕜 : Type u_7<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : β → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g ν<GOAL>MeasureTheory.Integrable (fun z => f z.1 • g z.2) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>L : Type u_7<VAR>RCLike L<VAR>f : α → L<VAR>g : β → L<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g ν<GOAL>MeasureTheory.Integrable (fun z => f z.1 * g z.2) (μ.prod ν)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>MeasureTheory.Integrable (fun x => ∫ (y : β), f (x, y) ∂ν) μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>MeasureTheory.Integrable (fun y => ∫ (x : α), f (x, y) ∂μ) ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<GOAL>∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (z : α × β), f z ∂μ.prod ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → E'<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<VAR>hg : MeasureTheory.Integrable g (μ.prod ν)<GOAL>∫ (x : α), F (∫ (y : β), f (x, y) + g (x, y) ∂ν) ∂μ = ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>E' : Type u_7<VAR>NormedAddCommGroup E'<VAR>NormedSpace ℝ E'<VAR>f g : α × β → E<VAR>F : E → E'<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<VAR>hg : MeasureTheory.Integrable g (μ.prod ν)<GOAL>∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ = ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f g : α × β → E<VAR>F : E → ℝ≥0∞<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<VAR>hg : MeasureTheory.Integrable g (μ.prod ν)<GOAL>∫⁻ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ = ∫⁻ (x : α), F (∫ (y : β), f (x, y) ∂ν - ∫ (y : β), g (x, y) ∂ν) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f g : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<VAR>hg : MeasureTheory.Integrable g (μ.prod ν)<GOAL>∫ (x : α), ∫ (y : β), f (x, y) + g (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f g : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<VAR>hg : MeasureTheory.Integrable g (μ.prod ν)<GOAL>∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ + ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f g : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<VAR>hg : MeasureTheory.Integrable g (μ.prod ν)<GOAL>∫ (x : α), ∫ (y : β), f (x, y) - g (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ - ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f g : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<VAR>hg : MeasureTheory.Integrable g (μ.prod ν)<GOAL>∫ (x : α), ∫ (y : β), (f - g) (x, y) ∂ν ∂μ = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ - ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<GOAL>Continuous fun f => ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>hf : MeasureTheory.Integrable f (μ.prod ν)<GOAL>∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α → β → E<VAR>hf : MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν)<GOAL>∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (z : α × β), f z.1 z.2 ∂μ.prod ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α → β → E<VAR>hf : MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν)<GOAL>∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (z : β × α), f z.2 z.1 ∂ν.prod μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α → β → E<VAR>hf : MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν)<GOAL>∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α × β → E<VAR>s : Set α<VAR>t : Set β<VAR>hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.prod ν)<GOAL>∫ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>𝕜 : Type u_8<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : β → E<GOAL>∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>L : Type u_8<VAR>RCLike L<VAR>f : α → L<VAR>g : β → L<GOAL>∫ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) * ∫ (y : β), g y ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>MeasureTheory.SFinite ν<VAR>MeasureTheory.SFinite μ<VAR>L : Type u_8<VAR>RCLike L<VAR>f : α → L<VAR>g : β → L<VAR>s : Set α<VAR>t : Set β<GOAL>∫ (z : α × β) in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ (x : α) in s, f x ∂μ) * ∫ (y : β) in t, g y ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : β → E<GOAL>∫ (z : α × β), f z.2 ∂μ.prod ν = (μ Set.univ).toReal • ∫ (y : β), f y ∂ν
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>MeasurableSpace β<VAR>μ : MeasureTheory.Measure α<VAR>ν : MeasureTheory.Measure β<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SFinite ν<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : α → E<GOAL>∫ (z : α × β), f z.1 ∂μ.prod ν = (ν Set.univ).toReal • ∫ (x : α), f x ∂μ
<VAR>E : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>X : Type u_8<VAR>Y : Type u_9<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>MeasurableSpace X<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace X<VAR>OpensMeasurableSpace Y<VAR>f : X → Y → E<VAR>hf : Continuous (Function.uncurry f)<VAR>h'f : HasCompactSupport (Function.uncurry f)<VAR>μ : MeasureTheory.Measure X<VAR>ν : MeasureTheory.Measure Y<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>MeasureTheory.IsFiniteMeasureOnCompacts ν<GOAL>∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<GOAL>IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Ι a b) μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : IntervalIntegrable f μ a b<GOAL>MeasureTheory.IntegrableOn f (Ι a b) μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hab : a ≤ b<GOAL>IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<GOAL>IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f [[a, b]] μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<GOAL>IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Icc a b) μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<VAR>hab : a ≤ b<GOAL>IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ico a b) μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.NoAtoms μ<VAR>hab : a ≤ b<GOAL>IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>IntervalIntegrable f μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : MeasureTheory.IntegrableOn f [[a, b]] μ<GOAL>IntervalIntegrable f μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>c : E<GOAL>IntervalIntegrable (fun x => c) μ a b ↔ c = 0 ∨ μ (Ι a b) < ⊤
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>c : E<GOAL>IntervalIntegrable (fun x => c) μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : IntervalIntegrable f μ a b<GOAL>IntervalIntegrable f μ b a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a : ℝ<VAR>μ : MeasureTheory.Measure ℝ<GOAL>IntervalIntegrable f μ a a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a b c : ℝ<VAR>hab : IntervalIntegrable f μ a b<VAR>hbc : IntervalIntegrable f μ b c<GOAL>IntervalIntegrable f μ a c
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a : ℕ → ℝ<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hint : ∀ k ∈ Set.Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))<GOAL>IntervalIntegrable f μ (a m) (a n)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a : ℕ → ℝ<VAR>n : ℕ<VAR>hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))<GOAL>IntervalIntegrable f μ (a 0) (a n)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : IntervalIntegrable f μ a b<GOAL>IntervalIntegrable (-f) μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : IntervalIntegrable f μ a b<GOAL>IntervalIntegrable (fun x => ‖f x‖) μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>μ : MeasureTheory.Measure ℝ<VAR>a b : ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Ι a b))<GOAL>IntervalIntegrable (fun t => ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → ℝ<VAR>h : IntervalIntegrable f μ a b<GOAL>IntervalIntegrable (fun x => |f x|) μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b c d : ℝ<VAR>μ ν : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f ν a b<VAR>h1 : [[c, d]] ⊆ [[a, b]]<VAR>h2 : μ ≤ ν<GOAL>IntervalIntegrable f μ c d
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ ν : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f ν a b<VAR>h : μ ≤ ν<GOAL>IntervalIntegrable f μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b c d : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>h : [[c, d]] ⊆ [[a, b]]<GOAL>IntervalIntegrable f μ c d
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b c d : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>h : Ι c d ≤ᵐ[μ] Ι a b<GOAL>IntervalIntegrable f μ c d
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b c d : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>hsub : Ι c d ⊆ Ι a b<GOAL>IntervalIntegrable f μ c d
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>NormedAddCommGroup F<VAR>g : ℝ → F<VAR>hf : IntervalIntegrable f μ a b<VAR>hgm : MeasureTheory.AEStronglyMeasurable g (μ.restrict (Ι a b))<VAR>hle : (fun x => ‖g x‖) ≤ᵐ[μ.restrict (Ι a b)] fun x => ‖f x‖<GOAL>IntervalIntegrable g μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>g : ℝ → ℝ<VAR>hg : IntervalIntegrable g μ a b<VAR>hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Ι a b))<VAR>hle : (fun x => ‖f x‖) ≤ᵐ[μ.restrict (Ι a b)] g<GOAL>IntervalIntegrable f μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : IntervalIntegrable f μ a b<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b))
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : IntervalIntegrable f μ a b<GOAL>MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc b a))
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>h : IntervalIntegrable f μ a b<VAR>r : 𝕜<GOAL>IntervalIntegrable (r • f) μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<GOAL>IntervalIntegrable (fun x => f x + g x) μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<GOAL>IntervalIntegrable (fun x => f x - g x) μ a b
<VAR>ι : Type u_1<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>s : Finset ι<VAR>f : ι → ℝ → E<VAR>h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b<GOAL>IntervalIntegrable (∑ i ∈ s, f i) μ a b
<VAR>A : Type u_5<VAR>NormedRing A<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f g : ℝ → A<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : ContinuousOn g [[a, b]]<GOAL>IntervalIntegrable (fun x => f x * g x) μ a b
<VAR>A : Type u_5<VAR>NormedRing A<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f g : ℝ → A<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : ContinuousOn g [[a, b]]<GOAL>IntervalIntegrable (fun x => g x * f x) μ a b
<VAR>A : Type u_5<VAR>NormedRing A<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → A<VAR>hf : IntervalIntegrable f μ a b<VAR>c : A<GOAL>IntervalIntegrable (fun x => c * f x) μ a b
<VAR>A : Type u_5<VAR>NormedRing A<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>f : ℝ → A<VAR>hf : IntervalIntegrable f μ a b<VAR>c : A<GOAL>IntervalIntegrable (fun x => f x * c) μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>𝕜 : Type u_6<VAR>f : ℝ → 𝕜<VAR>NormedField 𝕜<VAR>h : IntervalIntegrable f μ a b<VAR>c : 𝕜<GOAL>IntervalIntegrable (fun x => f x / c) μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (c * x)) MeasureTheory.volume (a / c) (b / c)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b c : ℝ<VAR>hc : c ≠ 0<GOAL>IntervalIntegrable (fun x => f (c * x)) MeasureTheory.volume (a / c) (b / c) ↔ IntervalIntegrable f MeasureTheory.volume a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (x * c)) MeasureTheory.volume (a / c) (b / c)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (x + c)) MeasureTheory.volume (a - c) (b - c)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (c + x)) MeasureTheory.volume (a - c) (b - c)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (x - c)) MeasureTheory.volume (a + c) (b + c)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<GOAL>IntervalIntegrable f MeasureTheory.volume a b ↔ IntervalIntegrable (fun x => f (-x)) MeasureTheory.volume (-a) (-b)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => f (c - x)) MeasureTheory.volume (c - a) (c - b)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>u : ℝ → E<VAR>a b : ℝ<VAR>hu : ContinuousOn u [[a, b]]<GOAL>IntervalIntegrable u μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>u : ℝ → E<VAR>a b : ℝ<VAR>h : a ≤ b<VAR>hu : ContinuousOn u (Set.Icc a b)<GOAL>IntervalIntegrable u μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>u : ℝ → E<VAR>hu : Continuous u<VAR>a b : ℝ<GOAL>IntervalIntegrable u μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>u : ℝ → E<VAR>a b : ℝ<VAR>hu : MonotoneOn u [[a, b]]<GOAL>IntervalIntegrable u μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>u : ℝ → E<VAR>a b : ℝ<VAR>hu : AntitoneOn u [[a, b]]<GOAL>IntervalIntegrable u μ a b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>ConditionallyCompleteLinearOrder E<VAR>OrderTopology E<VAR>SecondCountableTopology E<VAR>u : ℝ → E<VAR>a b : ℝ<VAR>hu : Monotone u<GOAL>IntervalIntegrable u μ a b