ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Sort u_5<VAR>ι' : ι → Sort u_6<VAR>f : (i : ι) → ι' i → α → ℝ≥0∞<GOAL>⨆ i, ⨆ j, ∫⁻ (a : α), f i j a ∂μ ≤ ∫⁻ (a : α), ⨆ i, ⨆ j, f i j a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Sort u_5<VAR>f : ι → α → ℝ≥0∞<GOAL>∫⁻ (a : α), ⨅ i, f i a ∂μ ≤ ⨅ i, ∫⁻ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Sort u_5<VAR>ι' : ι → Sort u_6<VAR>f : (i : ι) → ι' i → α → ℝ≥0∞<GOAL>∫⁻ (a : α), ⨅ i, ⨅ h, f i h a ∂μ ≤ ⨅ i, ⨅ h, ∫⁻ (a : α), f i h a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ᵐ (a : α) ∂μ, f a ≤ g a<GOAL>∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x<GOAL>∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hg : Measurable g<VAR>hfg : ∀ x ∈ s, f x ≤ g x<GOAL>∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x<GOAL>∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>hfg : ∀ x ∈ s, f x ≤ g x<GOAL>∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : f =ᵐ[μ] g<GOAL>∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : ∀ (a : α), f a = g a<GOAL>∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s t : Set α<VAR>h : s =ᵐ[μ] t<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<GOAL>∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>h_nonneg : 0 ≤ᵐ[μ] f<GOAL>∫⁻ (x : α), ↑‖f x‖₊ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>h_nonneg : 0 ≤ f<GOAL>∫⁻ (x : α), ↑‖f x‖₊ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : Monotone f<GOAL>∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<GOAL>∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (F x))<GOAL>Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (𝓝 (∫⁻ (x : α), F x ∂μ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a ∂μ = ⨆ n, (MeasureTheory.SimpleFunc.eapprox f n).lintegral μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>l : Filter ι<VAR>s : ι → Set α<VAR>hl : Filter.Tendsto (⇑μ ∘ s) l (𝓝 0)<GOAL>Filter.Tendsto (fun i => ∫⁻ (x : α) in s i, f x ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ ≤ ∫⁻ (a : α), f a + g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>g : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂c • μ = c * ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>∫⁻ (a : α) in s, f a ∂c • μ = c * ∫⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → MeasureTheory.Measure α<GOAL>∫⁻ (a : α), f a ∂MeasureTheory.Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
<VAR>α : Type u_1<VAR>ι : Type u_5<GOAL>∀ {x : MeasurableSpace α} (f : α → ℝ≥0∞) (μ : ι → MeasureTheory.Measure α), HasSum (fun i => ∫⁻ (a : α), f a ∂μ i) (∫⁻ (a : α), f a ∂MeasureTheory.Measure.sum μ)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<GOAL>∫⁻ (a : α), f a ∂(μ + ν) = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), f a ∂ν
<VAR>α : Type u_1<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>s : Finset ι<VAR>f : α → ℝ≥0∞<VAR>μ : ι → MeasureTheory.Measure α<GOAL>∫⁻ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂0 = 0
<VAR>α : Type u_5<VAR>MeasurableSpace α<VAR>IsEmpty α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α), f x ∂μ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in ∅, f x ∂μ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hs' : μ s = 0<GOAL>∫⁻ (x : α) in s, f x ∂μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ b ∈ s, AEMeasurable (f b) μ<GOAL>∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ b ∈ s, Measurable (f b)<GOAL>∫⁻ (a : α), ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>∫⁻ (a : α), r * f a ∂μ = r * ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>(∫⁻ (a : α), f a ∂μ) * r ≤ ∫⁻ (a : α), f a * r ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>MeasurableSpace β<VAR>ν : MeasureTheory.Measure β<VAR>f : α → ℝ≥0∞<VAR>g : β → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g ν<GOAL>∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f f' : α → β<VAR>h : f =ᵐ[μ] f'<VAR>g : β → ℝ≥0∞<GOAL>∫⁻ (a : α), g (f a) ∂μ = ∫⁻ (a : α), g (f' a) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f₁ f₁' : α → β<VAR>f₂ f₂' : α → γ<VAR>h₁ : f₁ =ᵐ[μ] f₁'<VAR>h₂ : f₂ =ᵐ[μ] f₂'<VAR>g : β → γ → ℝ≥0∞<GOAL>∫⁻ (a : α), g (f₁ a) (f₂ a) ∂μ = ∫⁻ (a : α), g (f₁' a) (f₂' a) ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<GOAL>∫⁻ (a : α), s.indicator f a ∂μ ≤ ∫⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>c : ℝ≥0∞<GOAL>∫⁻ (a : α), s.indicator (fun x => c) a ∂μ ≤ c * μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>c : ℝ≥0∞<GOAL>∫⁻ (a : α), s.indicator (fun x => c) a ∂μ = c * μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>c : ℝ≥0∞<GOAL>∫⁻ (a : α), s.indicator (fun x => c) a ∂μ = c * μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>r : ℝ≥0∞<GOAL>∫⁻ (x : α) in {x | f x = r}, f x ∂μ = r * μ {x | f x = r}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>∫⁻ (a : α), s.indicator 1 a ∂μ ≤ μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>∫⁻ (a : α), s.indicator 1 a ∂μ = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α), s.indicator 1 a ∂μ = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hle : f ≤ᵐ[μ] g<VAR>hg : AEMeasurable g μ<VAR>ε : ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂μ + ε * μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>ε : ℝ≥0∞<GOAL>ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>μ s ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ (a : α), f a ≤ 1<VAR>h'f : ∀ a ∈ sᶜ, f a = 0<GOAL>∫⁻ (a : α), f a ∂μ ≤ μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hμf : μ {x | f x = ⊤} ≠ 0<GOAL>∫⁻ (x : α), f x ∂μ = ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hμf : μ {x | x ∈ s ∧ f x = ⊤} ≠ 0<GOAL>∫⁻ (x : α) in s, f x ∂μ = ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hμf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>μ {x | f x = ⊤} = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>s : Set α<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hμf : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤<GOAL>μ {x | x ∈ s ∧ f x = ⊤} = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hε' : ε ≠ ⊤<GOAL>μ {x | ε ≤ f x} ≤ (∫⁻ (a : α), f a ∂μ) / ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᵐ[μ] g<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ<GOAL>f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>0 < ∫⁻ (a : α), f a ∂μ ↔ 0 < μ (Function.support f)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<GOAL>0 < ∫⁻ (a : α) in s, f a ∂μ ↔ 0 < μ (Function.support f ∩ s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a<GOAL>∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤<VAR>h_le : g ≤ᵐ[μ] f<GOAL>∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : Measurable g<VAR>hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤<VAR>h_le : g ≤ᵐ[μ] f<GOAL>∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h_le : f ≤ᵐ[μ] g<VAR>h : ∃ᵐ (x : α) ∂μ, f x ≠ g x<GOAL>∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h_le : f ≤ᵐ[μ] g<VAR>s : Set α<VAR>hμs : μ s ≠ 0<VAR>h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x<GOAL>∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h : ∀ᵐ (x : α) ∂μ, f x < g x<GOAL>∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>s : Set α<VAR>hsm : MeasurableSet s<VAR>hs : μ s ≠ 0<VAR>hg : Measurable g<VAR>hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤<VAR>h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x<GOAL>∫⁻ (x : α) in s, f x ∂μ < ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>h_meas : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : ∀ (n : ℕ), f n.succ ≤ᵐ[μ] f n<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>h_meas : ∀ (n : ℕ), Measurable (f n)<VAR>h_anti : Antitone f<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i => f i a<VAR>h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<GOAL>∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>Countable β<VAR>f : β → α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hμ : μ ≠ 0<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ⊤<VAR>h_directed : Directed (fun x x_1 => x ≥ x_1) f<GOAL>∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ<GOAL>∫⁻ (a : α), Filter.liminf (fun n => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>h_meas : ∀ (n : ℕ), Measurable (f n)<GOAL>∫⁻ (a : α), Filter.liminf (fun n => f n a) Filter.atTop ∂μ ≤ Filter.liminf (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>hf_meas : ∀ (n : ℕ), Measurable (f n)<VAR>h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g<VAR>h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤<GOAL>Filter.limsup (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop ≤ ∫⁻ (a : α), Filter.limsup (fun n => f n a) Filter.atTop ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>F : ℕ → α → ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>bound : α → ℝ≥0∞<VAR>hF_meas : ∀ (n : ℕ), Measurable (F n)<VAR>h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (𝓝 (f a))<GOAL>Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>F : ℕ → α → ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>bound : α → ℝ≥0∞<VAR>hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ<VAR>h_bound : ∀ (n : ℕ), F n ≤ᵐ[μ] bound<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (𝓝 (f a))<GOAL>Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>F : ι → α → ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>bound : α → ℝ≥0∞<VAR>hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a<VAR>h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ⊤<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (𝓝 (f a))<GOAL>Filter.Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>F : α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), AEMeasurable (f n) μ<VAR>h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x<VAR>h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤<VAR>h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (F x))<GOAL>Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (𝓝 (∫⁻ (x : α), F x ∂μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), Measurable (f b)<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (b : β), AEMeasurable (f b) μ<VAR>h_directed : Directed (fun x x_1 => x ≤ x_1) f<GOAL>∫⁻ (a : α), ⨆ b, f b a ∂μ = ⨆ b, ∫⁻ (a : α), f b a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable β<VAR>f : β → α → ℝ≥0∞<VAR>hf : ∀ (i : β), AEMeasurable (f i) μ<GOAL>∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable β<VAR>s : β → Set α<VAR>hm : ∀ (i : β), MeasureTheory.NullMeasurableSet (s i) μ<VAR>hd : Pairwise (MeasureTheory.AEDisjoint μ on s)<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ i, s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable β<VAR>s : β → Set α<VAR>hm : ∀ (i : β), MeasurableSet (s i)<VAR>hd : Pairwise (Disjoint on s)<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ i, s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set β<VAR>s : β → Set α<VAR>ht : t.Countable<VAR>hm : ∀ i ∈ t, MeasureTheory.NullMeasurableSet (s i) μ<VAR>hd : t.Pairwise (MeasureTheory.AEDisjoint μ on s)<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set β<VAR>s : β → Set α<VAR>ht : t.Countable<VAR>hm : ∀ i ∈ t, MeasurableSet (s i)<VAR>hd : t.PairwiseDisjoint s<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ i ∈ t, s i, f a ∂μ = ∑' (i : ↑t), ∫⁻ (a : α) in s ↑i, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset β<VAR>t : β → Set α<VAR>hd : (↑s).Pairwise (MeasureTheory.AEDisjoint μ on t)<VAR>hm : ∀ b ∈ s, MeasureTheory.NullMeasurableSet (t b) μ<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Finset β<VAR>t : β → Set α<VAR>hd : (↑s).PairwiseDisjoint t<VAR>hm : ∀ b ∈ s, MeasurableSet (t b)<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Countable β<VAR>s : β → Set α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<VAR>A B : Set α<VAR>hB : MeasurableSet B<VAR>hAB : Disjoint A B<GOAL>∫⁻ (a : α) in A ∪ B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