ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>Nonempty ι<VAR>SemilatticeSup ι<VAR>hp : Fact (1 ≤ p)<VAR>f : ι → ↥(MeasureTheory.Lp E p μ)<GOAL>CauchySeq f ↔ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hp : Fact (1 ≤ p)<VAR>H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ) → ∀ (B : ℕ → ℝ≥0∞), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N) → ∃ f_lim, MeasureTheory.Memℒp f_lim p μ ∧ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (𝓝 0)<GOAL>CompleteSpace ↥(MeasureTheory.Lp E p μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm' (f n - f m) p μ < B N<VAR>n : ℕ<GOAL>MeasureTheory.eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>n : ℕ<VAR>hn : MeasureTheory.eLpNorm' (fun x => ∑ i ∈ Finset.range (n + 1), ‖f (i + 1) x - f i x‖) p μ ≤ ∑' (i : ℕ), B i<GOAL>∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>h : ∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p<GOAL>(∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h : (∫⁻ (a : α), (∑' (i : ℕ), ↑‖f (i + 1) a - f i a‖₊) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i<GOAL>∀ᵐ (x : α) ∂μ, ∑' (i : ℕ), ↑‖f (i + 1) x - f i x‖₊ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hp1 : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm' (f n - f m) p μ < B N<GOAL>∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 l)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hp : 1 ≤ p<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N<GOAL>∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 l)
<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 : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (f_lim x))<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ<VAR>f_lim : α → E<VAR>h_lim_meas : MeasureTheory.AEStronglyMeasurable f_lim μ<VAR>h_tendsto : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (𝓝 0)<GOAL>MeasureTheory.Memℒp f_lim p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∑' (i : ℕ), B i ≠ ⊤<VAR>h_cau : ∀ (N n m : ℕ), N ≤ n → N ≤ m → MeasureTheory.eLpNorm (f n - f m) p μ < B N<GOAL>∃ f_lim, MeasureTheory.Memℒp f_lim p μ ∧ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>f ∈ MeasureTheory.Lp.boundedContinuousFunction E p μ ↔ ∃ f₀, ContinuousMap.toAEEqFun μ f₀.toContinuousMap = ↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ 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>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ MeasureTheory.measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹ * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>Fact (1 ≤ p)<GOAL>(BoundedContinuousFunction.toLpHom p μ).range = MeasureTheory.Lp.boundedContinuousFunction E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : α →ᵇ E<GOAL>↑↑((BoundedContinuousFunction.toLp p μ 𝕜) f) =ᵐ[μ] ⇑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>(LinearMap.range (BoundedContinuousFunction.toLp p μ 𝕜)).toAddSubgroup = MeasureTheory.Lp.boundedContinuousFunction E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>‖BoundedContinuousFunction.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>f g : α →ᵇ E<VAR>μ.IsOpenPosMeasure<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>(BoundedContinuousFunction.toLp p μ 𝕜) f = (BoundedContinuousFunction.toLp p μ 𝕜) 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>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>μ.IsOpenPosMeasure<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>Function.Injective ⇑(BoundedContinuousFunction.toLp p μ 𝕜)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>(LinearMap.range (ContinuousMap.toLp p μ 𝕜)).toAddSubgroup = MeasureTheory.Lp.boundedContinuousFunction E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : C(α, E)<GOAL>↑↑((ContinuousMap.toLp p μ 𝕜) f) =ᵐ[μ] ⇑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : C(α, E)<GOAL>(ContinuousMap.toLp p μ 𝕜) f = (BoundedContinuousFunction.toLp p μ 𝕜) ((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : α →ᵇ E<GOAL>(ContinuousMap.toLp p μ 𝕜) f.toContinuousMap = (BoundedContinuousFunction.toLp p μ 𝕜) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : C(α, E)<GOAL>↑((ContinuousMap.toLp p μ 𝕜) f) = ContinuousMap.toAEEqFun μ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>μ.IsOpenPosMeasure<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>Function.Injective ⇑(ContinuousMap.toLp p μ 𝕜)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>f g : C(α, E)<VAR>μ.IsOpenPosMeasure<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>(ContinuousMap.toLp p μ 𝕜) f = (ContinuousMap.toLp p μ 𝕜) 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>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>β : Type u_6<VAR>μ.IsOpenPosMeasure<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>g : β → C(α, E)<VAR>f : C(α, E)<VAR>hg : Summable g<VAR>hg2 : HasSum (⇑(ContinuousMap.toLp p μ 𝕜) ∘ g) ((ContinuousMap.toLp p μ 𝕜) f)<GOAL>HasSum g f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>‖ContinuousMap.toLp p μ 𝕜‖ = ‖BoundedContinuousFunction.toLp p μ 𝕜‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>TopologicalSpace α<VAR>BorelSpace α<VAR>SecondCountableTopologyEither α E<VAR>CompactSpace α<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>Fact (1 ≤ p)<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>‖ContinuousMap.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ 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 μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<GOAL>(ε * μ {x | ε ≤ ↑‖↑↑f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ ENNReal.ofReal ‖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>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<GOAL>ε * μ {x | ε ≤ ↑‖↑↑f x‖₊ ^ p.toReal} ≤ ENNReal.ofReal ‖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 μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<GOAL>ε ^ p.toReal * μ {x | ε ≤ ↑‖↑↑f x‖₊} ≤ ENNReal.ofReal ‖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 μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>μ {x | ε ≤ ↑‖↑↑f x‖₊} ≤ ε⁻¹ ^ p.toReal * ENNReal.ofReal ‖f‖ ^ p.toReal
<VAR>M : Type u_2<VAR>MeasurableSpace M<VAR>Add M<VAR>self : MeasurableAdd M<VAR>c : M<GOAL>Measurable fun x => x + c
<VAR>M : Type u_2<VAR>MeasurableSpace M<VAR>Add M<VAR>self : MeasurableAdd M<VAR>c : M<GOAL>Measurable fun x => c + x
<VAR>M : Type u_2<VAR>MeasurableSpace M<VAR>Add M<VAR>self : MeasurableAdd₂ M<GOAL>Measurable fun p => p.1 + p.2
<VAR>M : Type u_2<VAR>MeasurableSpace M<VAR>Mul M<VAR>self : MeasurableMul M<VAR>c : M<GOAL>Measurable fun x => x * c
<VAR>M : Type u_2<VAR>MeasurableSpace M<VAR>Mul M<VAR>self : MeasurableMul M<VAR>c : M<GOAL>Measurable fun x => c * x
<VAR>M : Type u_2<VAR>MeasurableSpace M<VAR>Mul M<VAR>self : MeasurableMul₂ M<GOAL>Measurable fun p => p.1 * p.2
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Mul M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>MeasurableMul M<VAR>hf : Measurable f<VAR>c : M<GOAL>Measurable fun x => c * f x
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Add M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>MeasurableAdd M<VAR>hf : Measurable f<VAR>c : M<GOAL>Measurable fun x => c + f x
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Add M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableAdd M<VAR>hf : AEMeasurable f μ<VAR>c : M<GOAL>AEMeasurable (fun x => c + f x) μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Mul M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableMul M<VAR>hf : AEMeasurable f μ<VAR>c : M<GOAL>AEMeasurable (fun x => c * f x) μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Add M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>MeasurableAdd M<VAR>hf : Measurable f<VAR>c : M<GOAL>Measurable fun x => f x + c
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Mul M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>MeasurableMul M<VAR>hf : Measurable f<VAR>c : M<GOAL>Measurable fun x => f x * c
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Add M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableAdd M<VAR>hf : AEMeasurable f μ<VAR>c : M<GOAL>AEMeasurable (fun x => f x + c) μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Mul M<VAR>m : MeasurableSpace α<VAR>f : α → M<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableMul M<VAR>hf : AEMeasurable f μ<VAR>c : M<GOAL>AEMeasurable (fun x => f x * c) μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Add M<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>MeasurableAdd₂ M<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable (f + g)
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Mul M<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>MeasurableMul₂ M<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable (f * g)
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Mul M<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>MeasurableMul₂ M<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => f a * g a
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Add M<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>MeasurableAdd₂ M<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => f a + g a
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Add M<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableAdd₂ M<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (f + g) μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Mul M<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableMul₂ M<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (f * g) μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Mul M<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableMul₂ M<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => f a * g a) μ
<VAR>M : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace M<VAR>Add M<VAR>m : MeasurableSpace α<VAR>f g : α → M<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableAdd₂ M<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun a => f a + g a) μ
<VAR>G : Type u_2<VAR>SubNegMonoid G<VAR>MeasurableSpace G<VAR>MeasurableAdd G<VAR>g : G<GOAL>Measurable fun h => h - g
<VAR>G : Type u_2<VAR>DivInvMonoid G<VAR>MeasurableSpace G<VAR>MeasurableMul G<VAR>g : G<GOAL>Measurable fun h => h / g
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>Pow β γ<VAR>self : MeasurablePow β γ<GOAL>Measurable fun p => p.1 ^ p.2
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>Pow β γ<VAR>MeasurablePow β γ<VAR>m : MeasurableSpace α<VAR>f : α → β<VAR>g : α → γ<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun x => f x ^ g x
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>Pow β γ<VAR>MeasurablePow β γ<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>g : α → γ<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun x => f x ^ g x) μ
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>Pow β γ<VAR>MeasurablePow β γ<VAR>m : MeasurableSpace α<VAR>f : α → β<VAR>hf : Measurable f<VAR>c : γ<GOAL>Measurable fun x => f x ^ c
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>Pow β γ<VAR>MeasurablePow β γ<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>c : γ<GOAL>AEMeasurable (fun x => f x ^ c) μ
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>Pow β γ<VAR>MeasurablePow β γ<VAR>m : MeasurableSpace α<VAR>g : α → γ<VAR>hg : Measurable g<VAR>c : β<GOAL>Measurable fun x => c ^ g x
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>MeasurableSpace β<VAR>MeasurableSpace γ<VAR>Pow β γ<VAR>MeasurablePow β γ<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>g : α → γ<VAR>hg : AEMeasurable g μ<VAR>c : β<GOAL>AEMeasurable (fun x => c ^ g x) μ
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Sub G<VAR>self : MeasurableSub G<VAR>c : G<GOAL>Measurable fun x => c - x
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Sub G<VAR>self : MeasurableSub G<VAR>c : G<GOAL>Measurable fun x => x - c
<VAR>G : Type u_2<VAR>MeasurableSpace G<VAR>Sub G<VAR>self : MeasurableSub₂ G<GOAL>Measurable fun p => p.1 - p.2
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>Div G₀<VAR>self : MeasurableDiv G₀<VAR>c : G₀<GOAL>Measurable fun x => c / x
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>Div G₀<VAR>self : MeasurableDiv G₀<VAR>c : G₀<GOAL>Measurable fun x => x / c
<VAR>G₀ : Type u_2<VAR>MeasurableSpace G₀<VAR>Div G₀<VAR>self : MeasurableDiv₂ G₀<GOAL>Measurable fun p => p.1 / p.2
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Div G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>MeasurableDiv G<VAR>hf : Measurable f<VAR>c : G<GOAL>Measurable fun x => c / f x
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Sub G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>MeasurableSub G<VAR>hf : Measurable f<VAR>c : G<GOAL>Measurable fun x => c - f x
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Div G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableDiv G<VAR>hf : AEMeasurable f μ<VAR>c : G<GOAL>AEMeasurable (fun x => c / f x) μ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Sub G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSub G<VAR>hf : AEMeasurable f μ<VAR>c : G<GOAL>AEMeasurable (fun x => c - f x) μ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Sub G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>MeasurableSub G<VAR>hf : Measurable f<VAR>c : G<GOAL>Measurable fun x => f x - c
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Div G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>MeasurableDiv G<VAR>hf : Measurable f<VAR>c : G<GOAL>Measurable fun x => f x / c
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Sub G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSub G<VAR>hf : AEMeasurable f μ<VAR>c : G<GOAL>AEMeasurable (fun x => f x - c) μ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Div G<VAR>m : MeasurableSpace α<VAR>f : α → G<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableDiv G<VAR>hf : AEMeasurable f μ<VAR>c : G<GOAL>AEMeasurable (fun x => f x / c) μ
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Div G<VAR>m : MeasurableSpace α<VAR>f g : α → G<VAR>MeasurableDiv₂ G<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable (f / g)
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Sub G<VAR>m : MeasurableSpace α<VAR>f g : α → G<VAR>MeasurableSub₂ G<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable (f - g)
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Div G<VAR>m : MeasurableSpace α<VAR>f g : α → G<VAR>MeasurableDiv₂ G<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => f a / g a
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Sub G<VAR>m : MeasurableSpace α<VAR>f g : α → G<VAR>MeasurableSub₂ G<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => f a - g a
<VAR>G : Type u_2<VAR>α : Type u_3<VAR>MeasurableSpace G<VAR>Sub G<VAR>m : MeasurableSpace α<VAR>f g : α → G<VAR>μ : MeasureTheory.Measure α<VAR>MeasurableSub₂ G<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (f - g) μ