Padd_mixed_diff_zero

formal source

  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. -/
  85theorem Prcl_entangling : IsEntangling Prcl := by
  86  use 0, 0, 1, 1
  87  rw [Prcl_mixed_diff]
  88  norm_num
  89
  90/-- Prcl is NOT separable. -/