ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>g g' : α → 𝕜 → F<VAR>t : Set 𝕜<VAR>y₀ y : 𝕜<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun x => g x y₀<VAR>hy : y ∈ t<GOAL>Summable fun n => g n y
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>s : Set E<VAR>x₀ x : E<VAR>hu : Summable u<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n<VAR>hx₀ : x₀ ∈ s<VAR>hf0 : Summable fun n => f n x₀<VAR>hx : x ∈ s<GOAL>HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>g g' : α → 𝕜 → F<VAR>t : Set 𝕜<VAR>y₀ y : 𝕜<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun n => g n y₀<VAR>hy : y ∈ t<GOAL>HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>x₀ : E<VAR>hu : Summable u<VAR>hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n<VAR>hf0 : Summable fun n => f n x₀<VAR>x : E<GOAL>Summable fun n => f n x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>g g' : α → 𝕜 → F<VAR>y₀ : 𝕜<VAR>hu : Summable u<VAR>hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n<VAR>hg0 : Summable fun n => g n y₀<VAR>y : 𝕜<GOAL>Summable fun n => g n y
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>x₀ : E<VAR>hu : Summable u<VAR>hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n<VAR>hf0 : Summable fun n => f n x₀<VAR>x : E<GOAL>HasFDerivAt (fun y => ∑' (n : α), f n y) (∑' (n : α), f' n x) x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>g g' : α → 𝕜 → F<VAR>y₀ : 𝕜<VAR>hu : Summable u<VAR>hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n<VAR>hg0 : Summable fun n => g n y₀<VAR>y : 𝕜<GOAL>HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>hu : Summable u<VAR>hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n<GOAL>Differentiable 𝕜 fun y => ∑' (n : α), f n y
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>g g' : α → 𝕜 → F<VAR>hu : Summable u<VAR>hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n<GOAL>Differentiable 𝕜 fun z => ∑' (n : α), g n z
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>x₀ : E<VAR>hu : Summable u<VAR>hf : ∀ (n : α), Differentiable 𝕜 (f n)<VAR>hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n<VAR>hf0 : Summable fun n => f n x₀<VAR>x : E<GOAL>fderiv 𝕜 (fun y => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>g : α → 𝕜 → F<VAR>y₀ : 𝕜<VAR>hu : Summable u<VAR>hg : ∀ (n : α), Differentiable 𝕜 (g n)<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n<VAR>hg0 : Summable fun n => g n y₀<VAR>y : 𝕜<GOAL>deriv (fun z => ∑' (n : α), g n z) y = ∑' (n : α), deriv (g n) y
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>x₀ : E<VAR>hu : Summable u<VAR>hf : ∀ (n : α), Differentiable 𝕜 (f n)<VAR>hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n<VAR>hf0 : Summable fun n => f n x₀<GOAL>(fderiv 𝕜 fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), fderiv 𝕜 (f n) x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>g : α → 𝕜 → F<VAR>y₀ : 𝕜<VAR>hu : Summable u<VAR>hg : ∀ (n : α), Differentiable 𝕜 (g n)<VAR>hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n<VAR>hg0 : Summable fun n => g n y₀<GOAL>(deriv fun y => ∑' (n : α), g n y) = fun y => ∑' (n : α), deriv (g n) y
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>v : ℕ → α → ℝ<VAR>N : ℕ∞<VAR>hf : ∀ (i : α), ContDiff 𝕜 N (f i)<VAR>hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)<VAR>h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i<VAR>k : ℕ<VAR>hk : ↑k ≤ N<GOAL>(iteratedFDeriv 𝕜 k fun y => ∑' (n : α), f n y) = fun x => ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>v : ℕ → α → ℝ<VAR>N : ℕ∞<VAR>hf : ∀ (i : α), ContDiff 𝕜 N (f i)<VAR>hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)<VAR>h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i<VAR>k : ℕ<VAR>hk : ↑k ≤ N<VAR>x : E<GOAL>iteratedFDeriv 𝕜 k (fun y => ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>v : ℕ → α → ℝ<VAR>N : ℕ∞<VAR>hf : ∀ (i : α), ContDiff 𝕜 N (f i)<VAR>hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)<VAR>h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i<GOAL>ContDiff 𝕜 N fun x => ∑' (i : α), f i x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>v : ℕ → α → ℝ<VAR>N : ℕ∞<VAR>hf : ∀ (i : α), ContDiff 𝕜 N (f i)<VAR>hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)<VAR>h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in Filter.cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i<GOAL>ContDiff 𝕜 N fun x => ∑' (i : α), f i x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>f' : E ≃L[ℝ] F<VAR>c : ℝ≥0<VAR>hf : ApproximatesLinearOn f (↑f') s c<VAR>hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑f'.symm‖₊⁻¹<GOAL>∃ g, Set.EqOn f (⇑g) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' a : 𝕜<VAR>hf : HasStrictDerivAt f f' a<VAR>hf' : f' ≠ 0<GOAL>Filter.map f (𝓝 a) = 𝓝 (f a)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' a : 𝕜<VAR>hf : HasStrictDerivAt f f' a<VAR>hf' : f' ≠ 0<GOAL>HasStrictDerivAt (HasStrictDerivAt.localInverse f f' a hf hf') f'⁻¹ (f a)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' a : 𝕜<VAR>hf : HasStrictDerivAt f f' a<VAR>hf' : f' ≠ 0<VAR>g : 𝕜 → 𝕜<VAR>hg : ∀ᶠ (x : 𝕜) in 𝓝 a, g (f x) = x<GOAL>HasStrictDerivAt g f'⁻¹ (f a)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>f f' : 𝕜 → 𝕜<VAR>hf : ∀ (x : 𝕜), HasStrictDerivAt f (f' x) x<VAR>h0 : ∀ (x : 𝕜), f' x ≠ 0<GOAL>IsOpenMap f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<GOAL>Memℓp f 0 ↔ {i | f i ≠ 0}.Finite
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : {i | f i ≠ 0}.Finite<GOAL>Memℓp f 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<GOAL>Memℓp f ⊤ ↔ BddAbove (Set.range fun i => ‖f i‖)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : BddAbove (Set.range fun i => ‖f i‖)<GOAL>Memℓp f ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : (i : α) → E i<GOAL>Memℓp f p ↔ Summable fun i => ‖f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Summable fun i => ‖f i‖ ^ p.toReal<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>C : ℝ<VAR>f : (i : α) → E i<VAR>hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<GOAL>Memℓp 0 p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<GOAL>Memℓp (fun i => 0) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f 0<GOAL>{i | f i ≠ 0}.Finite
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f ⊤<GOAL>BddAbove (Set.range fun i => ‖f i‖)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : (i : α) → E i<VAR>hf : Memℓp f p<GOAL>Summable fun i => ‖f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f p<GOAL>Memℓp (-f) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<GOAL>Memℓp (-f) p ↔ Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>f : (i : α) → E i<VAR>hfq : Memℓp f q<VAR>hpq : q ≤ p<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<GOAL>Memℓp (f + g) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f g : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hg : Memℓp g p<GOAL>Memℓp (f - g) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → (i : α) → E i<VAR>hf : ∀ i ∈ s, Memℓp (f i) p<GOAL>Memℓp (fun a => ∑ i ∈ s, f i a) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>NormedRing 𝕜<VAR>(i : α) → Module 𝕜 (E i)<VAR>∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f p<VAR>c : 𝕜<GOAL>Memℓp (c • f) p
<VAR>α : Type u_1<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_3<VAR>NormedRing 𝕜<VAR>f : α → 𝕜<VAR>hf : Memℓp f p<VAR>c : 𝕜<GOAL>Memℓp (fun x => c * f x) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f g : ↥(lp E p)<VAR>h : ↑f = ↑g<GOAL>f = g
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f g : ↥(lp E p)<GOAL>f = g ↔ ↑f = ↑g
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>IsEmpty α<VAR>f : ↥(lp E p)<GOAL>f = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : q ≤ p<GOAL>lp E q ≤ lp E p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>Memℓp (↑f) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>↑(-f) = -↑f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f g : ↥(lp E p)<GOAL>↑(f + g) = ↑f + ↑g
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>f : ι → ↥(lp E p)<VAR>s : Finset ι<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f g : ↥(lp E p)<GOAL>↑(f - g) = ↑f - ↑g
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E 0)<GOAL>‖f‖ = ↑⋯.toFinset.card
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E ⊤)<GOAL>‖f‖ = ⨆ i, ‖↑f i‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>Nonempty α<VAR>f : ↥(lp E ⊤)<GOAL>IsLUB (Set.range fun i => ‖↑f i‖) ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>‖f‖ = (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>‖f‖ ^ p.toReal = ∑' (i : α), ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<GOAL>HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>0 ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<GOAL>‖0‖ = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>‖f‖ = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>f = 0 ↔ ↑f = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>‖-f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<GOAL>(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<GOAL>Summable fun i => ‖↑f i‖ * ‖↑g i‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>p q : ℝ≥0∞<VAR>hpq : p.toReal.IsConjExponent q.toReal<VAR>f : ↥(lp E p)<VAR>g : ↥(lp E q)<GOAL>∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : p ≠ 0<VAR>f : ↥(lp E p)<VAR>i : α<GOAL>‖↑f i‖ ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<GOAL>∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>Nonempty α<VAR>f : ↥(lp E ⊤)<VAR>C : ℝ<VAR>hCf : ∀ (i : α), ‖↑f i‖ ≤ C<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E ⊤)<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hCf : ∀ (i : α), ‖↑f i‖ ≤ C<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>f : ↥(lp E p)<VAR>hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>hp : 0 < p.toReal<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>f : ↥(lp E p)<VAR>hf : ∀ (s : Finset α), ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>NormedRing 𝕜<VAR>(i : α) → Module 𝕜 (E i)<VAR>∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>c : 𝕜<VAR>f : ↥(lp E p)<GOAL>c • ↑f ∈ lp E p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>NormedRing 𝕜<VAR>(i : α) → Module 𝕜 (E i)<VAR>∀ (i : α), BoundedSMul 𝕜 (E i)<GOAL>(lpSubmodule E p 𝕜).toAddSubgroup = lp E p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>NormedRing 𝕜<VAR>(i : α) → Module 𝕜 (E i)<VAR>∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>c : 𝕜<VAR>f : ↥(lp E p)<GOAL>↑(c • f) = c • ↑f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>NormedRing 𝕜<VAR>(i : α) → Module 𝕜 (E i)<VAR>∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>hp : p ≠ 0<VAR>c : 𝕜<VAR>f : ↥(lp E p)<GOAL>‖c • f‖ ≤ ‖c‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>NormedDivisionRing 𝕜<VAR>(i : α) → Module 𝕜 (E i)<VAR>∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>hp : p ≠ 0<VAR>c : 𝕜<VAR>f : ↥(lp E p)<GOAL>‖c • f‖ = ‖c‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>(i : α) → StarAddMonoid (E i)<VAR>∀ (i : α), NormedStarGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f p<GOAL>Memℓp (star f) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>(i : α) → StarAddMonoid (E i)<VAR>∀ (i : α), NormedStarGroup (E i)<VAR>f : (i : α) → E i<GOAL>Memℓp (star f) p ↔ Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>(i : α) → StarAddMonoid (E i)<VAR>∀ (i : α), NormedStarGroup (E i)<VAR>f : ↥(lp E p)<GOAL>↑(star f) = star ↑f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>(i : α) → StarAddMonoid (E i)<VAR>∀ (i : α), NormedStarGroup (E i)<VAR>f : ↥(lp E p)<VAR>i : α<GOAL>↑(star f) i = star (↑f i)
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NonUnitalNormedRing (B i)<VAR>f g : (i : I) → B i<VAR>hf : Memℓp f ⊤<VAR>hg : Memℓp g ⊤<GOAL>Memℓp (f * g) ⊤
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NonUnitalNormedRing (B i)<VAR>f g : ↥(lp B ⊤)<GOAL>↑(f * g) = ↑f * ↑g
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NormedRing (B i)<VAR>∀ (i : I), NormOneClass (B i)<GOAL>Memℓp 1 ⊤
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NormedRing (B i)<VAR>∀ (i : I), NormOneClass (B i)<VAR>f : (i : I) → B i<VAR>hf : Memℓp f ⊤<VAR>n : ℕ<GOAL>Memℓp (f ^ n) ⊤
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NormedRing (B i)<VAR>∀ (i : I), NormOneClass (B i)<VAR>n : ℕ<GOAL>Memℓp ↑n ⊤
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NormedRing (B i)<VAR>∀ (i : I), NormOneClass (B i)<VAR>z : ℤ<GOAL>Memℓp ↑z ⊤
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NormedRing (B i)<VAR>∀ (i : I), NormOneClass (B i)<GOAL>↑1 = 1
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NormedRing (B i)<VAR>∀ (i : I), NormOneClass (B i)<VAR>f : ↥(lp B ⊤)<VAR>n : ℕ<GOAL>↑(f ^ n) = ↑f ^ n
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NormedRing (B i)<VAR>∀ (i : I), NormOneClass (B i)<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>(i : I) → NormedRing (B i)<VAR>∀ (i : I), NormOneClass (B i)<VAR>z : ℤ<GOAL>↑↑z = ↑z
<VAR>I : Type u_3<VAR>𝕜 : Type u_4<VAR>B : I → Type u_5<VAR>NormedField 𝕜<VAR>(i : I) → NormedRing (B i)<VAR>(i : I) → NormedAlgebra 𝕜 (B i)<VAR>∀ (i : I), NormOneClass (B i)<VAR>k : 𝕜<GOAL>Memℓp ((algebraMap 𝕜 ((i : I) → B i)) k) ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<VAR>j : α<GOAL>↑(lp.single p i a) j = if h : j = i then ⋯ ▸ a else 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<GOAL>↑(lp.single p i a) i = a
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<VAR>j : α<VAR>hij : j ≠ i<GOAL>↑(lp.single p i a) j = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<GOAL>lp.single p i (-a) = -lp.single p i a
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>NormedRing 𝕜<VAR>(i : α) → Module 𝕜 (E i)<VAR>∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<VAR>c : 𝕜<GOAL>lp.single p i (c • a) = c • lp.single p i a
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : (i : α) → E i<VAR>s : Finset α<GOAL>‖∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : (i : α) → E i<VAR>i : α<GOAL>‖lp.single p i (f i)‖ = ‖f i‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<GOAL>‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>hp : 0 < p.toReal<VAR>f : ↥(lp E p)<VAR>s : Finset α<GOAL>‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>DecidableEq α<VAR>Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<GOAL>HasSum (fun i => lp.single p i (↑f i)) f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>_i : Fact (1 ≤ p)<GOAL>UniformContinuous Subtype.val
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l.NeBot<VAR>C : ℝ<VAR>F : ι → ↥(lp E ⊤)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Filter.Tendsto (id fun i => ↑(F i)) l (nhds f)<VAR>a : α<GOAL>‖f a‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Filter.Tendsto (id fun i => ↑(F i)) l (nhds f)<VAR>s : Finset α<GOAL>∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>C : ℝ<VAR>F : ι → ↥(lp E p)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : ↥(lp E p)<VAR>hf : Filter.Tendsto (id fun i => ↑(F i)) l (nhds ↑f)<GOAL>‖f‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p : ℝ≥0∞<VAR>(i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ι → ↥(lp E p)<VAR>hF : Bornology.IsBounded (Set.range F)<VAR>f : (a : α) → E a<VAR>hf : Filter.Tendsto (id fun i => ↑(F i)) l (nhds f)<GOAL>Memℓp f p