ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>f : ℝ ≃ᵐ ℝ<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x<VAR>g : ℝ → ℝ<VAR>hg : 0 ≤ᵐ[MeasureTheory.volume] g<VAR>hg_int : MeasureTheory.Integrable g MeasureTheory.volume<GOAL>(MeasureTheory.Measure.map (⇑f.symm) (MeasureTheory.volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.eLpNorm (↑(MeasureTheory.AEEqFun.mk f hf)) p μ = MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_5<VAR>E : Type u_6<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hfp : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.eLpNorm (↑(MeasureTheory.AEEqFun.mk 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>h : MeasureTheory.Memℒp f p μ<GOAL>↑(MeasureTheory.Memℒp.toLp f h) = MeasureTheory.AEEqFun.mk f ⋯
<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.toLp f hf) =ᵐ[μ] f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hfg : f =ᵐ[μ] g<GOAL>MeasureTheory.Memℒp.toLp f hf = MeasureTheory.Memℒp.toLp g hg
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.Memℒp.toLp f hf = MeasureTheory.Memℒp.toLp g hg ↔ f =ᵐ[μ] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>h : MeasureTheory.Memℒp 0 p μ<GOAL>MeasureTheory.Memℒp.toLp 0 h = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.Memℒp.toLp (f + g) ⋯ = MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg
<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.toLp (-f) ⋯ = -MeasureTheory.Memℒp.toLp f hf
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.Memℒp.toLp (f - g) ⋯ = MeasureTheory.Memℒp.toLp f hf - MeasureTheory.Memℒp.toLp g hg
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<VAR>h : ↑↑f =ᵐ[μ] ↑↑g<GOAL>f = g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>f = g ↔ ↑↑f =ᵐ[μ] ↑↑g
<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>f ∈ MeasureTheory.Lp E 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<GOAL>f ∈ MeasureTheory.Lp E p μ ↔ MeasureTheory.Memℒp (↑f) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<GOAL>MeasureTheory.Lp E q μ ≤ MeasureTheory.Lp E 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.eLpNorm (↑f) p μ < ⊤<GOAL>↑↑⟨f, hf⟩ = ↑f
<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.eLpNorm (↑f) p μ < ⊤<GOAL>↑⟨f, hf⟩ = f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>hf : MeasureTheory.Memℒp (↑↑f) p μ<GOAL>MeasureTheory.Memℒp.toLp (↑↑f) hf = f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E 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 : ↥(MeasureTheory.Lp E 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 : ↥(MeasureTheory.Lp E p μ)<GOAL>MeasureTheory.StronglyMeasurable ↑↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>MeasureTheory.AEStronglyMeasurable (↑↑f) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E 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<GOAL>↑↑0 =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(-f) =ᵐ[μ] -↑↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(f + g) =ᵐ[μ] ↑↑f + ↑↑g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(f - g) =ᵐ[μ] ↑↑f - ↑↑g
<VAR>E : Type u_2<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup E<VAR>α : Type u_5<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (c : E) [inst : MeasureTheory.IsFiniteMeasure μ], MeasureTheory.AEEqFun.const α c ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖f‖ = (MeasureTheory.eLpNorm (↑↑f) p μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖f‖₊ = (MeasureTheory.eLpNorm (↑↑f) p μ).toNNReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑‖f‖₊ = ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑‖f‖₊ = 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.toLp f hf‖ = (MeasureTheory.eLpNorm f p μ).toReal
<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.toLp f hf‖₊ = (MeasureTheory.eLpNorm f p μ).toNNReal
<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.toLp f hf‖₊ = 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 g : ↥(MeasureTheory.Lp E p μ)<GOAL>dist f g = (MeasureTheory.eLpNorm (↑↑f - ↑↑g) p μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>edist f g = MeasureTheory.eLpNorm (↑↑f - ↑↑g) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>edist f g = ENNReal.ofReal (dist f g)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>dist f g = (edist f g).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : ↥(MeasureTheory.Lp E p μ)<GOAL>dist f g = ‖f - g‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>edist (MeasureTheory.Memℒp.toLp f hf) (MeasureTheory.Memℒp.toLp g hg) = MeasureTheory.eLpNorm (f - g) 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>edist (MeasureTheory.Memℒp.toLp f hf) 0 = 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<GOAL>‖0‖₊ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<GOAL>‖0‖ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p 0)<GOAL>‖f‖ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E 0 μ)<GOAL>‖f‖ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>hp : 0 < p<GOAL>‖f‖₊ = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>hp : 0 < p<GOAL>‖f‖ = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>f = 0 ↔ ↑↑f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖-f‖₊ = ‖f‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖-f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>c : ℝ≥0<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>g : ↥(MeasureTheory.Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ c * ‖↑↑g x‖₊<GOAL>‖f‖₊ ≤ c * ‖g‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>c : ℝ<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>g : ↥(MeasureTheory.Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ c * ‖↑↑g x‖<GOAL>‖f‖ ≤ c * ‖g‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>g : ↥(MeasureTheory.Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖<GOAL>‖f‖ ≤ ‖g‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>c : ℝ≥0<VAR>f : α →ₘ[μ] E<VAR>g : ↥(MeasureTheory.Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ c * ‖↑↑g x‖₊<GOAL>f ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>c : ℝ<VAR>f : α →ₘ[μ] E<VAR>g : ↥(MeasureTheory.Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ c * ‖↑↑g x‖<GOAL>f ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α →ₘ[μ] E<VAR>g : ↥(MeasureTheory.Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ ‖↑↑g x‖₊<GOAL>f ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α →ₘ[μ] E<VAR>g : ↥(MeasureTheory.Lp F p μ)<VAR>h : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ ‖↑↑g x‖<GOAL>f ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α →ₘ[μ] E<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑f x‖₊ ≤ C<GOAL>f ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α →ₘ[μ] E<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ C<GOAL>f ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖₊ ≤ C<GOAL>‖f‖₊ ≤ MeasureTheory.measureUnivNNReal μ ^ p.toReal⁻¹ * C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : ↥(MeasureTheory.Lp E p μ)<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ C<GOAL>‖f‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹ * C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>c • ↑f ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<GOAL>(MeasureTheory.Lp.LpSubmodule E p μ 𝕜).toAddSubgroup = MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(c • f) =ᵐ[μ] c • ↑↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → E<VAR>c : 𝕜<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp.toLp (c • f) ⋯ = c • MeasureTheory.Memℒp.toLp f hf
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>s : Set α<VAR>f : α → G<GOAL>MeasureTheory.eLpNormEssSup (s.indicator f) μ ≤ MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>s : Set α<VAR>c : G<GOAL>MeasureTheory.eLpNormEssSup (s.indicator fun x => c) μ ≤ ↑‖c‖₊
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>s : Set α<VAR>c : G<VAR>hμs : μ s ≠ 0<GOAL>MeasureTheory.eLpNormEssSup (s.indicator fun x => c) μ = ↑‖c‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>f : α → E<GOAL>MeasureTheory.eLpNorm (s.indicator f) p μ ≤ MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>s : Set α<VAR>c : G<VAR>hs : MeasureTheory.NullMeasurableSet s μ<VAR>hp : p ≠ 0<VAR>hp_top : p ≠ ⊤<GOAL>MeasureTheory.eLpNorm (s.indicator fun x => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>s : Set α<VAR>c : G<VAR>hs : MeasurableSet s<VAR>hp : p ≠ 0<VAR>hp_top : p ≠ ⊤<GOAL>MeasureTheory.eLpNorm (s.indicator fun x => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>s : Set α<VAR>c : G<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ 0<VAR>hp : p ≠ 0<GOAL>MeasureTheory.eLpNorm (s.indicator fun x => c) p μ = ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>s : Set α<VAR>c : G<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm (s.indicator fun x => c) p μ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<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<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (s.indicator f) p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.eLpNormEssSup (s.indicator f) μ = MeasureTheory.eLpNormEssSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.eLpNorm (s.indicator f) p μ = MeasureTheory.eLpNorm f p (μ.restrict s)
<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.Memℒp (s.indicator f) p μ ↔ MeasureTheory.Memℒp f p (μ.restrict s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>p q : ℝ≥0∞<VAR>f : α → E<VAR>hfq : MeasureTheory.Memℒp f q μ<VAR>s : Set α<VAR>hf : ∀ x ∉ s, f x = 0<VAR>hs : μ s ≠ ⊤<VAR>hpq : p ≤ q<GOAL>MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>p : ℝ≥0∞<VAR>hs : MeasurableSet s<VAR>c : E<VAR>hμsc : c = 0 ∨ μ s ≠ ⊤<GOAL>MeasureTheory.Memℒp (s.indicator fun x => c) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hp : p ≠ ⊤<VAR>c : E<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ η, 0 < η ∧ ∀ (s : Set α), μ s ≤ ↑η → MeasureTheory.eLpNorm (s.indicator fun x => c) 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>DecidablePred fun x => x ∈ s<VAR>g : α → E<VAR>hs : MeasurableSet s<VAR>hf : MeasureTheory.Memℒp f p (μ.restrict s)<VAR>hg : MeasureTheory.Memℒp g p (μ.restrict sᶜ)<GOAL>MeasureTheory.Memℒp (s.piecewise f g) p μ
<VAR>E : Type u_2<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup E<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>f : X → E<VAR>hf : HasCompactSupport f<VAR>h2f : MeasureTheory.AEStronglyMeasurable f μ<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C<GOAL>MeasureTheory.Memℒp f p μ
<VAR>E : Type u_2<VAR>p : ℝ≥0∞<VAR>NormedAddCommGroup E<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>μ : MeasureTheory.Measure X<VAR>MeasureTheory.IsFiniteMeasureOnCompacts μ<VAR>OpensMeasurableSpace X<VAR>f : X → E<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c c' : E<GOAL>MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p hs hμs c' = MeasureTheory.indicatorConstLp p hs hμs (c + c')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c c' : E<GOAL>MeasureTheory.indicatorConstLp p hs hμs c - MeasureTheory.indicatorConstLp p hs hμs c' = MeasureTheory.indicatorConstLp p hs hμs (c - c')
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>↑↑(MeasureTheory.indicatorConstLp p hs hμs c) =ᵐ[μ] s.indicator fun x => c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) x = c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>∀ᵐ (x : α) ∂μ, x ∉ s → ↑↑(MeasureTheory.indicatorConstLp p hs hμs c) x = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>‖MeasureTheory.indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hμs_ne_zero : μ s ≠ 0<GOAL>‖MeasureTheory.indicatorConstLp ⊤ hs hμs c‖ = ‖c‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp_pos : p ≠ 0<VAR>hμs_pos : μ s ≠ 0<GOAL>‖MeasureTheory.indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>‖MeasureTheory.indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * (μ s).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>‖MeasureTheory.indicatorConstLp p hs hμs c‖₊ ≤ ‖c‖₊ * (μ s).toNNReal ^ (1 / p.toReal)