ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>μ.WeaklyRegular<VAR>p : ℝ<VAR>hp : 0 < p<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f (ENNReal.ofReal p) μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MeasureTheory.Memℒp (⇑g) (ENNReal.ofReal p) μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>μ.WeaklyRegular<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ g, ∫⁻ (x : α), ↑‖f x - g x‖₊ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>NormedSpace ℝ E<VAR>μ.WeaklyRegular<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f μ<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ g, ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ MeasureTheory.Integrable (⇑g) μ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedSpace ℝ E<VAR>SecondCountableTopologyEither α E<VAR>Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>μ.WeaklyRegular<GOAL>Dense ↑(MeasureTheory.Lp.boundedContinuousFunction E p μ)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>NormedSpace ℝ E<VAR>SecondCountableTopologyEither α E<VAR>Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>μ.WeaklyRegular<GOAL>(MeasureTheory.Lp.boundedContinuousFunction E p μ).topologicalClosure = ⊤
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SecondCountableTopologyEither α E<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>𝕜 : Type u_3<VAR>NormedField 𝕜<VAR>NormedAlgebra ℝ 𝕜<VAR>NormedSpace 𝕜 E<VAR>μ.WeaklyRegular<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>DenseRange ⇑(BoundedContinuousFunction.toLp p μ 𝕜)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>NormalSpace α<VAR>MeasurableSpace α<VAR>BorelSpace α<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>SecondCountableTopologyEither α E<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>𝕜 : Type u_3<VAR>NormedField 𝕜<VAR>NormedAlgebra ℝ 𝕜<VAR>NormedSpace 𝕜 E<VAR>CompactSpace α<VAR>μ.WeaklyRegular<VAR>MeasureTheory.IsFiniteMeasure μ<GOAL>DenseRange ⇑(ContinuousMap.toLp p μ 𝕜)
<VAR>α : Type u_2<VAR>self : MeasureTheory.OuterMeasure α<VAR>s₁ s₂ : Set α<GOAL>s₁ ⊆ s₂ → self.measureOf s₁ ≤ self.measureOf s₂
<VAR>α : Type u_2<VAR>self : MeasureTheory.OuterMeasure α<VAR>s : ℕ → Set α<GOAL>Pairwise (Disjoint on s) → self.measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), self.measureOf (s i)
<VAR>α : Type u_2<VAR>self : MeasureTheory.OuterMeasure α<GOAL>self.measureOf ∅ = 0
<VAR>F : Type u_2<VAR>α : outParam (Type u_3)<VAR>FunLike F (Set α) ℝ≥0∞<VAR>self : MeasureTheory.OuterMeasureClass F α<VAR>f : F<GOAL>f ∅ = 0
<VAR>F : Type u_2<VAR>α : outParam (Type u_3)<VAR>FunLike F (Set α) ℝ≥0∞<VAR>self : MeasureTheory.OuterMeasureClass F α<VAR>f : F<VAR>s t : Set α<GOAL>s ⊆ t → f s ≤ f t
<VAR>F : Type u_2<VAR>α : outParam (Type u_3)<VAR>FunLike F (Set α) ℝ≥0∞<VAR>self : MeasureTheory.OuterMeasureClass F α<VAR>f : F<VAR>s : ℕ → Set α<GOAL>Pairwise (Disjoint on s) → f (⋃ i, s i) ≤ ∑' (i : ℕ), f (s i)
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m.measureOf = ⇑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>NormedAddCommGroup β<GOAL>∀ {x : MeasurableSpace α} (f : ι → α → β) (p : ENNReal) (μ : MeasureTheory.Measure α), MeasureTheory.UnifTight f p μ ↔ ∀ ⦃ε : ENNReal⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), MeasureTheory.eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>NormedAddCommGroup β<GOAL>∀ {x : MeasurableSpace α} (f : ι → α → β) (p : ENNReal) (μ : MeasureTheory.Measure α), MeasureTheory.UnifTight f p μ ↔ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), MeasureTheory.eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ENNReal<VAR>hf : MeasureTheory.UnifTight f p μ<VAR>ε : ENNReal<VAR>hε : ε ≠ 0<GOAL>∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), MeasureTheory.eLpNorm (s.indicator (f i)) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ENNReal<VAR>hf : MeasureTheory.UnifTight f p μ<VAR>ε : ENNReal<VAR>hε : ε ≠ 0<GOAL>∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ ∀ (i : ι), MeasureTheory.eLpNorm (sᶜ.indicator (f i)) p μ ≤ ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ENNReal<VAR>hf : MeasureTheory.UnifTight f p μ<VAR>hg : MeasureTheory.UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ<GOAL>MeasureTheory.UnifTight (f + g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ENNReal<VAR>hf : MeasureTheory.UnifTight f p μ<GOAL>MeasureTheory.UnifTight (-f) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ENNReal<VAR>hf : MeasureTheory.UnifTight f p μ<VAR>hg : MeasureTheory.UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ<GOAL>MeasureTheory.UnifTight (f - g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ENNReal<VAR>hf : MeasureTheory.UnifTight f p μ<VAR>hfg : ∀ (n : ι), f n =ᵐ[μ] g n<GOAL>MeasureTheory.UnifTight g p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>f : ι → α → β<VAR>p : ENNReal<VAR>g : ι → α → β<VAR>hfg : ∀ (n : ι), f n =ᵐ[μ] g n<GOAL>MeasureTheory.UnifTight f p μ ↔ MeasureTheory.UnifTight g p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ENNReal<VAR>g : α → β<VAR>hp_ne_top : p ≠ ⊤<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.UnifTight (fun x => g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ENNReal<VAR>Subsingleton ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.UnifTight f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ENNReal<VAR>hp_top : p ≠ ⊤<VAR>n : ℕ<VAR>f : Fin n → α → β<VAR>hf : ∀ (i : Fin n), MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.UnifTight f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup β<VAR>p : ENNReal<VAR>Finite ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), MeasureTheory.Memℒp (f i) p μ<GOAL>MeasureTheory.UnifTight f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>μ : MeasureTheory.Measure α<VAR>p : ENNReal<VAR>f : ℕ → α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ<VAR>hf_tendsto : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop (nhds 0)<GOAL>MeasureTheory.UnifTight f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>μ : MeasureTheory.Measure α<VAR>p : ENNReal<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hfg : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)<GOAL>MeasureTheory.UnifTight f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>μ : MeasureTheory.Measure α<VAR>p : ENNReal<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hf : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f n)<VAR>hg : MeasureTheory.StronglyMeasurable g<VAR>hg' : MeasureTheory.Memℒp g p μ<VAR>hui : MeasureTheory.UnifIntegrable f p μ<VAR>hut : MeasureTheory.UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>μ : MeasureTheory.Measure α<VAR>f f' : ℕ → α → β<VAR>g g' : α → β<VAR>hff' : ∀ (n : ℕ), f n =ᵐ[μ] f' n<VAR>hgg' : g =ᵐ[μ] g'<VAR>hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f' n x) Filter.atTop (nhds (g' x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>μ : MeasureTheory.Measure α<VAR>p : ENNReal<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>haef : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hg' : MeasureTheory.Memℒp g p μ<VAR>hui : MeasureTheory.UnifIntegrable f p μ<VAR>hut : MeasureTheory.UnifTight f p μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>μ : MeasureTheory.Measure α<VAR>p : ENNReal<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hui : MeasureTheory.UnifIntegrable f p μ<VAR>hut : MeasureTheory.UnifTight f p μ<VAR>hfg : MeasureTheory.TendstoInMeasure μ f Filter.atTop g<GOAL>Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup β<VAR>μ : MeasureTheory.Measure α<VAR>p : ENNReal<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), MeasureTheory.Memℒp (f n) p μ<VAR>hg : MeasureTheory.Memℒp g p μ<GOAL>MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧ MeasureTheory.UnifIntegrable f p μ ∧ MeasureTheory.UnifTight f p μ ↔ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p ≤ q<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.eLpNorm' f p μ ≤ MeasureTheory.eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<GOAL>MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNormEssSup f μ * μ Set.univ ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>p q : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p ≤ q<VAR>μ : MeasureTheory.Measure α<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.eLpNorm' f p μ ≤ MeasureTheory.eLpNorm' f q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>q : ℝ<VAR>hq_pos : 0 < q<VAR>MeasureTheory.IsProbabilityMeasure μ<GOAL>MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>MeasureTheory.IsProbabilityMeasure μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>p q : ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hfq_lt_top : MeasureTheory.eLpNorm' f q μ < ⊤<VAR>hp_nonneg : 0 ≤ p<VAR>hpq : p ≤ q<GOAL>MeasureTheory.eLpNorm' f p μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>μ : MeasureTheory.Measure α<VAR>p q : ℝ≥0∞<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>f : α → E<VAR>hfq : MeasureTheory.Memℒp f q μ<VAR>hpq : p ≤ q<GOAL>MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>g : α → F<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<GOAL>MeasureTheory.eLpNorm (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm f ⊤ μ * MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>μ : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>g : α → F<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<GOAL>MeasureTheory.eLpNorm (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm f p μ * MeasureTheory.eLpNorm g ⊤ μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>MeasureTheory.eLpNorm' (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm' f q μ * MeasureTheory.eLpNorm' g r μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>MeasureTheory.eLpNorm (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm f q μ * MeasureTheory.eLpNorm g r μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m : MeasurableSpace α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>μ : MeasureTheory.Measure α<VAR>f : α → E<VAR>g : α → F<VAR>p q r : ℝ≥0∞<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>b : E → F → G<VAR>h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ‖f x‖ * ‖g x‖<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>MeasureTheory.eLpNorm (fun x => b (f x) (g x)) p μ ≤ MeasureTheory.eLpNorm f q μ * MeasureTheory.eLpNorm g r μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>NormedAddCommGroup E<VAR>MulActionWithZero 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → E<VAR>p : ℝ≥0∞<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>φ : α → 𝕜<GOAL>MeasureTheory.eLpNorm (φ • f) p μ ≤ MeasureTheory.eLpNorm φ ⊤ μ * MeasureTheory.eLpNorm f p μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>NormedAddCommGroup E<VAR>MulActionWithZero 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>φ : α → 𝕜<VAR>hφ : MeasureTheory.AEStronglyMeasurable φ μ<GOAL>MeasureTheory.eLpNorm (φ • f) p μ ≤ MeasureTheory.eLpNorm φ p μ * MeasureTheory.eLpNorm f ⊤ μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>NormedAddCommGroup E<VAR>MulActionWithZero 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>p q r : ℝ<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>φ : α → 𝕜<VAR>hφ : MeasureTheory.AEStronglyMeasurable φ μ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>MeasureTheory.eLpNorm' (φ • f) p μ ≤ MeasureTheory.eLpNorm' φ q μ * MeasureTheory.eLpNorm' f r μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>NormedAddCommGroup E<VAR>MulActionWithZero 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>p q r : ℝ≥0∞<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>φ : α → 𝕜<VAR>hφ : MeasureTheory.AEStronglyMeasurable φ μ<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>MeasureTheory.eLpNorm (φ • f) p μ ≤ MeasureTheory.eLpNorm φ q μ * MeasureTheory.eLpNorm f r μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>NormedAddCommGroup E<VAR>MulActionWithZero 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>p q r : ℝ≥0∞<VAR>f : α → E<VAR>φ : α → 𝕜<VAR>hf : MeasureTheory.Memℒp f r μ<VAR>hφ : MeasureTheory.Memℒp φ q μ<VAR>hpqr : 1 / p = 1 / q + 1 / r<GOAL>MeasureTheory.Memℒp (φ • f) p μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>NormedAddCommGroup E<VAR>MulActionWithZero 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>φ : α → 𝕜<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hφ : MeasureTheory.Memℒp φ ⊤ μ<GOAL>MeasureTheory.Memℒp (φ • f) p μ
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedRing 𝕜<VAR>NormedAddCommGroup E<VAR>MulActionWithZero 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>φ : α → 𝕜<VAR>hf : MeasureTheory.Memℒp f ⊤ μ<VAR>hφ : MeasureTheory.Memℒp φ p μ<GOAL>MeasureTheory.Memℒp (φ • f) p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<GOAL>μ ∅ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>μ s ≤ μ t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : μ t = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>hs : μ s ≠ 0<GOAL>0 < μ t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>Countable ι<VAR>s : ι → Set α<GOAL>μ (⋃ i, s i) ≤ ∑' (i : ι), μ (s i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>I : Set ι<VAR>μ : F<VAR>hI : I.Countable<VAR>s : ι → Set α<GOAL>μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>I : Finset ι<VAR>s : ι → Set α<GOAL>μ (⋃ i ∈ I, s i) ≤ ∑ i ∈ I, μ (s i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>Fintype ι<VAR>μ : F<VAR>s : ι → Set α<GOAL>μ (⋃ i, s i) ≤ ∑ i : ι, μ (s i)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>μ (s ∪ t) ≤ μ s + μ t
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>μ s ≤ μ (s ∩ t) + μ (s \ t)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>ht : μ t = 0<GOAL>μ (s \ t) = μ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>I : Set ι<VAR>hI : I.Countable<VAR>s : ι → Set α<GOAL>μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>S : Set (Set α)<VAR>hS : S.Countable<GOAL>μ (⋃₀ S) = 0 ↔ ∀ s ∈ S, μ s = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>ι : Sort u_4<VAR>Countable ι<VAR>s : ι → Set α<GOAL>μ (⋃ i, s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>hs : μ s = 0<VAR>ht : μ t = 0<GOAL>μ (s ∪ t) = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>s : Set α<VAR>hs : s.Countable<GOAL>μ s = 0 ↔ ∀ x ∈ s, μ {x} = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>ι : Type u_4<VAR>μ : F<VAR>s : ι → Set α<VAR>l : Filter ι<VAR>l.NeBot<VAR>h0 : Filter.Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (𝓝 0)<GOAL>μ (⋃ n, s n) = ⨆ n, μ (s n)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, μ u = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>FunLike F (Set α) ℝ≥0∞<VAR>MeasureTheory.OuterMeasureClass F α<VAR>μ : F<VAR>TopologicalSpace α<VAR>SecondCountableTopology α<VAR>s : Set α<VAR>hs : μ s ≠ 0<GOAL>∃ x ∈ s, ∀ t ∈ 𝓝[s] x, 0 < μ t
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<GOAL>m ∅ = 0
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>s₁ s₂ : Set α<VAR>h : s₁ ⊆ s₂<GOAL>m s₁ ≤ m s₂
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : m t = 0<GOAL>m s = 0
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>a b : Set α<VAR>hs : a ⊆ b<VAR>hnz : m a ≠ 0<GOAL>0 < m b
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>β : Type u_3<VAR>Countable β<VAR>s : β → Set α<GOAL>m (⋃ i, s i) ≤ ∑' (i : β), m (s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : Set β<VAR>hs : s.Countable<VAR>t : β → Set α<GOAL>m (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, m (t i) = 0
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>S : Set (Set α)<VAR>hS : S.Countable<GOAL>m (⋃₀ S) = 0 ↔ ∀ s ∈ S, m s = 0
<VAR>α : Type u_1<VAR>ι : Sort u_3<VAR>Countable ι<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : ι → Set α<GOAL>m (⋃ i, s i) = 0 ↔ ∀ (i : ι), m (s i) = 0
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>ι : Prop<VAR>s : ι → Set α<GOAL>m (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), m (s i) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasureTheory.OuterMeasure α<VAR>s : β → Set α<VAR>t : Finset β<GOAL>m (⋃ i ∈ t, s i) ≤ ∑ i ∈ t, m (s i)
<VAR>α : Type u_1<VAR>m : MeasureTheory.OuterMeasure α<VAR>s₁ s₂ : Set α<GOAL>m (s₁ ∪ s₂) ≤ m s₁ + m s₂