IndisputableMonolith.Cost.Ndim.Core

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# N-dimensional reciprocal cost: core definitions
   6
   7This module defines the multi-component reciprocal cost by lifting the scalar
   8kernel through a weighted log aggregate.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Cost
  13namespace Ndim
  14
  15open scoped BigOperators
  16
  17/-- `n`-component real vectors as coordinate functions. -/
  18abbrev Vec (n : ℕ) := Fin n → ℝ
  19
  20/-- Weighted dot product used by the logarithmic aggregate. -/
  21def dot {n : ℕ} (α t : Vec n) : ℝ := ∑ i : Fin n, α i * t i
  22
  23/-- Componentwise logarithm. -/
  24noncomputable def logVec {n : ℕ} (x : Vec n) : Vec n := fun i => Real.log (x i)
  25
  26/-- Componentwise multiplication. -/
  27def hadamardMul {n : ℕ} (x y : Vec n) : Vec n := fun i => x i * y i
  28
  29/-- Componentwise inversion. -/
  30noncomputable def hadamardInv {n : ℕ} (x : Vec n) : Vec n := fun i => (x i)⁻¹
  31
  32/-- Componentwise division. -/
  33noncomputable def hadamardDiv {n : ℕ} (x y : Vec n) : Vec n := fun i => x i / y i
  34
  35/-- Exponential aggregate `R(x) = exp(∑ αᵢ log xᵢ)`. -/
  36noncomputable def aggregate {n : ℕ} (α x : Vec n) : ℝ :=
  37  Real.exp (dot α (logVec x))
  38
  39/-- Log-coordinate `n`-dimensional cost. -/
  40noncomputable def JlogN {n : ℕ} (α t : Vec n) : ℝ :=
  41  Jcost (Real.exp (dot α t))
  42
  43/-- Original positive-coordinate `n`-dimensional cost. -/
  44noncomputable def JcostN {n : ℕ} (α x : Vec n) : ℝ :=
  45  JlogN α (logVec x)
  46
  47@[simp] theorem aggregate_pos {n : ℕ} (α x : Vec n) : 0 < aggregate α x := by
  48  unfold aggregate
  49  exact Real.exp_pos _
  50
  51@[simp] theorem JcostN_eq_Jcost_aggregate {n : ℕ} (α x : Vec n) :
  52    JcostN α x = Jcost (aggregate α x) := by
  53  rfl
  54
  55theorem JlogN_eq_cosh_sub_one {n : ℕ} (α t : Vec n) :
  56    JlogN α t = Real.cosh (dot α t) - 1 := by
  57  simpa [JlogN] using (Jcost_exp_cosh (dot α t))
  58
  59theorem JcostN_eq_cosh_logsum {n : ℕ} (α x : Vec n) :
  60    JcostN α x = Real.cosh (dot α (logVec x)) - 1 := by
  61  simpa [JcostN, JlogN] using (Jcost_exp_cosh (dot α (logVec x)))
  62
  63/-- Normalization at the identity vector. -/
  64theorem JcostN_unit {n : ℕ} (α : Vec n) :
  65    JcostN α (fun _ => 1) = 0 := by
  66  simp [JcostN, JlogN, dot, logVec, Jcost_unit0]
  67
  68/-- Non-negativity follows from scalar non-negativity at positive aggregate. -/
  69theorem JcostN_nonneg {n : ℕ} (α x : Vec n) : 0 ≤ JcostN α x := by
  70  rw [JcostN_eq_Jcost_aggregate]
  71  exact Jcost_nonneg (aggregate_pos α x)
  72
  73/-- Log-aggregate of a componentwise product. -/
  74theorem dot_log_hadamardMul {n : ℕ} (α x y : Vec n)
  75    (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) :
  76    dot α (logVec (hadamardMul x y)) = dot α (logVec x) + dot α (logVec y) := by
  77  unfold dot logVec hadamardMul
  78  calc
  79    ∑ i : Fin n, α i * Real.log (x i * y i)
  80        = ∑ i : Fin n, α i * (Real.log (x i) + Real.log (y i)) := by
  81            refine Finset.sum_congr rfl ?_
  82            intro i hi
  83            rw [Real.log_mul (show x i ≠ 0 from (hx i).ne') (show y i ≠ 0 from (hy i).ne')]
  84    _ = ∑ i : Fin n, (α i * Real.log (x i) + α i * Real.log (y i)) := by
  85          refine Finset.sum_congr rfl ?_
  86          intro i hi
  87          ring
  88    _ = (∑ i : Fin n, α i * Real.log (x i)) + (∑ i : Fin n, α i * Real.log (y i)) := by
  89          simpa using Finset.sum_add_distrib
  90
  91/-- Log-aggregate of a componentwise quotient. -/
  92theorem dot_log_hadamardDiv {n : ℕ} (α x y : Vec n)
  93    (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) :
  94    dot α (logVec (hadamardDiv x y)) = dot α (logVec x) - dot α (logVec y) := by
  95  unfold dot logVec hadamardDiv
  96  calc
  97    ∑ i : Fin n, α i * Real.log (x i / y i)
  98        = ∑ i : Fin n, α i * (Real.log (x i) - Real.log (y i)) := by
  99            refine Finset.sum_congr rfl ?_
 100            intro i hi
 101            rw [Real.log_div (show x i ≠ 0 from (hx i).ne') (show y i ≠ 0 from (hy i).ne')]
 102    _ = ∑ i : Fin n, (α i * Real.log (x i) - α i * Real.log (y i)) := by
 103          refine Finset.sum_congr rfl ?_
 104          intro i hi
 105          ring
 106    _ = (∑ i : Fin n, α i * Real.log (x i)) - (∑ i : Fin n, α i * Real.log (y i)) := by
 107          simp [Finset.sum_sub_distrib]
 108
 109/-- Log-aggregate of a componentwise inverse. -/
 110theorem dot_log_hadamardInv {n : ℕ} (α x : Vec n) :
 111    dot α (logVec (hadamardInv x)) = - dot α (logVec x) := by
 112  unfold dot logVec hadamardInv
 113  calc
 114    ∑ i : Fin n, α i * Real.log ((x i)⁻¹)
 115        = ∑ i : Fin n, α i * (-Real.log (x i)) := by
 116            refine Finset.sum_congr rfl ?_
 117            intro i hi
 118            rw [Real.log_inv]
 119    _ = ∑ i : Fin n, -(α i * Real.log (x i)) := by
 120          refine Finset.sum_congr rfl ?_
 121          intro i hi
 122          ring
 123    _ = - (∑ i : Fin n, α i * Real.log (x i)) := by
 124          simp
 125
 126/-- Reciprocity under componentwise inversion. -/
 127theorem JcostN_reciprocal {n : ℕ} (α x : Vec n) :
 128    JcostN α (hadamardInv x) = JcostN α x := by
 129  rw [JcostN_eq_cosh_logsum, JcostN_eq_cosh_logsum]
 130  rw [dot_log_hadamardInv, Real.cosh_neg]
 131
 132/-- Zero-cost characterization in log coordinates. -/
 133theorem JcostN_eq_zero_iff {n : ℕ} (α x : Vec n) :
 134    JcostN α x = 0 ↔ dot α (logVec x) = 0 := by
 135  unfold JcostN JlogN
 136  simpa [Jlog] using (Jlog_eq_zero_iff (t := dot α (logVec x)))
 137
 138end Ndim
 139end Cost
 140end IndisputableMonolith
 141