IndisputableMonolith.Cost.Ndim.RadicalDistribution

   1import IndisputableMonolith.Cost.Ndim.Hessian
   2
   3/-!
   4# Radical distribution for the rank-one log-coordinate metric
   5
   6The log-coordinate Hessian only detects the single active direction `α`.
   7Its radical distribution is therefore the constant hyperplane `dot α v = 0`.
   8
   9We formalize this distribution and its integrability via affine leaves
  10`{ t | dot α t = c }`.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Cost
  15namespace Ndim
  16
  17open scoped BigOperators
  18
  19/-- The radical distribution of the rank-one Hessian metric. -/
  20def Radical {n : ℕ} (α : Vec n) : Set (Vec n) :=
  21  { v | dot α v = 0 }
  22
  23/-- The affine leaves orthogonal to the active direction. -/
  24def LevelSet {n : ℕ} (α : Vec n) (c : ℝ) : Set (Vec n) :=
  25  { t | dot α t = c }
  26
  27/-- Affine translation along a constant direction. -/
  28def affineShift {n : ℕ} (t v : Vec n) (s : ℝ) : Vec n :=
  29  fun i => t i + s * v i
  30
  31@[simp] theorem mem_Radical_iff {n : ℕ} (α : Vec n) (v : Vec n) :
  32    v ∈ Radical α ↔ dot α v = 0 := Iff.rfl
  33
  34@[simp] theorem mem_LevelSet_iff {n : ℕ} (α : Vec n) (c : ℝ) (t : Vec n) :
  35    t ∈ LevelSet α c ↔ dot α t = c := Iff.rfl
  36
  37@[simp] theorem zero_mem_Radical {n : ℕ} (α : Vec n) :
  38    (fun _ => 0 : Vec n) ∈ Radical α := by
  39  unfold Radical dot
  40  simp
  41
  42theorem add_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
  43    (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
  44    v + w ∈ Radical α := by
  45  unfold Radical dot at hv hw ⊢
  46  have hv0 : ∑ i : Fin n, α i * v i = 0 := hv
  47  have hw0 : ∑ i : Fin n, α i * w i = 0 := hw
  48  calc
  49    ∑ i : Fin n, α i * (v i + w i)
  50        = (∑ i : Fin n, α i * v i) + ∑ i : Fin n, α i * w i := by
  51            simp [mul_add, Finset.sum_add_distrib]
  52    _ = 0 := by rw [hv0, hw0]; ring
  53
  54theorem smul_mem_Radical {n : ℕ} (α : Vec n) {v : Vec n} (s : ℝ)
  55    (hv : v ∈ Radical α) :
  56    s • v ∈ Radical α := by
  57  unfold Radical dot at hv ⊢
  58  calc
  59    ∑ i : Fin n, α i * (s * v i)
  60        = s * ∑ i : Fin n, α i * v i := by
  61            rw [Finset.mul_sum]
  62            apply Finset.sum_congr rfl
  63            intro i hi
  64            ring
  65    _ = 0 := by rw [hv]; ring
  66
  67theorem sub_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
  68    (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
  69    v - w ∈ Radical α := by
  70  simpa [sub_eq_add_neg] using
  71    add_mem_Radical α hv (smul_mem_Radical α (-1) hw)
  72
  73/-- The Hessian quadratic form vanishes exactly on the radical distribution. -/
  74theorem quadraticHessian_eq_zero_iff {n : ℕ} (α t v : Vec n) :
  75    quadraticHessian α t v = 0 ↔ v ∈ Radical α := by
  76  rw [quadraticHessian_eq]
  77  constructor
  78  · intro hq
  79    unfold Radical
  80    have hcosh : 0 < Real.cosh (dot α t) := by positivity
  81    have hsq : (dot α v) ^ 2 = 0 := by
  82      exact (mul_eq_zero.mp (by simpa using hq)).resolve_left hcosh.ne'
  83    have hdot : dot α v = 0 := sq_eq_zero_iff.mp hsq
  84    exact hdot
  85  · intro hv
  86    rw [mem_Radical_iff] at hv
  87    simp [hv]
  88
  89/-- Weighted dot product along an affine shift. -/
  90theorem dot_affineShift {n : ℕ} (α t v : Vec n) (s : ℝ) :
  91    dot α (affineShift t v s) = dot α t + s * dot α v := by
  92  unfold dot affineShift
  93  calc
  94    ∑ i : Fin n, α i * (t i + s * v i)
  95        = ∑ i : Fin n, (α i * t i + s * (α i * v i)) := by
  96            apply Finset.sum_congr rfl
  97            intro i hi
  98            ring
  99    _ = (∑ i : Fin n, α i * t i) + s * ∑ i : Fin n, α i * v i := by
 100          rw [Finset.sum_add_distrib, Finset.mul_sum]
 101
 102/-- Directions in the radical stay inside the affine leaves `dot α = c`. -/
 103theorem affineShift_mem_LevelSet {n : ℕ} (α : Vec n) {c s : ℝ} {t v : Vec n}
 104    (ht : t ∈ LevelSet α c) (hv : v ∈ Radical α) :
 105    affineShift t v s ∈ LevelSet α c := by
 106  rw [mem_LevelSet_iff] at ht ⊢
 107  have hv' : dot α v = 0 := hv
 108  rw [dot_affineShift, ht, hv']
 109  ring
 110
 111/-- The radical distribution is integrable: its integral leaves are the affine
 112hyperplanes `dot α = c`. -/
 113theorem radical_integrable_by_affine_leaves {n : ℕ} (α : Vec n) (c : ℝ) :
 114    ∀ ⦃t v : Vec n⦄, t ∈ LevelSet α c → v ∈ Radical α →
 115      ∀ s : ℝ, affineShift t v s ∈ LevelSet α c := by
 116  intro t v ht hv s
 117  exact affineShift_mem_LevelSet α ht hv
 118
 119/-- A constant direction preserves the affine leaf through `t` exactly when it
 120lies in the radical distribution. -/
 121theorem preserves_own_leaf_iff_mem_Radical {n : ℕ} (α t v : Vec n) :
 122    (∀ s : ℝ, affineShift t v s ∈ LevelSet α (dot α t)) ↔ v ∈ Radical α := by
 123  constructor
 124  · intro h
 125    have h1 := h 1
 126    rw [mem_LevelSet_iff, dot_affineShift] at h1
 127    unfold Radical
 128    have : dot α v = 0 := by linarith
 129    exact this
 130  · intro hv s
 131    exact affineShift_mem_LevelSet α (by simp [LevelSet]) hv
 132
 133end Ndim
 134end Cost
 135end IndisputableMonolith
 136