IndisputableMonolith.Cost.Ndim.Bridge

   1import IndisputableMonolith.Cost.Ndim.Core
   2
   3/-!
   4# Additive-multiplicative quadratic bridge
   5-/
   6
   7namespace IndisputableMonolith
   8namespace Cost
   9namespace Ndim
  10
  11open scoped BigOperators
  12
  13/-- Quadratic additive approximation `1/2 * Σ εᵢ²`. -/
  14noncomputable def additiveQuadratic {n : ℕ} (ε : Vec n) : ℝ :=
  15  (1 / 2 : ℝ) * ∑ i : Fin n, (ε i) ^ 2
  16
  17/-- Quadratic multiplicative approximation `1/2 * (Σ αᵢ εᵢ)²`. -/
  18noncomputable def multiplicativeQuadratic {n : ℕ} (α ε : Vec n) : ℝ :=
  19  (1 / 2 : ℝ) * (dot α ε) ^ 2
  20
  21/-- Residual compensatory quadratic term. -/
  22noncomputable def compensatoryQuadratic {n : ℕ} (α ε : Vec n) : ℝ :=
  23  additiveQuadratic ε - multiplicativeQuadratic α ε
  24
  25theorem additive_decomposition {n : ℕ} (α ε : Vec n) :
  26    additiveQuadratic ε
  27      = multiplicativeQuadratic α ε + compensatoryQuadratic α ε := by
  28  unfold compensatoryQuadratic
  29  ring
  30
  31/-- Squared Cauchy-Schwarz bound in our notation. -/
  32theorem dot_sq_le_sqNorm_mul {n : ℕ} (α ε : Vec n) :
  33    (dot α ε) ^ 2 ≤ (dot α α) * (∑ i : Fin n, (ε i) ^ 2) := by
  34  unfold dot
  35  simpa [pow_two] using
  36    (Finset.sum_mul_sq_le_sq_mul_sq (s := (Finset.univ : Finset (Fin n))) α ε)
  37
  38/-- If `‖α‖² ≤ 1`, multiplicative quadratic cost is bounded by additive quadratic cost. -/
  39theorem multiplicative_le_additive_of_sqNorm_le_one {n : ℕ}
  40    (α ε : Vec n) (hα : dot α α ≤ 1) :
  41    multiplicativeQuadratic α ε ≤ additiveQuadratic ε := by
  42  have hsq : (dot α ε) ^ 2 ≤ ∑ i : Fin n, (ε i) ^ 2 := by
  43    have hcs : (dot α ε) ^ 2 ≤ (dot α α) * (∑ i : Fin n, (ε i) ^ 2) :=
  44      dot_sq_le_sqNorm_mul α ε
  45    have hsum_nonneg : 0 ≤ ∑ i : Fin n, (ε i) ^ 2 := by
  46      exact Finset.sum_nonneg (fun i _ => sq_nonneg (ε i))
  47    have hmul : (dot α α) * (∑ i : Fin n, (ε i) ^ 2) ≤ 1 * (∑ i : Fin n, (ε i) ^ 2) :=
  48      mul_le_mul_of_nonneg_right hα hsum_nonneg
  49    exact le_trans hcs (by simpa using hmul)
  50  have hhalf : (0 : ℝ) ≤ 1 / 2 := by norm_num
  51  have hscaled := mul_le_mul_of_nonneg_left hsq hhalf
  52  simpa [multiplicativeQuadratic, additiveQuadratic, one_mul] using hscaled
  53
  54/-- Under normalized weights (`‖α‖² ≤ 1`), the compensatory term is nonnegative. -/
  55theorem compensatory_nonneg_of_sqNorm_le_one {n : ℕ}
  56    (α ε : Vec n) (hα : dot α α ≤ 1) :
  57    0 ≤ compensatoryQuadratic α ε := by
  58  unfold compensatoryQuadratic
  59  have hle := multiplicative_le_additive_of_sqNorm_le_one α ε hα
  60  linarith
  61
  62end Ndim
  63end Cost
  64end IndisputableMonolith
  65