PApply

formal source

  33  lam * dot β (sharp hInv β)
  34
  35/-- The normalized projector associated to `A`. -/
  36noncomputable def PApply {n : ℕ}
  37    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n) : Vec n → Vec n :=
  38  fun v => (mu lam hInv β)⁻¹ • AApply lam hInv β v
  39
  40/-- The induced almost-product operator `F = 2P - I`. -/
  41noncomputable def FApply {n : ℕ}
  42    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n) : Vec n → Vec n :=
  43  fun v => 2 • PApply lam hInv β v - v
  44
  45/-- The induced golden operator. -/
  46noncomputable def GApply {n : ℕ}
  47    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n) : Vec n → Vec n :=
  48  fun v => ((1 : ℝ) / 2) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v
  49
  50/-- The metallic family derived from the same almost-product operator. -/
  51noncomputable def MetallicApply {n : ℕ}
  52    (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n) : Vec n → Vec n :=
  53  fun v => (p / 2) • v + (Real.sqrt (p ^ 2 + 4 * q) / 2) • FApply lam hInv β v
  54
  55theorem AApply_smul {n : ℕ}
  56    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
  57    (c : ℝ) (v : Vec n) :
  58    AApply lam hInv β (c • v) = c • AApply lam hInv β v := by
  59  funext i
  60  unfold AApply dot
  61  calc
  62    lam * sharp hInv β i * ∑ j : Fin n, β j * (c * v j)
  63        = lam * sharp hInv β i * (c * ∑ j : Fin n, β j * v j) := by
  64            congr 1
  65            rw [Finset.mul_sum]
  66            apply Finset.sum_congr rfl