awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
refine : Summable (α := ℝ) fun (a : ℕ) ↦ ‖HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑a : ℤ)) • x a‖
⊢ Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n

Tactic:
refine Summable.of_norm ?_

Premises used: Summable.of_norm
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
have : (2 : ℝ)⁻¹ < 1 := by norm_num
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
this : LT.lt (α := ℝ) 2⁻¹ 1
⊢ Summable (α := ℝ) fun (a : ℕ) ↦ ‖HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑a : ℤ)) • x a‖

Tactic:
simp [norm_smul, hx_norm, ← inv_pow, this]

Premises used: norm_smul, inv_pow
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
⊢ Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n

Tactic:
have x_summable : Summable fun n : ℕ => (2 : ℝ) ^ (-(n : ℤ)) • x n := by
    refine Summable.of_norm ?_
    have : (2 : ℝ)⁻¹ < 1 := by norm_num
    simp [norm_smul, hx_norm, ← inv_pow, this]
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
⊢ ∃ (n : ℕ),
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
      HPow.hPow (α := ℝ) 2 n

Tactic:
tendsto_pow_atTop_atTop_of_one_lt one_lt_two |>.eventually_gt_atTop _
      |>.exists

Premises used: Filter.Eventually.exists, tendsto_pow_atTop_atTop_of_one_lt, one_lt_two, Filter.Tendsto.eventually_gt_atTop
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
obtain :
  ∀ (n : ℕ)
    (hn :
      norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
        HPow.hPow (α := ℝ) 2 n),
    False
⊢ False

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, ‖f (∑' (n : ℕ), (2 : ℝ) ^ (-(n : ℤ)) • x n)‖ < (2 : ℝ) ^ n :=
    tendsto_pow_atTop_atTop_of_one_lt one_lt_two |>.eventually_gt_atTop _
      |>.exists

Premises used: Nat.cast, Filter.Eventually.exists, tendsto_pow_atTop_atTop_of_one_lt, HPow.hPow, tsum, one_lt_two, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, Neg.neg, SummationFilter.unconditional, Filter.Tendsto.eventually_gt_atTop
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
apply :
  HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
⊢ False

Tactic:
apply hn.not_ge

Premises used: LT.lt.not_ge
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
trans :
  HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
trans₁ :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
⊢ HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)

Tactic:
trans ‖f ((2 : ℝ) ^ (-n : ℤ) • x n)‖

Premises used: Nat.cast, HPow.hPow, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
⊢ HPow.hPow (α := ℝ) 2 (2 * n) ≤ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)

Tactic:
have := hx n |>.le
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : HPow.hPow (α := ℝ) 2 (2 * n) ≤ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)
⊢ HPow.hPow (α := ℝ) 2 n * HPow.hPow (α := ℝ) 2 n ≤ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)

Tactic:
rw [pow_mul', sq] at this

Premises used: sq, pow_mul'
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : HPow.hPow (α := ℝ) 2 n * HPow.hPow (α := ℝ) 2 n ≤ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)
⊢ 0 < HPow.hPow (α := ℝ) 2 n

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : HPow.hPow (α := ℝ) 2 n * HPow.hPow (α := ℝ) 2 n ≤ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x n) : A₂)
⊢ HPow.hPow (α := ℝ) 2 n ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)

Tactic:
simpa [norm_smul] using (le_inv_mul_iff₀ (show 0 < (2 : ℝ) ^ n by positivity)).mpr this

Premises used: Iff.mpr, norm_smul, le_inv_mul_iff₀
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
m : ℕ
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ))

Tactic:
positivity
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
⊢ ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m

Tactic:
have (m : ℕ) : 0 ≤ ((2 : ℝ) ^ (-(m : ℤ)) • x m) := smul_nonneg (by positivity) (hx_nonneg m)
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)

Tactic:
CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg (this n)) ?_

