mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy' :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop * limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop
h_bdd : IsBoundedUnder LE.le atTop fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))
n : ℕ
⊢ 0 ≤ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp₁
f : X ⟶ Y
⊢ f ≫ mkHom (↑(Hom.hom f)).range.normedMk ⋯ = 0 ≫ mkHom (↑(Hom.hom f)).range.normedMk ⋯

Tactic:
ext x
      rw [Limits.zero_comp, comp_apply, SemiNormedGrp₁.mkHom_apply,
        SemiNormedGrp₁.zero_apply, ← NormedAddGroupHom.mem_ker, f.hom.1.range.ker_normedMk,
        f.hom.1.mem_range]
      use x

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
hu : IsUltrametricDist K
x : L
⊢ spectralNorm K L x = (invariantExtension K L) x

Tactic:
have hna := hu.isNonarchimedean_norm

Goal state after:
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean fun x ↦ ‖x‖
⊢ spectralNorm K L x = (invariantExtension K L) x
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
n : ℕ
⊢ 0 n ≤ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
h_mul : smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
n : ℕ
⊢ 0 n ≤ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NontrivialTopology M
N : ℝ
a✝ : N ≥ 0
hle : ∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖
x : M
h✝ : ‖x‖ ≠ 0
⊢ 0 < ‖normedMk x‖

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ (∑ a ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support, dist (f.ofLp a) (g.ofLp a) ^ ↑p) ^ (↑p)⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : μ x = 0
⊢ μ x ^ n ≤ 0

Tactic:
hx0,

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : μ x = 0
⊢ 0 ^ n ≤ 0
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : MetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ 0 ≤ (∑ a ∈ (zipWith dist ⋯ f.ofLp g.ofLp).support, dist (f.ofLp a) (g.ofLp a) ^ ↑p) ^ (↑p)⁻¹

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : μ x = 0
hxn : μ (x ^ n) = 0
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

Tactic:
hx0,

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : μ x = 0
hxn : μ (x ^ n) = 0
⊢ μ (x ^ n) ^ (1 / ↑n) = 0
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε
⊢ ε / 3 > 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable fun x ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
⊢ ε / 3 > 0

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℝ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : ↑{0}ᶜ
this : 0 < ‖↑x‖
⊢ 0 < ‖↑x‖ / r

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: 𝕜 : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_8
F : Type u_9
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : T2Space F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 F
hf : Injective ⇑f
⊢ f.HasLeftInverse

Tactic:
obtain ⟨g, hg⟩ :=
    f.toLinearMap.exists_leftInverse_of_injective (f.ker_eq_bot_of_injective hf)

Goal state after:
𝕜 : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_8
F : Type u_9
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : T2Space F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 F
hf : Injective ⇑f
g : F →ₗ[𝕜] E
hg : g ∘ₗ ↑f = LinearMap.id
⊢ f.HasLeftInverse
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : NormOneClass R
f : ι → R
inst✝ : CompleteSpace R
hf : Summable fun i ↦ ‖f i‖
ε : ℝ
hε : ε > 0
r₁ : ℝ
hr₁ : r₁ > 0
s₁ : Finset ι
hs₁ : ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, ‖1 + f i‖ ≤ r₁
⊢ 0 < ε / (2 * r₁)

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hu : Summable fun n ↦ ‖f n‖
i : ι
⊢ 0 ≤ ‖‖1 + f i‖ - 1‖

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
q : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (i : ι), ‖e i‖ ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
i : ι
hi : i ∈ s
⊢ 0 ≤ K * C

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
q : ℝ≥0∞
e : (i : ι) → E i
f : (i : ι) → F i
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (i : ι), ‖e i‖ ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
i : ι
hi : i ∈ s
⊢ 0 ≤ ‖f i‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : ⨂[𝕜] (i : ι), E i
⊢ 0 ≤ ‖x‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝² : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
x : 𝕜
m : (i : ι) → E i
a✝ : (x, m) ∈ FreeAddMonoid.toList p
h : ‖x‖ * ∏ x, ‖m x‖ = a
⊢ 0 ≤ ‖x‖ * ∏ x, ‖m x‖

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
this : ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤ C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)
i : ι
hi : i ∈ s
⊢ 0 ≤ K

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
this : ∑ i ∈ s, (‖e i‖ * ‖f i‖) ^ r.toReal ≤ C ^ (r.toReal / p.toReal) * D ^ (r.toReal / q.toReal)
i : ι
hi : i ∈ s
⊢ 0 ≤ ‖e i‖ * ‖f i‖

