internlm/Lean-Github huggingface dataset:
Theorem: classical_carleson
Proof state before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: classical_carleson
Proof state before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ 2 / 4 ≤ Real.pi
Tactic:
linarith [Real.two_le_pi]
Proof state after:
no goals
Theorem: classical_carleson
Proof state before:
f : ℝ → ℂ
unicontf : UniformContinuous f
periodicf : Function.Periodic f (2 * Real.pi)
ε : ℝ
εpos : 0 < ε
εle : ε ≤ 2 * Real.pi
ε' : ℝ := ε / 4 / C_control_approximation_effect ε
ε'def : ε' = ε / 4 / C_control_approximation_effect ε
ε'pos : ε' > 0
f₀ : ℝ → ℂ
contDiff_f₀ : ContDiff ℝ ⊤ f₀
periodic_f₀ : Function.Periodic f₀ (2 * Real.pi)
hf₀ : ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε'
ε4pos : ε / 4 > 0
N₀ : ℕ
hN₀ : ∀ N > N₀, ∀ x ∈ Set.Icc 0 (2 * Real.pi), Complex.abs (f₀ x - partialFourierSum f₀ N x) ≤ ε / 4
h : ℝ → ℂ := f₀ - f
hdef : h = f₀ - f
h_measurable : Measurable h
h_periodic : Function.Periodic h (2 * Real.pi)
h_bound : ∀ x ∈ Set.Icc (-Real.pi) (3 * Real.pi), Complex.abs (h x) ≤ ε'
E : Set ℝ
Esubset : E ⊆ Set.Icc 0 (2 * Real.pi)
Emeasurable : MeasurableSet E
Evolume : MeasureTheory.volume.real E ≤ ε
hE :
  ∀ x ∈ Set.Icc 0 (2 * Real.pi) \ E,
    ∀ (N : ℕ), Complex.abs (partialFourierSum h N x) ≤ C_control_approximation_effect ε * ε'
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi) \ E
N : ℕ
NgtN₀ : N > N₀
⊢ ε / 2 + ε / 4 + ε / 4 ≤ ε
Tactic:
linarith
Proof state after:
no goals
Theorem: k_of_neg_eq_conj_k
Proof state before:
x : ℝ
⊢ k (-x) = (starRingEnd ℂ) (k x)
Tactic:
simp [k, Complex.conj_ofReal, ←Complex.exp_conj, Complex.conj_I, neg_mul]
Proof state after:
no goals
Theorem: k_of_abs_le_one
Proof state before:
x : ℝ
abs_le_one : |x| ≤ 1
⊢ k x = (1 - ↑|x|) / (1 - (Complex.I * ↑x).exp)
Tactic:
rw [k, max_eq_left (by linarith)]
Proof state after:
x : ℝ
abs_le_one : |x| ≤ 1
⊢ ↑(1 - |x|) / (1 - (Complex.I * ↑x).exp) = (1 - ↑|x|) / (1 - (Complex.I * ↑x).exp)
Theorem: k_of_abs_le_one
Proof state before:
x : ℝ
abs_le_one : |x| ≤ 1
⊢ ↑(1 - |x|) / (1 - (Complex.I * ↑x).exp) = (1 - ↑|x|) / (1 - (Complex.I * ↑x).exp)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: k_of_abs_le_one
Proof state before:
x : ℝ
abs_le_one : |x| ≤ 1
⊢ 0 ≤ 1 - |x|
Tactic:
linarith
Proof state after:
no goals
Theorem: k_of_one_le_abs
Proof state before:
x : ℝ
abs_le_one : 1 ≤ |x|
⊢ k x = 0
Tactic:
rw [k, max_eq_right (by linarith)]
Proof state after:
x : ℝ
abs_le_one : 1 ≤ |x|
⊢ ↑0 / (1 - (Complex.I * ↑x).exp) = 0
Theorem: k_of_one_le_abs
Proof state before:
x : ℝ
abs_le_one : 1 ≤ |x|
⊢ ↑0 / (1 - (Complex.I * ↑x).exp) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: k_of_one_le_abs
Proof state before:
x : ℝ
abs_le_one : 1 ≤ |x|
⊢ 1 - |x| ≤ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: k_measurable
Proof state before:
⊢ Measurable k
Tactic:
apply Measurable.div
Proof state after:
case hf

⊢ Measurable fun a => ↑(max (1 - |a|) 0)

case hg

⊢ Measurable fun a => 1 - (Complex.I * ↑a).exp
Theorem: k_measurable
Proof state before:
case hg

⊢ Measurable fun a => 1 - (Complex.I * ↑a).exp
Tactic:
. measurability
Proof state after:
no goals
Theorem: k_measurable
Proof state before:
case hf

⊢ Measurable fun a => ↑(max (1 - |a|) 0)
Tactic:
apply Measurable.comp'
Proof state after:
case hf.hg

⊢ Measurable Complex.ofReal'

case hf.hf

⊢ Measurable fun x => max (1 - |x|) 0

case hf.x

⊢ MeasurableSpace ℝ
Theorem: k_measurable
Proof state before:
case hf.hg

⊢ Measurable Complex.ofReal'
Tactic:
exact Complex.measurable_ofReal
Proof state after:
no goals
Theorem: k_measurable
Proof state before:
case hf.hf

⊢ Measurable fun x => max (1 - |x|) 0
Tactic:
exact Measurable.max (measurable_const.sub measurable_norm) measurable_const
Proof state after:
no goals
Theorem: k_measurable
Proof state before:
case hg

