internlm/Lean-Github huggingface dataset:
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h_mono
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) n
⊢ (↑m + 2)⁻¹ < dist x y ∧ dist x y < 1
Tactic:
simp at hy
Proof state after:
case h_mono
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ (↑m + 2)⁻¹ < dist x y ∧ dist x y < 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h_mono
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ (↑m + 2)⁻¹ < dist x y ∧ dist x y < 1
Tactic:
constructor
Proof state after:
case h_mono.left
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ (↑m + 2)⁻¹ < dist x y

case h_mono.right
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h_mono.left
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ (↑m + 2)⁻¹ < dist x y

case h_mono.right
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Tactic:
. apply lt_of_le_of_lt _ hy.1
  rw [inv_le_inv]
  norm_cast
  all_goals linarith
Proof state after:
case h_mono.right
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h_mono.right
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Tactic:
. exact hy.2
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h_mono.left
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ (↑m + 2)⁻¹ < dist x y
Tactic:
apply lt_of_le_of_lt _ hy.1
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ (↑m + 2)⁻¹ ≤ (↑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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ (↑m + 2)⁻¹ ≤ (↑n + 2)⁻¹
Tactic:
rw [inv_le_inv]
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ ↑n + 2 ≤ ↑m + 2

case ha
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < ↑m + 2

case hb
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ ↑n + 2 ≤ ↑m + 2

case ha
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < ↑m + 2

case hb
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < ↑n + 2
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ n + 2 ≤ m + 2

case ha
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < ↑m + 2

case hb
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ n + 2 ≤ m + 2

case ha
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < ↑m + 2

case hb
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < ↑n + 2
Tactic:
all_goals linarith
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case hb
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < ↑n + 2
Tactic:
linarith
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h_mono.right
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
n m : ℕ
nlem : n ≤ m
y : ℝ
hy : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Tactic:
exact hy.2
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case hfi
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
⊢ MeasureTheory.IntegrableOn (fun x_1 => f x_1 * ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1)) (⋃ n, s n)
    MeasureTheory.volume
Tactic:
rw [← hs]
Proof state after:
case hfi
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
⊢ MeasureTheory.IntegrableOn (fun x_1 => f x_1 * ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1))
    {y | dist x y ∈ Set.Ioo 0 1} MeasureTheory.volume
Theorem: le_CarlesonOperatorReal'
Proof state before:
case hfi
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
⊢ MeasureTheory.IntegrableOn (fun x_1 => f x_1 * ↑(max (1 - |x - x_1|) 0) * dirichletKernel' N (x - x_1))
    {y | dist x y ∈ Set.Ioo 0 1} MeasureTheory.volume
Tactic:
exact integrableOn_mul_dirichletKernel'_specific hx hf
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)))
⊢ ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo 0 1}, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ =
    ↑‖∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊
Tactic:
congr
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)))
⊢ ↑‖∫ (y : ℝ) in ⋃ n, s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    ⨆ i, ↑‖∫ (y : ℝ) in s i, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊
Tactic:
apply le_iSup_of_tendsto
Proof state after:
case ha
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)))
⊢ 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)‖₊)
Theorem: le_CarlesonOperatorReal'
Proof state before:
case ha
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)))
⊢ 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)‖₊)
Tactic:
rw [ENNReal.tendsto_coe]
Proof state after:
case ha
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)))
⊢ 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)‖₊)
Theorem: le_CarlesonOperatorReal'
Proof state before:
case ha
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)))
⊢ 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)‖₊)
Tactic:
apply Tendsto.nnnorm this
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)))
⊢ ⨆ i, ↑‖∫ (y : ℝ) in s i, 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)‖₊
Tactic:
apply iSup_le
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 : ℕ),
    ↑‖∫ (y : ℝ) in s i, 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)‖₊
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 : ℕ),
    ↑‖∫ (y : ℝ) in s i, 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)‖₊
Tactic:
intro n
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 : ℕ
⊢ ↑‖∫ (y : ℝ) in 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)‖₊
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)‖₊ ≤
    ⨆ 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)‖₊
Tactic:
apply le_iSup_of_le (1 / (n + 2 : ℝ))
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 : ℕ
⊢ ↑‖∫ (y : ℝ) in s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    ⨆ (_ : 0 < 1 / (↑n + 2)),
      ⨆ (_ : 1 / (↑n + 2) < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1},
              f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - 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)))
n : ℕ
⊢ ↑‖∫ (y : ℝ) in s n, f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊ ≤
    ⨆ (_ : 0 < 1 / (↑n + 2)),
      ⨆ (_ : 1 / (↑n + 2) < 1),
        ↑‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1},
              f y * ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y)‖₊
Tactic:
apply le_iSup₂_of_le (by simp; linarith) (by rw [div_lt_iff] <;> linarith)
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 : ℕ
⊢ ↑‖∫ (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)‖₊