interactionDefect_RCLCombiner

formal source

 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 :
 131    SeparatelyAdditive (RCLCombiner 0) := by
 132  refine ⟨fun u => 2 * u, fun v => 2 * v, ?_⟩
 133  intro u v
 134  unfold RCLCombiner
 135  ring
 136
 137/-- For `c ≠ 0`, the RCL combiner has nonvanishing interaction defect
 138at the test point `(1, 1)`. -/
 139theorem RCLCombiner_nonzero_couples (c : ℝ) (hc : c ≠ 0) :
 140    interactionDefect (RCLCombiner c) 1 1 ≠ 0 := by
 141  rw [interactionDefect_RCLCombiner]
 142  simpa using hc
 143
 144/-- **The RCL combiner is a coupling combiner iff `c ≠ 0`.** -/
 145theorem RCLCombiner_isCoupling_iff (c : ℝ) :
 146    IsCouplingCombiner (RCLCombiner c) ↔ c ≠ 0 := by
 147  rw [isCouplingCombiner_iff_interactionDefect_nonzero]
 148  constructor
 149  · rintro ⟨u, v, huv⟩
 150    intro hc
 151    apply huv
 152    rw [interactionDefect_RCLCombiner, hc]