Theorem: Hilbert_kernel_bound (Carleson/Theorem1_1/Hilbert_kernel.lean)

State before:
x y : ℝ
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
by_cases h : 0 < |x - y| ∧ |x - y| < 1
State after:
case pos
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

case neg
x y : ℝ
h : ¬(0 < |x - y| ∧ |x - y| < 1)
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

State before:
case pos
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

case neg
x y : ℝ
h : ¬(0 < |x - y| ∧ |x - y| < 1)
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
. calc ‖K x y‖
    _ ≤ 1 / ‖1 - Complex.exp (Complex.I * ↑(x - y))‖ := by
      rw [K, k, norm_div]
      gcongr
      rw [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg]
      . apply max_le _ zero_le_one
        linarith [abs_nonneg (x-y)]
      . apply le_max_right
    _ ≤ 1 / (|x - y| / 2) := by
      gcongr
      . linarith
      . apply lower_secant_bound _ (by rfl)
        rw [Set.mem_Icc]
        constructor
        . simp
          calc |x - y|
            _ ≤ 1 := h.2.le
            _ ≤ 2 * Real.pi - 1 := by
              rw [le_sub_iff_add_le]
              linarith [Real.two_le_pi]
            _ ≤ 2 * Real.pi + (x - y) := by
              rw [sub_eq_add_neg]
              gcongr
              exact (abs_le.mp h.2.le).1
        . calc x - y
            _ ≤ |x - y| := le_abs_self (x - y)
            _ ≤ 1 := h.2.le
            _ ≤ 2 * Real.pi - 1 := by
              rw [le_sub_iff_add_le]
              linarith [Real.two_le_pi]
            _ ≤ 2 * Real.pi - |x - y| := by
              gcongr
              exact h.2.le
    _ = 2 / |x - y| := by
      field_simp
    _ ≤ (2 : ℝ) ^ (2 : ℝ) / (2 * |x - y|) := by
      ring_nf
      trivial
State after:
case neg
x y : ℝ
h : ¬(0 < |x - y| ∧ |x - y| < 1)
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

State before:
case neg
x y : ℝ
h : ¬(0 < |x - y| ∧ |x - y| < 1)
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
. push_neg at h
  have : ‖K x y‖ = 0 := by
    rw [norm_eq_zero, K, k, _root_.div_eq_zero_iff]
    by_cases xeqy : x = y
    . right
      simp [xeqy]
    . left
      simp only [Complex.ofReal_eq_zero, max_eq_right_iff, tsub_le_iff_right, zero_add]
      exact h (abs_pos.mpr (sub_ne_zero.mpr xeqy))
  rw [this]
  apply div_nonneg
  . norm_num
  . linarith [abs_nonneg (x-y)]
State after:
no goals

State before:
case pos
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
calc ‖K x y‖
  _ ≤ 1 / ‖1 - Complex.exp (Complex.I * ↑(x - y))‖ := by
    rw [K, k, norm_div]
    gcongr
    rw [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg]
    . apply max_le _ zero_le_one
      linarith [abs_nonneg (x-y)]
    . apply le_max_right
  _ ≤ 1 / (|x - y| / 2) := by
    gcongr
    . linarith
    . apply lower_secant_bound _ (by rfl)
      rw [Set.mem_Icc]
      constructor
      . simp
        calc |x - y|
          _ ≤ 1 := h.2.le
          _ ≤ 2 * Real.pi - 1 := by
            rw [le_sub_iff_add_le]
            linarith [Real.two_le_pi]
          _ ≤ 2 * Real.pi + (x - y) := by
            rw [sub_eq_add_neg]
            gcongr
            exact (abs_le.mp h.2.le).1
      . calc x - y
          _ ≤ |x - y| := le_abs_self (x - y)
          _ ≤ 1 := h.2.le
          _ ≤ 2 * Real.pi - 1 := by
            rw [le_sub_iff_add_le]
            linarith [Real.two_le_pi]
          _ ≤ 2 * Real.pi - |x - y| := by
            gcongr
            exact h.2.le
  _ = 2 / |x - y| := by
    field_simp
  _ ≤ (2 : ℝ) ^ (2 : ℝ) / (2 * |x - y|) := by
    ring_nf
    trivial
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖K x y‖ ≤ 1 / ‖1 - (Complex.I * ↑(x - y)).exp‖
Tactic:
rw [K, k, norm_div]
State after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖↑(max (1 - |x - y|) 0)‖ / ‖1 - (Complex.I * ↑(x - y)).exp‖ ≤ 1 / ‖1 - (Complex.I * ↑(x - y)).exp‖

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖↑(max (1 - |x - y|) 0)‖ / ‖1 - (Complex.I * ↑(x - y)).exp‖ ≤ 1 / ‖1 - (Complex.I * ↑(x - y)).exp‖
Tactic:
gcongr
State after:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖↑(max (1 - |x - y|) 0)‖ ≤ 1

