awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 x_2 : H₀ K
h_zero :
  ∀ (a : X × V),
    Eq.{u_1 + 1} (α := 𝕜)
      (match (motive := X × V → 𝕜) a with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star 0 * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)
      (0 : 𝕜)
h_add :
  ∀ (a : X × V) (b₁ b₂ : 𝕜),
    (match (motive := X × V → 𝕜) a with
      | (y, u) =>
        Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star (b₁ + b₂) * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
      HAdd.hAdd (α := 𝕜) (β := 𝕜)
        (match (motive := X × V → 𝕜) a with
          | (y, u) =>
            Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
              match (motive := X × V → 𝕜) x with
              | (x, v) => star b₁ * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
          𝕜)
        (match (motive := X × V → 𝕜) a with
          | (y, u) =>
            Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
              match (motive := X × V → 𝕜) x with
              | (x, v) => star b₂ * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
          𝕜)
⊢ (Finsupp.sum (x + x_1) fun (x : X × V) (z : 𝕜) ↦
      match (motive := X × V → 𝕜) x with
      | (y, u) =>
        Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HAdd.hAdd (α := 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜)
      (Finsupp.sum x_1 fun (x : X × V) (z : 𝕜) ↦
        match (motive := X × V → 𝕜) x with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜)

Tactic:
rw [Finsupp.sum_add_index']

Premises used: Finsupp.sum_add_index'
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 x_2 : H₀ K
⊢ ∀ (a : X × V),
    Eq.{u_1 + 1} (α := 𝕜)
      (match (motive := X × V → 𝕜) a with
        | (y, u) =>
          Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star 0 * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)
      (0 : 𝕜)

Tactic:
simp [← Finsupp.sum_add, add_mul]

Premises used: add_mul, Finsupp.sum_add
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 x_2 : H₀ K
⊢ ∀ (a : X × V) (b₁ b₂ : 𝕜),
    (match (motive := X × V → 𝕜) a with
      | (y, u) =>
        Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star (b₁ + b₂) * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
      HAdd.hAdd (α := 𝕜) (β := 𝕜)
        (match (motive := X × V → 𝕜) a with
          | (y, u) =>
            Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
              match (motive := X × V → 𝕜) x with
              | (x, v) => star b₁ * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
          𝕜)
        (match (motive := X × V → 𝕜) a with
          | (y, u) =>
            Finsupp.sum x_2 fun (x : X × V) (w : 𝕜) ↦
              match (motive := X × V → 𝕜) x with
              | (x, v) => star b₂ * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
          𝕜)

Tactic:
simp [← Finsupp.sum_add, add_mul]

Premises used: add_mul, Finsupp.sum_add
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 : H₀ K
x_2 : 𝕜
rw :
  (Finsupp.sum x fun (i : X × V) (a : 𝕜) ↦
      match (motive := X × V → 𝕜) i with
      | (y, u) =>
        Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star (x_2 * a) * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (y, u) =>
            Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
              match (motive := X × V → 𝕜) x with
              | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)
rw₁ :
  ∀ (i : X × V),
    Eq.{u_1 + 1} (α := 𝕜)
      (match (motive := X × V → 𝕜) i with
        | (y, u) =>
          Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star 0 * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)
      (0 : 𝕜)
⊢ (Finsupp.sum (x_2 • x) fun (x : X × V) (z : 𝕜) ↦
      match (motive := X × V → 𝕜) x with
      | (y, u) =>
        Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (y, u) =>
            Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
              match (motive := X × V → 𝕜) x with
              | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)

Tactic:
rw [Finsupp.sum_smul_index]

Premises used: Finsupp.sum_smul_index
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 : H₀ K
x_2 : 𝕜
⊢ (Finsupp.sum x fun (i : X × V) (a : 𝕜) ↦
      match (motive := X × V → 𝕜) i with
      | (y, u) =>
        Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star (x_2 * a) * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜)
      (Finsupp.sum x fun (x : X × V) (z : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (y, u) =>
            Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
              match (motive := X × V → 𝕜) x with
              | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)

Tactic:
simp [Finsupp.mul_sum, ← mul_assoc]

Premises used: mul_assoc, Finsupp.mul_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x x_1 : H₀ K
x_2 : 𝕜
⊢ ∀ (i : X × V),
    Eq.{u_1 + 1} (α := 𝕜)
      (match (motive := X × V → 𝕜) i with
        | (y, u) =>
          Finsupp.sum x_1 fun (x : X × V) (w : 𝕜) ↦
            match (motive := X × V → 𝕜) x with
            | (x, v) => star 0 * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜 :
        𝕜)
      (0 : 𝕜)

Tactic:
simp [Finsupp.mul_sum, ← mul_assoc]

Premises used: mul_assoc, Finsupp.mul_sum
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_4 : Fact K.PosSemidef
f g : H₀ K
⊢ ⟪f, g⟫_𝕜 =
    Finsupp.sum f fun (x : X × V) (z : 𝕜) ↦
      match (motive := X × V → 𝕜) x with
      | (y, u) =>
        Finsupp.sum g fun (x : X × V) (w : 𝕜) ↦
          match (motive := X × V → 𝕜) x with
          | (x, v) => star z * w * ⟪(K x y : (a : V) → V) u, v⟫_𝕜

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
x_1 x_2 : V
⊢ (↑(Finsupp.single (x, x_1 + x_2) 1) : UniformSpace.Completion (H₀ K)) =
    HAdd.hAdd (α := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1) 1) : UniformSpace.Completion (H₀ K))
      (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K))

Tactic:
UniformSpace.Completion.denseRange_coe.eq_of_inner_left 𝕜 fun f ↦ ?_

Premises used: DenseRange.eq_of_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
x_1 x_2 : V
refine :
  ∀ (f : H₀ K),
    inner 𝕜 (E := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1 + x_2) 1) : UniformSpace.Completion (H₀ K))
        (↑f : UniformSpace.Completion (H₀ K)) =
      ⟪HAdd.hAdd (α := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1) 1) : UniformSpace.Completion (H₀ K))
          (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K)),
        (↑f : UniformSpace.Completion (H₀ K))⟫_𝕜
