ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<VAR>y : E<VAR>hy_ne : y ≠ 0<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : ∀ (y : E), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<GOAL>MeasureTheory.Memℒp (↑f) p μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.Memℒp (↑f) p μ ↔ ∀ (y : E), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<GOAL>MeasureTheory.Integrable (↑f) μ ↔ ∀ (y : E), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.Memℒp (↑f) p μ ↔ MeasureTheory.Integrable (↑f) μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.Memℒp (↑f) p μ ↔ f.FinMeasSupp μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<GOAL>MeasureTheory.Integrable (↑f) μ ↔ f.FinMeasSupp μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>h : f.FinMeasSupp μ<GOAL>MeasureTheory.Integrable (↑f) μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>F : Type u_5<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>g : MeasureTheory.SimpleFunc α F<GOAL>MeasureTheory.Integrable (↑f) μ → MeasureTheory.Integrable (↑g) μ → MeasureTheory.Integrable (↑(f.pair g)) μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : MeasureTheory.SimpleFunc α E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>MeasureTheory.Memℒp (↑f) p μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : MeasureTheory.SimpleFunc α E<GOAL>MeasureTheory.Integrable (↑f) μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<VAR>x : E<VAR>hx : x ≠ 0<GOAL>μ (↑f ⁻¹' {x}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<VAR>f : MeasureTheory.SimpleFunc α β<VAR>hf : ∀ (y : β), y ≠ 0 → μ (↑f ⁻¹' {y}) < ⊤<GOAL>μ (Function.support ↑f) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>μ (Function.support ↑f) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>μ (Function.support ↑f) < ⊤
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>c : E<VAR>hc : c ≠ 0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hcs : MeasureTheory.Memℒp (↑(MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.const α 0))) p μ<GOAL>μ s < ⊤
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>↑↑f = ↑↑g → f = g
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>𝕜 : Type u_6<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>c : 𝕜<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>↑(c • f) = c • ↑f
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>𝕜 : Type u_6<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>Fact (1 ≤ p)<GOAL>BoundedSMul 𝕜 ↥(MeasureTheory.Lp.simpleFunc E p μ)
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<GOAL>↑(MeasureTheory.Lp.simpleFunc.toLp f hf) = MeasureTheory.Memℒp.toLp (↑f) hf
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<GOAL>↑↑(MeasureTheory.Lp.simpleFunc.toLp f hf) = MeasureTheory.AEEqFun.mk ↑f ⋯
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.Lp.simpleFunc.toLp 0 ⋯ = 0
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<VAR>hg : MeasureTheory.Memℒp (↑g) p μ<GOAL>MeasureTheory.Lp.simpleFunc.toLp (f + g) ⋯ = MeasureTheory.Lp.simpleFunc.toLp f hf + MeasureTheory.Lp.simpleFunc.toLp g hg
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<GOAL>MeasureTheory.Lp.simpleFunc.toLp (-f) ⋯ = -MeasureTheory.Lp.simpleFunc.toLp f hf
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<VAR>hg : MeasureTheory.Memℒp (↑g) p μ<GOAL>MeasureTheory.Lp.simpleFunc.toLp (f - g) ⋯ = MeasureTheory.Lp.simpleFunc.toLp f hf - MeasureTheory.Lp.simpleFunc.toLp g hg
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>𝕜 : Type u_6<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<VAR>c : 𝕜<GOAL>MeasureTheory.Lp.simpleFunc.toLp (c • f) ⋯ = c • MeasureTheory.Lp.simpleFunc.toLp f hf
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Memℒp (↑f) p μ<GOAL>‖MeasureTheory.Lp.simpleFunc.toLp f hf‖ = (MeasureTheory.eLpNorm (↑f) p μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace E<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>Measurable ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>MeasureTheory.StronglyMeasurable ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSpace E<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>AEMeasurable (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>MeasureTheory.AEStronglyMeasurable (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) =ᵐ[μ] ↑↑↑f
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>MeasureTheory.Memℒp (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) p μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>MeasureTheory.Lp.simpleFunc.toLp (MeasureTheory.Lp.simpleFunc.toSimpleFunc f) ⋯ = f
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hfi : MeasureTheory.Memℒp (↑f) p μ<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.Lp.simpleFunc.toLp f hfi)) =ᵐ[μ] ↑f
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc 0) =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (f + g)) =ᵐ[μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) + ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g)
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (-f)) =ᵐ[μ] -↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (f - g)) =ᵐ[μ] ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f) - ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc g)
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>𝕜 : Type u_6<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>k : 𝕜<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (k • f)) =ᵐ[μ] k • ↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>‖f‖ = (MeasureTheory.eLpNorm (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) p μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>↑(MeasureTheory.Lp.simpleFunc.indicatorConst p hs hμs c) = MeasureTheory.indicatorConstLp p hs hμs c
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.Lp.simpleFunc.indicatorConst p hs hμs c)) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.const α 0))
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(MeasureTheory.Lp.simpleFunc E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P (MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : MeasureTheory.SimpleFunc α E⦄ (hf : MeasureTheory.Memℒp (↑f) p μ) (hg : MeasureTheory.Memℒp (↑g) p μ), Disjoint (Function.support ↑f) (Function.support ↑g) → P (MeasureTheory.Lp.simpleFunc.toLp f hf) → P (MeasureTheory.Lp.simpleFunc.toLp g hg) → P (MeasureTheory.Lp.simpleFunc.toLp f hf + MeasureTheory.Lp.simpleFunc.toLp g hg)<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E p μ)<GOAL>P f
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<GOAL>UniformContinuous Subtype.val
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<GOAL>UniformEmbedding Subtype.val
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<GOAL>UniformInducing Subtype.val
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<GOAL>DenseEmbedding Subtype.val
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<GOAL>DenseInducing Subtype.val
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<GOAL>DenseRange Subtype.val
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<GOAL>Dense ↑(MeasureTheory.Lp.simpleFunc E p μ)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_7<VAR>NormedLatticeAddCommGroup G<VAR>f g : ↥(MeasureTheory.Lp.simpleFunc G p μ)<GOAL>↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ f ≤ g
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_7<VAR>NormedLatticeAddCommGroup G<GOAL>↑↑↑0 =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_7<VAR>NormedLatticeAddCommGroup G<VAR>f : ↥(MeasureTheory.Lp.simpleFunc G p μ)<GOAL>0 ≤ᵐ[μ] ↑↑↑f ↔ 0 ≤ f
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_7<VAR>NormedLatticeAddCommGroup G<VAR>f : ↥(MeasureTheory.Lp.simpleFunc G p μ)<VAR>hf : 0 ≤ f<GOAL>∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ↑f'
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>G : Type u_7<VAR>NormedLatticeAddCommGroup G<VAR>hp : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<GOAL>DenseRange (MeasureTheory.Lp.simpleFunc.coeSimpleFuncNonnegToLpNonneg p μ G)
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : ↥(MeasureTheory.Lp E p μ) → Prop<VAR>h_ind : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ⊤), P ↑(MeasureTheory.Lp.simpleFunc.indicatorConst p hs ⋯ c)<VAR>h_add : ∀ ⦃f g : α → E⦄ (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ), Disjoint (Function.support f) (Function.support g) → P (MeasureTheory.Memℒp.toLp f hf) → P (MeasureTheory.Memℒp.toLp g hg) → P (MeasureTheory.Memℒp.toLp f hf + MeasureTheory.Memℒp.toLp g hg)<VAR>h_closed : IsClosed {f | P f}<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>P f
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → E⦄, Disjoint (Function.support f) (Function.support g) → MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp g p μ → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑f}<VAR>h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MeasureTheory.Memℒp f p μ → P f → P g<VAR>f : α → E<GOAL>MeasureTheory.Memℒp f p μ → P f
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h0P : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, MeasureTheory.eLpNorm (g - s.indicator fun x => c) p μ ≤ ε ∧ P g<VAR>h1P : ∀ (f g : α → E), P f → P g → P (f + g)<VAR>h2P : ∀ (f : α → E), P f → MeasureTheory.AEStronglyMeasurable f μ<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, MeasureTheory.eLpNorm (f - g) p μ ≤ ε ∧ P g
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : MeasureTheory.SimpleFunc α E<VAR>hf : MeasureTheory.Integrable (↑f) μ<GOAL>↑(MeasureTheory.Lp.simpleFunc.toLp f ⋯) = MeasureTheory.Integrable.toL1 (↑f) hf
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp.simpleFunc E 1 μ)<GOAL>MeasureTheory.Integrable (↑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)) μ
<VAR>α : Type u_1<VAR>E : Type u_4<VAR>MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>P : (α → E) → Prop<VAR>h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → E⦄, Disjoint (Function.support f) (Function.support g) → MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑f}<VAR>h_ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MeasureTheory.Integrable f μ → P f → P g<VAR>f : α → E<GOAL>MeasureTheory.Integrable f μ → P f
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>self : IsUnifLocDoublingMeasure μ<GOAL>∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<GOAL>∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<GOAL>∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (Metric.closedBall x (2 * ε)) ≤ ↑(IsUnifLocDoublingMeasure.doublingConstant μ) * μ (Metric.closedBall x ε)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>K : ℝ<GOAL>∃ C, ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (Metric.closedBall x (t * ε)) ≤ ↑C * μ (Metric.closedBall x ε)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>K : ℝ<GOAL>1 ≤ IsUnifLocDoublingMeasure.scalingConstantOf μ K
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>K : ℝ<GOAL>∃ R, 0 < R ∧ ∀ (x : α) (t r : ℝ), t ∈ Set.Ioc 0 K → r ≤ R → μ (Metric.closedBall x (t * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>K : ℝ<GOAL>∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (Metric.closedBall x (K * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>hK : 0 < K<GOAL>∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (Metric.closedBall x r) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K⁻¹) * μ (Metric.closedBall x (K * r))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>K : ℝ<GOAL>0 < IsUnifLocDoublingMeasure.scalingScaleOf μ K
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>IsUnifLocDoublingMeasure μ<VAR>K : ℝ<VAR>x : α<VAR>t r : ℝ<VAR>ht : t ∈ Set.Ioc 0 K<VAR>hr : r ≤ IsUnifLocDoublingMeasure.scalingScaleOf μ K<GOAL>μ (Metric.closedBall x (t * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
<VAR>α : Type u_5<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ≥0∞), MeasureTheory.lintegral μ f = ⨆ g, ⨆ (_ : ↑g ≤ f), g.lintegral μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : MeasureTheory.SimpleFunc α ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<GOAL>∫⁻ (a : α), ↑f a ∂μ = f.lintegral μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>hμν : μ ≤ ν<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ g<GOAL>∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : ∀ (x : α), f x ≤ g x<VAR>h2 : μ ≤ ν<GOAL>MeasureTheory.lintegral μ f ≤ MeasureTheory.lintegral ν g
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ g<GOAL>∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : ∀ (x : α), f x ≤ g x<GOAL>MeasureTheory.lintegral μ f ≤ MeasureTheory.lintegral μ g
<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 : α → ℝ≥0∞<GOAL>⨆ g, ⨆ (_ : Measurable g), ⨆ (_ : g ≤ f), ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} ⦃μ : MeasureTheory.Measure α⦄ {s t : Set α} {f : α → ℝ≥0∞}, s ⊆ t → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} ⦃μ : MeasureTheory.Measure α⦄ {s t : Set α} {f : α → ℝ≥0∞}, s ≤ᵐ[μ] t → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in t, f x ∂μ
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} (μ : MeasureTheory.Measure α), Monotone (MeasureTheory.lintegral μ)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<GOAL>∫⁻ (x : α), c ∂μ = c * μ Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>∫⁻ (x : α), 0 ∂μ = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>MeasureTheory.lintegral μ 0 = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>∫⁻ (x : α), 1 ∂μ = μ Set.univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>c : ℝ≥0∞<GOAL>∫⁻ (x : α) in s, c ∂μ = c * μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>∫⁻ (x : α) in s, 1 ∂μ = μ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>s : Set α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>∫⁻ (x : α) in s, c ∂μ < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>∫⁻ (x : α), c ∂μ < ⊤
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ≥0∞<GOAL>∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<GOAL>∫⁻ (a : α), f a ∂μ = ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(↑φ x) ≤ f x), (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal φ).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>∃ φ, (∀ (x : α), ↑(↑φ x) ≤ f x) ∧ ∀ (ψ : MeasureTheory.SimpleFunc α ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (MeasureTheory.SimpleFunc.map ENNReal.ofNNReal (ψ - φ)).lintegral μ < ε
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>ι : Sort u_5<VAR>f : ι → α → ℝ≥0∞<GOAL>⨆ i, ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), ⨆ i, f i a ∂μ