Premises used: PositiveLinearMap.map_nonneg, CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m
refine :
  LE.le.{u_2} (α := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
    ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
⊢ norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) ≤
    norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)

Tactic:
refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (f.map_nonneg (this n)) ?_

Premises used: PositiveLinearMap.map_nonneg, CStarAlgebra.norm_le_norm_of_nonneg_of_le
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m
a : HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n ≤ ∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
⊢ LE.le.{u_2} (α := A₂) ((f : (a : A₁) → A₂) (HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)
    ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂)

Tactic:
gcongr
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m
⊢ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n ≤ ∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n

Tactic:
x_summable.le_tsum n fun m _ ↦ this m

Premises used: Summable.le_tsum
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
hcontra : ∀ (C : ℝ≥0), ∃ (a : A₁), 0 ≤ a ∧ (↑C : ℝ) * ‖a‖ < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂)
x : (n : ℕ) → A₁
hx_nonneg : ∀ (x_1 : ℕ), 0 ≤ x x_1
hx_norm : ∀ (x_1 : ℕ), ‖x x_1‖ = 1
hx : ∀ (x_1 : ℕ), HPow.hPow (α := ℝ) 2 (2 * x_1) < norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (x x_1) : A₂)
x_summable : Summable.{u_1, 0} (α := A₁) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n
n : ℕ
hn :
  norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) (∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n) : A₂) <
    HPow.hPow (α := ℝ) 2 n
this : ∀ (m : ℕ), 0 ≤ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑m : ℤ)) • x m
⊢ HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n ≤ ∑' (n : ℕ), HPow.hPow (α := ℝ) (β := ℤ) 2 (-(↑n : ℤ)) • x n

Tactic:
exact x_summable.le_tsum n fun m _ ↦ this m

Premises used: Summable.le_tsum
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
obtain :
  ∀ (C : ℝ≥0)
    (h :
      ∀ (a : A₁),
        norm.{u_2} (E := A₂) ((PositiveLinearMapClass.toPositiveLinearMap f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖),
    ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖
⊢ ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖

Tactic:
obtain ⟨C, h⟩ := exists_norm_apply_le (f : A₁ →ₚ[ℂ] A₂)

Premises used: PositiveLinearMap.exists_norm_apply_le, PositiveLinearMapClass.toPositiveLinearMap
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
C : ℝ≥0
h :
  ∀ (a : A₁),
    norm.{u_2} (E := A₂) ((PositiveLinearMapClass.toPositiveLinearMap f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
⊢ ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖

Tactic:
⟨C, h⟩

Premises used: Exists.intro, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
Goal:
A₁ : Type u_1
A₂ : Type u_2
B₁ : Type u_3
B₂ : Type u_4
inst : NonUnitalCStarAlgebra A₁
inst_1 : NonUnitalCStarAlgebra A₂
inst_2 : PartialOrder A₁
inst_3 : StarOrderedRing A₁
inst_4 : PartialOrder A₂
inst_5 : StarOrderedRing A₂
inst_6 : CStarAlgebra B₁
inst_7 : CStarAlgebra B₂
inst_8 : PartialOrder B₁
inst_9 : PartialOrder B₂
inst_10 : StarOrderedRing B₁
F : Type u_5
inst_11 : FunLike F A₁ A₂
inst_12 : LinearMapClass F ℂ A₁ A₂
inst_13 : OrderHomClass F A₁ A₂
f : F
C : ℝ≥0
h :
  ∀ (a : A₁),
    norm.{u_2} (E := A₂) ((PositiveLinearMapClass.toPositiveLinearMap f : (a : A₁) → A₂) a : A₂) ≤ (↑C : ℝ) * ‖a‖
⊢ ∃ (C : ℝ), ∀ (a : A₁), norm.{u_2} (E := A₂) ((f : (a : A₁) → A₂) a : A₂) ≤ C * ‖a‖

Tactic:
exact ⟨C, h⟩