⊢ (↑(Finsupp.single (x, x_1 + x_2) 1) : UniformSpace.Completion (H₀ K)) =
    HAdd.hAdd (α := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1) 1) : UniformSpace.Completion (H₀ K))
      (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K))

Tactic:
refine UniformSpace.Completion.denseRange_coe.eq_of_inner_left 𝕜 fun f ↦ ?_

Premises used: DenseRange.eq_of_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
x_1 x_2 : V
f : H₀ K
⊢ inner 𝕜 (E := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1 + x_2) 1) : UniformSpace.Completion (H₀ K))
      (↑f : UniformSpace.Completion (H₀ K)) =
    ⟪HAdd.hAdd (α := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1) 1) : UniformSpace.Completion (H₀ K))
        (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K)),
      (↑f : UniformSpace.Completion (H₀ K))⟫_𝕜

Tactic:
simp [inner_add_left, inner_H₀_def, ← Finsupp.sum_add, ← mul_add]

Premises used: inner_add_left, Finsupp.sum_add, mul_add, _private.0.RKHS.inner_H₀_def
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
x_1 : 𝕜
x_2 : V
⊢ (↑(Finsupp.single (x, x_1 • x_2) 1) : UniformSpace.Completion (H₀ K)) =
    HSMul.hSMul (α := 𝕜) (β := UniformSpace.Completion (H₀ K)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x_1 : 𝕜)
      (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K))

Tactic:
UniformSpace.Completion.denseRange_coe.eq_of_inner_left 𝕜 fun f ↦ ?_

Premises used: DenseRange.eq_of_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
x_1 : 𝕜
x_2 : V
refine :
  ∀ (f : H₀ K),
    inner 𝕜 (E := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1 • x_2) 1) : UniformSpace.Completion (H₀ K))
        (↑f : UniformSpace.Completion (H₀ K)) =
      ⟪HSMul.hSMul (α := 𝕜) (β := UniformSpace.Completion (H₀ K)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x_1 : 𝕜)
          (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K)),
        (↑f : UniformSpace.Completion (H₀ K))⟫_𝕜
⊢ (↑(Finsupp.single (x, x_1 • x_2) 1) : UniformSpace.Completion (H₀ K)) =
    HSMul.hSMul (α := 𝕜) (β := UniformSpace.Completion (H₀ K)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x_1 : 𝕜)
      (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K))

Tactic:
refine UniformSpace.Completion.denseRange_coe.eq_of_inner_left 𝕜 fun f ↦ ?_

Premises used: DenseRange.eq_of_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
x_1 : 𝕜
x_2 : V
f : H₀ K
⊢ inner 𝕜 (E := UniformSpace.Completion (H₀ K)) (↑(Finsupp.single (x, x_1 • x_2) 1) : UniformSpace.Completion (H₀ K))
      (↑f : UniformSpace.Completion (H₀ K)) =
    ⟪HSMul.hSMul (α := 𝕜) (β := UniformSpace.Completion (H₀ K)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x_1 : 𝕜)
        (↑(Finsupp.single (x, x_2) 1) : UniformSpace.Completion (H₀ K)),
      (↑f : UniformSpace.Completion (H₀ K))⟫_𝕜

Tactic:
simp [inner_smul_left, inner_H₀_def, Finsupp.mul_sum, ← mul_assoc, mul_comm]

Premises used: mul_assoc, mul_comm, Finsupp.mul_sum, inner_smul_left, _private.0.RKHS.inner_H₀_def
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
⊢ 0 ≤
    norm (E := UniformSpace.Completion (H₀ K))
      ((kerFunAux x : (a : V) → UniformSpace.Completion (H₀ K)) v : UniformSpace.Completion (H₀ K))

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
⊢ 0 ≤ √‖K x x‖ * ‖v‖

