def
definition
MetallicApply
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 51.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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) :
77 AApply lam hInv β (v + w) = AApply lam hInv β v + AApply lam hInv β w := by
78 funext i
79 unfold AApply dot
80 calc
81 lam * sharp hInv β i * ∑ j : Fin n, β j * (v j + w j)