internlm/Lean-Github huggingface dataset:
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.left.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}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < ↑n + 2

case h.left.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}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < dist x y
Tactic:
linarith
Proof state after:
case h.left.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}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < dist x y
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.left.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}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ 0 < dist x y
Tactic:
exact hy.1
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.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}
y : ℝ
hy : 0 < dist x y ∧ dist x y < 1
n : ℕ
hn : 1 / dist x y < ↑n
⊢ dist x y < 1
Tactic:
exact hy.2
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr
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}
y : ℝ
⊢ y ∈ ⋃ n, s n → y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Tactic:
intro hy
Proof state after:
case h.mpr
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}
y : ℝ
hy : y ∈ ⋃ n, s n
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr
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}
y : ℝ
hy : y ∈ ⋃ n, s n
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Tactic:
simp at hy
Proof state after:
case h.mpr
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}
y : ℝ
hy : ∃ i, y ∈ s i
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr
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}
y : ℝ
hy : ∃ i, y ∈ s i
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Tactic:
rcases hy with ⟨n, hn⟩
Proof state after:
case h.mpr.intro
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}
y : ℝ
n : ℕ
hn : y ∈ s n
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr.intro
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}
y : ℝ
n : ℕ
hn : y ∈ s n
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Tactic:
rw [sdef] at hn
Proof state after:
case h.mpr.intro
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}
y : ℝ
n : ℕ
hn : y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) n
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr.intro
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}
y : ℝ
n : ℕ
hn : y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) n
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Tactic:
simp at hn
Proof state after:
case h.mpr.intro
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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr.intro
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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ y ∈ {y | dist x y ∈ Set.Ioo 0 1}
Tactic:
constructor
Proof state after:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < dist x y

case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < dist x y

case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Tactic:
. apply lt_trans' hn.1
  norm_num
  linarith
Proof state after:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Tactic:
. exact hn.2
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < dist x y
Tactic:
apply lt_trans' hn.1
Proof state after:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < (↑n + 2)⁻¹
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < (↑n + 2)⁻¹
Tactic:
norm_num
Proof state after:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ 0 < ↑n + 2
Theorem: le_CarlesonOperatorReal'
Proof state before:
case h.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑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.mpr.intro.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}
y : ℝ
n : ℕ
hn : (↑n + 2)⁻¹ < dist x y ∧ dist x y < 1
⊢ dist x y < 1
Tactic:
exact hn.2
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
⊢ 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 MeasureTheory.tendsto_setIntegral_of_monotone
Proof state after:
case hsm
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
⊢ ∀ (i : ℕ), MeasurableSet (s i)

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
⊢ Monotone fun i => s i

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
Theorem: le_CarlesonOperatorReal'
Proof state before:
case hsm
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
⊢ ∀ (i : ℕ), MeasurableSet (s i)

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
⊢ Monotone fun i => s i

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:
. intro n
  exact annulus_measurableSet
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
⊢ Monotone fun i => s i

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
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
⊢ Monotone fun i => s i

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:
. intro n m nlem
  simp
  intro y hy
  rw [sdef]
  rw [sdef] at hy
  simp
  simp at hy
  constructor
  . apply lt_of_le_of_lt _ hy.1
    rw [inv_le_inv]
    norm_cast
    all_goals linarith
  . exact hy.2
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)) (⋃ n, s n)
    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)) (⋃ n, s n)
    MeasureTheory.volume
Tactic:
. rw [← hs]
  exact integrableOn_mul_dirichletKernel'_specific hx hf
Proof state after:
no goals
Theorem: le_CarlesonOperatorReal'
Proof state before:
case hsm
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
⊢ ∀ (i : ℕ), MeasurableSet (s i)
Tactic:
intro n
Proof state after:
case hsm
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 : ℕ
⊢ MeasurableSet (s n)
Theorem: le_CarlesonOperatorReal'
Proof state before:
case hsm
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 : ℕ
⊢ MeasurableSet (s n)
Tactic:
exact annulus_measurableSet
Proof state after:
no goals
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
⊢ Monotone fun i => s i
Tactic:
intro n m nlem
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
⊢ (fun i => s i) n ≤ (fun i => s i) m
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
⊢ (fun i => s i) n ≤ (fun i => s i) m
Tactic:
simp
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
⊢ s n ⊆ s m
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
⊢ s n ⊆ s m
Tactic:
intro y 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 : y ∈ s n
⊢ y ∈ s m
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 ∈ s n
⊢ y ∈ s m
Tactic:
rw [sdef]
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 : y ∈ s n
⊢ y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) m
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 ∈ s n
⊢ y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) m
Tactic:
rw [sdef] 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 : y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) n
⊢ y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) m
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
⊢ y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) m
Tactic:
simp
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 : y ∈ (fun n => {y | dist x y ∈ Set.Ioo (1 / (↑n + 2)) 1}) n
⊢ (↑m + 2)⁻¹ < dist x y ∧ dist x y < 1