ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm' (fun a => ‖f a‖) q μ = MeasureTheory.eLpNorm' f q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm (fun x => ‖f x‖) p μ = MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>p q : ℝ<VAR>hq_pos : 0 < q<GOAL>MeasureTheory.eLpNorm' (fun x => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm' f (p * q) μ ^ q
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hq_pos : 0 < q<GOAL>MeasureTheory.eLpNorm (fun x => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm f (p * ENNReal.ofReal q) μ ^ q
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f g : α → F<VAR>hfg : f =ᵐ[μ] g<GOAL>MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f g : α → E<VAR>hfg : f =ᵐ[μ] g<GOAL>MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp 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 : α → E<VAR>hfg : f =ᵐ[μ] g<VAR>hf_Lp : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp g 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 : α → F<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖<GOAL>MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>g : α → ℝ<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ g a<GOAL>MeasureTheory.Memℒp f 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 : α → F<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖<GOAL>MeasureTheory.Memℒp g 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 : α → F<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hg : MeasureTheory.AEStronglyMeasurable g μ<VAR>h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖<GOAL>MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp g p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>MeasureTheory.Memℒp f ⊤ μ
<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>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hμν : ν ≤ μ<VAR>hq : 0 ≤ q<GOAL>MeasureTheory.eLpNorm' f q ν ≤ MeasureTheory.eLpNorm' f q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hμν : ν ≪ μ<GOAL>MeasureTheory.eLpNormEssSup f ν ≤ MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hμν : ν ≤ μ<GOAL>MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hμν : ν ≤ μ<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp f p ν
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>MeasureTheory.eLpNorm f p (μ.restrict s) ≤ MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>s : Set α<VAR>f : α → F<VAR>hsf : Function.support f ⊆ s<GOAL>MeasureTheory.eLpNorm f p (μ.restrict s) = 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>s : Set α<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp f p (μ.restrict s)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>p : ℝ<VAR>hp : 0 ≤ p<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm' f p (c • μ) = c ^ (1 / p) * MeasureTheory.eLpNorm' f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>MeasureTheory.eLpNormEssSup f (c • μ) = MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>f : α → F<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>c : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f 1 (c • μ) = c * MeasureTheory.eLpNorm f 1 μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>μ' : MeasureTheory.Measure α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hμ'_le : μ' ≤ c • μ<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp f p μ'
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>c : ℝ≥0∞<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>hc : c ≠ ⊤<GOAL>MeasureTheory.Memℒp f p (c • μ)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>μ ν : MeasureTheory.Measure α<GOAL>MeasureTheory.eLpNorm f 1 (μ + ν) = MeasureTheory.eLpNorm f 1 μ + MeasureTheory.eLpNorm f 1 ν
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>μ ν : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm f p (μ + ν)
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>μ ν : MeasureTheory.Measure α<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f p ν ≤ MeasureTheory.eLpNorm f p (μ + ν)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>h : MeasureTheory.Memℒp f p (μ + ν)<GOAL>MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ ν : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>h : MeasureTheory.Memℒp f p (μ + ν)<GOAL>MeasureTheory.Memℒp f p ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>h : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (fun x => ‖f x‖) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.Memℒp (fun x => ‖f x‖) p μ ↔ MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<VAR>hq0_lt : 0 < q<VAR>hf_zero : f =ᵐ[μ] 0<GOAL>MeasureTheory.eLpNorm' f q μ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>hq0_ne : q ≠ 0<VAR>hμ : μ ≠ 0<VAR>f : α → F<VAR>hf_zero : f =ᵐ[μ] 0<GOAL>MeasureTheory.eLpNorm' f q μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hq0 : 0 ≤ q<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>h : MeasureTheory.eLpNorm' f q μ = 0<GOAL>f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>hq0_lt : 0 < q<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<GOAL>MeasureTheory.eLpNorm' f q μ = 0 ↔ f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup F<GOAL>∀ {x : MeasurableSpace α} (f : α → F) (μ : MeasureTheory.Measure α), ∀ᵐ (x_1 : α) ∂μ, ↑‖f x_1‖₊ ≤ MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>MeasureTheory.eLpNormEssSup 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 : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>h0 : p ≠ 0<GOAL>MeasureTheory.eLpNorm f p μ = 0 ↔ f =ᵐ[μ] 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>∀ᵐ (y : α) ∂μ, ↑‖f y‖₊ ≤ MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>f : α → F<GOAL>μ {y | MeasureTheory.eLpNormEssSup f μ < ↑‖f y‖₊} = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>f g : α → E<VAR>DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.eLpNormEssSup (s.piecewise f g) μ = max (MeasureTheory.eLpNormEssSup f (μ.restrict s)) (MeasureTheory.eLpNormEssSup g (μ.restrict sᶜ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>f g : α → E<VAR>DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.eLpNorm (s.piecewise f g) ⊤ μ = max (MeasureTheory.eLpNorm f ⊤ (μ.restrict s)) (MeasureTheory.eLpNorm g ⊤ (μ.restrict sᶜ))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ 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>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) 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>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Memℒp (g ∘ f) 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>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>hg : MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>MeasureTheory.Memℒp (g ∘ f) 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>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>ν : MeasureTheory.Measure β<VAR>hg : MeasureTheory.AEStronglyMeasurable g ν<VAR>hf : MeasureTheory.MeasurePreserving f μ ν<GOAL>MeasureTheory.eLpNorm (g ∘ f) p μ = MeasureTheory.eLpNorm g p ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>ν : MeasureTheory.Measure β<VAR>g : β →ₘ[ν] E<VAR>hf : MeasureTheory.MeasurePreserving f μ ν<GOAL>MeasureTheory.eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = MeasureTheory.eLpNorm (↑g) p ν
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>ν : MeasureTheory.Measure β<VAR>hg : MeasureTheory.Memℒp g p ν<VAR>hf : MeasureTheory.MeasurePreserving f μ ν<GOAL>MeasureTheory.Memℒp (g ∘ f) p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → F<VAR>hf : MeasurableEmbedding f<GOAL>MeasureTheory.eLpNormEssSup g (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNormEssSup (g ∘ f) μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → F<VAR>hf : MeasurableEmbedding f<GOAL>MeasureTheory.eLpNorm g p (MeasureTheory.Measure.map f μ) = MeasureTheory.eLpNorm (g ∘ f) p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → F<VAR>hf : MeasurableEmbedding f<GOAL>MeasureTheory.Memℒp g p (MeasureTheory.Measure.map f μ) ↔ MeasureTheory.Memℒp (g ∘ f) p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α ≃ᵐ β<VAR>g : β → F<GOAL>MeasureTheory.Memℒp g p (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.Memℒp (g ∘ ⇑f) p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ<VAR>hp : 0 < p<GOAL>MeasureTheory.eLpNorm' f p μ ≤ c • MeasureTheory.eLpNorm' g p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<GOAL>MeasureTheory.eLpNormEssSup f μ ≤ c • MeasureTheory.eLpNormEssSup g μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ≥0<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f p μ ≤ c • MeasureTheory.eLpNorm g p μ
<VAR>α : Type u_5<VAR>LinearOrderedSemiring α<VAR>a b c : α<VAR>ha : 0 ≤ a<VAR>hb : b < 0<VAR>hc : 0 ≤ c<GOAL>a ≤ b * c ↔ a = 0 ∧ c = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖<VAR>hc : c < 0<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f p μ = 0 ∧ MeasureTheory.eLpNorm g p μ = 0
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>c : ℝ<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖<VAR>p : ℝ≥0∞<GOAL>MeasureTheory.eLpNorm f p μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm g 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 : α → F<VAR>c : ℝ≥0<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊<GOAL>MeasureTheory.Memℒp f 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 : α → F<VAR>c : ℝ<VAR>hg : MeasureTheory.Memℒp g p μ<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖<GOAL>MeasureTheory.Memℒp f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>MulActionWithZero 𝕜 F<VAR>BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<VAR>hq_pos : 0 < q<GOAL>MeasureTheory.eLpNorm' (c • f) q μ ≤ ‖c‖₊ • MeasureTheory.eLpNorm' f q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>MulActionWithZero 𝕜 F<VAR>BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<GOAL>MeasureTheory.eLpNormEssSup (c • f) μ ≤ ‖c‖₊ • MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>MulActionWithZero 𝕜 F<VAR>BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm (c • f) p μ ≤ ‖c‖₊ • 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>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>MulActionWithZero 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>c : 𝕜<GOAL>MeasureTheory.Memℒp (c • f) p μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>R : Type u_6<VAR>NormedRing R<VAR>f : α → R<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>c : R<GOAL>MeasureTheory.Memℒp (fun x => c * f x) p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>q : ℝ<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NormedDivisionRing 𝕜<VAR>Module 𝕜 F<VAR>BoundedSMul 𝕜 F<VAR>f : α → F<VAR>c : 𝕜<VAR>hq_pos : 0 < q<GOAL>MeasureTheory.eLpNorm' (c • f) q μ = ‖c‖₊ • MeasureTheory.eLpNorm' f q μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NormedDivisionRing 𝕜<VAR>Module 𝕜 F<VAR>BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<GOAL>MeasureTheory.eLpNormEssSup (c • f) μ = ↑‖c‖₊ * MeasureTheory.eLpNormEssSup f μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NormedDivisionRing 𝕜<VAR>Module 𝕜 F<VAR>BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<GOAL>MeasureTheory.eLpNorm (c • f) p μ = ↑‖c‖₊ * MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>f : α → F<VAR>C : ℝ≥0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊<GOAL>C • μ s ^ (1 / p.toReal) ≤ MeasureTheory.eLpNorm f p μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (fun x => RCLike.re (f x)) p μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_5<VAR>RCLike 𝕜<VAR>f : α → 𝕜<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (fun x => RCLike.im (f x)) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R<GOAL>∀ᵐ (x : α) ∂μ, Filter.liminf (fun n => ↑‖f n x‖₊ ^ p.toReal) Filter.atTop < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasurableSpace E<VAR>OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>hp : p ≠ 0<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R<GOAL>∀ᵐ (x : α) ∂μ, Filter.liminf (fun n => ↑‖f n x‖₊) Filter.atTop < ⊤
<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>MeasurableSpace X<VAR>OpensMeasurableSpace X<VAR>f : X → E<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>μ : MeasureTheory.Measure X<GOAL>MeasureTheory.Memℒp f ⊤ μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_5<VAR>NormedAddCommGroup β<VAR>hp_top : p ≠ ⊤<VAR>f : α → β<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ s, MeasurableSet s ∧ μ s < ⊤ ∧ MeasureTheory.eLpNorm (sᶜ.indicator f) p μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>f : α → β<VAR>s : Set β<GOAL>MeasurableSet s ↔ MeasurableSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<GOAL>MeasurableSpace.map id m = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>f : α → β<VAR>g : β → γ<GOAL>MeasurableSpace.map g (MeasurableSpace.map f m) = MeasurableSpace.map (g ∘ f) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace β<VAR>f : α → β<GOAL>MeasurableSpace.comap f m = MeasurableSpace.generateFrom {t | ∃ s, MeasurableSet s ∧ f ⁻¹' s = t}
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<GOAL>MeasurableSpace.comap id m = m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>m : MeasurableSpace α<VAR>f : β → α<VAR>g : γ → β<GOAL>MeasurableSpace.comap g (MeasurableSpace.comap f m) = MeasurableSpace.comap (f ∘ g) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>m' : MeasurableSpace β<VAR>f : α → β<GOAL>MeasurableSpace.comap f m' ≤ m ↔ m' ≤ MeasurableSpace.map f m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>GaloisConnection (MeasurableSpace.comap f) (MeasurableSpace.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m₁ m₂ : MeasurableSpace α<VAR>f : α → β<VAR>h : m₁ ≤ m₂<GOAL>MeasurableSpace.map f m₁ ≤ MeasurableSpace.map f m₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Monotone (MeasurableSpace.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m₁ m₂ : MeasurableSpace α<VAR>g : β → α<VAR>h : m₁ ≤ m₂<GOAL>MeasurableSpace.comap g m₁ ≤ MeasurableSpace.comap g m₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : β → α<GOAL>Monotone (MeasurableSpace.comap g)