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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
congr 1
Proof state after:
case e_a
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊

case e_a
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊

case e_a
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
. congr
  ext y
  ring
Proof state after:
case e_a
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
. rw [←nnnorm_star, ←starRingEnd_apply, ←integral_conj]
  congr
  ext y
  simp
  ring
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
congr
Proof state after:
case e_a.e_a.e_f
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
⊢ (fun y => f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) = fun y =>
    cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a.e_a.e_f
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
⊢ (fun y => f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) = fun y =>
    cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))
Tactic:
ext y
Proof state after:
case e_a.e_a.e_f.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
y : ℝ
⊢ f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) =
    cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a.e_a.e_f.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
y : ℝ
⊢ f y * (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y)) =
    cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))
Tactic:
ring
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
rw [←nnnorm_star, ←starRingEnd_apply, ←integral_conj]
Proof state after:
case e_a
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
⊢ ‖∫ (x_1 : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        (starRingEnd ℂ) (f x_1 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a
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
⊢ ‖∫ (x_1 : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        (starRingEnd ℂ) (f x_1 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
        cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊
Tactic:
congr
Proof state after:
case e_a.e_a.e_f
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
⊢ (fun x_1 => (starRingEnd ℂ) (f x_1 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))) =
    fun y => cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a.e_a.e_f
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
⊢ (fun x_1 => (starRingEnd ℂ) (f x_1 * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x x_1 * cexp (I * ↑n * ↑x_1)))) =
    fun y => cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))
Tactic:
ext y
Proof state after:
case e_a.e_a.e_f.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
y : ℝ
⊢ (starRingEnd ℂ) (f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) =
    cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a.e_a.e_f.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
y : ℝ
⊢ (starRingEnd ℂ) (f y * (starRingEnd ℂ) (cexp (I * (-↑n * ↑x)) * K x y * cexp (I * ↑n * ↑y))) =
    cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))
Tactic:
simp
Proof state after:
case e_a.e_a.e_f.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
y : ℝ
⊢ (starRingEnd ℂ) (f y) * (cexp (-(I * (↑n * ↑x))) * K x y * cexp (I * ↑n * ↑y)) =
    cexp (-(I * (↑n * ↑x))) * ((starRingEnd ℂ) (f y) * K x y * cexp (I * ↑n * ↑y))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case e_a.e_a.e_f.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
y : ℝ
⊢ (starRingEnd ℂ) (f y) * (cexp (-(I * (↑n * ↑x))) * K x y * cexp (I * ↑n * ↑y)) =
    cexp (-(I * (↑n * ↑x))) * ((starRingEnd ℂ) (f y) * K x y * cexp (I * ↑n * ↑y))
Tactic:
ring
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊
Tactic:
rw [← NNReal.coe_inj]
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
⊢ ↑(‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊ +
        ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
            cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊) =
    ↑(‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
        ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊)
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
⊢ ↑(‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖₊ +
        ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
            cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖₊) =
    ↑(‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖₊ +
        ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖₊)
Tactic:
push_cast
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * (-↑n * ↑x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * (-↑n * ↑x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖
Tactic:
norm_cast
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
⊢ ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, cexp (I * ↑(↑(-n) * x)) * (f y * K x y * cexp (I * ↑n * ↑y))‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          cexp (I * ↑(↑(-n) * x)) * ((⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y))‖ =
    ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * K x y * cexp (I * ↑n * ↑y)‖ +
      ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, (⇑(starRingEnd ℂ) ∘ f) y * K x y * cexp (I * ↑n * ↑y)‖