Prcl_mixed_diff

formal source

  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. -/
  91theorem Prcl_not_separable : ¬ IsSeparable Prcl := by
  92  intro ⟨α, β, h⟩
  93  -- If Prcl(u,v) = α(u) + β(v), then the mixed second difference is 0
  94  have hsep : Prcl 1 1 - Prcl 1 0 - Prcl 0 1 + Prcl 0 0 = 0 := by
  95    calc Prcl 1 1 - Prcl 1 0 - Prcl 0 1 + Prcl 0 0
  96        = (α 1 + β 1) - (α 1 + β 0) - (α 0 + β 1) + (α 0 + β 0) := by
  97          simp only [h 1 1, h 1 0, h 0 1, h 0 0]
  98      _ = 0 := by ring
  99  rw [Prcl_mixed_diff] at hsep
 100  norm_num at hsep
 101
 102/-! ## Separability is Equivalent to Zero Mixed Difference -/
 103
 104/-- Separable implies zero mixed difference. -/
 105theorem separable_implies_zero_mixed_diff (P : ℝ → ℝ → ℝ) (hSep : IsSeparable P) :
 106    ∀ u₀ v₀ u₁ v₁, P u₁ v₁ - P u₁ v₀ - P u₀ v₁ + P u₀ v₀ = 0 := by
 107  obtain ⟨α, β, h⟩ := hSep
 108  intro u₀ v₀ u₁ v₁