ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<GOAL>ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ↑‖↑↑f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ↥(MeasureTheory.Lp β 1 μ)<GOAL>ENNReal.ofReal ‖f - g‖ = ∫⁻ (x : α), ↑‖↑↑f x - ↑↑g x‖₊ ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ↥(MeasureTheory.Lp β 1 μ)<VAR>hf : MeasureTheory.Integrable (↑↑f) μ<GOAL>MeasureTheory.Integrable.toL1 (↑↑f) hf = 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.Integrable.toL1 f hf) =ᵐ[μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>h : MeasureTheory.Integrable 0 μ<GOAL>MeasureTheory.Integrable.toL1 0 h = 0
<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.toL1 f hf) = MeasureTheory.AEEqFun.mk 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.toL1 f hf = MeasureTheory.Integrable.toL1 g hg ↔ 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.toL1 (f + g) ⋯ = MeasureTheory.Integrable.toL1 f hf + MeasureTheory.Integrable.toL1 g hg
<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.toL1 (-f) ⋯ = -MeasureTheory.Integrable.toL1 f hf
<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.toL1 (f - g) ⋯ = MeasureTheory.Integrable.toL1 f hf - MeasureTheory.Integrable.toL1 g hg
<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.toL1 f hf‖ = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal
<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.toL1 f hf‖₊ = ∫⁻ (a : α), ↑‖f 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.toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
<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>edist (MeasureTheory.Integrable.toL1 f hf) (MeasureTheory.Integrable.toL1 g hg) = ∫⁻ (a : α), edist (f a) (g 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>edist (MeasureTheory.Integrable.toL1 f hf) 0 = ∫⁻ (a : α), edist (f a) 0 ∂μ
<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>k : 𝕜<GOAL>MeasureTheory.Integrable.toL1 (fun a => k • f a) ⋯ = k • MeasureTheory.Integrable.toL1 f hf
<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>k : 𝕜<GOAL>MeasureTheory.Integrable.toL1 (k • f) ⋯ = k • MeasureTheory.Integrable.toL1 f hf
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>h : MeasureTheory.HasFiniteIntegral f μ<VAR>s : Set α<GOAL>MeasureTheory.HasFiniteIntegral f (μ.restrict s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>f_intble : MeasureTheory.Integrable f μ<VAR>s : Set α<GOAL>MeasureTheory.Integrable f (μ.restrict s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>H : Type u_7<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>φ : α → H<VAR>L : H →L[𝕜] E<VAR>φ_int : MeasureTheory.Integrable φ μ<GOAL>MeasureTheory.Integrable (fun a => L (φ a)) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>H : Type u_7<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>φ : α → H<VAR>L : H ≃L[𝕜] E<GOAL>MeasureTheory.Integrable (fun a => L (φ a)) μ ↔ MeasureTheory.Integrable φ μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>H : Type u_7<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>φ : α → H<VAR>L : H ≃ₗᵢ[𝕜] E<GOAL>MeasureTheory.Integrable (fun a => L (φ a)) μ ↔ MeasureTheory.Integrable φ μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>H : Type u_7<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>φ : α → H →L[𝕜] E<VAR>φ_int : MeasureTheory.Integrable φ μ<VAR>v : H<GOAL>MeasureTheory.Integrable (fun a => (φ a) v) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : α → E × F<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => (f x).1) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : α → E × F<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.Integrable (fun x => (f x).2) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : α → E × F<GOAL>MeasureTheory.Integrable f μ ↔ MeasureTheory.Integrable (fun x => (f x).1) μ ∧ MeasureTheory.Integrable (fun x => (f x).2) μ
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (Cardinal.aleph 1).ord).α<GOAL>s ⊆ MeasurableSpace.generateMeasurableRec s i
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (Cardinal.aleph 1).ord).α<GOAL>∅ ∈ MeasurableSpace.generateMeasurableRec s i
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i j : (Quotient.out (Cardinal.aleph 1).ord).α<VAR>h : j < i<VAR>t : Set α<VAR>ht : t ∈ MeasurableSpace.generateMeasurableRec s j<GOAL>tᶜ ∈ MeasurableSpace.generateMeasurableRec s i
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (Cardinal.aleph 1).ord).α<VAR>f : ℕ → Set α<VAR>hf : ∀ (n : ℕ), ∃ j < i, f n ∈ MeasurableSpace.generateMeasurableRec s j<GOAL>⋃ n, f n ∈ MeasurableSpace.generateMeasurableRec s i
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i j : (Quotient.out (Cardinal.aleph 1).ord).α<VAR>h : i ≤ j<GOAL>MeasurableSpace.generateMeasurableRec s i ⊆ MeasurableSpace.generateMeasurableRec s j
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (Cardinal.aleph 1).ord).α<GOAL>#↑(MeasurableSpace.generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>{t | MeasurableSpace.GenerateMeasurable s t} = ⋃ i, MeasurableSpace.generateMeasurableRec s i
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>#↑{t | MeasurableSpace.GenerateMeasurable s t} ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>#↑{t | MeasurableSet t} ≤ max (#↑s) 2 ^ ℵ₀
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>hs : #↑s ≤ 𝔠<GOAL>#↑{t | MeasurableSpace.GenerateMeasurable s t} ≤ 𝔠
<VAR>α : Type u<VAR>s : Set (Set α)<GOAL>#↑s ≤ 𝔠 → #↑{t | MeasurableSet t} ≤ 𝔠
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm' f p.toReal μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>p : ℝ≥0<VAR>hp : p ≠ 0<GOAL>MeasureTheory.eLpNorm f (↑p) μ = MeasureTheory.eLpNorm' f (↑p) μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm f p μ = (∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ) ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>p : ℝ≥0<VAR>hp : p ≠ 0<GOAL>MeasureTheory.eLpNorm f (↑p) μ = (∫⁻ (x : α), ↑‖f x‖₊ ^ ↑p ∂μ) ^ (1 / ↑p)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm f 1 μ = ∫⁻ (x : α), ↑‖f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm f ⊤ μ = MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>p : ℝ≥0∞<VAR>h : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hq0_lt : 0 < q<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ = MeasureTheory.eLpNorm' f q μ ^ q
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>p : ℝ≥0<VAR>hp : p ≠ 0<GOAL>MeasureTheory.eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (x : α), ↑‖f x‖₊ ^ ↑p ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hfp : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.eLpNorm f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hfp : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.eLpNorm f p μ ≠ ⊤
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hq0_lt : 0 < q<VAR>hfq : MeasureTheory.eLpNorm' f q μ < ⊤<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ < ⊤
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hfp : MeasureTheory.eLpNorm f p μ < ⊤<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ < ⊤
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.eLpNorm f p μ < ⊤ ↔ ∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ < ⊤
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm' f 0 μ = 1
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm f 0 μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<GOAL>MeasureTheory.Memℒp f 0 μ ↔ MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>hp0_lt : 0 < q<GOAL>MeasureTheory.eLpNorm' 0 q μ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>hq0_ne : q ≠ 0<VAR>hμ : μ ≠ 0<GOAL>MeasureTheory.eLpNorm' 0 q μ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<GOAL>MeasureTheory.eLpNormEssSup 0 μ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<GOAL>MeasureTheory.eLpNorm 0 p μ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<GOAL>MeasureTheory.eLpNorm (fun x => 0) p μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<GOAL>MeasureTheory.Memℒp 0 p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<GOAL>MeasureTheory.Memℒp (fun x => 0) p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>q : ℝ<VAR>NormedAddCommGroup F<VAR>MeasurableSpace α<VAR>f : α → F<VAR>hq_pos : 0 < q<GOAL>MeasureTheory.eLpNorm' f q 0 = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>MeasurableSpace α<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm' f 0 0 = 1
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>q : ℝ<VAR>NormedAddCommGroup F<VAR>MeasurableSpace α<VAR>f : α → F<VAR>hq_neg : q < 0<GOAL>MeasureTheory.eLpNorm' f q 0 = ⊤
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>MeasurableSpace α<VAR>f : α → F<GOAL>MeasureTheory.eLpNormEssSup f 0 = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup F<VAR>MeasurableSpace α<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm f p 0 = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm' (-f) q μ = MeasureTheory.eLpNorm' f q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm (-f) p μ = MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (-f) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<GOAL>MeasureTheory.Memℒp (-f) p μ ↔ MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>c : F<VAR>hq_pos : 0 < q<GOAL>MeasureTheory.eLpNorm' (fun x => c) q μ = ↑‖c‖₊ * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : F<VAR>hc_ne_zero : c ≠ 0<VAR>hq_ne_zero : q ≠ 0<GOAL>MeasureTheory.eLpNorm' (fun x => c) q μ = ↑‖c‖₊ * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>c : F<VAR>hμ : μ ≠ 0<GOAL>MeasureTheory.eLpNormEssSup (fun x => c) μ = ↑‖c‖₊
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>c : F<VAR>hq_pos : 0 < q<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>MeasureTheory.eLpNorm' (fun x => c) q μ = ↑‖c‖₊
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>c : F<VAR>h0 : p ≠ 0<VAR>hμ : μ ≠ 0<GOAL>MeasureTheory.eLpNorm (fun x => c) p μ = ↑‖c‖₊ * μ Set.univ ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>c : F<VAR>h0 : p ≠ 0<VAR>h_top : p ≠ ⊤<GOAL>MeasureTheory.eLpNorm (fun x => c) p μ = ↑‖c‖₊ * μ Set.univ ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>c : F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>c : E<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>MeasureTheory.Memℒp (fun x => c) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>c : E<GOAL>MeasureTheory.Memℒp (fun x => c) ⊤ μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>c : E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.Memℒp (fun x => c) p μ ↔ c = 0 ∨ μ Set.univ < ⊤
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>hq : 0 ≤ q<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊<GOAL>MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>hq : 0 ≤ q<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖<GOAL>MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNorm' g q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f g : α → F<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊<GOAL>MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f g : α → F<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖<GOAL>MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f g : α → F<VAR>hfg : f =ᵐ[μ] g<GOAL>MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f g : α → F<VAR>hfg : f =ᵐ[μ] g<GOAL>MeasureTheory.eLpNormEssSup f μ = MeasureTheory.eLpNormEssSup g μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f g : α → F<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊<GOAL>MeasureTheory.eLpNormEssSup f μ ≤ MeasureTheory.eLpNormEssSup g μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>g : α → ℝ<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>h : ∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>h : ∀ (x : α), ‖f x‖ ≤ ‖g x‖<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>g : α → ℝ<VAR>h : ∀ (x : α), ‖f x‖ ≤ g x<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C<GOAL>MeasureTheory.eLpNormEssSup f μ ≤ ↑C
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>MeasureTheory.eLpNormEssSup f μ ≤ ENNReal.ofReal C
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C<GOAL>MeasureTheory.eLpNormEssSup f μ < ⊤
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>MeasureTheory.eLpNormEssSup f μ < ⊤
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C<GOAL>MeasureTheory.eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>MeasureTheory.eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊<GOAL>MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖<GOAL>MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s t : Set α<VAR>f : α → E<GOAL>MeasureTheory.eLpNorm (s.indicator f - t.indicator f) p μ = MeasureTheory.eLpNorm ((symmDiff s t).indicator f) p μ