Padd_separable

formal source

  51def Padd (u v : ℝ) : ℝ := 2 * u + 2 * v
  52
  53/-- Padd is separable: P(u,v) = 2u + 2v = α(u) + β(v). -/
  54theorem Padd_separable : IsSeparable Padd := by
  55  use fun u => 2 * u, fun v => 2 * v
  56  intro u v
  57  rfl
  58
  59/-- The mixed second difference of Padd is zero. -/
  60theorem Padd_mixed_diff_zero : ∀ u₀ v₀ u₁ v₁ : ℝ,
  61    Padd u₁ v₁ - Padd u₁ v₀ - Padd u₀ v₁ + Padd u₀ v₀ = 0 := by
  62  intro u₀ v₀ u₁ v₁
  63  simp only [Padd]
  64  ring
  65
  66/-- Padd is not entangling. -/
  67theorem Padd_not_entangling : ¬ IsEntangling Padd := by
  68  intro ⟨u₀, v₀, u₁, v₁, h⟩
  69  exact h (Padd_mixed_diff_zero u₀ v₀ u₁ v₁)
  70
  71/-! ## The RCL Combiner is Entangling -/
  72
  73/-- The RCL combiner. -/
  74def Prcl (u v : ℝ) : ℝ := 2 * u * v + 2 * u + 2 * v
  75
  76/-- The mixed second difference of Prcl equals 2(u₁-u₀)(v₁-v₀).
  77    In particular, it's nonzero when u₁ ≠ u₀ and v₁ ≠ v₀. -/
  78theorem Prcl_mixed_diff : ∀ u₀ v₀ u₁ v₁ : ℝ,
  79    Prcl u₁ v₁ - Prcl u₁ v₀ - Prcl u₀ v₁ + Prcl u₀ v₀ = 2 * (u₁ - u₀) * (v₁ - v₀) := by
  80  intro u₀ v₀ u₁ v₁
  81  simp only [Prcl]
  82  ring
  83
  84/-- Prcl is entangling. Witness: (0,0) and (1,1) give mixed diff = 2. -/