AApply

formal source

  23
  24/-- The rank-one operator `A = h^{-1} \tilde g` in coordinates, where
  25`\tilde g = λ β ⊗ β`. -/
  26noncomputable def AApply {n : ℕ}
  27    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n) : Vec n → Vec n :=
  28  fun v => fun i => lam * sharp hInv β i * dot β v
  29
  30/-- The scalar coefficient in the quadratic relation `A² = μ A`. -/
  31noncomputable def mu {n : ℕ}
  32    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n) : ℝ :=
  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)