internlm/Lean-Github huggingface dataset:
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
Tactic:
calc ‖(I * (-↑n * ↑x)).exp * K x y * (I * ↑n * ↑y).exp‖
  _ = ‖(I * (-↑n * ↑x)).exp‖ * ‖K x y‖ * ‖(I * ↑n * ↑y).exp‖ := by
    rw [norm_mul, norm_mul]
  _ ≤ 1 * (2 ^ (2 : ℝ) / (2 * |x - y|)) * 1 := by
    gcongr
    . rw [norm_eq_abs, mul_comm]
      norm_cast
      rw [abs_exp_ofReal_mul_I]
    . apply Hilbert_kernel_bound
    . rw [norm_eq_abs, mul_assoc, mul_comm]
      norm_cast
      rw [abs_exp_ofReal_mul_I]
  _ ≤ (2 ^ (2 : ℝ) / (2 * r)) := by
    rw [one_mul, mul_one, ← Real.dist_eq]
    gcongr
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ = ‖cexp (I * (-↑n * ↑x))‖ * ‖K x y‖ * ‖cexp (I * ↑n * ↑y)‖
Tactic:
rw [norm_mul, norm_mul]
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * (-↑n * ↑x))‖ * ‖K x y‖ * ‖cexp (I * ↑n * ↑y)‖ ≤ 1 * (2 ^ 2 / (2 * |x - y|)) * 1
Tactic:
gcongr
Proof state after:
case h₁.h₁
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * (-↑n * ↑x))‖ ≤ 1

case h₁.h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * ↑n * ↑y)‖ ≤ 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₁.h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)

case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * ↑n * ↑y)‖ ≤ 1
Tactic:
. apply Hilbert_kernel_bound
Proof state after:
case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * ↑n * ↑y)‖ ≤ 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * ↑n * ↑y)‖ ≤ 1
Tactic:
. rw [norm_eq_abs, mul_assoc, mul_comm]
  norm_cast
  rw [abs_exp_ofReal_mul_I]
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₁.h₁
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * (-↑n * ↑x))‖ ≤ 1
Tactic:
rw [norm_eq_abs, mul_comm]
Proof state after:
case h₁.h₁
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ Complex.abs (cexp (-↑n * ↑x * I)) ≤ 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₁.h₁
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ Complex.abs (cexp (-↑n * ↑x * I)) ≤ 1
Tactic:
norm_cast
Proof state after:
case h₁.h₁
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ Complex.abs (cexp (↑(↑(-n) * x) * I)) ≤ 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₁.h₁
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ Complex.abs (cexp (↑(↑(-n) * x) * I)) ≤ 1
Tactic:
rw [abs_exp_ofReal_mul_I]
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₁.h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖K x y‖ ≤ 2 ^ 2 / (2 * |x - y|)
Tactic:
apply Hilbert_kernel_bound
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ ‖cexp (I * ↑n * ↑y)‖ ≤ 1
Tactic:
rw [norm_eq_abs, mul_assoc, mul_comm]
Proof state after:
case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ Complex.abs (cexp (↑n * ↑y * I)) ≤ 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ Complex.abs (cexp (↑n * ↑y * I)) ≤ 1
Tactic:
norm_cast
Proof state after:
case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ Complex.abs (cexp (↑(↑n * y) * I)) ≤ 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h₂
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ Complex.abs (cexp (↑(↑n * y) * I)) ≤ 1
Tactic:
rw [abs_exp_ofReal_mul_I]
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ 1 * (2 ^ 2 / (2 * |x - y|)) * 1 ≤ 2 ^ 2 / (2 * r)
Tactic:
rw [one_mul, mul_one, ← Real.dist_eq]
Proof state after:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ 2 ^ 2 / (2 * dist x y) ≤ 2 ^ 2 / (2 * r)
Theorem: le_CarlesonOperatorReal'
Proof state before:
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
y : ℝ
h : r ≤ dist x y
⊢ 2 ^ 2 / (2 * dist x y) ≤ 2 ^ 2 / (2 * r)
Tactic:
gcongr
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a.hf
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
⊢ MeasureTheory.Integrable (fun y => f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)))
    (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
Tactic:
conv => pattern ((f _) * _); rw [mul_comm]
Proof state after:
case e_a.hf
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
⊢ MeasureTheory.Integrable (fun y => cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) * f y)
    (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a.hf
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
⊢ MeasureTheory.Integrable (fun y => cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y) * f y)
    (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
Tactic:
apply MeasureTheory.Integrable.bdd_mul' integrable₁ measurable₁.aestronglyMeasurable
Proof state after:
case e_a.hf
f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1},
    ‖cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)‖ ≤ ?m.492969

f : ℝ → ℂ
hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) (3 * Real.pi)
N : ℕ
x : ℝ
hx : x ∈ Set.Icc 0 (2 * Real.pi)
s : ℕ → Set ℝ := fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
sdef : s = fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}
hs : {y | dist x y ∈ Set.Ioo 0 1} = ⋃ n, s n
this :
  Tendsto (fun i => ∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) atTop
    (𝓝 (∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)))
n : ℤ
r : ℝ
rpos : 0 < r
rle1 : r < 1
measurable₁ : Measurable fun x_1 => cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)
boundedness₁ : ∀ {y : ℝ}, r ≤ dist x y → ‖cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)‖ ≤ 2 ^ 2 / (2 * r)
integrable₁ : MeasureTheory.Integrable (fun x => f x) (MeasureTheory.volume.restrict {y | dist x y ∈ Set.Ioo r 1})
⊢ ℝ