mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ ∀ i ∉ ⋯.toFinset, ‖f i‖ ^ p.toReal = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖ ^ q.toReal)
i : α
⊢ 0 ≤ ‖f i‖ ^ q.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
⊢ 0 < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
⊢ {x | 1 ≤ ‖f x‖ ^ q.toReal}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
i : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
⊢ 0 ≤ ‖f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
⊢ Memℓp f p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
⊢ Memℓp (f + g) p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
⊢ Memℓp (f - g) p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ i ∈ s, Memℓp (f i) p
⊢ Memℓp (fun a ↦ ∑ i ∈ s, f i a) p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
⊢ Memℓp (c • f) p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : p = 0
⊢ ℝ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ∞)
⊢ IsLUB (Set.range fun i ↦ ‖↑f i‖) ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ‖f‖ = (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun x ↦ f x x₀
hx : x ∈ s
⊢ Summable fun n ↦ f n x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal * p.toReal) = ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
field_simp
    simp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ‖f‖ ^ p.toReal = ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
x : ↥(lp E p)
⊢ ‖toNorm x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x ↦ g x y₀
hy : y ∈ t
⊢ Summable fun n ↦ g n y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n ↦ f n x₀
hx : x ∈ s
⊢ ∀ x ∈ s, Tendsto (fun t ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
i : α
⊢ 0 ≤ ‖↑f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun n ↦ f n x₀
hx : x ∈ s
⊢ HasFDerivAt (fun y ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ 0 ≤ ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ (∑' (i : α), ‖↑0 i‖ ^ p.toReal) ^ (1 / p.toReal) = 0

Tactic:
have hp' : 1 / p.toReal ≠ 0 := one_div_ne_zero hp.ne'

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
hp' : 1 / p.toReal ≠ 0
⊢ (∑' (i : α), ‖↑0 i‖ ^ p.toReal) ^ (1 / p.toReal) = 0
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ f = 0 → ‖f‖ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
⊢ {i | ¬↑f i = 0} = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun n ↦ g n y₀
hy : y ∈ t
⊢ HasDerivAt (fun z ↦ ∑' (n : α), g n z) (∑' (n : α), g' n y) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
x₀ : E
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n ↦ f n x₀
x : E
⊢ Summable fun n ↦ f n x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable fun n ↦ g n y₀
y : 𝕜
⊢ Summable fun n ↦ g n y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : Nonempty α
⊢ IsLUB (Set.range fun i ↦ ‖↑f i‖) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
x₀ : E
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n ↦ f n x₀
x : E
⊢ HasFDerivAt (fun y ↦ ∑' (n : α), f n y) (∑' (n : α), f' n x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
⊢ HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable fun n ↦ g n y₀
y : 𝕜
⊢ HasDerivAt (fun z ↦ ∑' (n : α), g n z) (∑' (n : α), g' n y) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) 0
i : α
⊢ 0 ≤ ‖↑f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i ↦ ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
⊢ ↑f i = 0 ∧ p.toReal ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ ‖f‖ = 0 ↔ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ f = 0 ↔ ↑f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
h : ∀ (x₀ : E), ¬Summable fun n ↦ f n x₀
⊢ (fun x ↦ ∑' (n : α), f n x) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
this : ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal
⊢ ‖-f‖ = ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
⊢ ‖-f‖ = ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
⊢ Differentiable 𝕜 fun y ↦ ∑' (n : α), f n y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
⊢ Differentiable 𝕜 fun z ↦ ∑' (n : α), g n z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
x₀ : E
hu : Summable u
hf : ∀ (n : α), Differentiable 𝕜 (f n)
hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n
hf0 : Summable fun n ↦ f n x₀
⊢ (fderiv 𝕜 fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), fderiv 𝕜 (f n) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable fun n ↦ g n y₀
⊢ (deriv fun y ↦ ∑' (n : α), g n y) = fun y ↦ ∑' (n : α), deriv (g n) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x✝ : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x✝, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x✝) l)
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x✝)
this✝¹ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝ :
  TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) 0 (l ×ˢ l) (𝓝 x✝) ∧
    TendstoUniformlyOnFilter (fun n x ↦ f n.1 x✝ - f n.2 x✝) 0 (l ×ˢ l) (𝓝 x✝)
this :
  TendstoUniformlyOnFilter ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) 0
    (l ×ˢ l) (𝓝 x✝)
x : (ι × ι) × E
⊢ ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x✝ - f n.2 x✝)) + -fun n x ↦ f n.1 x✝ - f n.2 x✝) x.1 x.2 =
    -f x.1.1 x.2 + f x.1.2 x.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this :
  TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (𝓝 x) ∧
    TendstoUniformlyOnFilter (fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
⊢ TendstoUniformlyOnFilter (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
⊢ (Summable fun i ↦ ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i✝ : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
i : α
⊢ 0 ≤ ‖↑f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
i : α
x✝¹ x✝ : ↥(lp E p)
⊢ dist (↑x✝¹ i) (↑x✝ i) ≤ dist x✝¹ x✝

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
i : α
⊢ 0 ≤ ‖↑f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Nonempty α
f : ↥(lp E ∞)
C : ℝ
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ‖f‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
hk : ↑k ≤ N
⊢ (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
hp : ∞ ≠ 0
x : ↥(lp E ∞)
y : ↥(lp F ∞)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
⊢ 0 ≤ ‖y‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
hk : ↑k ≤ N
x : E
⊢ iteratedFDeriv 𝕜 k (fun y ↦ ∑' (n : α), f n y) x = ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp✝ : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
hp : 0 < p.toReal
s : Finset α
⊢ ∑ i ∈ s, ‖↑x i‖ ^ p.toReal ≤ ∑ i ∈ s, ‖↑y i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
by

Goal state after: