def
definition
GApply
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cost.Ndim.Projector on GitHub at line 46.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
72 ring
73
74theorem AApply_add {n : ℕ}
75 (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
76 (v w : Vec n) :