FApply

formal source

  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
  67            intro j hj
  68            ring
  69    _ = lam * sharp hInv β i * (c * dot β v) := by
  70          simp [dot]
  71    _ = c * (lam * sharp hInv β i * dot β v) := by