Tactic:
positivity

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

Goal state before:
pp: case hf
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
i✝ : ι
a✝ : i✝ ∈ s
⊢ 0 ≤ ‖e i✝‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁶ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝² : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
inst✝ : DecidableEq ι
i : ι
u v : E i →L[𝕜] E' i
⊢ mapL (update f i (u + v)) = mapL (update f i u) + mapL (update f i v)

Tactic:
ext
  simp [mapL_add_smul_aux, PiTensorProduct.map_update_add]

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

Goal state before:
pp: case hg
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : (i : ι) → NormedAddCommGroup (F i)
inst✝² : (i : ι) → NormedSpace 𝕜 (F i)
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
e : (i : ι) → E i
f : (i : ι) → F i
hp : 0 < p.toReal
hq : 0 < q.toReal
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K C D : ℝ
hBK : ∀ (i : ι), ‖B i‖ ≤ K
hK : 0 ≤ K
hC : 0 ≤ C
hCe : ∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C
hDf : ∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D
s : Finset ι
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hr : 0 < r.toReal
i✝ : ι
a✝ : i✝ ∈ s
⊢ 0 ≤ ‖f i✝‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
⊢ 0 ≤ ∏ i, ‖f i‖

Tactic:
positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ 0 ≤ ∏ i, ‖f i‖

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝² : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ ∞)
hpqr : ∞.HolderTriple ∞ ∞
⊢ 0 ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
positivity

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

Goal state before:
pp: case inl.inl.refine_1
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝² : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ ∞)
hpqr : ∞.HolderTriple ∞ ∞
i : ι
⊢ ‖↑e i‖ ≤ ‖e‖

Tactic:
exact norm_apply_le_norm (by simp) ..

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

Goal state before:
pp: case inl.inl.refine_2
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝² : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ ∞)
hpqr : ∞.HolderTriple ∞ ∞
i : ι
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
exact norm_apply_le_norm (by simp) ..

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝ : Fact (1 ≤ r)
f : ↥(lp F r)
hpqr : ∞.HolderTriple r r
hq : 1 ≤ r.toReal
⊢ 0 ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝ : Fact (1 ≤ r)
f : ↥(lp F r)
hpqr : ∞.HolderTriple r r
hq : 1 ≤ r.toReal
s : Finset ι
⊢ 0 ≤ ↑K * ‖e‖

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝ : Fact (1 ≤ r)
f : ↥(lp F r)
hpqr : ∞.HolderTriple r r
hq : 1 ≤ r.toReal
s : Finset ι
⊢ 0 ≤ ‖f‖

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝ : Fact (1 ≤ r)
f : ↥(lp F r)
hpqr : ∞.HolderTriple r r
hq : 1 ≤ r.toReal
s : Finset ι
⊢ 0 ≤ ↑K

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
inst✝ : Fact (1 ≤ r)
f : ↥(lp F r)
hpqr : ∞.HolderTriple r r
hq : 1 ≤ r.toReal
s : Finset ι
⊢ 0 ≤ ‖e‖

Tactic:
positivity

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
r : ℝ≥0∞
inst✝² : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
inst✝¹ : Fact (1 ≤ ∞)
f : ↥(lp F ∞)
inst✝ : Fact (1 ≤ r)
e : ↥(lp E r)
hp : 1 ≤ r.toReal
hpqr : r.HolderTriple ∞ r
⊢ 0 ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
positivity

Goal state after: