isCouplingCombiner_iff_interactionDefect_nonzero

formal source

  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
 113/-! ## The RCL Combiner -/
 114
 115/-- The polynomial combiner attached to the RCL family with parameter
 116`c`: `P(u, v) = 2u + 2v + c·u·v`. -/
 117def RCLCombiner (c : ℝ) : ℝ → ℝ → ℝ :=
 118  fun u v => 2 * u + 2 * v + c * u * v
 119
 120/-- The interaction defect of the RCL combiner at `(u, v)` is exactly
 121`c · u · v`. -/
 122theorem interactionDefect_RCLCombiner (c u v : ℝ) :
 123    interactionDefect (RCLCombiner c) u v = c * u * v := by
 124  unfold interactionDefect RCLCombiner
 125  ring
 126
 127/-- For `c = 0`, the RCL combiner is the additive combiner
 128`P(u, v) = 2u + 2v`, separately additive with `p(u) = 2u` and
 129`q(v) = 2v`. -/
 130theorem RCLCombiner_zero_separatelyAdditive :