IndisputableMonolith.Cost.Ndim.DAlembert

   1import IndisputableMonolith.Cost.Ndim.Core
   2
   3/-!
   4# Multidimensional d'Alembert / RCL identity
   5-/
   6
   7namespace IndisputableMonolith
   8namespace Cost
   9namespace Ndim
  10
  11theorem JcostN_dAlembert {n : ℕ} (α x y : Vec n)
  12    (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) :
  13    JcostN α (hadamardMul x y) + JcostN α (hadamardDiv x y)
  14      = 2 * JcostN α x + 2 * JcostN α y + 2 * JcostN α x * JcostN α y := by
  15  let u : ℝ := Real.exp (dot α (logVec x))
  16  let v : ℝ := Real.exp (dot α (logVec y))
  17  have hu : 0 < u := by
  18    dsimp [u]
  19    exact Real.exp_pos _
  20  have hv : 0 < v := by
  21    dsimp [v]
  22    exact Real.exp_pos _
  23  have hmul :
  24      JcostN α (hadamardMul x y) = Jcost (u * v) := by
  25    calc
  26      JcostN α (hadamardMul x y)
  27          = Jcost (Real.exp (dot α (logVec (hadamardMul x y)))) := by
  28              simp [JcostN, JlogN]
  29      _ = Jcost (Real.exp (dot α (logVec x) + dot α (logVec y))) := by
  30            rw [dot_log_hadamardMul α x y hx hy]
  31      _ = Jcost (u * v) := by
  32            simp [u, v, Real.exp_add]
  33  have hdiv :
  34      JcostN α (hadamardDiv x y) = Jcost (u / v) := by
  35    calc
  36      JcostN α (hadamardDiv x y)
  37          = Jcost (Real.exp (dot α (logVec (hadamardDiv x y)))) := by
  38              simp [JcostN, JlogN]
  39      _ = Jcost (Real.exp (dot α (logVec x) - dot α (logVec y))) := by
  40            rw [dot_log_hadamardDiv α x y hx hy]
  41      _ = Jcost (u / v) := by
  42            simp [u, v, Real.exp_sub]
  43  have hbase := dalembert_identity (x := u) (y := v) hu hv
  44  calc
  45    JcostN α (hadamardMul x y) + JcostN α (hadamardDiv x y)
  46        = Jcost (u * v) + Jcost (u / v) := by rw [hmul, hdiv]
  47    _ = 2 * Jcost u + 2 * Jcost v + 2 * Jcost u * Jcost v := hbase
  48    _ = 2 * JcostN α x + 2 * JcostN α y + 2 * JcostN α x * JcostN α y := by
  49          simp [u, v, JcostN, JlogN]
  50
  51lemma JcostN_submult {n : ℕ} (α x y : Vec n)
  52    (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) :
  53    JcostN α (hadamardMul x y)
  54      ≤ 2 * JcostN α x + 2 * JcostN α y + 2 * JcostN α x * JcostN α y := by
  55  have h := JcostN_dAlembert α x y hx hy
  56  have hnonneg : 0 ≤ JcostN α (hadamardDiv x y) := JcostN_nonneg α (hadamardDiv x y)
  57  linarith
  58
  59end Ndim
  60end Cost
  61end IndisputableMonolith
  62