/-
 - Created in 2024 by Gaëtan Serré
-/

/-
- https://github.com/gaetanserre/SBS-Proofs
-/

import Mathlib.Analysis.InnerProductSpace.Basic

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

open scoped RealInnerProductSpace
open BigOperators Finset

set_option maxHeartbeats 4000000

/-=====================================RKHS SECTION=====================================-/

/-
  Here we define the product RKHS.
-/

/-
  We provide a typeclass definition for a generic RKHS.
-/

class RKHS {E F : Type*} [RCLike F] (H : Set (E → F)) [NormedAddCommGroup H] [InnerProductSpace F H] where
  k : E → E → F
  memb : ∀ (x : E), k x ∈ H
  repro : ∀ (f : H), ∀ (x : E), f.1 x = inner f ⟨k x, memb x⟩

def product_RKHS {α : Type*} (H : Set (α → ℝ)) [NormedAddCommGroup H] [InnerProductSpace ℝ H] [RKHS H] {d : ℕ} (_ : d ≠ 0) := Fin d → H

namespace RKHS

variable {α : Type*} {H : Set (α → ℝ)} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [RKHS H]

variable {d : ℕ} {hd : d ≠ 0}

instance : Inner ℝ (product_RKHS H hd) where
  inner := λ f g ↦ ∑ i, inner (f i) (g i)

instance : Norm (product_RKHS H hd) where
  norm := λ f ↦ inner f f

lemma norm_eq_zero_iff (f : product_RKHS H hd) : ‖f‖ = 0 ↔ ∀ i, f i = 0 := 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
‖f‖ = 0 ↔ ∀ (i : Fin d), f i = 0constructor
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mpr
(∀ (i : Fin d), f i = 0) → ‖f‖ = 0
  
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
‖f‖ = 0 ↔ ∀ (i : Fin d), f i = 0·
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0 
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mpr
(∀ (i : Fin d), f i = 0) → ‖f‖ = 0intro norm_eq_0
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ‖f‖ = 0
mp
∀ (i : Fin d), f i = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0rw [
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ‖f‖ = 0
mp
∀ (i : Fin d), f i = 0show ‖f‖ = inner f f by 
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ‖f‖ = 0
mp
∀ (i : Fin d), f i = 0rfl
Goals accomplished!
Goals accomplished! 🐙]
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: inner f f = 0
mp
∀ (i : Fin d), f i = 0 at norm_eq_0
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: inner f f = 0
mp
∀ (i : Fin d), f i = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0rw [
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: inner f f = 0
mp
∀ (i : Fin d), f i = 0show inner f f = ∑ i, inner (f i) (f i) by 
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: inner f f = 0
mp
∀ (i : Fin d), f i = 0rfl
Goals accomplished!
Goals accomplished! 🐙]
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ∑ i, inner (f i) (f i) = 0
mp
∀ (i : Fin d), f i = 0 at norm_eq_0
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ∑ i, inner (f i) (f i) = 0
mp
∀ (i : Fin d), f i = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0simp_rw [
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ∑ i, inner (f i) (f i) = 0
mp
∀ (i : Fin d), f i = 0λ i ↦ real_inner_self_eq_norm_sq (f i)
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ∑ x, ‖f x‖ ^ 2 = 0
mp
∀ (i : Fin d), f i = 0] at norm_eq_0
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ∑ x, ‖f x‖ ^ 2 = 0
mp
∀ (i : Fin d), f i = 0

    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0intro i
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ∑ x, ‖f x‖ ^ 2 = 0
i: Fin d
mp
f i = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0suffices h : ‖f i‖^2 = 0 from norm_eq_zero.mp <| sq_eq_zero_iff.mp h
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ∑ x, ‖f x‖ ^ 2 = 0
i: Fin d
mp
‖f i‖ ^ 2 = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0have sq_norm_nonneg : ∀ i ∈ univ, (0 : ℝ) <= ‖f i‖^2 := λ i _ ↦ sq_nonneg (‖f i‖)
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
norm_eq_0: ∑ x, ‖f x‖ ^ 2 = 0
i: Fin d
sq_norm_nonneg: ∀ i ∈ univ, 0 ≤ ‖f i‖ ^ 2
mp
‖f i‖ ^ 2 = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
mp
‖f‖ = 0 → ∀ (i : Fin d), f i = 0exact (sum_eq_zero_iff_of_nonneg sq_norm_nonneg).mp norm_eq_0 i (mem_univ i)
Goals accomplished!
Goals accomplished! 🐙

  
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
‖f‖ = 0 ↔ ∀ (i : Fin d), f i = 0intro hf
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
mpr
‖f‖ = 0
  
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
‖f‖ = 0 ↔ ∀ (i : Fin d), f i = 0rw [
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
mpr
‖f‖ = 0show ‖f‖ = inner f f by 
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
mpr
‖f‖ = 0rfl
Goals accomplished!
Goals accomplished! 🐙]
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
mpr
inner f f = 0
  
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
‖f‖ = 0 ↔ ∀ (i : Fin d), f i = 0rw [
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
mpr
inner f f = 0show inner f f = ∑ i, inner (f i) (f i) by 
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
mpr
inner f f = 0rfl
Goals accomplished!
Goals accomplished! 🐙]
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
mpr
∑ i, inner (f i) (f i) = 0
  
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
‖f‖ = 0 ↔ ∀ (i : Fin d), f i = 0have inner_eq_0 : ∀ i ∈ univ, inner (f i) (f i) = (0 : ℝ) := 
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
mpr
∑ i, inner (f i) (f i) = 0by
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
∀ i ∈ univ, inner (f i) (f i) = 0{
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
∀ i ∈ univ, inner (f i) (f i) = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
∀ i ∈ univ, inner (f i) (f i) = 0intro i _
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
i: Fin d
a✝: i ∈ univ
inner (f i) (f i) = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
∀ i ∈ univ, inner (f i) (f i) = 0rw [
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
i: Fin d
a✝: i ∈ univ
inner (f i) (f i) = 0hf i
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
i: Fin d
a✝: i ∈ univ
inner 0 0 = 0]
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
i: Fin d
a✝: i ∈ univ
inner 0 0 = 0
    
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
∀ i ∈ univ, inner (f i) (f i) = 0exact inner_zero_right 0
Goals accomplished!
Goals accomplished! 🐙
  }
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
‖f‖ = 0 ↔ ∀ (i : Fin d), f i = 0rw [
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
inner_eq_0: ∀ i ∈ univ, inner (f i) (f i) = 0
mpr
∑ i, inner (f i) (f i) = 0sum_congr rfl inner_eq_0
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
inner_eq_0: ∀ i ∈ univ, inner (f i) (f i) = 0
mpr
∑ x, 0 = 0]
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
hf: ∀ (i : Fin d), f i = 0
inner_eq_0: ∀ i ∈ univ, inner (f i) (f i) = 0
mpr
∑ x, 0 = 0
  
Goals accomplished!
α: Type u_1
H: Set (α → ℝ)
inst✝²: NormedAddCommGroup ↑H
inst✝¹: InnerProductSpace ℝ ↑H
inst✝: RKHS H
d: ℕ
hd: d ≠ 0
f: product_RKHS H hd
‖f‖ = 0 ↔ ∀ (i : Fin d), f i = 0exact sum_const_zero
Goals accomplished!
Goals accomplished! 🐙

end RKHS