State before:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖↑(max (1 - |x - y|) 0)‖ ≤ 1
Tactic:
rw [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg]
State after:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ max (1 - |x - y|) 0 ≤ 1

case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 ≤ max (1 - |x - y|) 0

State before:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ max (1 - |x - y|) 0 ≤ 1

case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
. apply max_le _ zero_le_one
  linarith [abs_nonneg (x-y)]
State after:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 ≤ max (1 - |x - y|) 0

State before:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
. apply le_max_right
State after:
no goals

State before:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ max (1 - |x - y|) 0 ≤ 1
Tactic:
apply max_le _ zero_le_one
State after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 - |x - y| ≤ 1

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 - |x - y| ≤ 1
Tactic:
linarith [abs_nonneg (x-y)]
State after:
no goals

State before:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
apply le_max_right
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 / ‖1 - (Complex.I * ↑(x - y)).exp‖ ≤ 1 / (|x - y| / 2)
Tactic:
gcongr
State after:
case hc
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 < |x - y| / 2

case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| / 2 ≤ ‖1 - (Complex.I * ↑(x - y)).exp‖

State before:
case hc
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 < |x - y| / 2

case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| / 2 ≤ ‖1 - (Complex.I * ↑(x - y)).exp‖
Tactic:
. linarith
State after:
case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| / 2 ≤ ‖1 - (Complex.I * ↑(x - y)).exp‖

State before:
case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| / 2 ≤ ‖1 - (Complex.I * ↑(x - y)).exp‖
Tactic:
. apply lower_secant_bound _ (by rfl)
  rw [Set.mem_Icc]
  constructor
  . simp
    calc |x - y|
      _ ≤ 1 := h.2.le
      _ ≤ 2 * Real.pi - 1 := by
        rw [le_sub_iff_add_le]
        linarith [Real.two_le_pi]
      _ ≤ 2 * Real.pi + (x - y) := by
        rw [sub_eq_add_neg]
        gcongr
        exact (abs_le.mp h.2.le).1
  . calc x - y
      _ ≤ |x - y| := le_abs_self (x - y)
      _ ≤ 1 := h.2.le
      _ ≤ 2 * Real.pi - 1 := by
        rw [le_sub_iff_add_le]
        linarith [Real.two_le_pi]
      _ ≤ 2 * Real.pi - |x - y| := by
        gcongr
        exact h.2.le
State after:
no goals

State before:
case hc
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 < |x - y| / 2
Tactic:
linarith
State after:
no goals

State before:
case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| / 2 ≤ ‖1 - (Complex.I * ↑(x - y)).exp‖
Tactic:
apply lower_secant_bound _ (by rfl)
State after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ x - y ∈ Set.Icc (-2 * Real.pi + |x - y|) (2 * Real.pi - |x - y|)

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ x - y ∈ Set.Icc (-2 * Real.pi + |x - y|) (2 * Real.pi - |x - y|)
Tactic:
rw [Set.mem_Icc]
State after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -2 * Real.pi + |x - y| ≤ x - y ∧ x - y ≤ 2 * Real.pi - |x - y|

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -2 * Real.pi + |x - y| ≤ x - y ∧ x - y ≤ 2 * Real.pi - |x - y|
Tactic:
constructor
State after:
case left
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -2 * Real.pi + |x - y| ≤ x - y

case right
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ x - y ≤ 2 * Real.pi - |x - y|

State before:
case left
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -2 * Real.pi + |x - y| ≤ x - y

case right
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ x - y ≤ 2 * Real.pi - |x - y|
Tactic:
. simp
  calc |x - y|
    _ ≤ 1 := h.2.le
    _ ≤ 2 * Real.pi - 1 := by
      rw [le_sub_iff_add_le]
      linarith [Real.two_le_pi]
    _ ≤ 2 * Real.pi + (x - y) := by
      rw [sub_eq_add_neg]
      gcongr
      exact (abs_le.mp h.2.le).1
State after:
case right
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ x - y ≤ 2 * Real.pi - |x - y|

State before:
case right
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ x - y ≤ 2 * Real.pi - |x - y|
Tactic:
. calc x - y
    _ ≤ |x - y| := le_abs_self (x - y)
    _ ≤ 1 := h.2.le
    _ ≤ 2 * Real.pi - 1 := by
      rw [le_sub_iff_add_le]
      linarith [Real.two_le_pi]
    _ ≤ 2 * Real.pi - |x - y| := by
      gcongr
      exact h.2.le
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ |x - y|
Tactic:
rfl
State after:
no goals

State before:
case left
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -2 * Real.pi + |x - y| ≤ x - y
Tactic:
simp
State after:
case left
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ 2 * Real.pi + (x - y)

