ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s t : Set α<GOAL>∫⁻ (a : α) in s ∪ t, f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ + ∫⁻ (a : α) in t, f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>B : Set α<VAR>f : α → ℝ≥0∞<VAR>A : Set α<VAR>hB : MeasurableSet B<GOAL>∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>A : Set α<VAR>hA : MeasurableSet A<GOAL>∫⁻ (x : α) in A, f x ∂μ + ∫⁻ (x : α) in Aᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hsm : MeasurableSet s<VAR>hfs : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤<GOAL>∫⁻ (x : α) in sᶜ, f x ∂μ = ∫⁻ (x : α), f x ∂μ - ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_5<VAR>Countable ι<VAR>f : α → ℝ≥0∞<VAR>s : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) s<GOAL>∫⁻ (x : α) in ⋃ i, s i, f x ∂μ = ⨆ i, ∫⁻ (x : α) in s i, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (x : α), max (f x) (g x) ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set α<GOAL>∫⁻ (x : α) in s, max (f x) (g x) ∂μ = ∫⁻ (x : α) in s ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in s ∩ {x | g x < f x}, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : AEMeasurable f (MeasureTheory.Measure.map g μ)<VAR>hg : AEMeasurable g μ<GOAL>∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mβ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hg : Measurable g<GOAL>∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ ≤ ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>MeasureTheory.lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (y : β) in s, f y ∂MeasureTheory.Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>s : Set β<VAR>hf : Measurable f<VAR>hs : MeasurableSet s<VAR>c : ℝ≥0∞<GOAL>∫⁻ (a : α), s.indicator (fun x => c) (f a) ∂μ = c * μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace β<VAR>g : α → β<VAR>hg : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<GOAL>∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α ≃ᵐ β<GOAL>∫⁻ (a : β), f a ∂MeasureTheory.Measure.map (⇑g) μ = ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : β → ℝ≥0∞<VAR>g : α ≃ᵐ β<VAR>hg : MeasureTheory.MeasurePreserving (⇑g) μ ν<GOAL>∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f (g a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mb : MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>g : α → β<VAR>hg : MeasureTheory.MeasurePreserving g μ ν<VAR>f : β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mb : MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>g : α → β<VAR>hg : MeasureTheory.MeasurePreserving g μ ν<VAR>hge : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<GOAL>∫⁻ (a : α), f (g a) ∂μ = ∫⁻ (b : β), f b ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mb : MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>g : α → β<VAR>hg : MeasureTheory.MeasurePreserving g μ ν<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>f : β → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mb : MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>g : α → β<VAR>hg : MeasureTheory.MeasurePreserving g μ ν<VAR>hge : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<VAR>s : Set β<GOAL>∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>mb : MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>g : α → β<VAR>hg : MeasureTheory.MeasurePreserving g μ ν<VAR>hge : MeasurableEmbedding g<VAR>f : β → ℝ≥0∞<VAR>s : Set α<GOAL>∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : ↑s), f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set ↑s<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : ↑s) in t, f ↑x ∂MeasureTheory.Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a ∂MeasureTheory.Measure.dirac a = f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂MeasureTheory.Measure.dirac a = f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>Decidable (a ∈ s)<GOAL>∫⁻ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>MeasurableSingletonClass α<VAR>Decidable (a ∈ s)<GOAL>∫⁻ (x : α) in s, f x ∂MeasureTheory.Measure.dirac a = if a ∈ s then f a else 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a ∂MeasureTheory.Measure.count = ∑' (a : α), f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂MeasureTheory.Measure.count = ∑' (a : α), f a
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>c : ℝ≥0∞<GOAL>∑' (x : α), c = c * MeasureTheory.Measure.count Set.univ
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α → ℝ≥0∞<VAR>a_mble : Measurable a<VAR>c : ℝ≥0∞<VAR>tsum_le_c : ∑' (i : α), a i ≤ c<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>ε_ne_top : ε ≠ ⊤<GOAL>MeasureTheory.Measure.count {i | ε ≤ a i} ≤ c / ε
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>MeasurableSingletonClass α<VAR>a : α → ℝ≥0<VAR>a_mble : Measurable a<VAR>a_summable : Summable a<VAR>c : ℝ≥0<VAR>tsum_le_c : ∑' (i : α), a i ≤ c<VAR>ε : ℝ≥0<VAR>ε_ne_zero : ε ≠ 0<GOAL>MeasureTheory.Measure.count {i | ε ≤ a i} ≤ ↑c / ↑ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable α<VAR>MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂μ = ∑' (a : α), f a * μ {a}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<VAR>a : α<GOAL>∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : s.Countable<GOAL>∫⁻ (a : α) in s, f a ∂μ = ∑' (a : ↑s), f ↑a * μ {↑a}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in insert a s, f x ∂μ = f a * μ {a} + ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, f x * μ {x}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSingletonClass α<VAR>Fintype α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α), f x ∂μ = ∑ x : α, f x * μ {x}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Unique α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α), f x ∂μ = f default * μ Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, f x < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, f x < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : μ s ≠ ⊤<VAR>f : α → ℝ≥0∞<VAR>hbdd : ∃ y, ∀ x ∈ s, f x ≤ ↑y<GOAL>∫⁻ (x : α) in s, f x ∂μ < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : μ s ≠ ⊤<VAR>f : α → ℝ≥0<VAR>hbdd : BddAbove (f '' s)<GOAL>∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : μ s ≠ ⊤<VAR>hsc : IsCompact s<VAR>f : α → ℝ≥0<VAR>hf : Continuous f<GOAL>∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤
<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>μ_fin : MeasureTheory.IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c<GOAL>∫⁻ (x : α), f x ∂μ < ⊤
<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>hF_meas : AEMeasurable F μ<VAR>hf_tendsto : Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<GOAL>∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (𝓝 (F a))
<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hF_meas : AEMeasurable F μ<VAR>hf_tendsto : Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a<VAR>h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤<GOAL>∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (𝓝 (F a))
<VAR>α : Type u_5<VAR>mα : MeasurableSpace α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>hf_tendsto : Filter.Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) Filter.atTop (𝓝 (∫⁻ (a : α), F a ∂μ))<VAR>hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a<VAR>h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<GOAL>∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun i => f i a) Filter.atTop (𝓝 (F a))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SFinite μ<VAR>f : α → ℝ≥0∞<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ε
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.trim hm)<GOAL>∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : Set α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C<VAR>h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)<GOAL>f Set.univ ≤ C
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>hm : m ≤ m0<VAR>MeasureTheory.SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C<GOAL>∫⁻ (x : α), f x ∂μ ≤ C
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>C : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C<GOAL>∫⁻ (x : α), f x ∂μ ≤ C
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0<VAR>L : ℝ≥0∞<VAR>hL : L < ∫⁻ (x : α), ↑(↑f x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ ↑f x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>L : ℝ≥0∞<VAR>hL : L < ∫⁻ (x : α), ↑(f x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_6<VAR>L : Filter ι<VAR>L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>μ : MeasureTheory.Measure α<VAR>A_mble : MeasurableSet A<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>B : Set α<VAR>B_mble : MeasurableSet B<VAR>B_finmeas : μ B ≠ ⊤<VAR>As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>Filter.Tendsto (fun i => μ (As i)) L (𝓝 (μ A))
<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_6<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>L.IsCountablyGenerated<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>A_mble : MeasurableSet A<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>Filter.Tendsto (fun i => μ (As i)) L (𝓝 (μ A))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UniformIntegrable f p μ<VAR>i : ι<GOAL>MeasureTheory.AEStronglyMeasurable (f i) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UniformIntegrable f p μ<GOAL>MeasureTheory.UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UniformIntegrable f p μ<VAR>i : ι<GOAL>MeasureTheory.Memℒp (f i) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UnifIntegrable f p μ<VAR>hg : MeasureTheory.UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ<GOAL>MeasureTheory.UnifIntegrable (f + g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UnifIntegrable f p μ<GOAL>MeasureTheory.UnifIntegrable (-f) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UnifIntegrable f p μ<VAR>hg : MeasureTheory.UnifIntegrable g p μ<VAR>hp : 1 ≤ p<VAR>hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ<GOAL>MeasureTheory.UnifIntegrable (f - g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UnifIntegrable f p μ<VAR>hfg : ∀ (n : ι), f n =ᵐ[μ] g n<GOAL>MeasureTheory.UnifIntegrable g p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UnifIntegrable f p μ<VAR>E : Set α<GOAL>MeasureTheory.UnifIntegrable (fun i => E.indicator (f i)) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.UnifIntegrable f p μ<VAR>E : Set α<GOAL>MeasureTheory.UnifIntegrable f p (μ.restrict E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>NormedAddCommGroup β<VAR>MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>f : ι → α → β<GOAL>MeasureTheory.UnifIntegrable f p 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f g : ι → α → β<VAR>hfg : ∀ (n : ι), f n =ᵐ[μ] g n<GOAL>MeasureTheory.UnifIntegrable f p μ ↔ MeasureTheory.UnifIntegrable g p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>x : α<GOAL>Filter.Tendsto (fun M => {x | ↑M ≤ ↑‖f x‖₊}.indicator f x) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Memℒp f 1 μ<VAR>hmeas : MeasureTheory.StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ M, ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Memℒp f 1 μ<VAR>hmeas : MeasureTheory.StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ M, 0 ≤ M ∧ ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Memℒp f 1 μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ M, 0 ≤ M ∧ ∫⁻ (x : α), ↑‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖₊ ∂μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : α → β<VAR>hf : MeasureTheory.Memℒp f ⊤ μ<VAR>hmeas : MeasureTheory.StronglyMeasurable f<GOAL>∃ M, MeasureTheory.eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hmeas : MeasureTheory.StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ M, MeasureTheory.eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hmeas : MeasureTheory.StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ M, 0 < M ∧ MeasureTheory.eLpNorm ({x | M ≤ ↑‖f x‖₊}.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hmeas : MeasureTheory.StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hmeas : MeasureTheory.StronglyMeasurable f<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp_ne_top : p ≠ ⊤<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.UnifIntegrable (fun x => g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>Subsingleton ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>n : ℕ<VAR>f : Fin n → α → β<VAR>hf : ∀ (i : Fin n), MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>Finite ι<VAR>hp_one : 1 ≤ p<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>hp' : p ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f g : α → β<VAR>c : ℝ<VAR>hc : 0 ≤ c<VAR>hf : ∀ x ∈ s, dist (f x) (g x) ≤ c<GOAL>MeasureTheory.eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal)