ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace δ<VAR>NormedAddCommGroup β<VAR>f : α ≃ᵐ δ<VAR>g : δ → β<GOAL>MeasureTheory.Integrable g (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.Integrable (g ∘ ⇑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace δ<VAR>NormedAddCommGroup β<VAR>ν : MeasureTheory.Measure δ<VAR>g : δ → β<VAR>f : α → δ<VAR>hf : MeasureTheory.MeasurePreserving f μ ν<VAR>hg : MeasureTheory.AEStronglyMeasurable g ν<GOAL>MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace δ<VAR>NormedAddCommGroup β<VAR>f : α → δ<VAR>ν : MeasureTheory.Measure δ<VAR>h₁ : MeasureTheory.MeasurePreserving f μ ν<VAR>h₂ : MeasurableEmbedding f<VAR>g : δ → β<GOAL>MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>∫⁻ (a : α), edist (f a) (g a) ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<GOAL>MeasureTheory.Integrable (fun x => 0) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.HasFiniteIntegral (f + g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable (f + g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → α → β<VAR>hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ<GOAL>MeasureTheory.Integrable (∑ i ∈ s, f i) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → α → β<VAR>hf : ∀ i ∈ s, MeasureTheory.Integrable (f i) μ<GOAL>MeasureTheory.Integrable (fun a => ∑ i ∈ s, f i a) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (-f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>MeasureTheory.Integrable (-f) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (g + f) μ ↔ MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>h_meas : MeasureTheory.AEStronglyMeasurable f μ<VAR>hf : 0 ≤ᵐ[μ] f<VAR>hg : 0 ≤ᵐ[μ] g<VAR>h_int : MeasureTheory.Integrable (f + g) μ<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>h_meas : MeasureTheory.AEStronglyMeasurable f μ<VAR>hf : 0 ≤ᵐ[μ] f<VAR>hg : 0 ≤ᵐ[μ] g<VAR>h_int : MeasureTheory.Integrable (f + g) μ<GOAL>MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>h_meas : MeasureTheory.AEStronglyMeasurable f μ<VAR>hf : 0 ≤ᵐ[μ] f<VAR>hg : 0 ≤ᵐ[μ] g<GOAL>MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ<VAR>h_meas : MeasureTheory.AEStronglyMeasurable f μ<VAR>hf : f ≤ᵐ[μ] 0<VAR>hg : g ≤ᵐ[μ] 0<GOAL>MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable f μ ∧ MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → β<VAR>c : β<GOAL>MeasureTheory.Integrable (fun x => f x + c) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → β<VAR>c : β<GOAL>MeasureTheory.Integrable (fun x => c + f x) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable (f - g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun a => ‖f a‖) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>NormedLatticeAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable (f ⊓ g) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>NormedLatticeAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable (f ⊔ g) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>NormedLatticeAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun a => |f a|) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>F : Type u_5<VAR>NormedDivisionRing F<VAR>f g : α → F<VAR>hint : MeasureTheory.Integrable g μ<VAR>hm : MeasureTheory.AEStronglyMeasurable f μ<VAR>hfbdd : ∃ C, ∀ (x : α), ‖f x‖ ≤ C<GOAL>MeasureTheory.Integrable (fun x => f x * g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 β<VAR>f : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : α → 𝕜<VAR>g_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<GOAL>MeasureTheory.Integrable (fun x => g x • f x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<VAR>g : α → β<VAR>g_aestronglyMeasurable : MeasureTheory.AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<GOAL>MeasureTheory.Integrable (fun x => f x • g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.Integrable (fun a => ‖f a‖) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f₀ f₁ : α → β<VAR>g : α → ℝ<VAR>hf₁_m : MeasureTheory.AEStronglyMeasurable f₁ μ<VAR>hf₀_i : MeasureTheory.Integrable f₀ μ<VAR>hg_i : MeasureTheory.Integrable g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a<GOAL>MeasureTheory.Integrable f₁ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>NormedAddCommGroup γ<VAR>f : α → β<VAR>g : α → γ<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.Integrable (fun x => (f x, g x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>q : ℝ≥0∞<VAR>hq1 : 1 ≤ q<VAR>f : α → β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hfq : MeasureTheory.Memℒp f q μ<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>μ {x | ε ≤ ‖f x‖} < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>μ {x | ε < ‖f x‖} < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<GOAL>μ {a | ε ≤ f a} < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>c : ℝ<VAR>c_neg : c < 0<GOAL>μ {a | f a ≤ c} < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<GOAL>μ {a | ε < f a} < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<VAR>c : ℝ<VAR>c_neg : c < 0<GOAL>μ {a | f a < c} < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>NormedAddCommGroup γ<VAR>K K' : ℝ≥0<VAR>f : α → β<VAR>g : β → γ<VAR>hg : LipschitzWith K g<VAR>hg' : AntilipschitzWith K' g<VAR>g0 : g 0 = 0<GOAL>MeasureTheory.Integrable (g ∘ f) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => ↑(f x).toNNReal) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>(fun x => ENNReal.ofReal (f x).toReal) =ᵐ[μ] f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>(fun x => ↑(f x).toNNReal) =ᵐ[μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>MeasurableSingletonClass α<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral f MeasureTheory.Measure.count ↔ Summable fun x => ‖f x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>MeasurableSingletonClass α<VAR>f : α → β<GOAL>MeasureTheory.Integrable f MeasureTheory.Measure.count ↔ Summable fun x => ‖f x‖
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>g : α → E<GOAL>MeasureTheory.Integrable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.Integrable (fun x => ↑(f x) • g x) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>g : α → E<GOAL>MeasureTheory.Integrable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.Integrable (fun x => f x • g x) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → E<GOAL>MeasureTheory.Integrable g (μ.withDensity f) ↔ MeasureTheory.Integrable (fun x => (f x).toReal • g x) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → E<GOAL>MeasureTheory.Integrable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.Integrable (fun x => ↑(f x) • g x) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → E<GOAL>MeasureTheory.Integrable g (μ.withDensity fun x => ↑(f x)) ↔ MeasureTheory.Integrable (fun x => f x • g x) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤<VAR>g : α → ℝ<GOAL>MeasureTheory.Integrable g (μ.withDensity f) ↔ MeasureTheory.Integrable (fun x => g x * (f x).toReal) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>f_meas : Measurable f<VAR>u : ↥(MeasureTheory.Lp E 1 (μ.withDensity fun x => ↑(f x)))<GOAL>MeasureTheory.Memℒp (fun x => f x • ↑↑u x) 1 μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>f_meas : Measurable f<VAR>u : ↥(MeasureTheory.Lp E 1 (μ.withDensity fun x => ↑(f x)))<GOAL>(MeasureTheory.withDensitySMulLI μ f_meas) u = MeasureTheory.Memℒp.toLp (fun x => f x • ↑↑u x) ⋯
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>MeasureTheory.Memℒp (fun x => (f x).toReal) 1 μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>MeasureTheory.Integrable (fun x => (f x).toReal) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun a => max (f a) 0) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun a => max (-f a) 0) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedAddCommGroup 𝕜<VAR>SMulZeroClass 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>f : α → β<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (c • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>hc : IsUnit c<VAR>f : α → β<GOAL>MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedDivisionRing 𝕜<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>f : α → β<GOAL>MeasureTheory.Integrable (c • f) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>f : α → β<VAR>φ : α → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<VAR>hφ : MeasureTheory.Memℒp φ ⊤ μ<GOAL>MeasureTheory.Integrable (φ • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>f : α → β<VAR>φ : α → 𝕜<VAR>hφ : MeasureTheory.Integrable φ μ<VAR>hf : MeasureTheory.Memℒp f ⊤ μ<GOAL>MeasureTheory.Integrable (φ • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<VAR>c : β<GOAL>MeasureTheory.Integrable (fun x => f x • c) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>E : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>c : E<VAR>hc : c ≠ 0<GOAL>MeasureTheory.Integrable (fun x => f x • c) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>f : α → 𝕜<VAR>h : MeasureTheory.Integrable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.Integrable (fun x => c * f x) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>f : α → 𝕜<VAR>h : MeasureTheory.Integrable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.Integrable ((fun x => c) * f) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>f : α → 𝕜<VAR>h : MeasureTheory.Integrable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.Integrable (fun x => f x * c) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>f : α → 𝕜<VAR>h : MeasureTheory.Integrable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.Integrable (f * fun x => c) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>c : 𝕜<VAR>hc : IsUnit c<VAR>f : α → 𝕜<GOAL>MeasureTheory.Integrable (fun x => c * f x) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>c : 𝕜<VAR>hc : IsUnit c<VAR>f : α → 𝕜<GOAL>MeasureTheory.Integrable (fun x => f x * c) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>f g : α → 𝕜<VAR>c : ℝ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<GOAL>MeasureTheory.Integrable (fun x => f x * g x) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedDivisionRing 𝕜<VAR>f : α → 𝕜<VAR>h : MeasureTheory.Integrable f μ<VAR>c : 𝕜<GOAL>MeasureTheory.Integrable (fun x => f x / c) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => ↑(f x)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : α → 𝕜<GOAL>MeasureTheory.Integrable (fun x => RCLike.re (f x)) μ ∧ MeasureTheory.Integrable (fun x => RCLike.im (f x)) μ ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => RCLike.re (f x)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => RCLike.im (f x)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : MeasureTheory.Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_int : MeasureTheory.Integrable f μ'<VAR>hf : MeasureTheory.StronglyMeasurable f<GOAL>MeasureTheory.Integrable f (μ'.trim hm)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>H : Type u_5<VAR>NormedAddCommGroup H<VAR>m0 : MeasurableSpace α<VAR>μ' : MeasureTheory.Measure α<VAR>f : α → H<VAR>hm : m ≤ m0<VAR>hf_int : MeasureTheory.Integrable f (μ'.trim hm)<GOAL>MeasureTheory.Integrable f μ'
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>E : Type u_5<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>hC : C < ⊤<VAR>f : α → E<VAR>hf_meas : MeasureTheory.AEStronglyMeasurable f μ<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ ≤ C<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>MeasureTheory.SigmaFinite μ<VAR>C : ℝ≥0∞<VAR>hC : C < ⊤<VAR>f : α → E<VAR>hf_meas : MeasureTheory.AEStronglyMeasurable f μ<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ ≤ C<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>(MeasureTheory.AEEqFun.mk f hf).Integrable ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α →ₘ[μ] β<GOAL>MeasureTheory.Integrable (↑f) μ ↔ f.Integrable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<GOAL>MeasureTheory.AEEqFun.Integrable 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α →ₘ[μ] β<GOAL>f.Integrable → (-f).Integrable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α →ₘ[μ] β<GOAL>f.Integrable ↔ f ∈ MeasureTheory.Lp β 1 μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α →ₘ[μ] β<GOAL>f.Integrable → g.Integrable → (f + g).Integrable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α →ₘ[μ] β<VAR>hf : f.Integrable<VAR>hg : g.Integrable<GOAL>(f - g).Integrable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>f : α →ₘ[μ] β<GOAL>f.Integrable → (c • f).Integrable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<GOAL>MeasureTheory.Integrable (↑↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<GOAL>MeasureTheory.HasFiniteIntegral (↑↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<GOAL>MeasureTheory.StronglyMeasurable ↑↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<GOAL>Measurable ↑↑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<GOAL>MeasureTheory.AEStronglyMeasurable (↑↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasurableSpace β<VAR>BorelSpace β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<GOAL>AEMeasurable (↑↑f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ↥(MeasureTheory.Lp β 1 μ)<GOAL>edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ↥(MeasureTheory.Lp β 1 μ)<GOAL>dist f g = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<GOAL>‖f‖ = (∫⁻ (a : α), ↑‖↑↑f a‖₊ ∂μ).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ↥(MeasureTheory.Lp β 1 μ)<GOAL>‖f - g‖ = (∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ).toReal