separatelyAdditive_of_interactionDefect_zero

formal source

  79/-- Conversely: a combiner whose interaction defect is identically zero is
  80separately additive. The witness functions are `p(u) := P(u, 0) - P(0, 0)`
  81and `q(v) := P(0, v)`. -/
  82theorem separatelyAdditive_of_interactionDefect_zero
  83    {P : ℝ → ℝ → ℝ} (h : ∀ u v : ℝ, interactionDefect P u v = 0) :
  84    SeparatelyAdditive P := by
  85  refine ⟨fun u => P u 0 - P 0 0, fun v => P 0 v, ?_⟩
  86  intro u v
  87  have h_uv := h u v
  88  unfold interactionDefect at h_uv
  89  linarith
  90
  91/-- **Equivalence: separate additivity is identical vanishing of the
  92interaction defect.** -/
  93theorem separatelyAdditive_iff_interactionDefect_zero
  94    (P : ℝ → ℝ → ℝ) :
  95    SeparatelyAdditive P ↔ ∀ u v : ℝ, interactionDefect P u v = 0 :=
  96  ⟨interactionDefect_eq_zero_of_separatelyAdditive,
  97   separatelyAdditive_of_interactionDefect_zero⟩
  98
  99/-- **Equivalence: coupling is non-vanishing interaction defect.** -/
 100theorem isCouplingCombiner_iff_interactionDefect_nonzero
 101    (P : ℝ → ℝ → ℝ) :
 102    IsCouplingCombiner P ↔ ∃ u v : ℝ, interactionDefect P u v ≠ 0 := by
 103  unfold IsCouplingCombiner
 104  rw [separatelyAdditive_iff_interactionDefect_zero]
 105  constructor
 106  · intro h
 107    by_contra hno
 108    push_neg at hno
 109    exact h hno
 110  · rintro ⟨u, v, huv⟩ hall
 111    exact huv (hall u v)
 112