ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → ℝ≥0<VAR>f_meas : Measurable f<VAR>g : X → E<GOAL>(∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : X → E<GOAL>(∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → ℝ≥0<VAR>f_meas : Measurable f<VAR>g : X → E<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>(∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → ℝ≥0<VAR>s : Set X<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>g : X → E<VAR>hs : MeasurableSet s<GOAL>(∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ
<VAR>X : Type u_1<VAR>E : Type u_3<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasureTheory.SFinite μ<VAR>f : X → ℝ≥0<VAR>s : Set X<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>g : X → E<GOAL>(∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>PseudoEMetricSpace X<VAR>μ : MeasureTheory.Measure X<VAR>E : Set X<VAR>E_mble : MeasurableSet E<VAR>δ : ℝ<GOAL>μ E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ
<VAR>X : Type u_1<VAR>MeasurableSpace X<VAR>PseudoEMetricSpace X<VAR>μ : MeasureTheory.Measure X<VAR>E : Set X<VAR>E_mble : MeasurableSet E<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<GOAL>μ E ≤ ∫⁻ (x : X), ↑((thickenedIndicator δ_pos E) x) ∂μ
<VAR>X : Type u_1<VAR>f : X → ℝ<VAR>m0 : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>g : MeasureTheory.SimpleFunc X ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (↑g * f) μ
<VAR>X : Type u_1<VAR>f : X → ℝ<VAR>m m0 : MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>hm : m ≤ m0<VAR>g : MeasureTheory.SimpleFunc X ℝ<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (↑g * f) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>μ : MeasureTheory.Measure Y<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FirstCountableTopology X<VAR>LocallyCompactSpace X<VAR>OpensMeasurableSpace Y<VAR>SecondCountableTopologyEither Y E<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>f : X → Y → E<VAR>hf : Continuous (Function.uncurry f)<VAR>s : Set Y<VAR>hs : IsCompact s<GOAL>Continuous fun x => ∫ (y : Y) in s, f x y ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace Y<VAR>μ : MeasureTheory.Measure Y<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : MeasureTheory.IntegrableOn g k μ<GOAL>ContinuousOn (fun x => ∫ (y : Y), (L (g y)) (f x y) ∂μ) s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>MeasurableSpace Y<VAR>OpensMeasurableSpace Y<VAR>μ : MeasureTheory.Measure Y<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : X → Y → E<VAR>s : Set X<VAR>k : Set Y<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<GOAL>ContinuousOn (fun x => ∫ (y : Y), f x y ∂μ) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g h : α → β<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hh : MeasureTheory.AEStronglyMeasurable h μ<GOAL>∫⁻ (a : α), edist (f a) (g a) ∂μ ≤ ∫⁻ (a : α), edist (f a) (h a) ∂μ + ∫⁻ (a : α), edist (g a) (h a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<GOAL>∫⁻ (x : α), ↑‖0‖₊ ∂μ = 0
<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>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>g : α → γ<GOAL>∫⁻ (a : α), ↑‖f a‖₊ + ↑‖g a‖₊ ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ + ∫⁻ (a : α), ↑‖g a‖₊ ∂μ
<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>hg : MeasureTheory.AEStronglyMeasurable g μ<GOAL>∫⁻ (a : α), ↑‖f a‖₊ + ↑‖g a‖₊ ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ + ∫⁻ (a : α), ↑‖g a‖₊ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>∫⁻ (a : α), ↑‖(-f) a‖₊ ∂μ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<GOAL>∀ {x : MeasurableSpace α} (f : α → β) (μ : MeasureTheory.Measure α), MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>h : 0 ≤ᵐ[μ] f<GOAL>MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0<GOAL>MeasureTheory.HasFiniteIntegral (fun x => ↑(f x)) μ ↔ ∫⁻ (a : α), ↑(f a) ∂μ < ⊤
<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>hg : MeasureTheory.HasFiniteIntegral g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖<GOAL>MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>g : α → ℝ<VAR>hg : MeasureTheory.HasFiniteIntegral g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a<GOAL>MeasureTheory.HasFiniteIntegral 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.HasFiniteIntegral f μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖<GOAL>MeasureTheory.HasFiniteIntegral g μ
<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>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖<GOAL>MeasureTheory.HasFiniteIntegral f μ ↔ MeasureTheory.HasFiniteIntegral g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>hf : MeasureTheory.HasFiniteIntegral f μ<VAR>h : f =ᵐ[μ] g<GOAL>MeasureTheory.HasFiniteIntegral g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>h : f =ᵐ[μ] g<GOAL>MeasureTheory.HasFiniteIntegral f μ ↔ MeasureTheory.HasFiniteIntegral g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>c : β<GOAL>MeasureTheory.HasFiniteIntegral (fun x => c) μ ↔ c = 0 ∨ μ Set.univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : β<GOAL>MeasureTheory.HasFiniteIntegral (fun x => c) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → β<VAR>C : ℝ<VAR>hC : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ C<GOAL>MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>Finite α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>h : MeasureTheory.HasFiniteIntegral f ν<VAR>hμ : μ ≤ ν<GOAL>MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hμ : MeasureTheory.HasFiniteIntegral f μ<VAR>hν : MeasureTheory.HasFiniteIntegral f ν<GOAL>MeasureTheory.HasFiniteIntegral f (μ + ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>h : MeasureTheory.HasFiniteIntegral f (μ + ν)<GOAL>MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>h : MeasureTheory.HasFiniteIntegral f (μ + ν)<GOAL>MeasureTheory.HasFiniteIntegral f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral f (μ + ν) ↔ MeasureTheory.HasFiniteIntegral f μ ∧ MeasureTheory.HasFiniteIntegral f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>h : MeasureTheory.HasFiniteIntegral f μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>MeasureTheory.HasFiniteIntegral f (c • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>m : MeasurableSpace α<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<GOAL>MeasureTheory.HasFiniteIntegral (fun x => 0) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hfi : MeasureTheory.HasFiniteIntegral f μ<GOAL>MeasureTheory.HasFiniteIntegral (-f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral (-f) μ ↔ MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hfi : MeasureTheory.HasFiniteIntegral f μ<GOAL>MeasureTheory.HasFiniteIntegral (fun a => ‖f a‖) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral (fun a => ‖f a‖) μ ↔ MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>MeasureTheory.HasFiniteIntegral (fun x => (f x).toReal) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hfi : MeasureTheory.HasFiniteIntegral f μ<GOAL>MeasureTheory.IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>F : ℕ → α → β<VAR>bound : α → ℝ<VAR>h : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>n : ℕ<GOAL>∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>h : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (𝓝 (f a))<GOAL>∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => ENNReal.ofReal ‖F n a‖) Filter.atTop (𝓝 (ENNReal.ofReal ‖f a‖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (𝓝 (f a))<GOAL>∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (𝓝 (f a))<GOAL>MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>F_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ<VAR>bound_hasFiniteIntegral : MeasureTheory.HasFiniteIntegral bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (𝓝 (f a))<GOAL>Filter.Tendsto (fun n => ∫⁻ (a : α), ENNReal.ofReal ‖F n a - f a‖ ∂μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.HasFiniteIntegral f μ<GOAL>MeasureTheory.HasFiniteIntegral (fun a => max (f a) 0) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.HasFiniteIntegral f μ<GOAL>MeasureTheory.HasFiniteIntegral (fun a => min (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 : α → β<GOAL>MeasureTheory.HasFiniteIntegral f μ → MeasureTheory.HasFiniteIntegral (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>MulActionWithZero 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>hc : IsUnit c<VAR>f : α → β<GOAL>MeasureTheory.HasFiniteIntegral (c • f) μ ↔ MeasureTheory.HasFiniteIntegral f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>f : α → 𝕜<VAR>h : MeasureTheory.HasFiniteIntegral f μ<VAR>c : 𝕜<GOAL>MeasureTheory.HasFiniteIntegral (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.HasFiniteIntegral f μ<VAR>c : 𝕜<GOAL>MeasureTheory.HasFiniteIntegral (fun x => f x * c) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<GOAL>MeasureTheory.Memℒp f 1 μ ↔ 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 μ<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 : α → β<VAR>hf : MeasureTheory.Integrable f μ<GOAL>AEMeasurable f μ
<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.HasFiniteIntegral 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>hg : MeasureTheory.Integrable g μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>g : α → ℝ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>h : ∀ᵐ (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.AEStronglyMeasurable g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖<GOAL>MeasureTheory.Integrable g μ
<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.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖<GOAL>MeasureTheory.Integrable 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>h : f =ᵐ[μ] g<GOAL>MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : α → β<VAR>h : f =ᵐ[μ] g<GOAL>MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>c : β<GOAL>MeasureTheory.Integrable (fun x => c) μ ↔ c = 0 ∨ μ Set.univ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : β<GOAL>MeasureTheory.Integrable (fun x => c) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>Finite α<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → β<GOAL>MeasureTheory.Integrable (fun a => f a) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.Integrable (fun x => ‖f x‖ ^ p.toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Integrable (fun x => ‖f x‖ ^ p.toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>h : MeasureTheory.Integrable f ν<VAR>hμ : μ ≤ ν<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>μ' : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<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 : α → β<VAR>hμ : MeasureTheory.Integrable f μ<VAR>hν : 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 : α → β<VAR>h : 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 : α → β<VAR>h : 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 μ ∧ MeasureTheory.Integrable f ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<GOAL>∀ {x : MeasurableSpace α} {f : α → β}, MeasureTheory.Integrable f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>f : α → β<VAR>μ : ι → MeasureTheory.Measure α<VAR>s : Finset ι<GOAL>MeasureTheory.Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, MeasureTheory.Integrable f (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>h : MeasureTheory.Integrable f μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>MeasureTheory.Integrable f (c • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>h : MeasureTheory.Integrable f μ<VAR>c : ℝ≥0<GOAL>MeasureTheory.Integrable f (c • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>c : ℝ≥0∞<VAR>h₁ : c ≠ 0<VAR>h₂ : c ≠ ⊤<GOAL>MeasureTheory.Integrable f (c • μ) ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>c : ℝ≥0∞<VAR>h₁ : c ≠ 0<VAR>h₂ : c ≠ ⊤<GOAL>MeasureTheory.Integrable f (c⁻¹ • μ) ↔ MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>h : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable f ((μ Set.univ)⁻¹ • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → β<GOAL>MeasureTheory.Integrable f ((μ Set.univ)⁻¹ • μ) ↔ MeasureTheory.Integrable f μ
<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 : δ → β<VAR>hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<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>f : α → δ<VAR>g : δ → β<VAR>hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>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>f : α → δ<VAR>g : δ → β<VAR>hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ)<VAR>hf : Measurable f<GOAL>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>f : α → δ<VAR>hf : MeasurableEmbedding f<VAR>g : δ → β<GOAL>MeasureTheory.Integrable g (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Integrable (g ∘ f) μ