IndisputableMonolith.Cost.Ndim.Projector

   1import IndisputableMonolith.Cost.Ndim.Hessian
   2
   3/-!
   4# Cost-induced projector, almost-product, golden, and metallic operators
   5
   6This module packages the finite-dimensional operator algebra behind the
   7rank-one tensor picture. A covector `β` and an inverse metric kernel
   8`hInv` determine a sharp vector `β♯`, an operator
   9`A = h⁻¹ \tilde g`, its quadratic law `A² = μ A`, and the normalized
  10projector `P`.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Cost
  15namespace Ndim
  16
  17open scoped BigOperators
  18
  19/-- Raise a one-form `β` using the inverse metric kernel `hInv`. -/
  20noncomputable def sharp {n : ℕ}
  21    (hInv : Fin n → Fin n → ℝ) (β : Vec n) : Vec n :=
  22  fun i => ∑ j : Fin n, hInv i j * β j
  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)
  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)
  82        = lam * sharp hInv β i * ((∑ j : Fin n, β j * v j) + ∑ j : Fin n, β j * w j) := by
  83            congr 1
  84            simp [mul_add, Finset.sum_add_distrib]
  85    _ = lam * sharp hInv β i * dot β v + lam * sharp hInv β i * dot β w := by
  86          simp [dot]
  87          ring
  88    _ = (AApply lam hInv β v + AApply lam hInv β w) i := by
  89          simp [AApply]
  90
  91theorem AApply_neg {n : ℕ}
  92    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β w : Vec n) :
  93    AApply lam hInv β (-w) = -AApply lam hInv β w := by
  94  simpa using AApply_smul lam hInv β (-1) w
  95
  96theorem AApply_sub {n : ℕ}
  97    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
  98    (v w : Vec n) :
  99    AApply lam hInv β (v - w) = AApply lam hInv β v - AApply lam hInv β w := by
 100  ext i
 101  simp [sub_eq_add_neg, AApply_add, AApply_neg]
 102
 103theorem dot_AApply {n : ℕ}
 104    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β v : Vec n) :
 105    dot β (AApply lam hInv β v) = mu lam hInv β * dot β v := by
 106  unfold dot AApply mu
 107  calc
 108    ∑ i : Fin n, β i * (lam * sharp hInv β i * dot β v)
 109        = (lam * dot β v) * ∑ i : Fin n, β i * sharp hInv β i := by
 110            rw [Finset.mul_sum]
 111            apply Finset.sum_congr rfl
 112            intro i hi
 113            ring
 114    _ = (lam * ∑ i : Fin n, β i * sharp hInv β i) * dot β v := by
 115          ring
 116    _ = mu lam hInv β * dot β v := by
 117          simp [mu, dot]
 118
 119theorem AApply_sq {n : ℕ}
 120    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β v : Vec n) :
 121    AApply lam hInv β (AApply lam hInv β v) = mu lam hInv β • AApply lam hInv β v := by
 122  funext i
 123  have hdot :
 124      dot β (fun k => lam * sharp hInv β k * dot β v) = mu lam hInv β * dot β v := by
 125    simpa [AApply] using dot_AApply lam hInv β v
 126  unfold AApply
 127  rw [hdot]
 128  simp [mu]
 129  ring
 130
 131theorem PApply_smul {n : ℕ}
 132    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 133    (c : ℝ) (v : Vec n) :
 134    PApply lam hInv β (c • v) = c • PApply lam hInv β v := by
 135  ext i
 136  simp [PApply, AApply_smul, mul_assoc, mul_comm]
 137
 138theorem PApply_add {n : ℕ}
 139    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 140    (v w : Vec n) :
 141    PApply lam hInv β (v + w) = PApply lam hInv β v + PApply lam hInv β w := by
 142  ext i
 143  simp [PApply, AApply_add]
 144  ring
 145
 146theorem PApply_neg {n : ℕ}
 147    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β w : Vec n) :
 148    PApply lam hInv β (-w) = -PApply lam hInv β w := by
 149  simpa using PApply_smul lam hInv β (-1) w
 150
 151theorem PApply_sub {n : ℕ}
 152    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 153    (v w : Vec n) :
 154    PApply lam hInv β (v - w) = PApply lam hInv β v - PApply lam hInv β w := by
 155  ext i
 156  simp [sub_eq_add_neg, PApply_add, PApply_neg]
 157
 158theorem PApply_idempotent {n : ℕ}
 159    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 160    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 161    PApply lam hInv β (PApply lam hInv β v) = PApply lam hInv β v := by
 162  ext i
 163  simp [PApply, AApply_smul, AApply_sq, hμ, mul_comm]
 164
 165theorem PApply_FApply {n : ℕ}
 166    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 167    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 168    PApply lam hInv β (FApply lam hInv β v) = PApply lam hInv β v := by
 169  ext i
 170  have hsubi :
 171      PApply lam hInv β (FApply lam hInv β v) i
 172        = PApply lam hInv β (2 • PApply lam hInv β v) i - PApply lam hInv β v i := by
 173    unfold FApply
 174    rw [PApply_sub]
 175    rfl
 176  have hsmuli :
 177      PApply lam hInv β (2 • PApply lam hInv β v) i
 178        = (2 • PApply lam hInv β (PApply lam hInv β v)) i := by
 179    simpa using congrFun (PApply_smul lam hInv β 2 (PApply lam hInv β v)) i
 180  have hidi : PApply lam hInv β (PApply lam hInv β v) i = PApply lam hInv β v i := by
 181    simpa using congrFun (PApply_idempotent lam hInv β hμ v) i
 182  rw [hsubi, hsmuli]
 183  simp [hidi]
 184  ring
 185
 186theorem FApply_smul {n : ℕ}
 187    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 188    (c : ℝ) (v : Vec n) :
 189    FApply lam hInv β (c • v) = c • FApply lam hInv β v := by
 190  ext i
 191  simp [FApply, PApply_smul, mul_comm]
 192  ring
 193
 194theorem FApply_add {n : ℕ}
 195    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 196    (v w : Vec n) :
 197    FApply lam hInv β (v + w) = FApply lam hInv β v + FApply lam hInv β w := by
 198  ext i
 199  simp [FApply, PApply_add]
 200  ring
 201
 202theorem FApply_neg {n : ℕ}
 203    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β w : Vec n) :
 204    FApply lam hInv β (-w) = -FApply lam hInv β w := by
 205  simpa using FApply_smul lam hInv β (-1) w
 206
 207theorem FApply_sub {n : ℕ}
 208    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 209    (v w : Vec n) :
 210    FApply lam hInv β (v - w) = FApply lam hInv β v - FApply lam hInv β w := by
 211  ext i
 212  simp [sub_eq_add_neg, FApply_add, FApply_neg]
 213
 214theorem FApply_square {n : ℕ}
 215    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 216    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 217    FApply lam hInv β (FApply lam hInv β v) = v := by
 218  ext i
 219  have hPFi : PApply lam hInv β (FApply lam hInv β v) i = PApply lam hInv β v i := by
 220    simpa using congrFun (PApply_FApply lam hInv β hμ v) i
 221  calc
 222    FApply lam hInv β (FApply lam hInv β v) i
 223        = (2 • PApply lam hInv β (FApply lam hInv β v) - FApply lam hInv β v) i := by
 224            simp [FApply]
 225    _ = (2 • PApply lam hInv β v - FApply lam hInv β v) i := by
 226          simp [hPFi]
 227    _ = v i := by
 228          simp [FApply]
 229
 230theorem FApply_GApply {n : ℕ}
 231    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 232    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 233    FApply lam hInv β (GApply lam hInv β v)
 234      = ((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v := by
 235  unfold GApply
 236  rw [FApply_add, FApply_smul, FApply_smul, FApply_square _ _ _ hμ]
 237
 238theorem FApply_MetallicApply {n : ℕ}
 239    (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 240    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 241    FApply lam hInv β (MetallicApply p q lam hInv β v)
 242      = (p / 2) • FApply lam hInv β v
 243        + (Real.sqrt (p ^ 2 + 4 * q) / 2) • v := by
 244  unfold MetallicApply
 245  rw [FApply_add, FApply_smul, FApply_smul, FApply_square _ _ _ hμ]
 246
 247theorem GApply_square {n : ℕ}
 248    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 249    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 250    GApply lam hInv β (GApply lam hInv β v) = GApply lam hInv β v + v := by
 251  ext i
 252  have hFGi :
 253      FApply lam hInv β
 254          (((1 : ℝ) / 2) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v) i
 255        = (((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v) i := by
 256    simpa [GApply] using congrFun (FApply_GApply lam hInv β hμ v) i
 257  have hsqrt : Real.sqrt 5 * Real.sqrt 5 = 5 := by
 258    nlinarith [Real.sq_sqrt (by positivity : 0 ≤ (5 : ℝ))]
 259  have hsqrtq : (Real.sqrt 5 / 2) * (Real.sqrt 5 / 2) = 5 / 4 := by
 260    nlinarith [hsqrt]
 261  have hFGi' :
 262      FApply lam hInv β (((2 : ℝ)⁻¹) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v) i
 263        = (((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v) i := by
 264    simpa using hFGi
 265  simp [GApply]
 266  rw [hFGi']
 267  have hmul : (Real.sqrt 5 / 2) * ((Real.sqrt 5 / 2) * v i) = (5 / 4) * v i := by
 268    calc
 269      (Real.sqrt 5 / 2) * ((Real.sqrt 5 / 2) * v i)
 270          = ((Real.sqrt 5 / 2) * (Real.sqrt 5 / 2)) * v i := by
 271              ring
 272      _ = (5 / 4) * v i := by rw [hsqrtq]
 273  simp
 274  nlinarith [hmul]
 275
 276theorem MetallicApply_square {n : ℕ}
 277    (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 278    (hμ : mu lam hInv β ≠ 0) (hq : 0 ≤ p ^ 2 + 4 * q) (v : Vec n) :
 279    MetallicApply p q lam hInv β (MetallicApply p q lam hInv β v)
 280      = p • MetallicApply p q lam hInv β v + q • v := by
 281  ext i
 282  have hFMi :
 283      FApply lam hInv β
 284          ((p / 2) • v + (Real.sqrt (p ^ 2 + 4 * q) / 2) • FApply lam hInv β v) i
 285        = ((p / 2) • FApply lam hInv β v
 286          + (Real.sqrt (p ^ 2 + 4 * q) / 2) • v) i := by
 287    simpa [MetallicApply] using congrFun (FApply_MetallicApply p q lam hInv β hμ v) i
 288  have hsqrt : Real.sqrt (p ^ 2 + 4 * q) * Real.sqrt (p ^ 2 + 4 * q) = p ^ 2 + 4 * q := by
 289    nlinarith [Real.sq_sqrt hq]
 290  have hsqrtq :
 291      (Real.sqrt (p ^ 2 + 4 * q) / 2) * (Real.sqrt (p ^ 2 + 4 * q) / 2)
 292        = (p ^ 2 + 4 * q) / 4 := by
 293    nlinarith [hsqrt]
 294  simp [MetallicApply, hFMi]
 295  have hmul :
 296      (Real.sqrt (p ^ 2 + 4 * q) / 2) *
 297          ((Real.sqrt (p ^ 2 + 4 * q) / 2) * v i)
 298        = ((p ^ 2 + 4 * q) / 4) * v i := by
 299    calc
 300      (Real.sqrt (p ^ 2 + 4 * q) / 2) *
 301          ((Real.sqrt (p ^ 2 + 4 * q) / 2) * v i)
 302          = ((Real.sqrt (p ^ 2 + 4 * q) / 2) *
 303              (Real.sqrt (p ^ 2 + 4 * q) / 2)) * v i := by
 304              ring
 305      _ = ((p ^ 2 + 4 * q) / 4) * v i := by rw [hsqrtq]
 306  nlinarith [hmul]
 307
 308end Ndim
 309end Cost
 310end IndisputableMonolith
 311