interactionDefect

formal source

  60\]
  61For a separately additive combiner this is identically zero. The defect
  62is the canonical detector of coupling. -/
  63def interactionDefect (P : ℝ → ℝ → ℝ) (u v : ℝ) : ℝ :=
  64  P u v - P u 0 - P 0 v + P 0 0
  65
  66/-! ## Equivalent Forms -/
  67
  68/-- A separately additive combiner has identically vanishing interaction
  69defect. -/
  70theorem interactionDefect_eq_zero_of_separatelyAdditive
  71    {P : ℝ → ℝ → ℝ} (h : SeparatelyAdditive P) :
  72    ∀ u v : ℝ, interactionDefect P u v = 0 := by
  73  rcases h with ⟨p, q, hP⟩
  74  intro u v
  75  unfold interactionDefect
  76  rw [hP u v, hP u 0, hP 0 v, hP 0 0]
  77  ring
  78
  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