State before:
case left
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ 2 * Real.pi + (x - y)
Tactic:
calc |x - y|
  _ ≤ 1 := h.2.le
  _ ≤ 2 * Real.pi - 1 := by
    rw [le_sub_iff_add_le]
    linarith [Real.two_le_pi]
  _ ≤ 2 * Real.pi + (x - y) := by
    rw [sub_eq_add_neg]
    gcongr
    exact (abs_le.mp h.2.le).1
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 ≤ 2 * Real.pi - 1
Tactic:
rw [le_sub_iff_add_le]
State after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 + 1 ≤ 2 * Real.pi

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 + 1 ≤ 2 * Real.pi
Tactic:
linarith [Real.two_le_pi]
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 * Real.pi - 1 ≤ 2 * Real.pi + (x - y)
Tactic:
rw [sub_eq_add_neg]
State after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 * Real.pi + -1 ≤ 2 * Real.pi + (x - y)

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 * Real.pi + -1 ≤ 2 * Real.pi + (x - y)
Tactic:
gcongr
State after:
case bc
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -1 ≤ x - y

State before:
case bc
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -1 ≤ x - y
Tactic:
exact (abs_le.mp h.2.le).1
State after:
no goals

State before:
case right
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ x - y ≤ 2 * Real.pi - |x - y|
Tactic:
calc x - y
  _ ≤ |x - y| := le_abs_self (x - y)
  _ ≤ 1 := h.2.le
  _ ≤ 2 * Real.pi - 1 := by
    rw [le_sub_iff_add_le]
    linarith [Real.two_le_pi]
  _ ≤ 2 * Real.pi - |x - y| := by
    gcongr
    exact h.2.le
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 * Real.pi - 1 ≤ 2 * Real.pi - |x - y|
Tactic:
gcongr
State after:
case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ 1

State before:
case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ 1
Tactic:
exact h.2.le
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 / (|x - y| / 2) = 2 / |x - y|
Tactic:
field_simp
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 / |x - y| ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
ring_nf
State after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y|⁻¹ * 2 ≤ |x - y|⁻¹ * 2

State before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y|⁻¹ * 2 ≤ |x - y|⁻¹ * 2
Tactic:
trivial
State after:
no goals

State before:
case neg
x y : ℝ
h : ¬(0 < |x - y| ∧ |x - y| < 1)
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
push_neg at h
State after:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

State before:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
have : ‖K x y‖ = 0 := by
  rw [norm_eq_zero, K, k, _root_.div_eq_zero_iff]
  by_cases xeqy : x = y
  . right
    simp [xeqy]
  . left
    simp only [Complex.ofReal_eq_zero, max_eq_right_iff, tsub_le_iff_right, zero_add]
    exact h (abs_pos.mpr (sub_ne_zero.mpr xeqy))
State after:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

State before:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
rw [this]
State after:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 ^ 2 / (2 * |x - y|)

State before:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
apply div_nonneg
State after:
case neg.ha
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 ^ 2

case neg.hb
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 * |x - y|

State before:
case neg.ha
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 ^ 2

case neg.hb
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 * |x - y|
Tactic:
. norm_num
State after:
case neg.hb
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 * |x - y|

State before:
case neg.hb
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 * |x - y|
Tactic:
. linarith [abs_nonneg (x-y)]
State after:
no goals

State before:
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
⊢ ‖K x y‖ = 0
Tactic:
rw [norm_eq_zero, K, k, _root_.div_eq_zero_iff]
State after:
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0

State before:
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0
Tactic:
by_cases xeqy : x = y
State after:
case pos
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : x = y
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0

case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0

State before:
case pos
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : x = y
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0

case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0
Tactic:
. right
  simp [xeqy]
State after:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0

State before:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0
Tactic:
. left
  simp only [Complex.ofReal_eq_zero, max_eq_right_iff, tsub_le_iff_right, zero_add]
  exact h (abs_pos.mpr (sub_ne_zero.mpr xeqy))
State after:
no goals

State before:
case pos
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : x = y
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0
Tactic:
right
State after:
case pos.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : x = y
⊢ 1 - (Complex.I * ↑(x - y)).exp = 0

State before:
case pos.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : x = y
⊢ 1 - (Complex.I * ↑(x - y)).exp = 0
Tactic:
simp [xeqy]
State after:
no goals

State before:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0
Tactic:
left
State after:
case neg.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ ↑(max (1 - |x - y|) 0) = 0

State before:
case neg.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ ↑(max (1 - |x - y|) 0) = 0
Tactic:
simp only [Complex.ofReal_eq_zero, max_eq_right_iff, tsub_le_iff_right, zero_add]
State after:
case neg.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ 1 ≤ |x - y|

State before:
case neg.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ 1 ≤ |x - y|
Tactic:
exact h (abs_pos.mpr (sub_ne_zero.mpr xeqy))
State after:
no goals

State before:
case neg.ha
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 ^ 2
Tactic:
norm_num
State after:
no goals

State before:
case neg.hb
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 * |x - y|
Tactic:
linarith [abs_nonneg (x-y)]
State after:
no goals