Tactic:
simp [mul_nonneg]

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
refine :
  HPow.hPow (β := ℕ)
      (norm (E := UniformSpace.Completion (H₀ K))
        ((kerFunAux x : (a : V) → UniformSpace.Completion (H₀ K)) v : UniformSpace.Completion (H₀ K)))
      2 ≤
    HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
⊢ norm (E := UniformSpace.Completion (H₀ K))
      ((kerFunAux x : (a : V) → UniformSpace.Completion (H₀ K)) v : UniformSpace.Completion (H₀ K)) ≤
    √‖K x x‖ * ‖v‖

Tactic:
refine (sq_le_sq₀ (by simp) (by simp [mul_nonneg])).mp ?_

Premises used: sq_le_sq₀, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
simp : ‖inner 𝕜 (E := H₀ K) (Finsupp.single (x, v) 1) (Finsupp.single (x, v) 1)‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
⊢ HPow.hPow (β := ℕ)
      (norm (E := UniformSpace.Completion (H₀ K))
        ((kerFunAux x : (a : V) → UniformSpace.Completion (H₀ K)) v : UniformSpace.Completion (H₀ K)))
      2 ≤
    HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2

Tactic:
simp only [LinearMap.coe_mk, AddHom.coe_mk, UniformSpace.Completion.norm_coe,
    ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_self_re_eq_norm]

Premises used: LinearMap.coe_mk, UniformSpace.Completion.norm_coe, inner_self_eq_norm_sq, inner_self_re_eq_norm, AddHom.coe_mk
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
simp : ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
⊢ ‖inner 𝕜 (E := H₀ K) (Finsupp.single (x, v) 1) (Finsupp.single (x, v) 1)‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2

Tactic:
simp only [inner_H₀_def, RCLike.star_def, mul_zero, zero_mul,
    Finsupp.sum_single_index, mul_one, map_zero, map_one, one_mul]

Premises used: RCLike.star_def, Finsupp.sum_single_index, MulZeroClass.zero_mul, map_zero, MulZeroClass.mul_zero, map_one, mul_one, one_mul, _private.0.RKHS.inner_H₀_def
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
⊢ ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖

Tactic:
simp [norm_inner_le_norm]

Premises used: norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
⊢ norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖ ≤ ‖K x x‖ * ‖v‖ * ‖v‖

Tactic:
simp [mul_le_mul_of_nonneg_right, le_opNorm]

Premises used: ContinuousLinearMap.le_opNorm, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
⊢ ‖K x x‖ * ‖v‖ * ‖v‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2

Tactic:
simp [mul_pow, mul_assoc, ← sq]

Premises used: mul_assoc, sq, mul_pow
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
x : X
v : V
_ : ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖
_₁ : norm (E := V) ((K x x : (a : V) → V) v : V) * ‖v‖ ≤ ‖K x x‖ * ‖v‖ * ‖v‖
_₂ : ‖K x x‖ * ‖v‖ * ‖v‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2
⊢ ‖⟪(K x x : (a : V) → V) v, v⟫_𝕜‖ ≤ HPow.hPow (β := ℕ) (√‖K x x‖ * ‖v‖) 2

Tactic:
calc
    _ ≤ ‖K x x v‖ * ‖v‖ := by simp [norm_inner_le_norm]
    _ ≤ ‖K x x‖ * ‖v‖ * ‖v‖ := by simp [mul_le_mul_of_nonneg_right, le_opNorm]
    _ ≤ _ := by simp [mul_pow, mul_assoc, ← sq]

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
⊢ Function.Injective (α := OfKernel K) (β := X → V)
    (⇑(ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
          (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
            (kerFun K x)) :
      (a : OfKernel K) → X → V)

Tactic:
(injective_iff_map_eq_zero _).mpr fun f h ↦ ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Reproducing
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
X : Type u_2
V : Type u_3
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
H : Type u_4
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
inst_5 : RKHS 𝕜 H X V
inst_6 : CompleteSpace H
inst_7 : CompleteSpace V
K : Matrix.{u_2, u_2, u_3} X X (V →L[𝕜] V)
inst_8 : Fact K.PosSemidef
refine :
  ∀ (f : OfKernel K)
    (h :
      Eq (α := X → V)
        ((ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
                (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
                  (kerFun K x) :
              (a : OfKernel K) → X → V)
            f :
          X → V)
        (0 : X → V)),
    f = 0
⊢ Function.Injective (α := OfKernel K) (β := X → V)
    (⇑(ContinuousLinearMap.pi (φ := fun (a : X) ↦ V) fun (x : X) ↦
          (adjoint : (a : V →L[𝕜] UniformSpace.Completion (H₀ K)) → UniformSpace.Completion (H₀ K) →L[𝕜] V)
            (kerFun K x)) :
      (a : OfKernel K) → X → V)

Tactic:
refine (injective_iff_map_eq_zero _).mpr fun f h ↦ ?_

Premises used: Iff.mpr, injective_iff_map_eq_zero