⊢ Measurable fun a => 1 - (Complex.I * ↑a).exp
Tactic:
measurability
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
by_cases h : 0 < |x - y| ∧ |x - y| < 1
Proof 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|)
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
case neg
x y : ℝ
h : ¬(0 < |x - y| ∧ |x - y| < 1)
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Theorem: Hilbert_kernel_bound
Proof 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)]
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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]
Proof 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‖
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ ‖↑(max (1 - |x - y|) 0)‖ ≤ 1
Theorem: Hilbert_kernel_bound
Proof 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]
Proof 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
Theorem: Hilbert_kernel_bound
Proof 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)]
Proof state after:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 ≤ max (1 - |x - y|) 0
Theorem: Hilbert_kernel_bound
Proof state before:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
. apply le_max_right
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 - |x - y| ≤ 1
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 - |x - y| ≤ 1
Tactic:
linarith [abs_nonneg (x-y)]
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
case hab
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 ≤ max (1 - |x - y|) 0
Tactic:
apply le_max_right
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 / ‖1 - (Complex.I * ↑(x - y)).exp‖ ≤ 1 / (|x - y| / 2)
Tactic:
gcongr
Proof 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‖
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| / 2 ≤ ‖1 - (Complex.I * ↑(x - y)).exp‖
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
case hc
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 0 < |x - y| / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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)
Proof 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|)
Theorem: Hilbert_kernel_bound
Proof 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]
Proof 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|
Theorem: Hilbert_kernel_bound
Proof 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
Proof 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|
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
case right
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ x - y ≤ 2 * Real.pi - |x - y|
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ |x - y|
Tactic:
rfl
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
case left
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -2 * Real.pi + |x - y| ≤ x - y
Tactic:
simp
Proof state after:
case left
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ 2 * Real.pi + (x - y)
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 ≤ 2 * Real.pi - 1
Tactic:
rw [le_sub_iff_add_le]
Proof state after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 + 1 ≤ 2 * Real.pi
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 + 1 ≤ 2 * Real.pi
Tactic:
linarith [Real.two_le_pi]
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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]
Proof state after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 * Real.pi + -1 ≤ 2 * Real.pi + (x - y)
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 * Real.pi + -1 ≤ 2 * Real.pi + (x - y)
Tactic:
gcongr
Proof state after:
case bc
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ -1 ≤ x - y
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 * Real.pi - 1 ≤ 2 * Real.pi - |x - y|
Tactic:
gcongr
Proof state after:
case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ 1
Theorem: Hilbert_kernel_bound
Proof state before:
case h
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y| ≤ 1
Tactic:
exact h.2.le
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 1 / (|x - y| / 2) = 2 / |x - y|
Tactic:
field_simp
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ 2 / |x - y| ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
ring_nf
Proof state after:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y|⁻¹ * 2 ≤ |x - y|⁻¹ * 2
Theorem: Hilbert_kernel_bound
Proof state before:
x y : ℝ
h : 0 < |x - y| ∧ |x - y| < 1
⊢ |x - y|⁻¹ * 2 ≤ |x - y|⁻¹ * 2
Tactic:
trivial
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Theorem: Hilbert_kernel_bound
Proof 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))
Proof 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|)
Theorem: Hilbert_kernel_bound
Proof 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]
Proof state after:
case neg
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 ^ 2 / (2 * |x - y|)
Theorem: Hilbert_kernel_bound
Proof 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
Proof 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|
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
case neg.hb
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
this : ‖K x y‖ = 0
⊢ 0 ≤ 2 * |x - y|
Theorem: Hilbert_kernel_bound
Proof 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)]
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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]
Proof state after:
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
⊢ ↑(max (1 - |x - y|) 0) = 0 ∨ 1 - (Complex.I * ↑(x - y)).exp = 0
Theorem: Hilbert_kernel_bound
Proof 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
Proof 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
Theorem: Hilbert_kernel_bound
Proof 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]
Proof 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
Theorem: Hilbert_kernel_bound
Proof 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))
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
case pos.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : x = y
⊢ 1 - (Complex.I * ↑(x - y)).exp = 0
Theorem: Hilbert_kernel_bound
Proof 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]
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
case neg.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ ↑(max (1 - |x - y|) 0) = 0
Theorem: Hilbert_kernel_bound
Proof 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]
Proof state after:
case neg.h
x y : ℝ
h : 0 < |x - y| → 1 ≤ |x - y|
xeqy : ¬x = y
⊢ 1 ≤ |x - y|
Theorem: Hilbert_kernel_bound
Proof 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))
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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
Proof state after:
no goals
Theorem: Hilbert_kernel_bound
Proof 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)]
Proof state after:
no goals
Theorem: Real.volume_uIoc
Proof state before:
a b : ℝ
⊢ MeasureTheory.volume (Ι a b) = ENNReal.ofReal |b - a|
Tactic:
rw [Set.uIoc, volume_Ioc, max_sub_min_eq_abs]
Proof state after:
no goals
Theorem: Hilbert_kernel_regularity_main_part
Proof state before:
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ ‖k (-y) - k (-y')‖ ≤ 2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)
Tactic:
rw [k_of_abs_le_one, k_of_abs_le_one]
Proof state after:
y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ ‖(1 - ↑|(-y)|) / (1 - (Complex.I * ↑(-y)).exp) - (1 - ↑|(-y')|) / (1 - (Complex.I * ↑(-y')).exp)‖ ≤
    2 ^ 6 * (1 / |y|) * (|y - y'| / |y|)

y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ |(-y')| ≤ 1

y y' : ℝ
yy'nonneg : 0 ≤ y ∧ 0 ≤ y'
ypos : 0 < y
y2ley' : y / 2 ≤ y'
hy : y ≤ 1
hy' : y' ≤ 1
⊢ |(-y)| ≤ 1