internlm/Lean-Github huggingface dataset:
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 : ℕ
⊢ ↑‖∫ (y : ℝ) in s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1},
          f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊
Tactic:
rfl
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 : ℕ
⊢ 0 < 1 / (↑n + 2)
Tactic:
simp
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 : ℕ
⊢ 0 < ↑n + 2
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 : ℕ
⊢ 0 < ↑n + 2
Tactic:
linarith
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 : ℕ
⊢ 1 / (↑n + 2) < 1
Tactic:
rw [div_lt_iff] <;> linarith
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)))
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨆ (_ : r < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
                f y *
                  (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Tactic:
apply iSup_congr
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)))
⊢ ∀ (i : ℝ),
    ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
      ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1},
                f y *
                  (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
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)))
⊢ ∀ (i : ℝ),
    ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
      ⨆ (_ : 0 < i),
        ⨆ (_ : i < 1),
          ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo i 1},
                f y *
                  (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                    (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Tactic:
intro r
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)))
r : ℝ
⊢ ⨆ (_ : 0 < r),
      ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
    ⨆ (_ : 0 < r),
      ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
              f y *
                (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                  (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
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)))
r : ℝ
⊢ ⨆ (_ : 0 < r),
      ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
    ⨆ (_ : 0 < r),
      ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
              f y *
                (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                  (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Tactic:
apply iSup_congr
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)))
r : ℝ
⊢ 0 < r →
    ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
      ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
              f y *
                (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                  (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
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)))
r : ℝ
⊢ 0 < r →
    ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
      ⨆ (_ : r < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
              f y *
                (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                  (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Tactic:
intro _
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)))
r : ℝ
i✝ : 0 < r
⊢ ⨆ (_ : r < 1),
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
    ⨆ (_ : r < 1),
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
            f y *
              (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
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)))
r : ℝ
i✝ : 0 < r
⊢ ⨆ (_ : r < 1),
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
    ⨆ (_ : r < 1),
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
            f y *
              (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Tactic:
apply iSup_congr
Proof state after:
case h.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)))
r : ℝ
i✝ : 0 < r
⊢ r < 1 →
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
            f y *
              (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.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)))
r : ℝ
i✝ : 0 < r
⊢ r < 1 →
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
      ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
            f y *
              (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
                (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Tactic:
intro _
Proof state after:
case h.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)))
r : ℝ
i✝¹ : 0 < r
i✝ : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          f y *
            (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
              (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.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)))
r : ℝ
i✝¹ : 0 < r
i✝ : r < 1
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
    ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo r 1},
          f y *
            (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
              (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))‖₊
Tactic:
congr
Proof state after:
case h.h.h.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)))
r : ℝ
i✝¹ : 0 < r
i✝ : r < 1
⊢ (fun y => f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) = fun y =>
    f y *
      (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
        (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.h.h.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)))
r : ℝ
i✝¹ : 0 < r
i✝ : r < 1
⊢ (fun y => f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)) = fun y =>
    f y *
      (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
        (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))
Tactic:
ext y
Proof state after:
case h.h.h.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)))
r : ℝ
i✝¹ : 0 < r
i✝ : r < 1
y : ℝ
⊢ f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) =
    f y *
      (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
        (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.h.h.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)))
r : ℝ
i✝¹ : 0 < r
i✝ : r < 1
y : ℝ
⊢ f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) =
    f y *
      (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
        (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))
Tactic:
rw [mul_assoc, dirichlet_Hilbert_eq]
Proof state after:
case h.h.h.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)))
r : ℝ
i✝¹ : 0 < r
i✝ : r < 1
y : ℝ
⊢ f y *
      (cexp (I * (-↑N * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
        (starRingEnd ℂ) (cexp (I * (-↑N * ↑x)) * K x y * cexp (I * ↑N * ↑y))) =
    f y *
      (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
        (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.h.h.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)))
r : ℝ
i✝¹ : 0 < r
i✝ : r < 1
y : ℝ
⊢ f y *
      (cexp (I * (-↑N * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
        (starRingEnd ℂ) (cexp (I * (-↑N * ↑x)) * K x y * cexp (I * ↑N * ↑y))) =
    f y *
      (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
        (starRingEnd ℂ) (cexp (I * (-↑(Int.ofNat N) * ↑x)) * K x y * cexp (I * ↑(Int.ofNat N) * ↑y)))
Tactic:
norm_cast
Proof state after:
no goals