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>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<GOAL>↑‖MeasureTheory.indicatorConstLp p hs hμs c‖₊ ≤ ↑‖c‖₊ * μ s ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>edist (MeasureTheory.indicatorConstLp p hs hμs c) (MeasureTheory.indicatorConstLp p ht hμt c) = ↑‖MeasureTheory.indicatorConstLp p ⋯ ⋯ c‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>dist (MeasureTheory.indicatorConstLp p hs hμs c) (MeasureTheory.indicatorConstLp p ht hμt c) = ‖MeasureTheory.indicatorConstLp p ⋯ ⋯ c‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>c : E<VAR>hp₁ : Fact (1 ≤ p)<VAR>β : Type u_5<VAR>l : Filter β<VAR>t : β → Set α<VAR>ht : ∀ (b : β), MeasurableSet (t b)<VAR>hμt : ∀ (b : β), μ (t b) ≠ ⊤<VAR>hp : p ≠ ⊤<VAR>h : Filter.Tendsto (fun b => μ (t b ∆ s)) l (𝓝 0)<GOAL>Filter.Tendsto (fun b => MeasureTheory.indicatorConstLp p ⋯ ⋯ c) l (𝓝 (MeasureTheory.indicatorConstLp p hs hμs c))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>c : E<VAR>Fact (1 ≤ p)<VAR>X : Type u_5<VAR>TopologicalSpace X<VAR>s : X → Set α<VAR>hs : ∀ (x : X), MeasurableSet (s x)<VAR>hμs : ∀ (x : X), μ (s x) ≠ ⊤<VAR>hp : p ≠ ⊤<VAR>h : ∀ (x : X), Filter.Tendsto (fun y => μ (s y ∆ s x)) (𝓝 x) (𝓝 0)<GOAL>Continuous fun x => MeasureTheory.indicatorConstLp p ⋯ ⋯ c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>c : E<GOAL>MeasureTheory.indicatorConstLp p ⋯ ⋯ c = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>hsμ : μ s ≠ ⊤<VAR>ht : MeasurableSet t<VAR>htμ : μ t ≠ ⊤<VAR>c : E<VAR>hc : c ≠ 0<GOAL>MeasureTheory.indicatorConstLp p hs hsμ c = MeasureTheory.indicatorConstLp p ht htμ c ↔ s =ᵐ[μ] t
<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>h : Disjoint (Function.support f) (Function.support g)<VAR>hf : MeasureTheory.StronglyMeasurable f<VAR>hg : MeasureTheory.StronglyMeasurable g<GOAL>MeasureTheory.Memℒp (f + g) p μ ↔ 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>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>c : E<GOAL>MeasureTheory.indicatorConstLp p ⋯ ⋯ c = MeasureTheory.indicatorConstLp p hs hμs c + MeasureTheory.indicatorConstLp p ht hμt c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : E<GOAL>↑↑((MeasureTheory.Lp.const p μ) c) =ᵐ[μ] Function.const α c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : E<GOAL>↑((MeasureTheory.Lp.const p μ) c) = MeasureTheory.AEEqFun.const α c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : E<GOAL>MeasureTheory.Memℒp.toLp (fun x => c) ⋯ = (MeasureTheory.Lp.const p μ) c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : E<GOAL>MeasureTheory.indicatorConstLp p ⋯ ⋯ c = (MeasureTheory.Lp.const p μ) c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : E<VAR>NeZero μ<VAR>hp_zero : p ≠ 0<GOAL>‖(MeasureTheory.Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : E<VAR>hp_zero : p ≠ 0<VAR>hp_top : p ≠ ⊤<GOAL>‖(MeasureTheory.Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>c : E<GOAL>‖(MeasureTheory.Lp.const p μ) c‖ ≤ ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>a : E<GOAL>(MeasureTheory.Lp.constₗ p μ 𝕜) a = (MeasureTheory.Lp.const p μ) a
<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>𝕜 : Type u_5<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>Fact (1 ≤ p)<VAR>a : E<GOAL>(MeasureTheory.Lp.constL p μ 𝕜) a = (MeasureTheory.Lp.const p μ) a
<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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>Fact (1 ≤ p)<GOAL>‖MeasureTheory.Lp.constL p μ 𝕜‖ ≤ (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<VAR>q : ℝ≥0∞<GOAL>MeasureTheory.Memℒp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>q : ℝ≥0∞<VAR>f : α → E<VAR>hf : MeasureTheory.AEStronglyMeasurable f μ<VAR>q_zero : q ≠ 0<VAR>q_top : q ≠ ⊤<GOAL>MeasureTheory.Memℒp (fun x => ‖f x‖ ^ q.toReal) (p / q) μ ↔ 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>hf : MeasureTheory.Memℒp f p μ<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>MeasureTheory.Memℒp (fun x => ‖f x‖ ^ p.toReal) 1 μ
<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>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>g : β →ₘ[μb] E<VAR>hg : g ∈ MeasureTheory.Lp E p μb<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>g.compMeasurePreserving f hf ∈ MeasureTheory.Lp E p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>β : Type u_5<VAR>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : ↥(MeasureTheory.Lp E p μb)<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>↑((MeasureTheory.Lp.compMeasurePreserving f hf) g) = (↑g).compMeasurePreserving f hf
<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>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : ↥(MeasureTheory.Lp E p μb)<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>↑↑((MeasureTheory.Lp.compMeasurePreserving f hf) g) =ᵐ[μ] ↑↑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>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : ↥(MeasureTheory.Lp E p μb)<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>‖(MeasureTheory.Lp.compMeasurePreserving f hf) g‖ = ‖g‖
<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>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>Fact (1 ≤ p)<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>Isometry ⇑(MeasureTheory.Lp.compMeasurePreserving f hf)
<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>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>g : β → E<VAR>hg : MeasureTheory.Memℒp g p μb<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>(MeasureTheory.Lp.compMeasurePreserving f hf) (MeasureTheory.Memℒp.toLp g hg) = MeasureTheory.Memℒp.toLp (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>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>f : α → β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hμs : μb s ≠ ⊤<VAR>c : E<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>(MeasureTheory.Lp.compMeasurePreserving f hf) (MeasureTheory.indicatorConstLp p hs hμs c) = MeasureTheory.indicatorConstLp p ⋯ ⋯ c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>β : Type u_5<VAR>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>𝕜 : Type u_6<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>∀ (a : ↥(MeasureTheory.Lp E p μb)), (MeasureTheory.Lp.compMeasurePreservingₗ 𝕜 f hf) a = (↑(MeasureTheory.Lp.compMeasurePreserving f hf)).toFun a
<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>MeasurableSpace β<VAR>μb : MeasureTheory.Measure β<VAR>𝕜 : Type u_6<VAR>NormedRing 𝕜<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>Fact (1 ≤ p)<VAR>f : α → β<VAR>hf : MeasureTheory.MeasurePreserving f μ μb<GOAL>∀ (a : ↥(MeasureTheory.Lp E p μb)), ↑((MeasureTheory.Lp.compMeasurePreservingₗᵢ 𝕜 f hf) a) = (↑a).compMeasurePreserving f hf
<VAR>p : ℝ≥0∞<VAR>α : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>K : ℝ≥0<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : E → F<VAR>hg : LipschitzWith K g<VAR>g0 : g 0 = 0<VAR>hL : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (g ∘ f) p μ
<VAR>p : ℝ≥0∞<VAR>α : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>K' : ℝ≥0<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : E → F<VAR>hL : MeasureTheory.Memℒp (g ∘ f) p μ<VAR>hg : UniformContinuous g<VAR>hg' : AntilipschitzWith K' g<VAR>g0 : g 0 = 0<GOAL>MeasureTheory.Memℒp f p μ
<VAR>p : ℝ≥0∞<VAR>α : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>K K' : ℝ≥0<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>f : α → E<VAR>g : E → F<VAR>hg : LipschitzWith K g<VAR>hg' : AntilipschitzWith K' g<VAR>g0 : g 0 = 0<GOAL>MeasureTheory.Memℒp (g ∘ f) p μ ↔ 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>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(hg.compLp g0 f) =ᵐ[μ] g ∘ ↑↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<GOAL>hg.compLp g0 0 = 0
<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>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>f f' : ↥(MeasureTheory.Lp E p μ)<GOAL>‖hg.compLp g0 f - hg.compLp g0 f'‖ ≤ ↑c * ‖f - f'‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖hg.compLp g0 f‖ ≤ ↑c * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>g : E → F<VAR>c : ℝ≥0<VAR>Fact (1 ≤ p)<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<GOAL>LipschitzWith c (hg.compLp g0)
<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>g : E → F<VAR>c : ℝ≥0<VAR>Fact (1 ≤ p)<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<GOAL>Continuous (hg.compLp g0)
<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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] F<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>∀ᵐ (a : α) ∂μ, ↑↑(L.compLp f) a = L (↑↑f a)
<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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] F<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑(L.compLp f) =ᵐ[μ] fun a => L (↑↑f a)
<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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] F<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>MeasureTheory.Memℒp (⇑L ∘ ↑↑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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] F<VAR>f : α → E<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (⇑L ∘ f) p μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>K : Type u_6<VAR>RCLike K<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (fun x => ↑(f x)) p μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>K : Type u_6<VAR>RCLike K<VAR>f : α → K<GOAL>MeasureTheory.Memℒp (fun x => RCLike.re (f x)) p μ ∧ MeasureTheory.Memℒp (fun x => RCLike.im (f x)) p μ ↔ 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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>L L' : E →L[𝕜] F<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>(L + L').compLp f = L.compLp f + L'.compLp f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>𝕜' : Type u_6<VAR>NormedRing 𝕜'<VAR>Module 𝕜' F<VAR>BoundedSMul 𝕜' F<VAR>SMulCommClass 𝕜 𝕜' F<VAR>c : 𝕜'<VAR>L : E →L[𝕜] F<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>(c • L).compLp f = c • L.compLp f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>L : E →L[𝕜] F<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>‖L.compLp f‖ ≤ ‖L‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>Fact (1 ≤ p)<VAR>L : E →L[𝕜] F<VAR>f : ↥(MeasureTheory.Lp E p μ)<GOAL>↑↑((ContinuousLinearMap.compLpL p μ L) f) =ᵐ[μ] fun a => L (↑↑f a)
<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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>Fact (1 ≤ p)<VAR>L L' : E →L[𝕜] F<GOAL>ContinuousLinearMap.compLpL p μ (L + L') = ContinuousLinearMap.compLpL p μ L + ContinuousLinearMap.compLpL p μ L'
<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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>Fact (1 ≤ p)<VAR>𝕜' : Type u_6<VAR>NormedRing 𝕜'<VAR>Module 𝕜' F<VAR>BoundedSMul 𝕜' F<VAR>SMulCommClass 𝕜 𝕜' F<VAR>c : 𝕜'<VAR>L : E →L[𝕜] F<GOAL>ContinuousLinearMap.compLpL p μ (c • L) = c • ContinuousLinearMap.compLpL p μ L
<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>𝕜 : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>Fact (1 ≤ p)<VAR>L : E →L[𝕜] F<GOAL>‖ContinuousLinearMap.compLpL p μ L‖ ≤ ‖L‖
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>s : Set α<VAR>NormedSpace ℝ F<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : F<GOAL>MeasureTheory.indicatorConstLp 2 hs hμs x = (ContinuousLinearMap.toSpanSingleton ℝ x).compLp (MeasureTheory.indicatorConstLp 2 hs hμs 1)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (fun x => max (f x) 0) p μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : α → ℝ<VAR>hf : MeasureTheory.Memℒp f p μ<GOAL>MeasureTheory.Memℒp (fun x => max (-f x) 0) p μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp ℝ p μ)<GOAL>↑(MeasureTheory.Lp.posPart f) = (↑f).posPart
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp ℝ p μ)<GOAL>↑↑(MeasureTheory.Lp.posPart f) =ᵐ[μ] fun a => max (↑↑f a) 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp ℝ p μ)<GOAL>∀ᵐ (a : α) ∂μ, ↑↑(MeasureTheory.Lp.negPart f) a = max (-↑↑f a) 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>f : ↥(MeasureTheory.Lp ℝ p μ)<GOAL>∀ᵐ (a : α) ∂μ, ↑↑(MeasureTheory.Lp.negPart f) a = -min (↑↑f a) 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<GOAL>Continuous fun f => MeasureTheory.Lp.posPart f
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>Fact (1 ≤ p)<GOAL>Continuous fun f => MeasureTheory.Lp.negPart f
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>ι : Type u_5<VAR>Nonempty ι<VAR>LinearOrder ι<VAR>f : ι → α → G<VAR>p : ℝ<VAR>hp_nonneg : 0 ≤ p<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (f_lim x))<GOAL>MeasureTheory.eLpNorm' f_lim p μ = (∫⁻ (a : α), Filter.liminf (fun m => ↑‖f m a‖₊ ^ p) Filter.atTop ∂μ) ^ (1 / p)
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>p : ℝ<VAR>hp_pos : 0 < p<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (f_lim x))<GOAL>MeasureTheory.eLpNorm' f_lim p μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm' (f n) p μ) Filter.atTop
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup G<VAR>ι : Type u_5<VAR>Nonempty ι<VAR>LinearOrder ι<VAR>f : ι → α → G<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (f_lim x))<GOAL>MeasureTheory.eLpNorm f_lim ⊤ μ = essSup (fun x => Filter.liminf (fun m => ↑‖f m x‖₊) Filter.atTop) μ
<VAR>α : Type u_1<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>NormedAddCommGroup F<VAR>ι : Type u_5<VAR>Nonempty ι<VAR>Countable ι<VAR>LinearOrder ι<VAR>f : ι → α → F<VAR>f_lim : α → F<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (f_lim x))<GOAL>MeasureTheory.eLpNorm f_lim ⊤ μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm (f n) ⊤ μ) Filter.atTop
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>f : ℕ → α → E<VAR>hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>f_lim : α → E<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (f_lim x))<GOAL>MeasureTheory.eLpNorm f_lim p μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop
<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>fi : Filter ι<VAR>Fact (1 ≤ p)<VAR>f : ι → ↥(MeasureTheory.Lp E p μ)<VAR>f_lim : ↥(MeasureTheory.Lp E p μ)<GOAL>Filter.Tendsto f fi (𝓝 f_lim) ↔ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (𝓝 0)
<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>fi : Filter ι<VAR>Fact (1 ≤ p)<VAR>f : ι → ↥(MeasureTheory.Lp E p μ)<VAR>f_lim : α → E<VAR>f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ<GOAL>Filter.Tendsto f fi (𝓝 (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp)) ↔ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
<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>fi : Filter ι<VAR>Fact (1 ≤ p)<VAR>f : ι → α → E<VAR>f_ℒp : ∀ (n : ι), MeasureTheory.Memℒp (f n) p μ<VAR>f_lim : α → E<VAR>f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ<GOAL>Filter.Tendsto (fun n => MeasureTheory.Memℒp.toLp (f n) ⋯) fi (𝓝 (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp)) ↔ Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) fi (𝓝 0)
<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>fi : Filter ι<VAR>Fact (1 ≤ p)<VAR>f : ι → ↥(MeasureTheory.Lp E p μ)<VAR>f_lim : α → E<VAR>f_lim_ℒp : MeasureTheory.Memℒp f_lim p μ<VAR>h_tendsto : Filter.Tendsto (fun n => MeasureTheory.eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)<GOAL>Filter.Tendsto f fi (𝓝 (MeasureTheory.Memℒp.toLp f_lim f_lim_ℒp))